Metamath Proof Explorer

Theorem dvhvaddass

Description: Associativity of vector sum. (Contributed by NM, 31-Oct-2013)

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 dvhvaddass ( ( ( ðū ∈ 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 coass âŠĒ ( ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) ∘ ( 1st ‘ 𝐞 ) ) = ( ( 1st ‘ ðđ ) ∘ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) )
9 1 2 3 4 5 7 6 dvhvadd âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + 𝐚 ) = âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âŸĐ )
10 9 3adantr3 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + 𝐚 ) = âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âŸĐ )
11 10 fveq2d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 1st ‘ ( ðđ + 𝐚 ) ) = ( 1st ‘ âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âŸĐ ) )
12 fvex âŠĒ ( 1st ‘ ðđ ) ∈ V
13 fvex âŠĒ ( 1st ‘ 𝐚 ) ∈ V
14 12 13 coex âŠĒ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) ∈ V
15 ovex âŠĒ ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) ∈ V
16 14 15 op1st âŠĒ ( 1st ‘ âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âŸĐ ) = ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) )
17 11 16 eqtrdi âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 1st ‘ ( ðđ + 𝐚 ) ) = ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) )
18 17 coeq1d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( 1st ‘ ( ðđ + 𝐚 ) ) ∘ ( 1st ‘ 𝐞 ) ) = ( ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) ∘ ( 1st ‘ 𝐞 ) ) )
19 1 2 3 4 5 7 6 dvhvadd âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 𝐚 + 𝐞 ) = âŸĻ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ )
20 19 3adantr1 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 𝐚 + 𝐞 ) = âŸĻ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ )
21 20 fveq2d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 1st ‘ ( 𝐚 + 𝐞 ) ) = ( 1st ‘ âŸĻ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ ) )
22 fvex âŠĒ ( 1st ‘ 𝐞 ) ∈ V
23 13 22 coex âŠĒ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) ∈ V
24 ovex âŠĒ ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) ∈ V
25 23 24 op1st âŠĒ ( 1st ‘ âŸĻ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ ) = ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) )
26 21 25 eqtrdi âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 1st ‘ ( 𝐚 + 𝐞 ) ) = ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) )
27 26 coeq2d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ ( 𝐚 + 𝐞 ) ) ) = ( ( 1st ‘ ðđ ) ∘ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) ) )
28 8 18 27 3eqtr4a âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( 1st ‘ ( ðđ + 𝐚 ) ) ∘ ( 1st ‘ 𝐞 ) ) = ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ ( 𝐚 + 𝐞 ) ) ) )
29 xp2nd âŠĒ ( ðđ ∈ ( 𝑇 × ðļ ) → ( 2nd ‘ ðđ ) ∈ ðļ )
30 xp2nd âŠĒ ( 𝐚 ∈ ( 𝑇 × ðļ ) → ( 2nd ‘ 𝐚 ) ∈ ðļ )
31 xp2nd âŠĒ ( 𝐞 ∈ ( 𝑇 × ðļ ) → ( 2nd ‘ 𝐞 ) ∈ ðļ )
32 29 30 31 3anim123i âŠĒ ( ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) → ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) )
33 eqid âŠĒ ( ( EDRing ‘ ðū ) ‘ 𝑊 ) = ( ( EDRing ‘ ðū ) ‘ 𝑊 )
34 1 33 4 5 dvhsca âŠĒ ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) → 𝐷 = ( ( EDRing ‘ ðū ) ‘ 𝑊 ) )
35 1 33 erngdv âŠĒ ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) → ( ( EDRing ‘ ðū ) ‘ 𝑊 ) ∈ DivRing )
36 34 35 eqeltrd âŠĒ ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) → 𝐷 ∈ DivRing )
37 drnggrp âŠĒ ( 𝐷 ∈ DivRing → 𝐷 ∈ Grp )
38 36 37 syl âŠĒ ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) → 𝐷 ∈ Grp )
39 38 adantr âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → 𝐷 ∈ Grp )
40 simpr1 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( 2nd ‘ ðđ ) ∈ ðļ )
41 eqid âŠĒ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
42 1 3 4 5 41 dvhbase âŠĒ ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) → ( Base ‘ 𝐷 ) = ðļ )
43 42 adantr âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( Base ‘ 𝐷 ) = ðļ )
44 40 43 eleqtrrd âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( 2nd ‘ ðđ ) ∈ ( Base ‘ 𝐷 ) )
45 simpr2 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( 2nd ‘ 𝐚 ) ∈ ðļ )
46 45 43 eleqtrrd âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( 2nd ‘ 𝐚 ) ∈ ( Base ‘ 𝐷 ) )
47 simpr3 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( 2nd ‘ 𝐞 ) ∈ ðļ )
48 47 43 eleqtrrd âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( 2nd ‘ 𝐞 ) ∈ ( Base ‘ 𝐷 ) )
49 41 6 grpass âŠĒ ( ( 𝐷 ∈ Grp ∧ ( ( 2nd ‘ ðđ ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝐚 ) ∈ ( Base ‘ 𝐷 ) ∧ ( 2nd ‘ 𝐞 ) ∈ ( Base ‘ 𝐷 ) ) ) → ( ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) = ( ( 2nd ‘ ðđ ) âĻĢ ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) ) )
50 39 44 46 48 49 syl13anc âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( 2nd ‘ ðđ ) ∈ ðļ ∧ ( 2nd ‘ 𝐚 ) ∈ ðļ ∧ ( 2nd ‘ 𝐞 ) ∈ ðļ ) ) → ( ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) = ( ( 2nd ‘ ðđ ) âĻĢ ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) ) )
51 32 50 sylan2 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) = ( ( 2nd ‘ ðđ ) âĻĢ ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) ) )
52 10 fveq2d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 2nd ‘ ( ðđ + 𝐚 ) ) = ( 2nd ‘ âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âŸĐ ) )
53 14 15 op2nd âŠĒ ( 2nd ‘ âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ 𝐚 ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âŸĐ ) = ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) )
54 52 53 eqtrdi âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 2nd ‘ ( ðđ + 𝐚 ) ) = ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) )
55 54 oveq1d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( 2nd ‘ ( ðđ + 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) = ( ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) )
56 20 fveq2d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 2nd ‘ ( 𝐚 + 𝐞 ) ) = ( 2nd ‘ âŸĻ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ ) )
57 23 24 op2nd âŠĒ ( 2nd ‘ âŸĻ ( ( 1st ‘ 𝐚 ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ ) = ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) )
58 56 57 eqtrdi âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 2nd ‘ ( 𝐚 + 𝐞 ) ) = ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) )
59 58 oveq2d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ ( 𝐚 + 𝐞 ) ) ) = ( ( 2nd ‘ ðđ ) âĻĢ ( ( 2nd ‘ 𝐚 ) âĻĢ ( 2nd ‘ 𝐞 ) ) ) )
60 51 55 59 3eqtr4d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( 2nd ‘ ( ðđ + 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) = ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ ( 𝐚 + 𝐞 ) ) ) )
61 28 60 opeq12d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → âŸĻ ( ( 1st ‘ ( ðđ + 𝐚 ) ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ ( ðđ + 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ = âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ ( 𝐚 + 𝐞 ) ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ ( 𝐚 + 𝐞 ) ) ) âŸĐ )
62 simpl âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) )
63 1 2 3 4 5 6 7 dvhvaddcl âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + 𝐚 ) ∈ ( 𝑇 × ðļ ) )
64 63 3adantr3 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + 𝐚 ) ∈ ( 𝑇 × ðļ ) )
65 simpr3 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → 𝐞 ∈ ( 𝑇 × ðļ ) )
66 1 2 3 4 5 7 6 dvhvadd âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ( ðđ + 𝐚 ) ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( ðđ + 𝐚 ) + 𝐞 ) = âŸĻ ( ( 1st ‘ ( ðđ + 𝐚 ) ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ ( ðđ + 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ )
67 62 64 65 66 syl12anc âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( ðđ + 𝐚 ) + 𝐞 ) = âŸĻ ( ( 1st ‘ ( ðđ + 𝐚 ) ) ∘ ( 1st ‘ 𝐞 ) ) , ( ( 2nd ‘ ( ðđ + 𝐚 ) ) âĻĢ ( 2nd ‘ 𝐞 ) ) âŸĐ )
68 simpr1 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ðđ ∈ ( 𝑇 × ðļ ) )
69 1 2 3 4 5 6 7 dvhvaddcl âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 𝐚 + 𝐞 ) ∈ ( 𝑇 × ðļ ) )
70 69 3adantr1 âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( 𝐚 + 𝐞 ) ∈ ( 𝑇 × ðļ ) )
71 1 2 3 4 5 7 6 dvhvadd âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ ( 𝐚 + 𝐞 ) ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + ( 𝐚 + 𝐞 ) ) = âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ ( 𝐚 + 𝐞 ) ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ ( 𝐚 + 𝐞 ) ) ) âŸĐ )
72 62 68 70 71 syl12anc âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + ( 𝐚 + 𝐞 ) ) = âŸĻ ( ( 1st ‘ ðđ ) ∘ ( 1st ‘ ( 𝐚 + 𝐞 ) ) ) , ( ( 2nd ‘ ðđ ) âĻĢ ( 2nd ‘ ( 𝐚 + 𝐞 ) ) ) âŸĐ )
73 61 67 72 3eqtr4d âŠĒ ( ( ( ðū ∈ HL ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ∧ 𝐞 ∈ ( 𝑇 × ðļ ) ) ) → ( ( ðđ + 𝐚 ) + 𝐞 ) = ( ðđ + ( 𝐚 + 𝐞 ) ) )