Step | Hyp | Ref
| Expression |
1 | | dochlkr.k |
. . . . . . . 8
β’ (π β (πΎ β HL β§ π β π»)) |
2 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
3 | | dochlkr.f |
. . . . . . . . 9
β’ πΉ = (LFnlβπ) |
4 | | dochlkr.l |
. . . . . . . . 9
β’ πΏ = (LKerβπ) |
5 | | dochlkr.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
6 | | dochlkr.u |
. . . . . . . . . 10
β’ π = ((DVecHβπΎ)βπ) |
7 | 5, 6, 1 | dvhlmod 39623 |
. . . . . . . . 9
β’ (π β π β LMod) |
8 | | dochlkr.g |
. . . . . . . . 9
β’ (π β πΊ β πΉ) |
9 | 2, 3, 4, 7, 8 | lkrssv 37608 |
. . . . . . . 8
β’ (π β (πΏβπΊ) β (Baseβπ)) |
10 | | dochlkr.o |
. . . . . . . . 9
β’ β₯ =
((ocHβπΎ)βπ) |
11 | 5, 6, 2, 10 | dochocss 39879 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΏβπΊ) β (Baseβπ)) β (πΏβπΊ) β ( β₯ β( β₯
β(πΏβπΊ)))) |
12 | 1, 9, 11 | syl2anc 585 |
. . . . . . 7
β’ (π β (πΏβπΊ) β ( β₯ β( β₯
β(πΏβπΊ)))) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β (πΏβπΊ) β ( β₯ β( β₯
β(πΏβπΊ)))) |
14 | | dochlkr.y |
. . . . . . 7
β’ π = (LSHypβπ) |
15 | 5, 6, 1 | dvhlvec 39622 |
. . . . . . . 8
β’ (π β π β LVec) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β π β LVec) |
17 | 7 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β π β LMod) |
18 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β ( β₯ β( β₯
β(πΏβπΊ))) β π) |
19 | 2, 14, 17, 18 | lshpne 37494 |
. . . . . . . . . 10
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β ( β₯ β( β₯
β(πΏβπΊ))) β (Baseβπ)) |
20 | 19 | ex 414 |
. . . . . . . . 9
β’ (π β (( β₯ β( β₯
β(πΏβπΊ))) β π β ( β₯ β( β₯
β(πΏβπΊ))) β (Baseβπ))) |
21 | 2, 14, 3, 4, 15, 8 | lkrshpor 37619 |
. . . . . . . . . . . 12
β’ (π β ((πΏβπΊ) β π β¨ (πΏβπΊ) = (Baseβπ))) |
22 | 21 | ord 863 |
. . . . . . . . . . 11
β’ (π β (Β¬ (πΏβπΊ) β π β (πΏβπΊ) = (Baseβπ))) |
23 | | 2fveq3 6851 |
. . . . . . . . . . . . . 14
β’ ((πΏβπΊ) = (Baseβπ) β ( β₯ β( β₯
β(πΏβπΊ))) = ( β₯ β( β₯
β(Baseβπ)))) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΏβπΊ) = (Baseβπ)) β ( β₯ β( β₯
β(πΏβπΊ))) = ( β₯ β( β₯
β(Baseβπ)))) |
25 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΏβπΊ) = (Baseβπ)) β (πΎ β HL β§ π β π»)) |
26 | 5, 6, 10, 2, 25 | dochoc1 39874 |
. . . . . . . . . . . . 13
β’ ((π β§ (πΏβπΊ) = (Baseβπ)) β ( β₯ β( β₯
β(Baseβπ))) =
(Baseβπ)) |
27 | 24, 26 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ (πΏβπΊ) = (Baseβπ)) β ( β₯ β( β₯
β(πΏβπΊ))) = (Baseβπ)) |
28 | 27 | ex 414 |
. . . . . . . . . . 11
β’ (π β ((πΏβπΊ) = (Baseβπ) β ( β₯ β( β₯
β(πΏβπΊ))) = (Baseβπ))) |
29 | 22, 28 | syld 47 |
. . . . . . . . . 10
β’ (π β (Β¬ (πΏβπΊ) β π β ( β₯ β( β₯
β(πΏβπΊ))) = (Baseβπ))) |
30 | 29 | necon1ad 2957 |
. . . . . . . . 9
β’ (π β (( β₯ β( β₯
β(πΏβπΊ))) β (Baseβπ) β (πΏβπΊ) β π)) |
31 | 20, 30 | syld 47 |
. . . . . . . 8
β’ (π β (( β₯ β( β₯
β(πΏβπΊ))) β π β (πΏβπΊ) β π)) |
32 | 31 | imp 408 |
. . . . . . 7
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β (πΏβπΊ) β π) |
33 | 14, 16, 32, 18 | lshpcmp 37500 |
. . . . . 6
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β ((πΏβπΊ) β ( β₯ β( β₯
β(πΏβπΊ))) β (πΏβπΊ) = ( β₯ β( β₯
β(πΏβπΊ))))) |
34 | 13, 33 | mpbid 231 |
. . . . 5
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β (πΏβπΊ) = ( β₯ β( β₯
β(πΏβπΊ)))) |
35 | 34 | eqcomd 2739 |
. . . 4
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β ( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ)) |
36 | 35, 32 | jca 513 |
. . 3
β’ ((π β§ ( β₯ β( β₯
β(πΏβπΊ))) β π) β (( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ) β§ (πΏβπΊ) β π)) |
37 | 36 | ex 414 |
. 2
β’ (π β (( β₯ β( β₯
β(πΏβπΊ))) β π β (( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ) β§ (πΏβπΊ) β π))) |
38 | | eleq1 2822 |
. . 3
β’ (( β₯
β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β (( β₯ β( β₯
β(πΏβπΊ))) β π β (πΏβπΊ) β π)) |
39 | 38 | biimpar 479 |
. 2
β’ ((( β₯
β( β₯ β(πΏβπΊ))) = (πΏβπΊ) β§ (πΏβπΊ) β π) β ( β₯ β( β₯
β(πΏβπΊ))) β π) |
40 | 37, 39 | impbid1 224 |
1
β’ (π β (( β₯ β( β₯
β(πΏβπΊ))) β π β (( β₯ β( β₯
β(πΏβπΊ))) = (πΏβπΊ) β§ (πΏβπΊ) β π))) |