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 \in X ⟼ [x] (G ~_{QG} Y))$
Assertion	qusghm	$⊢ Y \in NrmSGrp (G) \to F \in (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 \in X ⟼ [x] (G ~_{QG} Y))$
4		eqid	$⊢ {Base}_{H} = {Base}_{H}$
5		eqid	$⊢ +_{G} = +_{G}$
6		eqid	$⊢ +_{H} = +_{H}$
7		nsgsubg	$⊢ Y \in NrmSGrp (G) \to Y \in SubGrp (G)$
8		subgrcl	$⊢ Y \in SubGrp (G) \to G \in Grp$
9	7 8	syl	$⊢ Y \in NrmSGrp (G) \to G \in Grp$
10	2	qusgrp	$⊢ Y \in NrmSGrp (G) \to H \in Grp$
11	2 1 4	quseccl	$⊢ (Y \in NrmSGrp (G) \land x \in X) \to [x] (G ~_{QG} Y) \in {Base}_{H}$
12	11 3	fmptd	$⊢ Y \in NrmSGrp (G) \to F : X ⟶ {Base}_{H}$
13	2 1 5 6	qusadd	$⊢ (Y \in NrmSGrp (G) \land y \in X \land z \in X) \to [y] (G ~_{QG} Y) +_{H} [z] (G ~_{QG} Y) = [(y +_{G} z)] (G ~_{QG} Y)$
14	13	3expb	$⊢ (Y \in NrmSGrp (G) \land (y \in X \land z \in X)) \to [y] (G ~_{QG} Y) +_{H} [z] (G ~_{QG} Y) = [(y +_{G} z)] (G ~_{QG} Y)$
15		eceq1	$⊢ x = y \to [x] (G ~_{QG} Y) = [y] (G ~_{QG} Y)$
16		ovex	$⊢ G ~_{QG} Y \in V$
17		ecexg	$⊢ G ~_{QG} Y \in V \to [x] (G ~_{QG} Y) \in V$
18	16 17	ax-mp	$⊢ [x] (G ~_{QG} Y) \in V$
19	15 3 18	fvmpt3i	$⊢ y \in X \to F (y) = [y] (G ~_{QG} Y)$
20	19	ad2antrl	$⊢ (Y \in NrmSGrp (G) \land (y \in X \land z \in X)) \to F (y) = [y] (G ~_{QG} Y)$
21		eceq1	$⊢ x = z \to [x] (G ~_{QG} Y) = [z] (G ~_{QG} Y)$
22	21 3 18	fvmpt3i	$⊢ z \in X \to F (z) = [z] (G ~_{QG} Y)$
23	22	ad2antll	$⊢ (Y \in NrmSGrp (G) \land (y \in X \land z \in X)) \to F (z) = [z] (G ~_{QG} Y)$
24	20 23	oveq12d	$⊢ (Y \in NrmSGrp (G) \land (y \in X \land z \in X)) \to F (y) +_{H} F (z) = [y] (G ~_{QG} Y) +_{H} [z] (G ~_{QG} Y)$
25	1 5	grpcl	$⊢ (G \in Grp \land y \in X \land z \in X) \to y +_{G} z \in X$
26	25	3expb	$⊢ (G \in Grp \land (y \in X \land z \in X)) \to y +_{G} z \in X$
27	9 26	sylan	$⊢ (Y \in NrmSGrp (G) \land (y \in X \land z \in X)) \to y +_{G} z \in X$
28		eceq1	$⊢ x = y +_{G} z \to [x] (G ~_{QG} Y) = [(y +_{G} z)] (G ~_{QG} Y)$
29	28 3 18	fvmpt3i	$⊢ y +_{G} z \in X \to F (y +_{G} z) = [(y +_{G} z)] (G ~_{QG} Y)$
30	27 29	syl	$⊢ (Y \in NrmSGrp (G) \land (y \in X \land z \in X)) \to F (y +_{G} z) = [(y +_{G} z)] (G ~_{QG} Y)$
31	14 24 30	3eqtr4rd	$⊢ (Y \in NrmSGrp (G) \land (y \in X \land z \in X)) \to F (y +_{G} z) = F (y) +_{H} F (z)$
32	1 4 5 6 9 10 12 31	isghmd	$⊢ Y \in NrmSGrp (G) \to F \in (G GrpHom H)$

Metamath Proof Explorer

Theorem qusghm

Proof