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 ⊢G∈Grp→SubGrp⁡G∈ACS⁡B

Proof

Step Hyp Ref Expression
1 subgacs.b ⊢B=BaseG
2 eqid ⊢invg⁡G=invg⁡G
3 2 issubg3 ⊢G∈Grp→s∈SubGrp⁡G↔s∈SubMnd⁡G∧∀x∈sinvg⁡G⁡x∈s
4 1 submss ⊢s∈SubMnd⁡G→s⊆B
5 4 adantl ⊢G∈Grp∧s∈SubMnd⁡G→s⊆B
6 velpw ⊢s∈𝒫B↔s⊆B
7 5 6 sylibr ⊢G∈Grp∧s∈SubMnd⁡G→s∈𝒫B
8 eleq2w ⊢y=s→invg⁡G⁡x∈y↔invg⁡G⁡x∈s
9 8 raleqbi1dv ⊢y=s→∀x∈yinvg⁡G⁡x∈y↔∀x∈sinvg⁡G⁡x∈s
10 9 elrab3 ⊢s∈𝒫B→s∈y∈𝒫B|∀x∈yinvg⁡G⁡x∈y↔∀x∈sinvg⁡G⁡x∈s
11 7 10 syl ⊢G∈Grp∧s∈SubMnd⁡G→s∈y∈𝒫B|∀x∈yinvg⁡G⁡x∈y↔∀x∈sinvg⁡G⁡x∈s
12 11 pm5.32da ⊢G∈Grp→s∈SubMnd⁡G∧s∈y∈𝒫B|∀x∈yinvg⁡G⁡x∈y↔s∈SubMnd⁡G∧∀x∈sinvg⁡G⁡x∈s
13 3 12 bitr4d ⊢G∈Grp→s∈SubGrp⁡G↔s∈SubMnd⁡G∧s∈y∈𝒫B|∀x∈yinvg⁡G⁡x∈y
14 elin ⊢s∈SubMnd⁡G∩y∈𝒫B|∀x∈yinvg⁡G⁡x∈y↔s∈SubMnd⁡G∧s∈y∈𝒫B|∀x∈yinvg⁡G⁡x∈y
15 13 14 bitr4di ⊢G∈Grp→s∈SubGrp⁡G↔s∈SubMnd⁡G∩y∈𝒫B|∀x∈yinvg⁡G⁡x∈y
16 15 eqrdv ⊢G∈Grp→SubGrp⁡G=SubMnd⁡G∩y∈𝒫B|∀x∈yinvg⁡G⁡x∈y
17 1 fvexi ⊢B∈V
18 mreacs ⊢B∈V→ACS⁡B∈Moore⁡𝒫B
19 17 18 mp1i ⊢G∈Grp→ACS⁡B∈Moore⁡𝒫B
20 grpmnd ⊢G∈Grp→G∈Mnd
21 1 submacs ⊢G∈Mnd→SubMnd⁡G∈ACS⁡B
22 20 21 syl ⊢G∈Grp→SubMnd⁡G∈ACS⁡B
23 1 2 grpinvcl ⊢G∈Grp∧x∈B→invg⁡G⁡x∈B
24 23 ralrimiva ⊢G∈Grp→∀x∈Binvg⁡G⁡x∈B
25 acsfn1 ⊢B∈V∧∀x∈Binvg⁡G⁡x∈B→y∈𝒫B|∀x∈yinvg⁡G⁡x∈y∈ACS⁡B
26 17 24 25 sylancr ⊢G∈Grp→y∈𝒫B|∀x∈yinvg⁡G⁡x∈y∈ACS⁡B
27 mreincl ⊢ACS⁡B∈Moore⁡𝒫B∧SubMnd⁡G∈ACS⁡B∧y∈𝒫B|∀x∈yinvg⁡G⁡x∈y∈ACS⁡B→SubMnd⁡G∩y∈𝒫B|∀x∈yinvg⁡G⁡x∈y∈ACS⁡B
28 19 22 26 27 syl3anc ⊢G∈Grp→SubMnd⁡G∩y∈𝒫B|∀x∈yinvg⁡G⁡x∈y∈ACS⁡B
29 16 28 eqeltrd ⊢G∈Grp→SubGrp⁡G∈ACS⁡B