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