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 Z=CntrM
Assertion cntrnsg MGrpZNrmSGrpM

Proof

Step Hyp Ref Expression
1 cntrnsg.z Z=CntrM
2 eqid BaseM=BaseM
3 eqid CntzM=CntzM
4 2 3 cntrval CntzMBaseM=CntrM
5 1 4 eqtr4i Z=CntzMBaseM
6 ssid BaseMBaseM
7 2 3 cntzsubg MGrpBaseMBaseMCntzMBaseMSubGrpM
8 6 7 mpan2 MGrpCntzMBaseMSubGrpM
9 5 8 eqeltrid MGrpZSubGrpM
10 ssid ZZ
11 1 cntrsubgnsg ZSubGrpMZZZNrmSGrpM
12 9 10 11 sylancl MGrpZNrmSGrpM