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