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