Metamath Proof Explorer

Theorem dvhvaddass

Description: Associativity of vector sum. (Contributed by NM, 31-Oct-2013)

Ref Expression
Hypotheses dvhvaddcl.h 
|- H = ( LHyp ` K )
dvhvaddcl.t 
|- T = ( ( LTrn ` K ) ` W )
dvhvaddcl.e 
|- E = ( ( TEndo ` K ) ` W )
dvhvaddcl.u 
|- U = ( ( DVecH ` K ) ` W )
dvhvaddcl.d 
|- D = ( Scalar ` U )
dvhvaddcl.p 
|- .+^ = ( +g ` D )
dvhvaddcl.a 
|- .+ = ( +g ` U )
Assertion dvhvaddass 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = ( F .+ ( G .+ I ) ) )

Proof

Step Hyp Ref Expression
1 dvhvaddcl.h 
 |-  H = ( LHyp ` K )
2 dvhvaddcl.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 dvhvaddcl.e 
 |-  E = ( ( TEndo ` K ) ` W )
4 dvhvaddcl.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dvhvaddcl.d 
 |-  D = ( Scalar ` U )
6 dvhvaddcl.p 
 |-  .+^ = ( +g ` D )
7 dvhvaddcl.a 
 |-  .+ = ( +g ` U )
8 coass 
 |-  ( ( ( 1st ` F ) o. ( 1st ` G ) ) o. ( 1st ` I ) ) = ( ( 1st ` F ) o. ( ( 1st ` G ) o. ( 1st ` I ) ) )
9 1 2 3 4 5 7 6 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )
10 9 3adantr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( F .+ G ) = <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. )
11 10 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( F .+ G ) ) = ( 1st ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) )
12 fvex 
 |-  ( 1st ` F ) e. _V
13 fvex 
 |-  ( 1st ` G ) e. _V
14 12 13 coex 
 |-  ( ( 1st ` F ) o. ( 1st ` G ) ) e. _V
15 ovex 
 |-  ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) e. _V
16 14 15 op1st 
 |-  ( 1st ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) = ( ( 1st ` F ) o. ( 1st ` G ) )
17 11 16 eqtrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( F .+ G ) ) = ( ( 1st ` F ) o. ( 1st ` G ) ) )
18 17 coeq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) = ( ( ( 1st ` F ) o. ( 1st ` G ) ) o. ( 1st ` I ) ) )
19 1 2 3 4 5 7 6 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) = <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. )
20 19 3adantr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) = <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. )
21 20 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( G .+ I ) ) = ( 1st ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) )
22 fvex 
 |-  ( 1st ` I ) e. _V
23 13 22 coex 
 |-  ( ( 1st ` G ) o. ( 1st ` I ) ) e. _V
24 ovex 
 |-  ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) e. _V
25 23 24 op1st 
 |-  ( 1st ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) = ( ( 1st ` G ) o. ( 1st ` I ) )
26 21 25 eqtrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 1st ` ( G .+ I ) ) = ( ( 1st ` G ) o. ( 1st ` I ) ) )
27 26 coeq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) = ( ( 1st ` F ) o. ( ( 1st ` G ) o. ( 1st ` I ) ) ) )
28 8 18 27 3eqtr4a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) = ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) )
29 xp2nd 
 |-  ( F e. ( T X. E ) -> ( 2nd ` F ) e. E )
30 xp2nd 
 |-  ( G e. ( T X. E ) -> ( 2nd ` G ) e. E )
31 xp2nd 
 |-  ( I e. ( T X. E ) -> ( 2nd ` I ) e. E )
32 29 30 31 3anim123i 
 |-  ( ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) -> ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) )
33 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
34 1 33 4 5 dvhsca 
 |-  ( ( K e. HL /\ W e. H ) -> D = ( ( EDRing ` K ) ` W ) )
35 1 33 erngdv 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( EDRing ` K ) ` W ) e. DivRing )
36 34 35 eqeltrd 
 |-  ( ( K e. HL /\ W e. H ) -> D e. DivRing )
37 drnggrp 
 |-  ( D e. DivRing -> D e. Grp )
38 36 37 syl 
 |-  ( ( K e. HL /\ W e. H ) -> D e. Grp )
39 38 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> D e. Grp )
40 simpr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` F ) e. E )
41 eqid 
 |-  ( Base ` D ) = ( Base ` D )
