Metamath Proof Explorer


Theorem subgacs

Description: Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypothesis subgacs.b B=BaseG
Assertion subgacs GGrpSubGrpGACSB

Proof

Step Hyp Ref Expression
1 subgacs.b B=BaseG
2 eqid invgG=invgG
3 2 issubg3 GGrpsSubGrpGsSubMndGxsinvgGxs
4 1 submss sSubMndGsB
5 4 adantl GGrpsSubMndGsB
6 velpw s𝒫BsB
7 5 6 sylibr GGrpsSubMndGs𝒫B
8 eleq2w y=sinvgGxyinvgGxs
9 8 raleqbi1dv y=sxyinvgGxyxsinvgGxs
10 9 elrab3 s𝒫Bsy𝒫B|xyinvgGxyxsinvgGxs
11 7 10 syl GGrpsSubMndGsy𝒫B|xyinvgGxyxsinvgGxs
12 11 pm5.32da GGrpsSubMndGsy𝒫B|xyinvgGxysSubMndGxsinvgGxs
13 3 12 bitr4d GGrpsSubGrpGsSubMndGsy𝒫B|xyinvgGxy
14 elin sSubMndGy𝒫B|xyinvgGxysSubMndGsy𝒫B|xyinvgGxy
15 13 14 bitr4di GGrpsSubGrpGsSubMndGy𝒫B|xyinvgGxy
16 15 eqrdv GGrpSubGrpG=SubMndGy𝒫B|xyinvgGxy
17 1 fvexi BV
18 mreacs BVACSBMoore𝒫B
19 17 18 mp1i GGrpACSBMoore𝒫B
20 grpmnd GGrpGMnd
21 1 submacs GMndSubMndGACSB
22 20 21 syl GGrpSubMndGACSB
23 1 2 grpinvcl GGrpxBinvgGxB
24 23 ralrimiva GGrpxBinvgGxB
25 acsfn1 BVxBinvgGxBy𝒫B|xyinvgGxyACSB
26 17 24 25 sylancr GGrpy𝒫B|xyinvgGxyACSB
27 mreincl ACSBMoore𝒫BSubMndGACSBy𝒫B|xyinvgGxyACSBSubMndGy𝒫B|xyinvgGxyACSB
28 19 22 26 27 syl3anc GGrpSubMndGy𝒫B|xyinvgGxyACSB
29 16 28 eqeltrd GGrpSubGrpGACSB