Step | Hyp | Ref
| Expression |
1 | | df-pss 3930 |
. . 3
β’ ((πΎβπΊ) β (πΎβπ») β ((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»))) |
2 | | simpr 486 |
. . . . . . . 8
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β (πΎβπΊ) β (πΎβπ»)) |
3 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
4 | | lkrpss.f |
. . . . . . . . . 10
β’ πΉ = (LFnlβπ) |
5 | | lkrpss.k |
. . . . . . . . . 10
β’ πΎ = (LKerβπ) |
6 | | lkrpss.w |
. . . . . . . . . . 11
β’ (π β π β LVec) |
7 | | lveclmod 20570 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
β’ (π β π β LMod) |
9 | | lkrpss.h |
. . . . . . . . . 10
β’ (π β π» β πΉ) |
10 | 3, 4, 5, 8, 9 | lkrssv 37561 |
. . . . . . . . 9
β’ (π β (πΎβπ») β (Baseβπ)) |
11 | 10 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β (πΎβπ») β (Baseβπ)) |
12 | 2, 11 | psssstrd 4070 |
. . . . . . 7
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β (πΎβπΊ) β (Baseβπ)) |
13 | 12 | pssned 4059 |
. . . . . 6
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β (πΎβπΊ) β (Baseβπ)) |
14 | 1, 13 | sylan2br 596 |
. . . . 5
β’ ((π β§ ((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»))) β (πΎβπΊ) β (Baseβπ)) |
15 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β (πΎβπΊ) β (πΎβπ»)) |
16 | | eqid 2737 |
. . . . . . . . . . 11
β’
(LSHypβπ) =
(LSHypβπ) |
17 | 6 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β π β LVec) |
18 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) β (LSHypβπ)) β (πΎβπΊ) β (LSHypβπ)) |
19 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (πΎβπ») β (LSHypβπ)) |
20 | 10 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (πΎβπ») β (Baseβπ)) |
21 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (πΎβπΊ) = (Baseβπ)) |
22 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (πΎβπΊ) β (πΎβπ»)) |
23 | 21, 22 | eqsstrrd 3984 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (Baseβπ) β (πΎβπ»)) |
24 | 20, 23 | eqssd 3962 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (πΎβπ») = (Baseβπ)) |
25 | 3, 16, 4, 5, 6, 9 | lkrshp4 37573 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΎβπ») β (Baseβπ) β (πΎβπ») β (LSHypβπ))) |
26 | 25 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β ((πΎβπ») β (Baseβπ) β (πΎβπ») β (LSHypβπ))) |
27 | 26 | necon1bbid 2984 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (Β¬ (πΎβπ») β (LSHypβπ) β (πΎβπ») = (Baseβπ))) |
28 | 24, 27 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β Β¬ (πΎβπ») β (LSHypβπ)) |
29 | 19, 28 | pm2.21dd 194 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β§ (πΎβπΊ) = (Baseβπ)) β (πΎβπΊ) β (LSHypβπ)) |
30 | | lkrpss.g |
. . . . . . . . . . . . . 14
β’ (π β πΊ β πΉ) |
31 | 3, 16, 4, 5, 6, 30 | lkrshpor 37572 |
. . . . . . . . . . . . 13
β’ (π β ((πΎβπΊ) β (LSHypβπ) β¨ (πΎβπΊ) = (Baseβπ))) |
32 | 31 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β ((πΎβπΊ) β (LSHypβπ) β¨ (πΎβπΊ) = (Baseβπ))) |
33 | 18, 29, 32 | mpjaodan 958 |
. . . . . . . . . . 11
β’ (((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β (πΎβπΊ) β (LSHypβπ)) |
34 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β (πΎβπ») β (LSHypβπ)) |
35 | 16, 17, 33, 34 | lshpcmp 37453 |
. . . . . . . . . 10
β’ (((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β ((πΎβπΊ) β (πΎβπ») β (πΎβπΊ) = (πΎβπ»))) |
36 | 15, 35 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ (πΎβπΊ) β (πΎβπ»)) β§ (πΎβπ») β (LSHypβπ)) β (πΎβπΊ) = (πΎβπ»)) |
37 | 36 | ex 414 |
. . . . . . . 8
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β ((πΎβπ») β (LSHypβπ) β (πΎβπΊ) = (πΎβπ»))) |
38 | 37 | necon3ad 2957 |
. . . . . . 7
β’ ((π β§ (πΎβπΊ) β (πΎβπ»)) β ((πΎβπΊ) β (πΎβπ») β Β¬ (πΎβπ») β (LSHypβπ))) |
39 | 38 | impr 456 |
. . . . . 6
β’ ((π β§ ((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»))) β Β¬ (πΎβπ») β (LSHypβπ)) |
40 | 25 | necon1bbid 2984 |
. . . . . . 7
β’ (π β (Β¬ (πΎβπ») β (LSHypβπ) β (πΎβπ») = (Baseβπ))) |
41 | 40 | adantr 482 |
. . . . . 6
β’ ((π β§ ((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»))) β (Β¬ (πΎβπ») β (LSHypβπ) β (πΎβπ») = (Baseβπ))) |
42 | 39, 41 | mpbid 231 |
. . . . 5
β’ ((π β§ ((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»))) β (πΎβπ») = (Baseβπ)) |
43 | 14, 42 | jca 513 |
. . . 4
β’ ((π β§ ((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»))) β ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) |
44 | 3, 4, 5, 8, 30 | lkrssv 37561 |
. . . . . . 7
β’ (π β (πΎβπΊ) β (Baseβπ)) |
45 | 44 | adantr 482 |
. . . . . 6
β’ ((π β§ ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) β (πΎβπΊ) β (Baseβπ)) |
46 | | simprr 772 |
. . . . . . 7
β’ ((π β§ ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) β (πΎβπ») = (Baseβπ)) |
47 | 46 | eqcomd 2743 |
. . . . . 6
β’ ((π β§ ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) β (Baseβπ) = (πΎβπ»)) |
48 | 45, 47 | sseqtrd 3985 |
. . . . 5
β’ ((π β§ ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) β (πΎβπΊ) β (πΎβπ»)) |
49 | | simprl 770 |
. . . . . 6
β’ ((π β§ ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) β (πΎβπΊ) β (Baseβπ)) |
50 | 49, 47 | neeqtrd 3014 |
. . . . 5
β’ ((π β§ ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) β (πΎβπΊ) β (πΎβπ»)) |
51 | 48, 50 | jca 513 |
. . . 4
β’ ((π β§ ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ))) β ((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»))) |
52 | 43, 51 | impbida 800 |
. . 3
β’ (π β (((πΎβπΊ) β (πΎβπ») β§ (πΎβπΊ) β (πΎβπ»)) β ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ)))) |
53 | 1, 52 | bitrid 283 |
. 2
β’ (π β ((πΎβπΊ) β (πΎβπ») β ((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ)))) |
54 | | lkrpss.d |
. . . . 5
β’ π· = (LDualβπ) |
55 | | lkrpss.o |
. . . . 5
β’ 0 =
(0gβπ·) |
56 | 3, 4, 5, 54, 55, 8, 30 | lkr0f2 37626 |
. . . 4
β’ (π β ((πΎβπΊ) = (Baseβπ) β πΊ = 0 )) |
57 | 56 | necon3bid 2989 |
. . 3
β’ (π β ((πΎβπΊ) β (Baseβπ) β πΊ β 0 )) |
58 | 3, 4, 5, 54, 55, 8, 9 | lkr0f2 37626 |
. . 3
β’ (π β ((πΎβπ») = (Baseβπ) β π» = 0 )) |
59 | 57, 58 | anbi12d 632 |
. 2
β’ (π β (((πΎβπΊ) β (Baseβπ) β§ (πΎβπ») = (Baseβπ)) β (πΊ β 0 β§ π» = 0 ))) |
60 | 53, 59 | bitrd 279 |
1
β’ (π β ((πΎβπΊ) β (πΎβπ») β (πΊ β 0 β§ π» = 0 ))) |