Metamath Proof Explorer

Theorem dvhvaddcomN

Description: Commutativity of vector sum. (Contributed by NM, 26-Oct-2013) (Revised by Mario Carneiro, 23-Jun-2014) (New usage is discouraged.)

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 dvhvaddcomN ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → F + ˙ G = G + ˙ F

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 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → K ∈ HL ∧ W ∈ H
9 xp1st ⊢ F ∈ T × E → 1 st ⁡ F ∈ T
10 9 ad2antrl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ F ∈ T
11 xp1st ⊢ G ∈ T × E → 1 st ⁡ G ∈ T
12 11 ad2antll ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ G ∈ T
13 1 2 ltrncom ⊢ K ∈ HL ∧ W ∈ H ∧ 1 st ⁡ F ∈ T ∧ 1 st ⁡ G ∈ T → 1 st ⁡ F ∘ 1 st ⁡ G = 1 st ⁡ G ∘ 1 st ⁡ F
14 8 10 12 13 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ F ∘ 1 st ⁡ G = 1 st ⁡ G ∘ 1 st ⁡ F
15 xp2nd ⊢ F ∈ T × E → 2 nd ⁡ F ∈ E
16 xp2nd ⊢ G ∈ T × E → 2 nd ⁡ G ∈ E
17 15 16 anim12i ⊢ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E
18 eqid ⊢ a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c = a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c
19 1 2 3 18 tendoplcom ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E → 2 nd ⁡ F a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ G = 2 nd ⁡ G a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ F
20 19 3expb ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E → 2 nd ⁡ F a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ G = 2 nd ⁡ G a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ F
21 17 20 sylan2 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ G = 2 nd ⁡ G a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ F
22 1 2 3 4 5 18 6 dvhfplusr ⊢ K ∈ HL ∧ W ∈ H → ⨣ ˙ = a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c
23 22 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → ⨣ ˙ = a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c
24 23 oveqd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G = 2 nd ⁡ F a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ G
25 23 oveqd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ F = 2 nd ⁡ G a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ F
26 21 24 25 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G = 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ F
27 14 26 opeq12d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G = 1 st ⁡ G ∘ 1 st ⁡ F 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ F
28 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
29 1 2 3 4 5 7 6 dvhvadd ⊢ K ∈ HL ∧ W ∈ H ∧ G ∈ T × E ∧ F ∈ T × E → G + ˙ F = 1 st ⁡ G ∘ 1 st ⁡ F 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ F
30 29 ancom2s ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → G + ˙ F = 1 st ⁡ G ∘ 1 st ⁡ F 2 nd ⁡ G ⨣ ˙ 2 nd ⁡ F
31 27 28 30 3eqtr4d ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → F + ˙ G = G + ˙ F