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 ) )