42 1 3 4 5 41 dvhbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` D ) = E )
43 42 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( Base ` D ) = E )
44 40 43 eleqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` F ) e. ( Base ` D ) )
45 simpr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` G ) e. E )
46 45 43 eleqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` G ) e. ( Base ` D ) )
47 simpr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` I ) e. E )
48 47 43 eleqtrrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( 2nd ` I ) e. ( Base ` D ) )
49 41 6 grpass 
 |-  ( ( D e. Grp /\ ( ( 2nd ` F ) e. ( Base ` D ) /\ ( 2nd ` G ) e. ( Base ` D ) /\ ( 2nd ` I ) e. ( Base ` D ) ) ) -> ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) )
50 39 44 46 48 49 syl13anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( 2nd ` F ) e. E /\ ( 2nd ` G ) e. E /\ ( 2nd ` I ) e. E ) ) -> ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) )
51 32 50 sylan2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) )
52 10 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( F .+ G ) ) = ( 2nd ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) )
53 14 15 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` F ) o. ( 1st ` G ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) >. ) = ( ( 2nd ` F ) .+^ ( 2nd ` G ) )
54 52 53 eqtrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( F .+ G ) ) = ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) )
55 54 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) = ( ( ( 2nd ` F ) .+^ ( 2nd ` G ) ) .+^ ( 2nd ` I ) ) )
56 20 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( G .+ I ) ) = ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) )
57 23 24 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` G ) o. ( 1st ` I ) ) , ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) >. ) = ( ( 2nd ` G ) .+^ ( 2nd ` I ) )
58 56 57 eqtrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( 2nd ` ( G .+ I ) ) = ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) )
59 58 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) = ( ( 2nd ` F ) .+^ ( ( 2nd ` G ) .+^ ( 2nd ` I ) ) ) )
60 51 55 59 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) = ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) )
61 28 60 opeq12d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> <. ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) , ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) >. = <. ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) >. )
62 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( K e. HL /\ W e. H ) )
63 1 2 3 4 5 6 7 dvhvaddcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) ) ) -> ( F .+ G ) e. ( T X. E ) )
64 63 3adantr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( F .+ G ) e. ( T X. E ) )
65 simpr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> I e. ( T X. E ) )
66 1 2 3 4 5 7 6 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( F .+ G ) e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = <. ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) , ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) >. )
67 62 64 65 66 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = <. ( ( 1st ` ( F .+ G ) ) o. ( 1st ` I ) ) , ( ( 2nd ` ( F .+ G ) ) .+^ ( 2nd ` I ) ) >. )
68 simpr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> F e. ( T X. E ) )
69 1 2 3 4 5 6 7 dvhvaddcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) e. ( T X. E ) )
70 69 3adantr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( G .+ I ) e. ( T X. E ) )
71 1 2 3 4 5 7 6 dvhvadd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ ( G .+ I ) e. ( T X. E ) ) ) -> ( F .+ ( G .+ I ) ) = <. ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) >. )
72 62 68 70 71 syl12anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( F .+ ( G .+ I ) ) = <. ( ( 1st ` F ) o. ( 1st ` ( G .+ I ) ) ) , ( ( 2nd ` F ) .+^ ( 2nd ` ( G .+ I ) ) ) >. )
73 61 67 72 3eqtr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. ( T X. E ) /\ G e. ( T X. E ) /\ I e. ( T X. E ) ) ) -> ( ( F .+ G ) .+ I ) = ( F .+ ( G .+ I ) ) )