Metamath Proof Explorer

Theorem cntrsubgnsg

Description: A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypothesis cntrnsg.z 
|- Z = ( Cntr ` M )
Assertion cntrsubgnsg 
|- ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) -> X e. ( NrmSGrp ` M ) )

Proof

Step Hyp Ref Expression
1 cntrnsg.z 
 |-  Z = ( Cntr ` M )
2 simpl 
 |-  ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) -> X e. ( SubGrp ` M ) )
3 simplr 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> X C_ Z )
4 simprr 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> y e. X )
5 3 4 sseldd 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> y e. Z )
6 eqid 
 |-  ( Base ` M ) = ( Base ` M )
7 eqid 
 |-  ( Cntz ` M ) = ( Cntz ` M )
8 6 7 cntrval 
 |-  ( ( Cntz ` M ) ` ( Base ` M ) ) = ( Cntr ` M )
9 8 1 eqtr4i 
 |-  ( ( Cntz ` M ) ` ( Base ` M ) ) = Z
10 5 9 eleqtrrdi 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> y e. ( ( Cntz ` M ) ` ( Base ` M ) ) )
11 simprl 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> x e. ( Base ` M ) )
12 eqid 
 |-  ( +g ` M ) = ( +g ` M )
13 12 7 cntzi 
 |-  ( ( y e. ( ( Cntz ` M ) ` ( Base ` M ) ) /\ x e. ( Base ` M ) ) -> ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) )
14 10 11 13 syl2anc 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) )
15 14 oveq1d 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> ( ( y ( +g ` M ) x ) ( -g ` M ) x ) = ( ( x ( +g ` M ) y ) ( -g ` M ) x ) )
16 subgrcl 
 |-  ( X e. ( SubGrp ` M ) -> M e. Grp )
17 16 ad2antrr 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> M e. Grp )
18 6 subgss 
 |-  ( X e. ( SubGrp ` M ) -> X C_ ( Base ` M ) )
19 18 ad2antrr 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> X C_ ( Base ` M ) )
20 19 4 sseldd 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> y e. ( Base ` M ) )
21 eqid 
 |-  ( -g ` M ) = ( -g ` M )
22 6 12 21 grppncan 
 |-  ( ( M e. Grp /\ y e. ( Base ` M ) /\ x e. ( Base ` M ) ) -> ( ( y ( +g ` M ) x ) ( -g ` M ) x ) = y )
23 17 20 11 22 syl3anc 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> ( ( y ( +g ` M ) x ) ( -g ` M ) x ) = y )
24 15 23 eqtr3d 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> ( ( x ( +g ` M ) y ) ( -g ` M ) x ) = y )
25 24 4 eqeltrd 
 |-  ( ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) /\ ( x e. ( Base ` M ) /\ y e. X ) ) -> ( ( x ( +g ` M ) y ) ( -g ` M ) x ) e. X )
26 25 ralrimivva 
 |-  ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) -> A. x e. ( Base ` M ) A. y e. X ( ( x ( +g ` M ) y ) ( -g ` M ) x ) e. X )
27 6 12 21 isnsg3 
 |-  ( X e. ( NrmSGrp ` M ) <-> ( X e. ( SubGrp ` M ) /\ A. x e. ( Base ` M ) A. y e. X ( ( x ( +g ` M ) y ) ( -g ` M ) x ) e. X ) )
28 2 26 27 sylanbrc 
 |-  ( ( X e. ( SubGrp ` M ) /\ X C_ Z ) -> X e. ( NrmSGrp ` M ) )