Step | Hyp | Ref
| Expression |
1 | | eqidd 2734 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (Scalarβπ) = (Scalarβπ)) |
2 | | dialss.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | | eqid 2733 |
. . . . 5
β’
((TEndoβπΎ)βπ) = ((TEndoβπΎ)βπ) |
4 | | dialss.u |
. . . . 5
β’ π = ((DVecAβπΎ)βπ) |
5 | | eqid 2733 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2733 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | 2, 3, 4, 5, 6 | dvabase 39520 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβ(Scalarβπ)) = ((TEndoβπΎ)βπ)) |
8 | 7 | eqcomd 2739 |
. . 3
β’ ((πΎ β HL β§ π β π») β ((TEndoβπΎ)βπ) = (Baseβ(Scalarβπ))) |
9 | 8 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β ((TEndoβπΎ)βπ) = (Baseβ(Scalarβπ))) |
10 | | eqid 2733 |
. . . . 5
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
11 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
12 | 2, 10, 4, 11 | dvavbase 39526 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβπ) = ((LTrnβπΎ)βπ)) |
13 | 12 | eqcomd 2739 |
. . 3
β’ ((πΎ β HL β§ π β π») β ((LTrnβπΎ)βπ) = (Baseβπ)) |
14 | 13 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β ((LTrnβπΎ)βπ) = (Baseβπ)) |
15 | | eqidd 2734 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (+gβπ) = (+gβπ)) |
16 | | eqidd 2734 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (
Β·π βπ) = ( Β·π
βπ)) |
17 | | dialss.s |
. . 3
β’ π = (LSubSpβπ) |
18 | 17 | a1i 11 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β π = (LSubSpβπ)) |
19 | | dialss.b |
. . 3
β’ π΅ = (BaseβπΎ) |
20 | | dialss.l |
. . 3
β’ β€ =
(leβπΎ) |
21 | | dialss.i |
. . 3
β’ πΌ = ((DIsoAβπΎ)βπ) |
22 | 19, 20, 2, 10, 21 | diass 39555 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β ((LTrnβπΎ)βπ)) |
23 | 19, 20, 2, 21 | dian0 39552 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β β
) |
24 | | simpll 766 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (πΎ β HL β§ π β π»)) |
25 | | simpr1 1195 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π₯ β ((TEndoβπΎ)βπ)) |
26 | | simplr 768 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (π β π΅ β§ π β€ π)) |
27 | | simpr2 1196 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β (πΌβπ)) |
28 | 19, 20, 2, 10, 21 | diael 39556 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π β (πΌβπ)) β π β ((LTrnβπΎ)βπ)) |
29 | 24, 26, 27, 28 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β ((LTrnβπΎ)βπ)) |
30 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
31 | 2, 10, 3, 4, 30 | dvavsca 39530 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ))) β (π₯( Β·π
βπ)π) = (π₯βπ)) |
32 | 24, 25, 29, 31 | syl12anc 836 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (π₯( Β·π
βπ)π) = (π₯βπ)) |
33 | 32 | oveq1d 7376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π₯( Β·π
βπ)π)(+gβπ)π) = ((π₯βπ)(+gβπ)π)) |
34 | 2, 10, 3 | tendocl 39280 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π₯ β ((TEndoβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (π₯βπ) β ((LTrnβπΎ)βπ)) |
35 | 24, 25, 29, 34 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (π₯βπ) β ((LTrnβπΎ)βπ)) |
36 | | simpr3 1197 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β (πΌβπ)) |
37 | 19, 20, 2, 10, 21 | diael 39556 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π β (πΌβπ)) β π β ((LTrnβπΎ)βπ)) |
38 | 24, 26, 36, 37 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β ((LTrnβπΎ)βπ)) |
39 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
40 | 2, 10, 4, 39 | dvavadd 39528 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π₯βπ) β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ))) β ((π₯βπ)(+gβπ)π) = ((π₯βπ) β π)) |
41 | 24, 35, 38, 40 | syl12anc 836 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π₯βπ)(+gβπ)π) = ((π₯βπ) β π)) |
42 | 33, 41 | eqtrd 2773 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π₯( Β·π
βπ)π)(+gβπ)π) = ((π₯βπ) β π)) |
43 | 2, 10 | ltrnco 39232 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π₯βπ) β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β ((π₯βπ) β π) β ((LTrnβπΎ)βπ)) |
44 | 24, 35, 38, 43 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π₯βπ) β π) β ((LTrnβπΎ)βπ)) |
45 | | hllat 37875 |
. . . . . 6
β’ (πΎ β HL β πΎ β Lat) |
46 | 45 | ad3antrrr 729 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β πΎ β Lat) |
47 | | eqid 2733 |
. . . . . . 7
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
48 | 19, 2, 10, 47 | trlcl 38677 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π₯βπ) β π) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π₯βπ) β π)) β π΅) |
49 | 24, 44, 48 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)β((π₯βπ) β π)) β π΅) |
50 | 19, 2, 10, 47 | trlcl 38677 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π₯βπ) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(π₯βπ)) β π΅) |
51 | 24, 35, 50 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)β(π₯βπ)) β π΅) |
52 | 19, 2, 10, 47 | trlcl 38677 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β π΅) |
53 | 24, 38, 52 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)βπ) β π΅) |
54 | | eqid 2733 |
. . . . . . 7
β’
(joinβπΎ) =
(joinβπΎ) |
55 | 19, 54 | latjcl 18336 |
. . . . . 6
β’ ((πΎ β Lat β§
(((trLβπΎ)βπ)β(π₯βπ)) β π΅ β§ (((trLβπΎ)βπ)βπ) β π΅) β ((((trLβπΎ)βπ)β(π₯βπ))(joinβπΎ)(((trLβπΎ)βπ)βπ)) β π΅) |
56 | 46, 51, 53, 55 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((((trLβπΎ)βπ)β(π₯βπ))(joinβπΎ)(((trLβπΎ)βπ)βπ)) β π΅) |
57 | | simplrl 776 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β π΅) |
58 | 20, 54, 2, 10, 47 | trlco 39240 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π₯βπ) β ((LTrnβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β((π₯βπ) β π)) β€ ((((trLβπΎ)βπ)β(π₯βπ))(joinβπΎ)(((trLβπΎ)βπ)βπ))) |
59 | 24, 35, 38, 58 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)β((π₯βπ) β π)) β€ ((((trLβπΎ)βπ)β(π₯βπ))(joinβπΎ)(((trLβπΎ)βπ)βπ))) |
60 | 19, 2, 10, 47 | trlcl 38677 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β π΅) |
61 | 24, 29, 60 | syl2anc 585 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)βπ) β π΅) |
62 | 20, 2, 10, 47, 3 | tendotp 39274 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π₯ β ((TEndoβπΎ)βπ) β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(π₯βπ)) β€ (((trLβπΎ)βπ)βπ)) |
63 | 24, 25, 29, 62 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)β(π₯βπ)) β€ (((trLβπΎ)βπ)βπ)) |
64 | 19, 20, 2, 10, 47, 21 | diatrl 39557 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π β (πΌβπ)) β (((trLβπΎ)βπ)βπ) β€ π) |
65 | 24, 26, 27, 64 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)βπ) β€ π) |
66 | 19, 20, 46, 51, 61, 57, 63, 65 | lattrd 18343 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)β(π₯βπ)) β€ π) |
67 | 19, 20, 2, 10, 47, 21 | diatrl 39557 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π β (πΌβπ)) β (((trLβπΎ)βπ)βπ) β€ π) |
68 | 24, 26, 36, 67 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)βπ) β€ π) |
69 | 19, 20, 54 | latjle12 18347 |
. . . . . . 7
β’ ((πΎ β Lat β§
((((trLβπΎ)βπ)β(π₯βπ)) β π΅ β§ (((trLβπΎ)βπ)βπ) β π΅ β§ π β π΅)) β (((((trLβπΎ)βπ)β(π₯βπ)) β€ π β§ (((trLβπΎ)βπ)βπ) β€ π) β ((((trLβπΎ)βπ)β(π₯βπ))(joinβπΎ)(((trLβπΎ)βπ)βπ)) β€ π)) |
70 | 46, 51, 53, 57, 69 | syl13anc 1373 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((((trLβπΎ)βπ)β(π₯βπ)) β€ π β§ (((trLβπΎ)βπ)βπ) β€ π) β ((((trLβπΎ)βπ)β(π₯βπ))(joinβπΎ)(((trLβπΎ)βπ)βπ)) β€ π)) |
71 | 66, 68, 70 | mpbi2and 711 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((((trLβπΎ)βπ)β(π₯βπ))(joinβπΎ)(((trLβπΎ)βπ)βπ)) β€ π) |
72 | 19, 20, 46, 49, 56, 57, 59, 71 | lattrd 18343 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((trLβπΎ)βπ)β((π₯βπ) β π)) β€ π) |
73 | 19, 20, 2, 10, 47, 21 | diaelval 39546 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (((π₯βπ) β π) β (πΌβπ) β (((π₯βπ) β π) β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)β((π₯βπ) β π)) β€ π))) |
74 | 73 | adantr 482 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((π₯βπ) β π) β (πΌβπ) β (((π₯βπ) β π) β ((LTrnβπΎ)βπ) β§ (((trLβπΎ)βπ)β((π₯βπ) β π)) β€ π))) |
75 | 44, 72, 74 | mpbir2and 712 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π₯βπ) β π) β (πΌβπ)) |
76 | 42, 75 | eqeltrd 2834 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β§ (π₯ β ((TEndoβπΎ)βπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π₯( Β·π
βπ)π)(+gβπ)π) β (πΌβπ)) |
77 | 1, 9, 14, 15, 16, 18, 22, 23, 76 | islssd 20440 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β π) |