Claim L0: ...

...

Claim L1: ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ 127dd.. x0 x1 ⟶ ∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2) ⟶ 127dd.. x2 x3 ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . x5 ∈ setprod x0 x2 ⟶ ∀ x6 . x6 ∈ setprod x0 x2 ⟶ lam 2 (λ x7 . If_i (x7 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))) = x4 x5 x6) ⟶ 127dd.. (setprod x0 x2) x4

Let x0 of type ι be given.

Let x1 of type ι → ι → ι be given.

Assume H1: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0.

Assume H2: 127dd.. x0 x1.

Let x2 of type ι be given.

Let x3 of type ι → ι → ι be given.

Assume H3: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2.

Assume H4: 127dd.. x2 x3.

Let x4 of type ι → ι → ι be given.

Assume H5: ∀ x5 . x5 ∈ setprod x0 x2 ⟶ ∀ x6 . x6 ∈ setprod x0 x2 ⟶ lam 2 (λ x7 . If_i (x7 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))) = x4 x5 x6.

Apply H2 with 127dd.. (setprod x0 x2) x4.

Assume H6: explicit_Group x0 x1.

Assume H7: explicit_abelian x0 x1.

Apply H4 with 127dd.. (setprod x0 x2) x4.

Assume H8: explicit_Group x2 x3.

Assume H9: explicit_abelian x2 x3.

Apply andI with explicit_Group (setprod x0 x2) x4, explicit_abelian (setprod x0 x2) x4 leaving 2 subgoals.

Apply unknownprop_b94c81a80692cb6780c85e4ec6b658129aab5c4a1429b0045f10cd072e8bf363 with x0, x1, x2, x3, x4 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H6.

The subproof is completed by applying H3.

The subproof is completed by applying H8.

The subproof is completed by applying H5.

Let x5 of type ι be given.

Assume H10: x5 ∈ setprod x0 x2.

Let x6 of type ι be given.

Assume H11: x6 ∈ setprod x0 x2.

Apply H5 with x5, x6, λ x7 x8 . x7 = x4 x6 x5 leaving 3 subgoals.

The subproof is completed by applying H10.

The subproof is completed by applying H11.

Apply H5 with x6, x5, λ x7 x8 . lam 2 (λ x9 . If_i (x9 = 0) (x1 (ap x5 0) (ap x6 0)) (x3 (ap x5 1) (ap x6 1))) = x7 leaving 3 subgoals.

The subproof is completed by applying H11.

The subproof is completed by applying H10.

Apply H7 with ap x5 0, ap x6 0, λ x7 x8 . lam 2 (λ x9 . If_i (x9 = 0) x8 (x3 (ap x5 1) (ap x6 1))) = lam 2 ... leaving 3 subgoals.

...

Apply unknownprop_d305e4f28748e3527529c751b716fb93c014046566c5ce2cf4a34b9f2fbe0cdc with 127dd.. leaving 2 subgoals.

The subproof is completed by applying L0.

The subproof is completed by applying L1.

■

Proofgold Proof