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 ⊢ ⨣ ˙ = + D
dvhvaddcl.a ⊢ + ˙ = + U
Assertion dvhvaddass ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × 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 ⊢ ⨣ ˙ = + D
7 dvhvaddcl.a ⊢ + ˙ = + U
8 coass ⊢ 1 st ⁡ F ∘ 1 st ⁡ G ∘ 1 st ⁡ I = 1 st ⁡ F ∘ 1 st ⁡ G ∘ 1 st ⁡ I
9 1 2 3 4 5 7 6 dvhvadd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → F + ˙ G = 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G
10 9 3adantr3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → F + ˙ G = 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G
11 10 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ F + ˙ G = 1 st ⁡ 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G
12 fvex ⊢ 1 st ⁡ F ∈ V
13 fvex ⊢ 1 st ⁡ G ∈ V
14 12 13 coex ⊢ 1 st ⁡ F ∘ 1 st ⁡ G ∈ V
15 ovex ⊢ 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ∈ V
16 14 15 op1st ⊢ 1 st ⁡ 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G = 1 st ⁡ F ∘ 1 st ⁡ G
17 11 16 eqtrdi ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ F + ˙ G = 1 st ⁡ F ∘ 1 st ⁡ G
18 17 coeq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ F + ˙ G ∘ 1 st ⁡ I = 1 st ⁡ F ∘ 1 st ⁡ G ∘ 1 st ⁡ I
19 1 2 3 4 5 7 6 dvhvadd ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T × E ∧ I ∈ T × E → G + ˙ I = 1 st ⁡ G ∘ 1 st ⁡ I 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
20 19 3adantr1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → G + ˙ I = 1 st ⁡ G ∘ 1 st ⁡ I 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
21 20 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ G + ˙ I = 1 st ⁡ 1 st ⁡ G ∘ 1 st ⁡ I 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
22 fvex ⊢ 1 st ⁡ I ∈ V
23 13 22 coex ⊢ 1 st ⁡ G ∘ 1 st ⁡ I ∈ V
24 ovex ⊢ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I ∈ V
25 23 24 op1st ⊢ 1 st ⁡ 1 st ⁡ G ∘ 1 st ⁡ I 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I = 1 st ⁡ G ∘ 1 st ⁡ I
26 21 25 eqtrdi ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ G + ˙ I = 1 st ⁡ G ∘ 1 st ⁡ I
27 26 coeq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ F ∘ 1 st ⁡ G + ˙ I = 1 st ⁡ F ∘ 1 st ⁡ G ∘ 1 st ⁡ I
28 8 18 27 3eqtr4a ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ F + ˙ G ∘ 1 st ⁡ I = 1 st ⁡ F ∘ 1 st ⁡ G + ˙ I
29 xp2nd ⊢ F ∈ T × E → 2 nd ⁡ F ∈ E
30 xp2nd ⊢ G ∈ T × E → 2 nd ⁡ G ∈ E
31 xp2nd ⊢ I ∈ T × E → 2 nd ⁡ I ∈ E
32 29 30 31 3anim123i ⊢ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E
33 eqid ⊢ EDRing ⁡ K ⁡ W = EDRing ⁡ K ⁡ W
34 1 33 4 5 dvhsca ⊢ K ∈ HL ∧ W ∈ H → D = EDRing ⁡ K ⁡ W
35 1 33 erngdv ⊢ K ∈ HL ∧ W ∈ H → EDRing ⁡ K ⁡ W ∈ DivRing
36 34 35 eqeltrd ⊢ K ∈ HL ∧ W ∈ H → D ∈ DivRing
37 drnggrp ⊢ D ∈ DivRing → D ∈ Grp
38 36 37 syl ⊢ K ∈ HL ∧ W ∈ H → D ∈ Grp
39 38 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → D ∈ Grp
40 simpr1 ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → 2 nd ⁡ F ∈ E
41 eqid ⊢ Base D = Base D
42 1 3 4 5 41 dvhbase ⊢ K ∈ HL ∧ W ∈ H → Base D = E
43 42 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → Base D = E
44 40 43 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → 2 nd ⁡ F ∈ Base D
45 simpr2 ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → 2 nd ⁡ G ∈ E
46 45 43 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → 2 nd ⁡ G ∈ Base D
47 simpr3 ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → 2 nd ⁡ I ∈ E
48 47 43 eleqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → 2 nd ⁡ I ∈ Base D
49 41 6 grpass ⊢ D ∈ Grp ∧ 2 nd ⁡ F ∈ Base D ∧ 2 nd ⁡ G ∈ Base D ∧ 2 nd ⁡ I ∈ Base D → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
50 39 44 46 48 49 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E ∧ 2 nd ⁡ I ∈ E → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
51 32 50 sylan2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
52 10 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ F + ˙ G = 2 nd ⁡ 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G
53 14 15 op2nd ⊢ 2 nd ⁡ 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G
54 52 53 eqtrdi ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ F + ˙ G = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G
55 54 oveq1d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ F + ˙ G ⨣ ˙ 2 nd ⁡ I = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
56 20 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ G + ˙ I = 2 nd ⁡ 1 st ⁡ G ∘ 1 st ⁡ I 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
57 23 24 op2nd ⊢ 2 nd ⁡ 1 st ⁡ G ∘ 1 st ⁡ I 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I = 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
58 56 57 eqtrdi ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ G + ˙ I = 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
59 58 oveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G + ˙ I = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ I
60 51 55 59 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 2 nd ⁡ F + ˙ G ⨣ ˙ 2 nd ⁡ I = 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G + ˙ I
61 28 60 opeq12d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → 1 st ⁡ F + ˙ G ∘ 1 st ⁡ I 2 nd ⁡ F + ˙ G ⨣ ˙ 2 nd ⁡ I = 1 st ⁡ F ∘ 1 st ⁡ G + ˙ I 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G + ˙ I
62 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → K ∈ HL ∧ W ∈ H
63 1 2 3 4 5 6 7 dvhvaddcl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → F + ˙ G ∈ T × E
64 63 3adantr3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → F + ˙ G ∈ T × E
65 simpr3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → I ∈ T × E
66 1 2 3 4 5 7 6 dvhvadd ⊢ K ∈ HL ∧ W ∈ H ∧ F + ˙ G ∈ T × E ∧ I ∈ T × E → F + ˙ G + ˙ I = 1 st ⁡ F + ˙ G ∘ 1 st ⁡ I 2 nd ⁡ F + ˙ G ⨣ ˙ 2 nd ⁡ I
67 62 64 65 66 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → F + ˙ G + ˙ I = 1 st ⁡ F + ˙ G ∘ 1 st ⁡ I 2 nd ⁡ F + ˙ G ⨣ ˙ 2 nd ⁡ I
68 simpr1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → F ∈ T × E
69 1 2 3 4 5 6 7 dvhvaddcl ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T × E ∧ I ∈ T × E → G + ˙ I ∈ T × E
70 69 3adantr1 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → G + ˙ I ∈ T × E
71 1 2 3 4 5 7 6 dvhvadd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G + ˙ I ∈ T × E → F + ˙ G + ˙ I = 1 st ⁡ F ∘ 1 st ⁡ G + ˙ I 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G + ˙ I
72 62 68 70 71 syl12anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → F + ˙ G + ˙ I = 1 st ⁡ F ∘ 1 st ⁡ G + ˙ I 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G + ˙ I
73 61 67 72 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E ∧ I ∈ T × E → F + ˙ G + ˙ I = F + ˙ G + ˙ I