This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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