Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΎ β HL β§ π β π»)) |
2 | | xp1st 7954 |
. . . . 5
β’ (πΉ β (π Γ πΈ) β (1st βπΉ) β π) |
3 | 2 | ad2antrl 727 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (1st βπΉ) β π) |
4 | | xp1st 7954 |
. . . . 5
β’ (πΊ β (π Γ πΈ) β (1st βπΊ) β π) |
5 | 4 | ad2antll 728 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (1st βπΊ) β π) |
6 | | dvhvaddcl.h |
. . . . 5
β’ π» = (LHypβπΎ) |
7 | | dvhvaddcl.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
8 | 6, 7 | ltrncom 39204 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (1st βπΉ) β π β§ (1st βπΊ) β π) β ((1st βπΉ) β (1st
βπΊ)) =
((1st βπΊ)
β (1st βπΉ))) |
9 | 1, 3, 5, 8 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((1st βπΉ) β (1st
βπΊ)) =
((1st βπΊ)
β (1st βπΉ))) |
10 | | xp2nd 7955 |
. . . . . 6
β’ (πΉ β (π Γ πΈ) β (2nd βπΉ) β πΈ) |
11 | | xp2nd 7955 |
. . . . . 6
β’ (πΊ β (π Γ πΈ) β (2nd βπΊ) β πΈ) |
12 | 10, 11 | anim12i 614 |
. . . . 5
β’ ((πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ)) β ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ)) |
13 | | dvhvaddcl.e |
. . . . . . 7
β’ πΈ = ((TEndoβπΎ)βπ) |
14 | | eqid 2737 |
. . . . . . 7
β’ (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) |
15 | 6, 7, 13, 14 | tendoplcom 39248 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ) β ((2nd βπΉ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΊ)) = ((2nd βπΊ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΉ))) |
16 | 15 | 3expb 1121 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ)) β ((2nd βπΉ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΊ)) = ((2nd βπΊ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΉ))) |
17 | 12, 16 | sylan2 594 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((2nd βπΉ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΊ)) = ((2nd βπΊ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΉ))) |
18 | | dvhvaddcl.u |
. . . . . . 7
β’ π = ((DVecHβπΎ)βπ) |
19 | | dvhvaddcl.d |
. . . . . . 7
β’ π· = (Scalarβπ) |
20 | | dvhvaddcl.p |
. . . . . . 7
⒠⨣ =
(+gβπ·) |
21 | 6, 7, 13, 18, 19, 14, 20 | dvhfplusr 39550 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ⨣ = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
22 | 21 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ⨣ = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
23 | 22 | oveqd 7375 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((2nd βπΉ) ⨣ (2nd
βπΊ)) =
((2nd βπΉ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΊ))) |
24 | 22 | oveqd 7375 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((2nd βπΊ) ⨣ (2nd
βπΉ)) =
((2nd βπΊ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΉ))) |
25 | 17, 23, 24 | 3eqtr4d 2787 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((2nd βπΉ) ⨣ (2nd
βπΊ)) =
((2nd βπΊ)
⨣
(2nd βπΉ))) |
26 | 9, 25 | opeq12d 4839 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β β¨((1st
βπΉ) β
(1st βπΊ)),
((2nd βπΉ)
⨣
(2nd βπΊ))β© = β¨((1st
βπΊ) β
(1st βπΉ)),
((2nd βπΊ)
⨣
(2nd βπΉ))β©) |
27 | | dvhvaddcl.a |
. . 3
β’ + =
(+gβπ) |
28 | 6, 7, 13, 18, 19, 27, 20 | dvhvadd 39558 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) = β¨((1st βπΉ) β (1st
βπΊ)),
((2nd βπΉ)
⨣
(2nd βπΊ))β©) |
29 | 6, 7, 13, 18, 19, 27, 20 | dvhvadd 39558 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΊ β (π Γ πΈ) β§ πΉ β (π Γ πΈ))) β (πΊ + πΉ) = β¨((1st βπΊ) β (1st
βπΉ)),
((2nd βπΊ)
⨣
(2nd βπΉ))β©) |
30 | 29 | ancom2s 649 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΊ + πΉ) = β¨((1st βπΊ) β (1st
βπΉ)),
((2nd βπΊ)
⨣
(2nd βπΉ))β©) |
31 | 26, 28, 30 | 3eqtr4d 2787 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) = (πΊ + πΉ)) |