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 ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + 𝐚 ) = ( 𝐚 + ðđ ) )