Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (πΎ β HL β§ π β π»)) |
2 | | simp3l 1199 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β π β πΈ) |
3 | | cdlemn8.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
4 | | cdlemn8.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
5 | | cdlemn8.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
6 | | cdlemn8.p |
. . . . . . 7
β’ π = ((ocβπΎ)βπ) |
7 | 3, 4, 5, 6 | lhpocnel2 39193 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (π β π΄ β§ Β¬ π β€ π)) |
8 | 1, 7 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (π β π΄ β§ Β¬ π β€ π)) |
9 | | simp2l 1197 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (π β π΄ β§ Β¬ π β€ π)) |
10 | | cdlemn8.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
11 | | cdlemn8.f |
. . . . . 6
β’ πΉ = (β©β β π (ββπ) = π) |
12 | 3, 4, 5, 10, 11 | ltrniotacl 39753 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
13 | 1, 8, 9, 12 | syl3anc 1369 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β πΉ β π) |
14 | | cdlemn8.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
15 | 5, 10, 14 | tendocl 39941 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π βπΉ) β π) |
16 | 1, 2, 13, 15 | syl3anc 1369 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (π βπΉ) β π) |
17 | | simp3r 1200 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β π β π) |
18 | | cdlemn8.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
19 | | cdlemn8.o |
. . . . 5
β’ π = (β β π β¦ ( I βΎ π΅)) |
20 | 18, 5, 10, 14, 19 | tendo0cl 39964 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π β πΈ) |
21 | 1, 20 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β π β πΈ) |
22 | | cdlemn8.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
23 | | eqid 2730 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
24 | | cdlemn8.s |
. . . 4
β’ + =
(+gβπ) |
25 | | eqid 2730 |
. . . 4
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
26 | 5, 10, 14, 22, 23, 24, 25 | dvhopvadd 40267 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π βπΉ) β π β§ π β πΈ) β§ (π β π β§ π β πΈ)) β (β¨(π βπΉ), π β© + β¨π, πβ©) = β¨((π βπΉ) β π), (π (+gβ(Scalarβπ))π)β©) |
27 | 1, 16, 2, 17, 21, 26 | syl122anc 1377 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (β¨(π βπΉ), π β© + β¨π, πβ©) = β¨((π βπΉ) β π), (π (+gβ(Scalarβπ))π)β©) |
28 | | eqid 2730 |
. . . . . . 7
β’ (π‘ β πΈ, π’ β πΈ β¦ (β β π β¦ ((π‘ββ) β (π’ββ)))) = (π‘ β πΈ, π’ β πΈ β¦ (β β π β¦ ((π‘ββ) β (π’ββ)))) |
29 | 5, 10, 14, 22, 23, 28, 25 | dvhfplusr 40258 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β
(+gβ(Scalarβπ)) = (π‘ β πΈ, π’ β πΈ β¦ (β β π β¦ ((π‘ββ) β (π’ββ))))) |
30 | 1, 29 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β
(+gβ(Scalarβπ)) = (π‘ β πΈ, π’ β πΈ β¦ (β β π β¦ ((π‘ββ) β (π’ββ))))) |
31 | 30 | oveqd 7428 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (π (+gβ(Scalarβπ))π) = (π (π‘ β πΈ, π’ β πΈ β¦ (β β π β¦ ((π‘ββ) β (π’ββ))))π)) |
32 | 18, 5, 10, 14, 19, 28 | tendo0plr 39966 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π (π‘ β πΈ, π’ β πΈ β¦ (β β π β¦ ((π‘ββ) β (π’ββ))))π) = π ) |
33 | 1, 2, 32 | syl2anc 582 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (π (π‘ β πΈ, π’ β πΈ β¦ (β β π β¦ ((π‘ββ) β (π’ββ))))π) = π ) |
34 | 31, 33 | eqtrd 2770 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (π (+gβ(Scalarβπ))π) = π ) |
35 | 34 | opeq2d 4879 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β β¨((π βπΉ) β π), (π (+gβ(Scalarβπ))π)β© = β¨((π βπΉ) β π), π β©) |
36 | 27, 35 | eqtrd 2770 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
β π΄ β§ Β¬ π
β€ π)) β§ (π β πΈ β§ π β π)) β (β¨(π βπΉ), π β© + β¨π, πβ©) = β¨((π βπΉ) β π), π β©) |