Step | Hyp | Ref
| Expression |
1 | | lcfl9a.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | lcfl9a.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
3 | | lcfl9a.o |
. . . . 5
β’ β₯ =
((ocHβπΎ)βπ) |
4 | | lcfl9a.v |
. . . . 5
β’ π = (Baseβπ) |
5 | | lcfl9a.k |
. . . . 5
β’ (π β (πΎ β HL β§ π β π»)) |
6 | 1, 2, 3, 4, 5 | dochoc1 39874 |
. . . 4
β’ (π β ( β₯ β( β₯
βπ)) = π) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β§ π = (0gβπ)) β ( β₯ β( β₯
βπ)) = π) |
8 | | lcfl9a.f |
. . . . . . . 8
β’ πΉ = (LFnlβπ) |
9 | | lcfl9a.l |
. . . . . . . 8
β’ πΏ = (LKerβπ) |
10 | 1, 2, 5 | dvhlmod 39623 |
. . . . . . . 8
β’ (π β π β LMod) |
11 | | lcfl9a.g |
. . . . . . . 8
β’ (π β πΊ β πΉ) |
12 | 4, 8, 9, 10, 11 | lkrssv 37608 |
. . . . . . 7
β’ (π β (πΏβπΊ) β π) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π = (0gβπ)) β (πΏβπΊ) β π) |
14 | | sneq 4600 |
. . . . . . . . 9
β’ (π = (0gβπ) β {π} = {(0gβπ)}) |
15 | 14 | fveq2d 6850 |
. . . . . . . 8
β’ (π = (0gβπ) β ( β₯ β{π}) = ( β₯
β{(0gβπ)})) |
16 | | eqid 2733 |
. . . . . . . . . 10
β’
(0gβπ) = (0gβπ) |
17 | 1, 2, 3, 4, 16 | doch0 39871 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β ( β₯
β{(0gβπ)}) = π) |
18 | 5, 17 | syl 17 |
. . . . . . . 8
β’ (π β ( β₯
β{(0gβπ)}) = π) |
19 | 15, 18 | sylan9eqr 2795 |
. . . . . . 7
β’ ((π β§ π = (0gβπ)) β ( β₯ β{π}) = π) |
20 | | lcfl9a.s |
. . . . . . . 8
β’ (π β ( β₯ β{π}) β (πΏβπΊ)) |
21 | 20 | adantr 482 |
. . . . . . 7
β’ ((π β§ π = (0gβπ)) β ( β₯ β{π}) β (πΏβπΊ)) |
22 | 19, 21 | eqsstrrd 3987 |
. . . . . 6
β’ ((π β§ π = (0gβπ)) β π β (πΏβπΊ)) |
23 | 13, 22 | eqssd 3965 |
. . . . 5
β’ ((π β§ π = (0gβπ)) β (πΏβπΊ) = π) |
24 | 23 | fveq2d 6850 |
. . . 4
β’ ((π β§ π = (0gβπ)) β ( β₯ β(πΏβπΊ)) = ( β₯ βπ)) |
25 | 24 | fveq2d 6850 |
. . 3
β’ ((π β§ π = (0gβπ)) β ( β₯ β( β₯
β(πΏβπΊ))) = ( β₯ β( β₯
βπ))) |
26 | 7, 25, 23 | 3eqtr4d 2783 |
. 2
β’ ((π β§ π = (0gβπ)) β ( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ)) |
27 | 6 | adantr 482 |
. . 3
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β( β₯
βπ)) = π) |
28 | | simpr 486 |
. . . . 5
β’ ((π β§ (πΏβπΊ) = π) β (πΏβπΊ) = π) |
29 | 28 | fveq2d 6850 |
. . . 4
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β(πΏβπΊ)) = ( β₯ βπ)) |
30 | 29 | fveq2d 6850 |
. . 3
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β( β₯
β(πΏβπΊ))) = ( β₯ β( β₯
βπ))) |
31 | 27, 30, 28 | 3eqtr4d 2783 |
. 2
β’ ((π β§ (πΏβπΊ) = π) β ( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ)) |
32 | | lcfl9a.x |
. . . . . . 7
β’ (π β π β π) |
33 | 32 | snssd 4773 |
. . . . . 6
β’ (π β {π} β π) |
34 | | eqid 2733 |
. . . . . . 7
β’
((DIsoHβπΎ)βπ) = ((DIsoHβπΎ)βπ) |
35 | 1, 34, 2, 4, 3 | dochcl 39866 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ {π} β π) β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
36 | 5, 33, 35 | syl2anc 585 |
. . . . 5
β’ (π β ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) |
37 | 1, 34, 3 | dochoc 39880 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ( β₯ β{π}) β ran
((DIsoHβπΎ)βπ)) β ( β₯ β( β₯
β( β₯ β{π}))) = ( β₯ β{π})) |
38 | 5, 36, 37 | syl2anc 585 |
. . . 4
β’ (π β ( β₯ β( β₯
β( β₯ β{π}))) = ( β₯ β{π})) |
39 | 38 | adantr 482 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ( β₯ β( β₯
β( β₯ β{π}))) = ( β₯ β{π})) |
40 | 20 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ( β₯ β{π}) β (πΏβπΊ)) |
41 | | eqid 2733 |
. . . . . . 7
β’
(LSHypβπ) =
(LSHypβπ) |
42 | 1, 2, 5 | dvhlvec 39622 |
. . . . . . . 8
β’ (π β π β LVec) |
43 | 42 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β π β LVec) |
44 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β (πΎ β HL β§ π β π»)) |
45 | 32 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β π β π) |
46 | | simprl 770 |
. . . . . . . . 9
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β π β (0gβπ)) |
47 | | eldifsn 4751 |
. . . . . . . . 9
β’ (π β (π β {(0gβπ)}) β (π β π β§ π β (0gβπ))) |
48 | 45, 46, 47 | sylanbrc 584 |
. . . . . . . 8
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β π β (π β {(0gβπ)})) |
49 | 1, 3, 2, 4, 16, 41, 44, 48 | dochsnshp 39966 |
. . . . . . 7
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ( β₯ β{π}) β (LSHypβπ)) |
50 | | simprr 772 |
. . . . . . . 8
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β (πΏβπΊ) β π) |
51 | 4, 41, 8, 9, 42, 11 | lkrshp4 37620 |
. . . . . . . . 9
β’ (π β ((πΏβπΊ) β π β (πΏβπΊ) β (LSHypβπ))) |
52 | 51 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ((πΏβπΊ) β π β (πΏβπΊ) β (LSHypβπ))) |
53 | 50, 52 | mpbid 231 |
. . . . . . 7
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β (πΏβπΊ) β (LSHypβπ)) |
54 | 41, 43, 49, 53 | lshpcmp 37500 |
. . . . . 6
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β (( β₯ β{π}) β (πΏβπΊ) β ( β₯ β{π}) = (πΏβπΊ))) |
55 | 40, 54 | mpbid 231 |
. . . . 5
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ( β₯ β{π}) = (πΏβπΊ)) |
56 | 55 | fveq2d 6850 |
. . . 4
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ( β₯ β( β₯
β{π})) = ( β₯
β(πΏβπΊ))) |
57 | 56 | fveq2d 6850 |
. . 3
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ( β₯ β( β₯
β( β₯ β{π}))) = ( β₯ β( β₯
β(πΏβπΊ)))) |
58 | 39, 57, 55 | 3eqtr3d 2781 |
. 2
β’ ((π β§ (π β (0gβπ) β§ (πΏβπΊ) β π)) β ( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ)) |
59 | 26, 31, 58 | pm2.61da2ne 3030 |
1
β’ (π β ( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ)) |