This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ( 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 𝐻 ) )