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 = ( Cntr ` M )
Assertion cntrnsg 
|- ( M e. Grp -> Z e. ( NrmSGrp ` M ) )

Proof

Step Hyp Ref Expression
1 cntrnsg.z 
 |-  Z = ( Cntr ` M )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( Cntz ` M ) = ( Cntz ` M )
4 2 3 cntrval 
 |-  ( ( Cntz ` M ) ` ( Base ` M ) ) = ( Cntr ` M )
5 1 4 eqtr4i 
 |-  Z = ( ( Cntz ` M ) ` ( Base ` M ) )
6 ssid 
 |-  ( Base ` M ) C_ ( Base ` M )
7 2 3 cntzsubg 
 |-  ( ( M e. Grp /\ ( Base ` M ) C_ ( Base ` M ) ) -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubGrp ` M ) )
8 6 7 mpan2 
 |-  ( M e. Grp -> ( ( Cntz ` M ) ` ( Base ` M ) ) e. ( SubGrp ` M ) )
9 5 8 eqeltrid 
 |-  ( M e. Grp -> Z e. ( SubGrp ` M ) )
10 ssid 
 |-  Z C_ Z
11 1 cntrsubgnsg 
 |-  ( ( Z e. ( SubGrp ` M ) /\ Z C_ Z ) -> Z e. ( NrmSGrp ` M ) )
12 9 10 11 sylancl 
 |-  ( M e. Grp -> Z e. ( NrmSGrp ` M ) )