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