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

Metamath Proof Explorer

Theorem cntrnsg

Description: The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypothesis cntrnsg.z ⊢ 𝑍 = ( Cntr ‘ 𝑀 )
Assertion cntrnsg ( 𝑀 ∈ Grp → 𝑍 ∈ ( NrmSGrp ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 cntrnsg.z ⊢ 𝑍 = ( Cntr ‘ 𝑀 )
2 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 eqid ⊢ ( Cntz ‘ 𝑀 ) = ( Cntz ‘ 𝑀 )
4 2 3 cntrval ⊢ ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) = ( Cntr ‘ 𝑀 )
5 1 4 eqtr4i ⊢ 𝑍 = ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) )
6 ssid ⊢ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 )
7 2 3 cntzsubg ⊢ ( ( 𝑀 ∈ Grp ∧ ( Base ‘ 𝑀 ) ⊆ ( Base ‘ 𝑀 ) ) → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubGrp ‘ 𝑀 ) )
8 6 7 mpan2 ⊢ ( 𝑀 ∈ Grp → ( ( Cntz ‘ 𝑀 ) ‘ ( Base ‘ 𝑀 ) ) ∈ ( SubGrp ‘ 𝑀 ) )
9 5 8 eqeltrid ⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ ( SubGrp ‘ 𝑀 ) )
10 ssid ⊢ 𝑍 ⊆ 𝑍
11 1 cntrsubgnsg ⊢ ( ( 𝑍 ∈ ( SubGrp ‘ 𝑀 ) ∧ 𝑍 ⊆ 𝑍 ) → 𝑍 ∈ ( NrmSGrp ‘ 𝑀 ) )
12 9 10 11 sylancl ⊢ ( 𝑀 ∈ Grp → 𝑍 ∈ ( NrmSGrp ‘ 𝑀 ) )