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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	qusghm.h	⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
	qusghm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
Assertion	qusghm	⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		qusghm.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		qusghm.h	⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑌 ) )
3		qusghm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) )
4		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
5		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
6		eqid	⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
7		nsgsubg	⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑌 ∈ ( SubGrp ‘ 𝐺 ) )
8		subgrcl	⊢ ( 𝑌 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
9	7 8	syl	⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
10	2	qusgrp	⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
11	2 1 4	quseccl	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ ( Base ‘ 𝐻 ) )
12	11 3	fmptd	⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐹 : 𝑋 ⟶ ( Base ‘ 𝐻 ) )
13	2 1 5 6	qusadd	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ( +g ‘ 𝐻 ) [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ] ( 𝐺 ~QG 𝑌 ) )
14	13	3expb	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ( +g ‘ 𝐻 ) [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) ) = [ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ] ( 𝐺 ~QG 𝑌 ) )
15		eceq1	⊢ ( 𝑥 = 𝑦 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
16		ovex	⊢ ( 𝐺 ~QG 𝑌 ) ∈ V
17		ecexg	⊢ ( ( 𝐺 ~QG 𝑌 ) ∈ V → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ V )
18	16 17	ax-mp	⊢ [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) ∈ V
19	15 3 18	fvmpt3i	⊢ ( 𝑦 ∈ 𝑋 → ( 𝐹 ‘ 𝑦 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
20	19	ad2antrl	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑦 ) = [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) )
21		eceq1	⊢ ( 𝑥 = 𝑧 → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) )
22	21 3 18	fvmpt3i	⊢ ( 𝑧 ∈ 𝑋 → ( 𝐹 ‘ 𝑧 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) )
23	22	ad2antll	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝑧 ) = [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) )
24	20 23	oveq12d	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) = ( [ 𝑦 ] ( 𝐺 ~QG 𝑌 ) ( +g ‘ 𝐻 ) [ 𝑧 ] ( 𝐺 ~QG 𝑌 ) ) )
25	1 5	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
26	25	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
27	9 26	sylan	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 )
28		eceq1	⊢ ( 𝑥 = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) → [ 𝑥 ] ( 𝐺 ~QG 𝑌 ) = [ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ] ( 𝐺 ~QG 𝑌 ) )
29	28 3 18	fvmpt3i	⊢ ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑋 → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = [ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ] ( 𝐺 ~QG 𝑌 ) )
30	27 29	syl	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = [ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ] ( 𝐺 ~QG 𝑌 ) )
31	14 24 30	3eqtr4rd	⊢ ( ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) )
32	1 4 5 6 9 10 12 31	isghmd	⊢ ( 𝑌 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )