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