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

Metamath Proof Explorer

Theorem ecovcom

Description: Lemma used to transfer a commutative law via an equivalence relation. (Contributed by NM, 29-Aug-1995) (Revised by David Abernethy, 4-Jun-2013)

Ref Expression
Hypotheses ecovcom.1 
|- C = ( ( S X. S ) /. .~ )
ecovcom.2 
|- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. D , G >. ] .~ )
ecovcom.3 
|- ( ( ( z e. S /\ w e. S ) /\ ( x e. S /\ y e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )
ecovcom.4 
|- D = H
ecovcom.5 
|- G = J
Assertion ecovcom 
|- ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )

Proof

Step Hyp Ref Expression
1 ecovcom.1 
 |-  C = ( ( S X. S ) /. .~ )
2 ecovcom.2 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. D , G >. ] .~ )
3 ecovcom.3 
 |-  ( ( ( z e. S /\ w e. S ) /\ ( x e. S /\ y e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )
4 ecovcom.4 
 |-  D = H
5 ecovcom.5 
 |-  G = J
6 oveq1 
 |-  ( [ <. x , y >. ] .~ = A -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = ( A .+ [ <. z , w >. ] .~ ) )
7 oveq2 
 |-  ( [ <. x , y >. ] .~ = A -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = ( [ <. z , w >. ] .~ .+ A ) )
8 6 7 eqeq12d 
 |-  ( [ <. x , y >. ] .~ = A -> ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) <-> ( A .+ [ <. z , w >. ] .~ ) = ( [ <. z , w >. ] .~ .+ A ) ) )
9 oveq2 
 |-  ( [ <. z , w >. ] .~ = B -> ( A .+ [ <. z , w >. ] .~ ) = ( A .+ B ) )
10 oveq1 
 |-  ( [ <. z , w >. ] .~ = B -> ( [ <. z , w >. ] .~ .+ A ) = ( B .+ A ) )
11 9 10 eqeq12d 
 |-  ( [ <. z , w >. ] .~ = B -> ( ( A .+ [ <. z , w >. ] .~ ) = ( [ <. z , w >. ] .~ .+ A ) <-> ( A .+ B ) = ( B .+ A ) ) )
12 opeq12 
 |-  ( ( D = H /\ G = J ) -> <. D , G >. = <. H , J >. )
13 12 eceq1d 
 |-  ( ( D = H /\ G = J ) -> [ <. D , G >. ] .~ = [ <. H , J >. ] .~ )
14 4 5 13 mp2an 
 |-  [ <. D , G >. ] .~ = [ <. H , J >. ] .~
15 3 ancoms 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) = [ <. H , J >. ] .~ )
16 14 2 15 3eqtr4a 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = ( [ <. z , w >. ] .~ .+ [ <. x , y >. ] .~ ) )
17 1 8 11 16 2ecoptocl 
 |-  ( ( A e. C /\ B e. C ) -> ( A .+ B ) = ( B .+ A ) )