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

Metamath Proof Explorer

Theorem qusadd

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

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

Proof

Step Hyp Ref Expression
1 qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
2 qusadd.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
3 qusadd.p ⊢ + = ( +g ‘ 𝐺 )
4 qusadd.a ⊢ ✚ = ( +g ‘ 𝐻 )
5 1 a1i ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) ) )
6 2 a1i ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑉 = ( Base ‘ 𝐺 ) )
7 nsgsubg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
8 eqid ⊢ ( 𝐺 ~QG 𝑆 ) = ( 𝐺 ~QG 𝑆 )
9 2 8 eqger ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑆 ) Er 𝑉 )
10 7 9 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑆 ) Er 𝑉 )
11 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
12 7 11 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
13 2 8 3 eqgcpbl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( ( 𝑎 ( 𝐺 ~QG 𝑆 ) 𝑝 ∧ 𝑏 ( 𝐺 ~QG 𝑆 ) 𝑞 ) → ( 𝑎 + 𝑏 ) ( 𝐺 ~QG 𝑆 ) ( 𝑝 + 𝑞 ) ) )
14 2 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) → ( 𝑝 + 𝑞 ) ∈ 𝑉 )
15 14 3expb ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 + 𝑞 ) ∈ 𝑉 )
16 12 15 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( 𝑝 + 𝑞 ) ∈ 𝑉 )
17 5 6 10 12 13 16 3 4 qusaddval ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ✚ [ 𝑌 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 + 𝑌 ) ] ( 𝐺 ~QG 𝑆 ) )