Metamath Proof Explorer


Theorem cntrsubgnsg

Description: A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypothesis cntrnsg.z 𝑍 = ( Cntr ‘ 𝑀 )
Assertion cntrsubgnsg ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) → 𝑋 ∈ ( NrmSGrp ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 cntrnsg.z 𝑍 = ( Cntr ‘ 𝑀 )
2 simpl ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) → 𝑋 ∈ ( SubGrp ‘ 𝑀 ) )
3 simplr ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑋𝑍 )
4 simprr ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑦𝑋 )
5 3 4 sseldd ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑦𝑍 )
6 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
7 eqid ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 )
8 6 7 cntrval ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = ( Cntr ‘ 𝑀 )
9 8 1 eqtr4i ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = 𝑍
10 5 9 eleqtrrdi ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑦 ∈ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) )
11 simprl ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
12 eqid ( +g𝑀 ) = ( +g𝑀 )
13 12 7 cntzi ( ( 𝑦 ∈ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑦 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
14 10 11 13 syl2anc ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → ( 𝑦 ( +g𝑀 ) 𝑥 ) = ( 𝑥 ( +g𝑀 ) 𝑦 ) )
15 14 oveq1d ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → ( ( 𝑦 ( +g𝑀 ) 𝑥 ) ( -g𝑀 ) 𝑥 ) = ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( -g𝑀 ) 𝑥 ) )
16 subgrcl ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) → 𝑀 ∈ Grp )
17 16 ad2antrr ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑀 ∈ Grp )
18 6 subgss ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
19 18 ad2antrr ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑀 ) )
20 19 4 sseldd ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝑀 ) )
21 eqid ( -g𝑀 ) = ( -g𝑀 )
22 6 12 21 grppncan ( ( 𝑀 ∈ Grp ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑦 ( +g𝑀 ) 𝑥 ) ( -g𝑀 ) 𝑥 ) = 𝑦 )
23 17 20 11 22 syl3anc ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → ( ( 𝑦 ( +g𝑀 ) 𝑥 ) ( -g𝑀 ) 𝑥 ) = 𝑦 )
24 15 23 eqtr3d ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( -g𝑀 ) 𝑥 ) = 𝑦 )
25 24 4 eqeltrd ( ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦𝑋 ) ) → ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( -g𝑀 ) 𝑥 ) ∈ 𝑋 )
26 25 ralrimivva ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦𝑋 ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( -g𝑀 ) 𝑥 ) ∈ 𝑋 )
27 6 12 21 isnsg3 ( 𝑋 ∈ ( NrmSGrp ‘ 𝑀 ) ↔ ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦𝑋 ( ( 𝑥 ( +g𝑀 ) 𝑦 ) ( -g𝑀 ) 𝑥 ) ∈ 𝑋 ) )
28 2 26 27 sylanbrc ( ( 𝑋 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑋𝑍 ) → 𝑋 ∈ ( NrmSGrp ‘ 𝑀 ) )