Step | Hyp | Ref
| Expression |
1 | | lsat0cv.o |
. . 3
β’ 0 =
(0gβπ) |
2 | | lsat0cv.a |
. . 3
β’ π΄ = (LSAtomsβπ) |
3 | | lsat0cv.c |
. . 3
β’ πΆ = ( βL
βπ) |
4 | | lsat0cv.w |
. . . 4
β’ (π β π β LVec) |
5 | 4 | adantr 482 |
. . 3
β’ ((π β§ π β π΄) β π β LVec) |
6 | | simpr 486 |
. . 3
β’ ((π β§ π β π΄) β π β π΄) |
7 | 1, 2, 3, 5, 6 | lsatcv0 37522 |
. 2
β’ ((π β§ π β π΄) β { 0 }πΆπ) |
8 | | lsat0cv.s |
. . . . . . 7
β’ π = (LSubSpβπ) |
9 | | lveclmod 20583 |
. . . . . . . . 9
β’ (π β LVec β π β LMod) |
10 | 4, 9 | syl 17 |
. . . . . . . 8
β’ (π β π β LMod) |
11 | 10 | adantr 482 |
. . . . . . 7
β’ ((π β§ { 0 }πΆπ) β π β LMod) |
12 | 1, 8 | lsssn0 20424 |
. . . . . . . . 9
β’ (π β LMod β { 0 } β
π) |
13 | 10, 12 | syl 17 |
. . . . . . . 8
β’ (π β { 0 } β π) |
14 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ { 0 }πΆπ) β { 0 } β π) |
15 | | lsat0cv.u |
. . . . . . . 8
β’ (π β π β π) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ { 0 }πΆπ) β π β π) |
17 | | simpr 486 |
. . . . . . 7
β’ ((π β§ { 0 }πΆπ) β { 0 }πΆπ) |
18 | 8, 3, 11, 14, 16, 17 | lcvpss 37515 |
. . . . . 6
β’ ((π β§ { 0 }πΆπ) β { 0 } β π) |
19 | | pssnel 4435 |
. . . . . 6
β’ ({ 0 } β
π β βπ₯(π₯ β π β§ Β¬ π₯ β { 0 })) |
20 | 18, 19 | syl 17 |
. . . . 5
β’ ((π β§ { 0 }πΆπ) β βπ₯(π₯ β π β§ Β¬ π₯ β { 0 })) |
21 | 15 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ { 0 }πΆπ) β§ (π₯ β π β§ Β¬ π₯ β { 0 })) β π β π) |
22 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ { 0 }πΆπ) β§ (π₯ β π β§ Β¬ π₯ β { 0 })) β π₯ β π) |
23 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
24 | 23, 8 | lssel 20414 |
. . . . . . . . . . 11
β’ ((π β π β§ π₯ β π) β π₯ β (Baseβπ)) |
25 | 21, 22, 24 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ { 0 }πΆπ) β§ (π₯ β π β§ Β¬ π₯ β { 0 })) β π₯ β (Baseβπ)) |
26 | | velsn 4607 |
. . . . . . . . . . . . . 14
β’ (π₯ β { 0 } β π₯ = 0 ) |
27 | 26 | biimpri 227 |
. . . . . . . . . . . . 13
β’ (π₯ = 0 β π₯ β { 0 }) |
28 | 27 | necon3bi 2971 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β { 0 } β
π₯ β 0 ) |
29 | 28 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ Β¬ π₯ β { 0 }) β π₯ β 0 ) |
30 | 29 | adantl 483 |
. . . . . . . . . 10
β’ (((π β§ { 0 }πΆπ) β§ (π₯ β π β§ Β¬ π₯ β { 0 })) β π₯ β 0 ) |
31 | | eldifsn 4752 |
. . . . . . . . . 10
β’ (π₯ β ((Baseβπ) β { 0 }) β (π₯ β (Baseβπ) β§ π₯ β 0 )) |
32 | 25, 30, 31 | sylanbrc 584 |
. . . . . . . . 9
β’ (((π β§ { 0 }πΆπ) β§ (π₯ β π β§ Β¬ π₯ β { 0 })) β π₯ β ((Baseβπ) β { 0 })) |
33 | 32, 22 | jca 513 |
. . . . . . . 8
β’ (((π β§ { 0 }πΆπ) β§ (π₯ β π β§ Β¬ π₯ β { 0 })) β (π₯ β ((Baseβπ) β { 0 }) β§ π₯ β π)) |
34 | 33 | ex 414 |
. . . . . . 7
β’ ((π β§ { 0 }πΆπ) β ((π₯ β π β§ Β¬ π₯ β { 0 }) β (π₯ β ((Baseβπ) β { 0 }) β§ π₯ β π))) |
35 | 34 | eximdv 1921 |
. . . . . 6
β’ ((π β§ { 0 }πΆπ) β (βπ₯(π₯ β π β§ Β¬ π₯ β { 0 }) β βπ₯(π₯ β ((Baseβπ) β { 0 }) β§ π₯ β π))) |
36 | | df-rex 3075 |
. . . . . 6
β’
(βπ₯ β
((Baseβπ) β {
0 })π₯ β π β βπ₯(π₯ β ((Baseβπ) β { 0 }) β§ π₯ β π)) |
37 | 35, 36 | syl6ibr 252 |
. . . . 5
β’ ((π β§ { 0 }πΆπ) β (βπ₯(π₯ β π β§ Β¬ π₯ β { 0 }) β βπ₯ β ((Baseβπ) β { 0 })π₯ β π)) |
38 | 20, 37 | mpd 15 |
. . . 4
β’ ((π β§ { 0 }πΆπ) β βπ₯ β ((Baseβπ) β { 0 })π₯ β π) |
39 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β { 0 }πΆπ) |
40 | 8, 3, 4, 13, 15 | lcvbr2 37513 |
. . . . . . . . . . 11
β’ (π β ({ 0 }πΆπ β ({ 0 } β π β§ βπ β π (({ 0 } β π β§ π β π) β π = π)))) |
41 | 40 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ { 0 }πΆπ) β ({ 0 }πΆπ β ({ 0 } β π β§ βπ β π (({ 0 } β π β§ π β π) β π = π)))) |
42 | 41 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β ({ 0 }πΆπ β ({ 0 } β π β§ βπ β π (({ 0 } β π β§ π β π) β π = π)))) |
43 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β π β LMod) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β π β LMod) |
45 | | eldifi 4091 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β ((Baseβπ) β { 0 }) β π₯ β (Baseβπ)) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β π₯ β (Baseβπ)) |
47 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β π₯ β (Baseβπ)) |
48 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(LSpanβπ) =
(LSpanβπ) |
49 | 23, 8, 48 | lspsncl 20454 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ π₯ β (Baseβπ)) β ((LSpanβπ)β{π₯}) β π) |
50 | 44, 47, 49 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β ((LSpanβπ)β{π₯}) β π) |
51 | 1, 8 | lss0ss 20425 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§
((LSpanβπ)β{π₯}) β π) β { 0 } β
((LSpanβπ)β{π₯})) |
52 | 44, 50, 51 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β { 0 } β
((LSpanβπ)β{π₯})) |
53 | | eldifsni 4755 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β ((Baseβπ) β { 0 }) β π₯ β 0 ) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β π₯ β 0 ) |
55 | 54 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β π₯ β 0 ) |
56 | 23, 1, 48 | lspsneq0 20489 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π₯ β (Baseβπ)) β (((LSpanβπ)β{π₯}) = { 0 } β π₯ = 0 )) |
57 | 44, 47, 56 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β (((LSpanβπ)β{π₯}) = { 0 } β π₯ = 0 )) |
58 | 57 | necon3bid 2989 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β (((LSpanβπ)β{π₯}) β { 0 } β π₯ β 0 )) |
59 | 55, 58 | mpbird 257 |
. . . . . . . . . . . . . 14
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β ((LSpanβπ)β{π₯}) β { 0 }) |
60 | 59 | necomd 3000 |
. . . . . . . . . . . . 13
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β { 0 } β ((LSpanβπ)β{π₯})) |
61 | | df-pss 3934 |
. . . . . . . . . . . . 13
β’ ({ 0 } β
((LSpanβπ)β{π₯}) β ({ 0 } β
((LSpanβπ)β{π₯}) β§ { 0 } β ((LSpanβπ)β{π₯}))) |
62 | 52, 60, 61 | sylanbrc 584 |
. . . . . . . . . . . 12
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β { 0 } β
((LSpanβπ)β{π₯})) |
63 | 15 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β π β π) |
64 | 63 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β π β π) |
65 | | simplr 768 |
. . . . . . . . . . . . 13
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β π₯ β π) |
66 | 8, 48, 44, 64, 65 | lspsnel5a 20473 |
. . . . . . . . . . . 12
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β ((LSpanβπ)β{π₯}) β π) |
67 | 62, 66 | jca 513 |
. . . . . . . . . . 11
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β ({ 0 } β
((LSpanβπ)β{π₯}) β§ ((LSpanβπ)β{π₯}) β π)) |
68 | | psseq2 4053 |
. . . . . . . . . . . . . . 15
β’ (π = ((LSpanβπ)β{π₯}) β ({ 0 } β π β { 0 } β
((LSpanβπ)β{π₯}))) |
69 | | sseq1 3974 |
. . . . . . . . . . . . . . 15
β’ (π = ((LSpanβπ)β{π₯}) β (π β π β ((LSpanβπ)β{π₯}) β π)) |
70 | 68, 69 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = ((LSpanβπ)β{π₯}) β (({ 0 } β π β§ π β π) β ({ 0 } β
((LSpanβπ)β{π₯}) β§ ((LSpanβπ)β{π₯}) β π))) |
71 | | eqeq1 2741 |
. . . . . . . . . . . . . 14
β’ (π = ((LSpanβπ)β{π₯}) β (π = π β ((LSpanβπ)β{π₯}) = π)) |
72 | 70, 71 | imbi12d 345 |
. . . . . . . . . . . . 13
β’ (π = ((LSpanβπ)β{π₯}) β ((({ 0 } β π β§ π β π) β π = π) β (({ 0 } β
((LSpanβπ)β{π₯}) β§ ((LSpanβπ)β{π₯}) β π) β ((LSpanβπ)β{π₯}) = π))) |
73 | 72 | rspcv 3580 |
. . . . . . . . . . . 12
β’
(((LSpanβπ)β{π₯}) β π β (βπ β π (({ 0 } β π β§ π β π) β π = π) β (({ 0 } β
((LSpanβπ)β{π₯}) β§ ((LSpanβπ)β{π₯}) β π) β ((LSpanβπ)β{π₯}) = π))) |
74 | 50, 73 | syl 17 |
. . . . . . . . . . 11
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β (βπ β π (({ 0 } β π β§ π β π) β π = π) β (({ 0 } β
((LSpanβπ)β{π₯}) β§ ((LSpanβπ)β{π₯}) β π) β ((LSpanβπ)β{π₯}) = π))) |
75 | 67, 74 | mpid 44 |
. . . . . . . . . 10
β’
(((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β§ { 0 } β π) β (βπ β π (({ 0 } β π β§ π β π) β π = π) β ((LSpanβπ)β{π₯}) = π)) |
76 | 75 | expimpd 455 |
. . . . . . . . 9
β’ ((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β (({ 0 } β π β§ βπ β π (({ 0 } β π β§ π β π) β π = π)) β ((LSpanβπ)β{π₯}) = π)) |
77 | 42, 76 | sylbid 239 |
. . . . . . . 8
β’ ((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β ({ 0 }πΆπ β ((LSpanβπ)β{π₯}) = π)) |
78 | 39, 77 | mpd 15 |
. . . . . . 7
β’ ((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β ((LSpanβπ)β{π₯}) = π) |
79 | 78 | eqcomd 2743 |
. . . . . 6
β’ ((((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β§ π₯ β π) β π = ((LSpanβπ)β{π₯})) |
80 | 79 | ex 414 |
. . . . 5
β’ (((π β§ { 0 }πΆπ) β§ π₯ β ((Baseβπ) β { 0 })) β (π₯ β π β π = ((LSpanβπ)β{π₯}))) |
81 | 80 | reximdva 3166 |
. . . 4
β’ ((π β§ { 0 }πΆπ) β (βπ₯ β ((Baseβπ) β { 0 })π₯ β π β βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯}))) |
82 | 38, 81 | mpd 15 |
. . 3
β’ ((π β§ { 0 }πΆπ) β βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯})) |
83 | 4 | adantr 482 |
. . . 4
β’ ((π β§ { 0 }πΆπ) β π β LVec) |
84 | 23, 48, 1, 2 | islsat 37482 |
. . . 4
β’ (π β LVec β (π β π΄ β βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯}))) |
85 | 83, 84 | syl 17 |
. . 3
β’ ((π β§ { 0 }πΆπ) β (π β π΄ β βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯}))) |
86 | 82, 85 | mpbird 257 |
. 2
β’ ((π β§ { 0 }πΆπ) β π β π΄) |
87 | 7, 86 | impbida 800 |
1
β’ (π β (π β π΄ β { 0 }πΆπ)) |