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 
|- ( 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 ] .~ ) )