Theorem ecqusaddd

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

	Ref	Expression
Hypotheses	ecqusaddd.i	|- ( ph -> I e. ( NrmSGrp ` R ) )
	ecqusaddd.b	|- B = ( Base ` R )
	ecqusaddd.g	|- .~ = ( R ~QG I )
	ecqusaddd.q	|- Q = ( R /s .~ )
Assertion	ecqusaddd	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A ( +g ` R ) C ) ] .~ = ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) )

Proof

Step	Hyp	Ref	Expression
1		ecqusaddd.i	|- ( ph -> I e. ( NrmSGrp ` R ) )
2		ecqusaddd.b	|- B = ( Base ` R )
3		ecqusaddd.g	|- .~ = ( R ~QG I )
4		ecqusaddd.q	|- Q = ( R /s .~ )
5	1	anim1i	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( I e. ( NrmSGrp ` R ) /\ ( A e. B /\ C e. B ) ) )
6		3anass	|- ( ( I e. ( NrmSGrp ` R ) /\ A e. B /\ C e. B ) <-> ( I e. ( NrmSGrp ` R ) /\ ( A e. B /\ C e. B ) ) )
7	5 6	sylibr	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( I e. ( NrmSGrp ` R ) /\ A e. B /\ C e. B ) )
8	3	oveq2i	|- ( R /s .~ ) = ( R /s ( R ~QG I ) )
9	4 8	eqtri	|- Q = ( R /s ( R ~QG I ) )
10		eqid	|- ( +g ` R ) = ( +g ` R )
11		eqid	|- ( +g ` Q ) = ( +g ` Q )
12	9 2 10 11	qusadd	|- ( ( I e. ( NrmSGrp ` R ) /\ A e. B /\ C e. B ) -> ( [ A ] ( R ~QG I ) ( +g ` Q ) [ C ] ( R ~QG I ) ) = [ ( A ( +g ` R ) C ) ] ( R ~QG I ) )
13	7 12	syl	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] ( R ~QG I ) ( +g ` Q ) [ C ] ( R ~QG I ) ) = [ ( A ( +g ` R ) C ) ] ( R ~QG I ) )
14	3	eceq2i	|- [ A ] .~ = [ A ] ( R ~QG I )
15	3	eceq2i	|- [ C ] .~ = [ C ] ( R ~QG I )
16	14 15	oveq12i	|- ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) = ( [ A ] ( R ~QG I ) ( +g ` Q ) [ C ] ( R ~QG I ) )
17	3	eceq2i	|- [ ( A ( +g ` R ) C ) ] .~ = [ ( A ( +g ` R ) C ) ] ( R ~QG I )
18	13 16 17	3eqtr4g	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) = [ ( A ( +g ` R ) C ) ] .~ )
19	18	eqcomd	|- ( ( ph /\ ( A e. B /\ C e. B ) ) -> [ ( A ( +g ` R ) C ) ] .~ = ( [ A ] .~ ( +g ` Q ) [ C ] .~ ) )