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

Metamath Proof Explorer

Theorem ecqusaddd

Description: Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025)

Ref Expression
Hypotheses ecqusaddd.i ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
ecqusaddd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ecqusaddd.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
ecqusaddd.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
Assertion ecqusaddd ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ∼ = ( [ 𝐴 ] ∼ ( +g ‘ 𝑄 ) [ 𝐶 ] ∼ ) )

Proof

Step Hyp Ref Expression
1 ecqusaddd.i ⊢ ( 𝜑 → 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) )
2 ecqusaddd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 ecqusaddd.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
4 ecqusaddd.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
5 1 anim1i ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
6 3anass ⊢ ( ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ↔ ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) )
7 5 6 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) )
8 3 oveq2i ⊢ ( 𝑅 /s ∼ ) = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
9 4 8 eqtri ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝐼 ) )
10 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
12 9 2 10 11 qusadd ⊢ ( ( 𝐼 ∈ ( NrmSGrp ‘ 𝑅 ) ∧ 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( [ 𝐴 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ 𝑄 ) [ 𝐶 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ( 𝑅 ~QG 𝐼 ) )
13 7 12 syl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ 𝑄 ) [ 𝐶 ] ( 𝑅 ~QG 𝐼 ) ) = [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ( 𝑅 ~QG 𝐼 ) )
14 3 eceq2i ⊢ [ 𝐴 ] ∼ = [ 𝐴 ] ( 𝑅 ~QG 𝐼 )
15 3 eceq2i ⊢ [ 𝐶 ] ∼ = [ 𝐶 ] ( 𝑅 ~QG 𝐼 )
16 14 15 oveq12i ⊢ ( [ 𝐴 ] ∼ ( +g ‘ 𝑄 ) [ 𝐶 ] ∼ ) = ( [ 𝐴 ] ( 𝑅 ~QG 𝐼 ) ( +g ‘ 𝑄 ) [ 𝐶 ] ( 𝑅 ~QG 𝐼 ) )
17 3 eceq2i ⊢ [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ∼ = [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ( 𝑅 ~QG 𝐼 )
18 13 16 17 3eqtr4g ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( [ 𝐴 ] ∼ ( +g ‘ 𝑄 ) [ 𝐶 ] ∼ ) = [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ∼ )
19 18 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → [ ( 𝐴 ( +g ‘ 𝑅 ) 𝐶 ) ] ∼ = ( [ 𝐴 ] ∼ ( +g ‘ 𝑄 ) [ 𝐶 ] ∼ ) )