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 ‘ 𝑄 ) [ 𝐶 ] ∼ ) )