Step | Hyp | Ref
| Expression |
1 | | dvhvaddcl.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | dvhvaddcl.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
3 | | dvhvaddcl.e |
. . 3
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | | dvhvaddcl.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
5 | | dvhvaddcl.d |
. . 3
β’ π· = (Scalarβπ) |
6 | | dvhvaddcl.a |
. . 3
β’ + =
(+gβπ) |
7 | | dvhvaddcl.p |
. . 3
⒠⨣ =
(+gβπ·) |
8 | 1, 2, 3, 4, 5, 6, 7 | dvhvadd 39558 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) = β¨((1st βπΉ) β (1st
βπΊ)),
((2nd βπΉ)
⨣
(2nd βπΊ))β©) |
9 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΎ β HL β§ π β π»)) |
10 | | xp1st 7954 |
. . . . 5
β’ (πΉ β (π Γ πΈ) β (1st βπΉ) β π) |
11 | 10 | ad2antrl 727 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (1st βπΉ) β π) |
12 | | xp1st 7954 |
. . . . 5
β’ (πΊ β (π Γ πΈ) β (1st βπΊ) β π) |
13 | 12 | ad2antll 728 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (1st βπΊ) β π) |
14 | 1, 2 | ltrnco 39185 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (1st βπΉ) β π β§ (1st βπΊ) β π) β ((1st βπΉ) β (1st
βπΊ)) β π) |
15 | 9, 11, 13, 14 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((1st βπΉ) β (1st
βπΊ)) β π) |
16 | | eqid 2737 |
. . . . . . 7
β’ (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) |
17 | 1, 2, 3, 4, 5, 16,
7 | dvhfplusr 39550 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ⨣ = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
18 | 17 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ⨣ = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
19 | 18 | oveqd 7375 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((2nd βπΉ) ⨣ (2nd
βπΊ)) =
((2nd βπΉ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΊ))) |
20 | | xp2nd 7955 |
. . . . . 6
β’ (πΉ β (π Γ πΈ) β (2nd βπΉ) β πΈ) |
21 | 20 | ad2antrl 727 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (2nd βπΉ) β πΈ) |
22 | | xp2nd 7955 |
. . . . . 6
β’ (πΊ β (π Γ πΈ) β (2nd βπΊ) β πΈ) |
23 | 22 | ad2antll 728 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (2nd βπΊ) β πΈ) |
24 | 1, 2, 3, 16 | tendoplcl 39247 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ) β ((2nd βπΉ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΊ)) β πΈ) |
25 | 9, 21, 23, 24 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((2nd βπΉ)(π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))(2nd βπΊ)) β πΈ) |
26 | 19, 25 | eqeltrd 2838 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β ((2nd βπΉ) ⨣ (2nd
βπΊ)) β πΈ) |
27 | | opelxpi 5671 |
. . 3
β’
((((1st βπΉ) β (1st βπΊ)) β π β§ ((2nd βπΉ) ⨣ (2nd
βπΊ)) β πΈ) β β¨((1st
βπΉ) β
(1st βπΊ)),
((2nd βπΉ)
⨣
(2nd βπΊ))β© β (π Γ πΈ)) |
28 | 15, 26, 27 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β β¨((1st
βπΉ) β
(1st βπΊ)),
((2nd βπΉ)
⨣
(2nd βπΊ))β© β (π Γ πΈ)) |
29 | 8, 28 | eqeltrd 2838 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) β (π Γ πΈ)) |