Metamath Proof Explorer

Theorem nsgacs

Description: Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypothesis subgacs.b ⊢B=BaseG
Assertion nsgacs ⊢G∈Grp→NrmSGrp⁡G∈ACS⁡B

Proof

Step Hyp Ref Expression
1 subgacs.b ⊢B=BaseG
2 1 subgss ⊢s∈SubGrp⁡G→s⊆B
3 velpw ⊢s∈𝒫B↔s⊆B
4 2 3 sylibr ⊢s∈SubGrp⁡G→s∈𝒫B
5 eleq2w ⊢z=s→x+Gy-Gx∈z↔x+Gy-Gx∈s
6 5 raleqbi1dv ⊢z=s→∀y∈zx+Gy-Gx∈z↔∀y∈sx+Gy-Gx∈s
7 6 ralbidv ⊢z=s→∀x∈B∀y∈zx+Gy-Gx∈z↔∀x∈B∀y∈sx+Gy-Gx∈s
8 7 elrab3 ⊢s∈𝒫B→s∈z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z↔∀x∈B∀y∈sx+Gy-Gx∈s
9 4 8 syl ⊢s∈SubGrp⁡G→s∈z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z↔∀x∈B∀y∈sx+Gy-Gx∈s
10 9 bicomd ⊢s∈SubGrp⁡G→∀x∈B∀y∈sx+Gy-Gx∈s↔s∈z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z
11 10 pm5.32i ⊢s∈SubGrp⁡G∧∀x∈B∀y∈sx+Gy-Gx∈s↔s∈SubGrp⁡G∧s∈z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z
12 eqid ⊢+G=+G
13 eqid ⊢-G=-G
14 1 12 13 isnsg3 ⊢s∈NrmSGrp⁡G↔s∈SubGrp⁡G∧∀x∈B∀y∈sx+Gy-Gx∈s
15 elin ⊢s∈SubGrp⁡G∩z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z↔s∈SubGrp⁡G∧s∈z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z
16 11 14 15 3bitr4i ⊢s∈NrmSGrp⁡G↔s∈SubGrp⁡G∩z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z
17 16 eqriv ⊢NrmSGrp⁡G=SubGrp⁡G∩z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z
18 1 fvexi ⊢B∈V
19 mreacs ⊢B∈V→ACS⁡B∈Moore⁡𝒫B
20 18 19 mp1i ⊢G∈Grp→ACS⁡B∈Moore⁡𝒫B
21 1 subgacs ⊢G∈Grp→SubGrp⁡G∈ACS⁡B
22 simpl ⊢G∈Grp∧x∈B∧y∈B→G∈Grp
23 1 12 grpcl ⊢G∈Grp∧x∈B∧y∈B→x+Gy∈B
24 23 3expb ⊢G∈Grp∧x∈B∧y∈B→x+Gy∈B
25 simprl ⊢G∈Grp∧x∈B∧y∈B→x∈B
26 1 13 grpsubcl ⊢G∈Grp∧x+Gy∈B∧x∈B→x+Gy-Gx∈B
27 22 24 25 26 syl3anc ⊢G∈Grp∧x∈B∧y∈B→x+Gy-Gx∈B
28 27 ralrimivva ⊢G∈Grp→∀x∈B∀y∈Bx+Gy-Gx∈B
29 acsfn1c ⊢B∈V∧∀x∈B∀y∈Bx+Gy-Gx∈B→z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z∈ACS⁡B
30 18 28 29 sylancr ⊢G∈Grp→z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z∈ACS⁡B
31 mreincl ⊢ACS⁡B∈Moore⁡𝒫B∧SubGrp⁡G∈ACS⁡B∧z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z∈ACS⁡B→SubGrp⁡G∩z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z∈ACS⁡B
32 20 21 30 31 syl3anc ⊢G∈Grp→SubGrp⁡G∩z∈𝒫B|∀x∈B∀y∈zx+Gy-Gx∈z∈ACS⁡B
33 17 32 eqeltrid ⊢G∈Grp→NrmSGrp⁡G∈ACS⁡B