Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: abelian_Group x0.
Let x1 of type ι be given.
Assume H1: subgroup x1 x0.
Apply H1 with normal_subgroup x1 x0.
Assume H2: and (struct_b x0) (struct_b x1).
Assume H3: unpack_b_o x0 (λ x2 . λ x3 : ι → ι → ι . unpack_b_o x1 (λ x4 . λ x5 : ι → ι → ι . and (and (x1 = pack_b x4 x3) (Group (pack_b x4 x3))) (x4 ⊆ x2))).
Apply H2 with normal_subgroup x1 x0.
Assume H4: struct_b x0.
Assume H5: struct_b x1.
Claim L6: abelian_Group x0 ⟶ subgroup x1 x0 ⟶ normal_subgroup x1 x0
Apply H4 with λ x2 . abelian_Group x2 ⟶ subgroup x1 x2 ⟶ normal_subgroup x1 x2.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Assume H6: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2.
Assume H7: abelian_Group (pack_b x2 x3).
Apply abelian_Group_E with x2, x3, subgroup x1 (pack_b x2 x3) ⟶ normal_subgroup x1 (pack_b x2 x3) leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H8: Group (pack_b x2 x3).
Assume H9: explicit_abelian x2 x3.
Apply H5 with λ x4 . subgroup x4 (pack_b x2 x3) ⟶ normal_subgroup x4 (pack_b x2 x3).
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Assume H10: ∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ∈ x4.
Assume H11: subgroup (pack_b x4 x5) (pack_b x2 x3).
Claim L12: explicit_subgroup x2 x3 x4
Apply pack_b_subgroup_E with x4, x2, x5, x3, explicit_subgroup x2 x3 x4 leaving 2 subgoals.
The subproof is completed by applying H11.
Assume H12: pack_b x4 x5 = pack_b x4 x3.
Assume H13: explicit_subgroup x2 x3 x4.
The subproof is completed by applying H13.
Claim L13: x4 ⊆ x2
Apply L12 with x4 ⊆ x2.
Assume H13: Group (pack_b x4 x3).
Assume H14: x4 ⊆ x2.
The subproof is completed by applying H14.
Apply andI with subgroup (pack_b x4 x5) (pack_b x2 x3), unpack_b_o (pack_b x2 x3) (λ x6 . λ x7 : ι → ι → ι . unpack_b_o (pack_b x4 x5) (λ x8 . λ x9 : ι → ι → ι . explicit_normal x6 x7 x8)) leaving 2 subgoals.
The subproof is completed by applying H11.
Apply unknownprop_a38119175a5c7a068cd247f906b2f1feb5daeb7691af95918cb490283a35a18e with x4, x2, x5, x3, λ x6 x7 : ο . x7 leaving 3 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying L13.
Apply explicit_abelian_normal with x2, x3, x4 leaving 3 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying L12.
The subproof is completed by applying H9.
Apply L6 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■