Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Assume H0: Group (pack_b x0 x1).
Assume H1: explicit_subgroup x0 x1 x2.
Claim L2: ...
...
Claim L3: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5
Apply L2 with ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5.
Assume H3: and (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 ∈ x0) (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5).
Assume H4: ∃ x3 . and (x3 ∈ x0) (and (∀ x4 . x4 ∈ x0 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . ... ⟶ ∃ x5 . and (x5 ∈ x0) (and (x1 x4 x5 = x3) (x1 x5 x4 = x3)))).
...
Claim L4: x2 ⊆ x0
Apply H1 with x2 ⊆ x0.
Assume H4: Group (pack_b x2 x1).
Assume H5: x2 ⊆ x0.
The subproof is completed by applying H5.
Assume H5: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x1 x4 x3.
Let x3 of type ι be given.
Assume H6: x3 ∈ x0.
Let x4 of type ι be given.
Assume H7: x4 ∈ {x1 x3 (x1 x5 (explicit_Group_inverse x0 x1 x3))|x5 ∈ x2}.
Apply ReplE_impred with x2, λ x5 . x1 x3 (x1 x5 (explicit_Group_inverse x0 x1 x3)), x4, x4 ∈ x2 leaving 2 subgoals.
The subproof is completed by applying H7.
Let x5 of type ι be given.
Assume H8: x5 ∈ x2.
Assume H9: x4 = x1 x3 (x1 x5 (explicit_Group_inverse x0 x1 x3)).
Claim L10: explicit_Group_inverse x0 x1 x3 ∈ x0
Apply explicit_Group_inverse_in with x0, x1, x3 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H6.
Claim L11: x4 = x5
Apply H9 with λ x6 x7 . x7 = x5.
Apply H5 with explicit_Group_inverse x0 x1 x3, x5, λ x6 x7 . x1 x3 x6 = x5 leaving 3 subgoals.
The subproof is completed by applying L10.
Apply L4 with x5.
The subproof is completed by applying H8.
Apply L3 with x3, explicit_Group_inverse x0 x1 x3, x5, λ x6 x7 . x7 = x5 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L10.
Apply L4 with x5.
The subproof is completed by applying H8.
Apply explicit_Group_inverse_rinv with x0, x1, x3, λ x6 x7 . x1 x7 x5 = x5 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H6.
Apply explicit_Group_identity_lid with x0, x1, x5 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply L4 with x5.
The subproof is completed by applying H8.
Apply L11 with λ x6 x7 . x7 ∈ x2.
The subproof is completed by applying H8.
■