Metamath Proof Explorer

Theorem qusghm

Description: If Y is a normal subgroup of G , then the "natural map" from elements to their cosets is a group homomorphism from G to G / Y . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qusghm.x 
|- X = ( Base ` G )
qusghm.h 
|- H = ( G /s ( G ~QG Y ) )
qusghm.f 
|- F = ( x e. X |-> [ x ] ( G ~QG Y ) )
Assertion qusghm 
|- ( Y e. ( NrmSGrp ` G ) -> F e. ( G GrpHom H ) )

Proof

Step Hyp Ref Expression
1 qusghm.x 
 |-  X = ( Base ` G )
2 qusghm.h 
 |-  H = ( G /s ( G ~QG Y ) )
3 qusghm.f 
 |-  F = ( x e. X |-> [ x ] ( G ~QG Y ) )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 eqid 
 |-  ( +g ` H ) = ( +g ` H )
7 nsgsubg 
 |-  ( Y e. ( NrmSGrp ` G ) -> Y e. ( SubGrp ` G ) )
8 subgrcl 
 |-  ( Y e. ( SubGrp ` G ) -> G e. Grp )
9 7 8 syl 
 |-  ( Y e. ( NrmSGrp ` G ) -> G e. Grp )
10 2 qusgrp 
 |-  ( Y e. ( NrmSGrp ` G ) -> H e. Grp )
11 2 1 4 quseccl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ x e. X ) -> [ x ] ( G ~QG Y ) e. ( Base ` H ) )
12 11 3 fmptd 
 |-  ( Y e. ( NrmSGrp ` G ) -> F : X --> ( Base ` H ) )
13 2 1 5 6 qusadd 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ y e. X /\ z e. X ) -> ( [ y ] ( G ~QG Y ) ( +g ` H ) [ z ] ( G ~QG Y ) ) = [ ( y ( +g ` G ) z ) ] ( G ~QG Y ) )
14 13 3expb 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( y e. X /\ z e. X ) ) -> ( [ y ] ( G ~QG Y ) ( +g ` H ) [ z ] ( G ~QG Y ) ) = [ ( y ( +g ` G ) z ) ] ( G ~QG Y ) )
15 eceq1 
 |-  ( x = y -> [ x ] ( G ~QG Y ) = [ y ] ( G ~QG Y ) )
16 ovex 
 |-  ( G ~QG Y ) e. _V
17 ecexg 
 |-  ( ( G ~QG Y ) e. _V -> [ x ] ( G ~QG Y ) e. _V )
18 16 17 ax-mp 
 |-  [ x ] ( G ~QG Y ) e. _V
19 15 3 18 fvmpt3i 
 |-  ( y e. X -> ( F ` y ) = [ y ] ( G ~QG Y ) )
20 19 ad2antrl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( y e. X /\ z e. X ) ) -> ( F ` y ) = [ y ] ( G ~QG Y ) )
21 eceq1 
 |-  ( x = z -> [ x ] ( G ~QG Y ) = [ z ] ( G ~QG Y ) )
22 21 3 18 fvmpt3i 
 |-  ( z e. X -> ( F ` z ) = [ z ] ( G ~QG Y ) )
23 22 ad2antll 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( y e. X /\ z e. X ) ) -> ( F ` z ) = [ z ] ( G ~QG Y ) )
24 20 23 oveq12d 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( y e. X /\ z e. X ) ) -> ( ( F ` y ) ( +g ` H ) ( F ` z ) ) = ( [ y ] ( G ~QG Y ) ( +g ` H ) [ z ] ( G ~QG Y ) ) )
25 1 5 grpcl 
 |-  ( ( G e. Grp /\ y e. X /\ z e. X ) -> ( y ( +g ` G ) z ) e. X )
26 25 3expb 
 |-  ( ( G e. Grp /\ ( y e. X /\ z e. X ) ) -> ( y ( +g ` G ) z ) e. X )
27 9 26 sylan 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( y e. X /\ z e. X ) ) -> ( y ( +g ` G ) z ) e. X )
28 eceq1 
 |-  ( x = ( y ( +g ` G ) z ) -> [ x ] ( G ~QG Y ) = [ ( y ( +g ` G ) z ) ] ( G ~QG Y ) )
29 28 3 18 fvmpt3i 
 |-  ( ( y ( +g ` G ) z ) e. X -> ( F ` ( y ( +g ` G ) z ) ) = [ ( y ( +g ` G ) z ) ] ( G ~QG Y ) )
30 27 29 syl 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( y e. X /\ z e. X ) ) -> ( F ` ( y ( +g ` G ) z ) ) = [ ( y ( +g ` G ) z ) ] ( G ~QG Y ) )
31 14 24 30 3eqtr4rd 
 |-  ( ( Y e. ( NrmSGrp ` G ) /\ ( y e. X /\ z e. X ) ) -> ( F ` ( y ( +g ` G ) z ) ) = ( ( F ` y ) ( +g ` H ) ( F ` z ) ) )
32 1 4 5 6 9 10 12 31 isghmd 
 |-  ( Y e. ( NrmSGrp ` G ) -> F e. ( G GrpHom H ) )