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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvhvaddcl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvhvaddcl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvhvaddcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvhvaddcl.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
dvhvaddcl.p ⊢ ⨣ = ( +g ‘ 𝐷 )
dvhvaddcl.a ⊢ + = ( +g ‘ 𝑈 )
Assertion dvhvaddcomN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ( 𝐺 + 𝐹 ) )

Proof

Step Hyp Ref Expression
1 dvhvaddcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvhvaddcl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dvhvaddcl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 dvhvaddcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvhvaddcl.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
6 dvhvaddcl.p ⊢ ⨣ = ( +g ‘ 𝐷 )
7 dvhvaddcl.a ⊢ + = ( +g ‘ 𝑈 )
8 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 xp1st ⊢ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝐹 ) ∈ 𝑇 )
10 9 ad2antrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝐹 ) ∈ 𝑇 )
11 xp1st ⊢ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝐺 ) ∈ 𝑇 )
12 11 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝐺 ) ∈ 𝑇 )
13 1 2 ltrncom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 1st ‘ 𝐹 ) ∈ 𝑇 ∧ ( 1st ‘ 𝐺 ) ∈ 𝑇 ) → ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) = ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) )
14 8 10 12 13 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) = ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) )
15 xp2nd ⊢ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝐹 ) ∈ 𝐸 )
16 xp2nd ⊢ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝐺 ) ∈ 𝐸 )
17 15 16 anim12i ⊢ ( ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 2nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝐺 ) ∈ 𝐸 ) )
18 eqid ⊢ ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) )
19 1 2 3 18 tendoplcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝐺 ) ∈ 𝐸 ) → ( ( 2nd ‘ 𝐹 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐺 ) ) = ( ( 2nd ‘ 𝐺 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐹 ) ) )
20 19 3expb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 2nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝐺 ) ∈ 𝐸 ) ) → ( ( 2nd ‘ 𝐹 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐺 ) ) = ( ( 2nd ‘ 𝐺 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐹 ) ) )
21 17 20 sylan2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝐹 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐺 ) ) = ( ( 2nd ‘ 𝐺 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐹 ) ) )
22 1 2 3 4 5 18 6 dvhfplusr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) )
23 22 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ⨣ = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) )
24 23 oveqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) = ( ( 2nd ‘ 𝐹 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐺 ) ) )
25 23 oveqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝐺 ) ⨣ ( 2nd ‘ 𝐹 ) ) = ( ( 2nd ‘ 𝐺 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐹 ) ) )
26 21 24 25 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) = ( ( 2nd ‘ 𝐺 ) ⨣ ( 2nd ‘ 𝐹 ) ) )
27 14 26 opeq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) , ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) ⟩ = ⟨ ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) , ( ( 2nd ‘ 𝐺 ) ⨣ ( 2nd ‘ 𝐹 ) ) ⟩ )
28 1 2 3 4 5 7 6 dvhvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ⟨ ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) , ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) ⟩ )
29 1 2 3 4 5 7 6 dvhvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐺 + 𝐹 ) = ⟨ ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) , ( ( 2nd ‘ 𝐺 ) ⨣ ( 2nd ‘ 𝐹 ) ) ⟩ )
30 29 ancom2s ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐺 + 𝐹 ) = ⟨ ( ( 1st ‘ 𝐺 ) ∘ ( 1st ‘ 𝐹 ) ) , ( ( 2nd ‘ 𝐺 ) ⨣ ( 2nd ‘ 𝐹 ) ) ⟩ )
31 27 28 30 3eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ( 𝐺 + 𝐹 ) )