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 / 𝑠 G ~ QG Y
qusghm.f F = x X x G ~ QG Y
Assertion qusghm Y NrmSGrp G F G GrpHom H

Proof

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