Metamath Proof Explorer

Theorem qussub

Description: Value of the group subtraction operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
qusinv.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
qussub.p ⊢ − = ( -g ‘ 𝐺 )
qussub.a ⊢ 𝑁 = ( -g ‘ 𝐻 )
Assertion qussub ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) 𝑁 [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 − 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) )

Proof

Step Hyp Ref Expression
1 qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
2 qusinv.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
3 qussub.p ⊢ − = ( -g ‘ 𝐺 )
4 qussub.a ⊢ 𝑁 = ( -g ‘ 𝐻 )
5 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
6 1 2 5 quseccl ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
7 6 3adant3 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
8 1 2 5 quseccl ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ 𝑉 ) → [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
9 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
10 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
11 5 9 10 4 grpsubval ⊢ ( ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) ∧ [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) 𝑁 [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) = ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) ) )
12 7 8 11 3imp3i2an ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) 𝑁 [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) = ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) ) )
13 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
14 1 2 13 10 qusinv ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝐻 ) ‘ [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) )
15 14 3adant2 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝐻 ) ‘ [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) )
16 15 oveq2d ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) ( ( invg ‘ 𝐻 ) ‘ [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) ) = ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) ) )
17 nsgsubg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
18 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
19 17 18 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
20 2 13 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑉 )
21 19 20 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑉 )
22 21 3adant2 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑉 )
23 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
24 1 2 23 9 qusadd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ] ( 𝐺 ~QG 𝑆 ) )
25 22 24 syld3an3 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ] ( 𝐺 ~QG 𝑆 ) )
26 2 23 13 3 grpsubval ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
27 26 3adant1 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
28 27 eceq1d ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → [ ( 𝑋 − 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) = [ ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ] ( 𝐺 ~QG 𝑆 ) )
29 25 28 eqtr4d ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 − 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) )
30 12 16 29 3eqtrd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) 𝑁 [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 − 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) )