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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion nsgacs ( 𝐺 ∈ Grp → ( NrmSGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 subgacs.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 1 subgss ⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → 𝑠 ⊆ 𝐵 )
3 velpw ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↔ 𝑠 ⊆ 𝐵 )
4 2 3 sylibr ⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → 𝑠 ∈ 𝒫 𝐵 )
5 eleq2w ⊢ ( 𝑧 = 𝑠 → ( ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) )
6 5 raleqbi1dv ⊢ ( 𝑧 = 𝑠 → ( ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) )
7 6 ralbidv ⊢ ( 𝑧 = 𝑠 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) )
8 7 elrab3 ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) )
9 4 8 syl ⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) )
10 9 bicomd ⊢ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ↔ 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) )
11 10 pm5.32i ⊢ ( ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) )
12 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
13 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
14 1 12 13 isnsg3 ⊢ ( 𝑠 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑠 ) )
15 elin ⊢ ( 𝑠 ∈ ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ↔ ( 𝑠 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑠 ∈ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) )
16 11 14 15 3bitr4i ⊢ ( 𝑠 ∈ ( NrmSGrp ‘ 𝐺 ) ↔ 𝑠 ∈ ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) )
17 16 eqriv ⊢ ( NrmSGrp ‘ 𝐺 ) = ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } )
18 1 fvexi ⊢ 𝐵 ∈ V
19 mreacs ⊢ ( 𝐵 ∈ V → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
20 18 19 mp1i ⊢ ( 𝐺 ∈ Grp → ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) )
21 1 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
22 simpl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
23 1 12 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
24 23 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
25 simprl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
26 1 13 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
27 22 24 25 26 syl3anc ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
28 27 ralrimivva ⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
29 acsfn1c ⊢ ( ( 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 ) → { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ∈ ( ACS ‘ 𝐵 ) )
30 18 28 29 sylancr ⊢ ( 𝐺 ∈ Grp → { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ∈ ( ACS ‘ 𝐵 ) )
31 mreincl ⊢ ( ( ( ACS ‘ 𝐵 ) ∈ ( Moore ‘ 𝒫 𝐵 ) ∧ ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ∧ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ∈ ( ACS ‘ 𝐵 ) ) → ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ∈ ( ACS ‘ 𝐵 ) )
32 20 21 30 31 syl3anc ⊢ ( 𝐺 ∈ Grp → ( ( SubGrp ‘ 𝐺 ) ∩ { 𝑧 ∈ 𝒫 𝐵 ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝑧 ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( -g ‘ 𝐺 ) 𝑥 ) ∈ 𝑧 } ) ∈ ( ACS ‘ 𝐵 ) )
33 17 32 eqeltrid ⊢ ( 𝐺 ∈ Grp → ( NrmSGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )