Metamath Proof Explorer

Theorem ecovass

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

Ref Expression
Hypotheses ecovass.1 
|- D = ( ( S X. S ) /. .~ )
ecovass.2 
|- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. G , H >. ] .~ )
ecovass.3 
|- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. N , Q >. ] .~ )
ecovass.4 
|- ( ( ( G e. S /\ H e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )
ecovass.5 
|- ( ( ( x e. S /\ y e. S ) /\ ( N e. S /\ Q e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )
ecovass.6 
|- ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( G e. S /\ H e. S ) )
ecovass.7 
|- ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( N e. S /\ Q e. S ) )
ecovass.8 
|- J = L
ecovass.9 
|- K = M
Assertion ecovass 
|- ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )

Proof

Step Hyp Ref Expression
1 ecovass.1 
 |-  D = ( ( S X. S ) /. .~ )
2 ecovass.2 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = [ <. G , H >. ] .~ )
3 ecovass.3 
 |-  ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. N , Q >. ] .~ )
4 ecovass.4 
 |-  ( ( ( G e. S /\ H e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )
5 ecovass.5 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( N e. S /\ Q e. S ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )
6 ecovass.6 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( G e. S /\ H e. S ) )
7 ecovass.7 
 |-  ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( N e. S /\ Q e. S ) )
8 ecovass.8 
 |-  J = L
9 ecovass.9 
 |-  K = M
10 oveq1 
 |-  ( [ <. x , y >. ] .~ = A -> ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) = ( A .+ [ <. z , w >. ] .~ ) )
11 10 oveq1d 
 |-  ( [ <. x , y >. ] .~ = A -> ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( ( A .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) )
12 oveq1 
 |-  ( [ <. x , y >. ] .~ = A -> ( [ <. x , y >. ] .~ .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) = ( A .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) )
13 11 12 eqeq12d 
 |-  ( [ <. x , y >. ] .~ = A -> ( ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( [ <. x , y >. ] .~ .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) <-> ( ( A .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( A .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) ) )
14 oveq2 
 |-  ( [ <. z , w >. ] .~ = B -> ( A .+ [ <. z , w >. ] .~ ) = ( A .+ B ) )
15 14 oveq1d 
 |-  ( [ <. z , w >. ] .~ = B -> ( ( A .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( ( A .+ B ) .+ [ <. v , u >. ] .~ ) )
16 oveq1 
 |-  ( [ <. z , w >. ] .~ = B -> ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) = ( B .+ [ <. v , u >. ] .~ ) )
17 16 oveq2d 
 |-  ( [ <. z , w >. ] .~ = B -> ( A .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) = ( A .+ ( B .+ [ <. v , u >. ] .~ ) ) )
18 15 17 eqeq12d 
 |-  ( [ <. z , w >. ] .~ = B -> ( ( ( A .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( A .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) <-> ( ( A .+ B ) .+ [ <. v , u >. ] .~ ) = ( A .+ ( B .+ [ <. v , u >. ] .~ ) ) ) )
19 oveq2 
 |-  ( [ <. v , u >. ] .~ = C -> ( ( A .+ B ) .+ [ <. v , u >. ] .~ ) = ( ( A .+ B ) .+ C ) )
20 oveq2 
 |-  ( [ <. v , u >. ] .~ = C -> ( B .+ [ <. v , u >. ] .~ ) = ( B .+ C ) )
21 20 oveq2d 
 |-  ( [ <. v , u >. ] .~ = C -> ( A .+ ( B .+ [ <. v , u >. ] .~ ) ) = ( A .+ ( B .+ C ) ) )
22 19 21 eqeq12d 
 |-  ( [ <. v , u >. ] .~ = C -> ( ( ( A .+ B ) .+ [ <. v , u >. ] .~ ) = ( A .+ ( B .+ [ <. v , u >. ] .~ ) ) <-> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) ) )
23 opeq12 
 |-  ( ( J = L /\ K = M ) -> <. J , K >. = <. L , M >. )
24 23 eceq1d 
 |-  ( ( J = L /\ K = M ) -> [ <. J , K >. ] .~ = [ <. L , M >. ] .~ )
25 8 9 24 mp2an 
 |-  [ <. J , K >. ] .~ = [ <. L , M >. ] .~
26 2 oveq1d 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) -> ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) )
27 26 adantr 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) /\ ( v e. S /\ u e. S ) ) -> ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) )
28 6 4 sylan 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. G , H >. ] .~ .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )
29 27 28 eqtrd 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) ) /\ ( v e. S /\ u e. S ) ) -> ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )
30 29 3impa 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = [ <. J , K >. ] .~ )
31 3 oveq2d 
 |-  ( ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. x , y >. ] .~ .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) = ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) )
32 31 adantl 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) ) -> ( [ <. x , y >. ] .~ .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) = ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) )
33 7 5 sylan2 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) ) -> ( [ <. x , y >. ] .~ .+ [ <. N , Q >. ] .~ ) = [ <. L , M >. ] .~ )
34 32 33 eqtrd 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) ) -> ( [ <. x , y >. ] .~ .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) = [ <. L , M >. ] .~ )
35 34 3impb 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( [ <. x , y >. ] .~ .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) = [ <. L , M >. ] .~ )
36 25 30 35 3eqtr4a 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( v e. S /\ u e. S ) ) -> ( ( [ <. x , y >. ] .~ .+ [ <. z , w >. ] .~ ) .+ [ <. v , u >. ] .~ ) = ( [ <. x , y >. ] .~ .+ ( [ <. z , w >. ] .~ .+ [ <. v , u >. ] .~ ) ) )
37 1 13 18 22 36 3ecoptocl 
 |-  ( ( A e. D /\ B e. D /\ C e. D ) -> ( ( A .+ B ) .+ C ) = ( A .+ ( B .+ C ) ) )