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 ‘ 𝐵 ) )