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 = Base G
Assertion nsgacs G Grp NrmSGrp G ACS B

Proof

Step Hyp Ref Expression
1 subgacs.b B = Base G
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 + G y - G x z x + G y - G x s
6 5 raleqbi1dv z = s y z x + G y - G x z y s x + G y - G x s
7 6 ralbidv z = s x B y z x + G y - G x z x B y s x + G y - G x s
8 7 elrab3 s 𝒫 B s z 𝒫 B | x B y z x + G y - G x z x B y s x + G y - G x s
9 4 8 syl s SubGrp G s z 𝒫 B | x B y z x + G y - G x z x B y s x + G y - G x s
10 9 bicomd s SubGrp G x B y s x + G y - G x s s z 𝒫 B | x B y z x + G y - G x z
11 10 pm5.32i s SubGrp G x B y s x + G y - G x s s SubGrp G s z 𝒫 B | x B y z x + G y - G x z
12 eqid + G = + G
13 eqid - G = - G
14 1 12 13 isnsg3 s NrmSGrp G s SubGrp G x B y s x + G y - G x s
15 elin s SubGrp G z 𝒫 B | x B y z x + G y - G x z s SubGrp G s z 𝒫 B | x B y z x + G y - G x z
16 11 14 15 3bitr4i s NrmSGrp G s SubGrp G z 𝒫 B | x B y z x + G y - G x z
17 16 eqriv NrmSGrp G = SubGrp G z 𝒫 B | x B y z x + G y - G x 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 + G y B
24 23 3expb G Grp x B y B x + G y B
25 simprl G Grp x B y B x B
26 1 13 grpsubcl G Grp x + G y B x B x + G y - G x B
27 22 24 25 26 syl3anc G Grp x B y B x + G y - G x B
28 27 ralrimivva G Grp x B y B x + G y - G x B
29 acsfn1c B V x B y B x + G y - G x B z 𝒫 B | x B y z x + G y - G x z ACS B
30 18 28 29 sylancr G Grp z 𝒫 B | x B y z x + G y - G x z ACS B
31 mreincl ACS B Moore 𝒫 B SubGrp G ACS B z 𝒫 B | x B y z x + G y - G x z ACS B SubGrp G z 𝒫 B | x B y z x + G y - G x z ACS B
32 20 21 30 31 syl3anc G Grp SubGrp G z 𝒫 B | x B y z x + G y - G x z ACS B
33 17 32 eqeltrid G Grp NrmSGrp G ACS B