Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | dihlspsnat.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
3 | | dihlspsnat.i |
. . . . . 6
β’ πΌ = ((DIsoHβπΎ)βπ) |
4 | | dihlspsnat.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
5 | | eqid 2733 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
6 | 1, 2, 3, 4, 5 | dihf11 39780 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β πΌ:(BaseβπΎ)β1-1β(LSubSpβπ)) |
7 | 6 | 3ad2ant1 1134 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β πΌ:(BaseβπΎ)β1-1β(LSubSpβπ)) |
8 | | f1f1orn 6799 |
. . . 4
β’ (πΌ:(BaseβπΎ)β1-1β(LSubSpβπ) β πΌ:(BaseβπΎ)β1-1-ontoβran
πΌ) |
9 | 7, 8 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β πΌ:(BaseβπΎ)β1-1-ontoβran
πΌ) |
10 | | dihlspsnat.v |
. . . . 5
β’ π = (Baseβπ) |
11 | | dihlspsnat.n |
. . . . 5
β’ π = (LSpanβπ) |
12 | 2, 4, 10, 11, 3 | dihlsprn 39844 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran πΌ) |
13 | 12 | 3adant3 1133 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (πβ{π}) β ran πΌ) |
14 | | f1ocnvdm 7235 |
. . 3
β’ ((πΌ:(BaseβπΎ)β1-1-ontoβran
πΌ β§ (πβ{π}) β ran πΌ) β (β‘πΌβ(πβ{π})) β (BaseβπΎ)) |
15 | 9, 13, 14 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (β‘πΌβ(πβ{π})) β (BaseβπΎ)) |
16 | | fveq2 6846 |
. . . . 5
β’ ((β‘πΌβ(πβ{π})) = (0.βπΎ) β (πΌβ(β‘πΌβ(πβ{π}))) = (πΌβ(0.βπΎ))) |
17 | 2, 3 | dihcnvid2 39786 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πβ{π}) β ran πΌ) β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
18 | 12, 17 | syldan 592 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
19 | | eqid 2733 |
. . . . . . . . 9
β’
(0.βπΎ) =
(0.βπΎ) |
20 | | dihlspsnat.o |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
21 | 19, 2, 3, 4, 20 | dih0 39793 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (πΌβ(0.βπΎ)) = { 0 }) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(0.βπΎ)) = { 0 }) |
23 | 18, 22 | eqeq12d 2749 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((πΌβ(β‘πΌβ(πβ{π}))) = (πΌβ(0.βπΎ)) β (πβ{π}) = { 0 })) |
24 | | id 22 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (πΎ β HL β§ π β π»)) |
25 | 2, 4, 24 | dvhlmod 39623 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β π β LMod) |
26 | 10, 20, 11 | lspsneq0 20517 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β ((πβ{π}) = { 0 } β π = 0 )) |
27 | 25, 26 | sylan 581 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((πβ{π}) = { 0 } β π = 0 )) |
28 | 23, 27 | bitrd 279 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((πΌβ(β‘πΌβ(πβ{π}))) = (πΌβ(0.βπΎ)) β π = 0 )) |
29 | 16, 28 | imbitrid 243 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β ((β‘πΌβ(πβ{π})) = (0.βπΎ) β π = 0 )) |
30 | 29 | necon3d 2961 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (π β 0 β (β‘πΌβ(πβ{π})) β (0.βπΎ))) |
31 | 30 | 3impia 1118 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (β‘πΌβ(πβ{π})) β (0.βπΎ)) |
32 | | simpll1 1213 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β§ (πΌβπ₯) β (πβ{π})) β (πΎ β HL β§ π β π»)) |
33 | 2, 4, 32 | dvhlvec 39622 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β§ (πΌβπ₯) β (πβ{π})) β π β LVec) |
34 | | simplr 768 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β§ (πΌβπ₯) β (πβ{π})) β π₯ β (BaseβπΎ)) |
35 | 1, 2, 3, 4, 5 | dihlss 39763 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π₯ β (BaseβπΎ)) β (πΌβπ₯) β (LSubSpβπ)) |
36 | 32, 34, 35 | syl2anc 585 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β§ (πΌβπ₯) β (πβ{π})) β (πΌβπ₯) β (LSubSpβπ)) |
37 | | simpll2 1214 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β§ (πΌβπ₯) β (πβ{π})) β π β π) |
38 | | simpr 486 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β§ (πΌβπ₯) β (πβ{π})) β (πΌβπ₯) β (πβ{π})) |
39 | 10, 20, 5, 11 | lspsnat 20651 |
. . . . . 6
β’ (((π β LVec β§ (πΌβπ₯) β (LSubSpβπ) β§ π β π) β§ (πΌβπ₯) β (πβ{π})) β ((πΌβπ₯) = (πβ{π}) β¨ (πΌβπ₯) = { 0 })) |
40 | 33, 36, 37, 38, 39 | syl31anc 1374 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β§ (πΌβπ₯) β (πβ{π})) β ((πΌβπ₯) = (πβ{π}) β¨ (πΌβπ₯) = { 0 })) |
41 | 40 | ex 414 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) β (πβ{π}) β ((πΌβπ₯) = (πβ{π}) β¨ (πΌβπ₯) = { 0 }))) |
42 | | simp1 1137 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (πΎ β HL β§ π β π»)) |
43 | 42, 13, 17 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
44 | 43 | adantr 482 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β (πΌβ(β‘πΌβ(πβ{π}))) = (πβ{π})) |
45 | 44 | sseq2d 3980 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) β (πΌβ(β‘πΌβ(πβ{π}))) β (πΌβπ₯) β (πβ{π}))) |
46 | | simpl1 1192 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β (πΎ β HL β§ π β π»)) |
47 | | simpr 486 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β π₯ β (BaseβπΎ)) |
48 | 15 | adantr 482 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β (β‘πΌβ(πβ{π})) β (BaseβπΎ)) |
49 | | eqid 2733 |
. . . . . . 7
β’
(leβπΎ) =
(leβπΎ) |
50 | 1, 49, 2, 3 | dihord 39777 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π₯ β (BaseβπΎ) β§ (β‘πΌβ(πβ{π})) β (BaseβπΎ)) β ((πΌβπ₯) β (πΌβ(β‘πΌβ(πβ{π}))) β π₯(leβπΎ)(β‘πΌβ(πβ{π})))) |
51 | 46, 47, 48, 50 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) β (πΌβ(β‘πΌβ(πβ{π}))) β π₯(leβπΎ)(β‘πΌβ(πβ{π})))) |
52 | 45, 51 | bitr3d 281 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) β (πβ{π}) β π₯(leβπΎ)(β‘πΌβ(πβ{π})))) |
53 | 44 | eqeq2d 2744 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) = (πΌβ(β‘πΌβ(πβ{π}))) β (πΌβπ₯) = (πβ{π}))) |
54 | 1, 2, 3 | dih11 39778 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π₯ β (BaseβπΎ) β§ (β‘πΌβ(πβ{π})) β (BaseβπΎ)) β ((πΌβπ₯) = (πΌβ(β‘πΌβ(πβ{π}))) β π₯ = (β‘πΌβ(πβ{π})))) |
55 | 46, 47, 48, 54 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) = (πΌβ(β‘πΌβ(πβ{π}))) β π₯ = (β‘πΌβ(πβ{π})))) |
56 | 53, 55 | bitr3d 281 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) = (πβ{π}) β π₯ = (β‘πΌβ(πβ{π})))) |
57 | 46, 21 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β (πΌβ(0.βπΎ)) = { 0 }) |
58 | 57 | eqeq2d 2744 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) = (πΌβ(0.βπΎ)) β (πΌβπ₯) = { 0 })) |
59 | | simpl1l 1225 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β πΎ β HL) |
60 | | hlop 37874 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OP) |
61 | 1, 19 | op0cl 37696 |
. . . . . . . 8
β’ (πΎ β OP β
(0.βπΎ) β
(BaseβπΎ)) |
62 | 59, 60, 61 | 3syl 18 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β (0.βπΎ) β (BaseβπΎ)) |
63 | 1, 2, 3 | dih11 39778 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π₯ β (BaseβπΎ) β§ (0.βπΎ) β (BaseβπΎ)) β ((πΌβπ₯) = (πΌβ(0.βπΎ)) β π₯ = (0.βπΎ))) |
64 | 46, 47, 62, 63 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) = (πΌβ(0.βπΎ)) β π₯ = (0.βπΎ))) |
65 | 58, 64 | bitr3d 281 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β ((πΌβπ₯) = { 0 } β π₯ = (0.βπΎ))) |
66 | 56, 65 | orbi12d 918 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β (((πΌβπ₯) = (πβ{π}) β¨ (πΌβπ₯) = { 0 }) β (π₯ = (β‘πΌβ(πβ{π})) β¨ π₯ = (0.βπΎ)))) |
67 | 41, 52, 66 | 3imtr3d 293 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β§ π₯ β (BaseβπΎ)) β (π₯(leβπΎ)(β‘πΌβ(πβ{π})) β (π₯ = (β‘πΌβ(πβ{π})) β¨ π₯ = (0.βπΎ)))) |
68 | 67 | ralrimiva 3140 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β βπ₯ β (BaseβπΎ)(π₯(leβπΎ)(β‘πΌβ(πβ{π})) β (π₯ = (β‘πΌβ(πβ{π})) β¨ π₯ = (0.βπΎ)))) |
69 | | simp1l 1198 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β πΎ β HL) |
70 | | hlatl 37872 |
. . 3
β’ (πΎ β HL β πΎ β AtLat) |
71 | | dihlspsnat.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
72 | 1, 49, 19, 71 | isat3 37819 |
. . 3
β’ (πΎ β AtLat β ((β‘πΌβ(πβ{π})) β π΄ β ((β‘πΌβ(πβ{π})) β (BaseβπΎ) β§ (β‘πΌβ(πβ{π})) β (0.βπΎ) β§ βπ₯ β (BaseβπΎ)(π₯(leβπΎ)(β‘πΌβ(πβ{π})) β (π₯ = (β‘πΌβ(πβ{π})) β¨ π₯ = (0.βπΎ)))))) |
73 | 69, 70, 72 | 3syl 18 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β ((β‘πΌβ(πβ{π})) β π΄ β ((β‘πΌβ(πβ{π})) β (BaseβπΎ) β§ (β‘πΌβ(πβ{π})) β (0.βπΎ) β§ βπ₯ β (BaseβπΎ)(π₯(leβπΎ)(β‘πΌβ(πβ{π})) β (π₯ = (β‘πΌβ(πβ{π})) β¨ π₯ = (0.βπΎ)))))) |
74 | 15, 31, 68, 73 | mpbir3and 1343 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (β‘πΌβ(πβ{π})) β π΄) |