Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι → ι → ι be given.
Assume H0: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4.
Apply explicit_Group_repindep with
x0,
x1,
x2,
127dd.. x0 x2 = 127dd.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply explicit_abelian_repindep with
x0,
x1,
x2,
127dd.. x0 x2 = 127dd.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply prop_ext_2 with
127dd.. x0 x2,
127dd.. x0 x1 leaving 2 subgoals.
Apply H5 with
127dd.. x0 x1.
Apply andI with
explicit_Group x0 x1,
explicit_abelian x0 x1 leaving 2 subgoals.
Apply H2.
The subproof is completed by applying H6.
Apply H4.
The subproof is completed by applying H7.
Apply H5 with
127dd.. x0 x2.
Apply andI with
explicit_Group x0 x2,
explicit_abelian x0 x2 leaving 2 subgoals.
Apply H1.
The subproof is completed by applying H6.
Apply H3.
The subproof is completed by applying H7.