Step | Hyp | Ref
| Expression |
1 | | lsatcv0.w |
. . . . 5
β’ (π β π β LVec) |
2 | | lveclmod 20583 |
. . . . 5
β’ (π β LVec β π β LMod) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β π β LMod) |
4 | | eqid 2737 |
. . . . 5
β’
(LSubSpβπ) =
(LSubSpβπ) |
5 | | lsatcv0.a |
. . . . 5
β’ π΄ = (LSAtomsβπ) |
6 | | lsatcv0.q |
. . . . 5
β’ (π β π β π΄) |
7 | 4, 5, 3, 6 | lsatlssel 37488 |
. . . 4
β’ (π β π β (LSubSpβπ)) |
8 | | lsatcv0.o |
. . . . 5
β’ 0 =
(0gβπ) |
9 | 8, 4 | lss0ss 20425 |
. . . 4
β’ ((π β LMod β§ π β (LSubSpβπ)) β { 0 } β π) |
10 | 3, 7, 9 | syl2anc 585 |
. . 3
β’ (π β { 0 } β π) |
11 | 8, 5, 3, 6 | lsatn0 37490 |
. . . 4
β’ (π β π β { 0 }) |
12 | 11 | necomd 3000 |
. . 3
β’ (π β { 0 } β π) |
13 | | df-pss 3934 |
. . 3
β’ ({ 0 } β
π β ({ 0 } β
π β§ { 0 } β π)) |
14 | 10, 12, 13 | sylanbrc 584 |
. 2
β’ (π β { 0 } β π) |
15 | | eqid 2737 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
16 | | eqid 2737 |
. . . . . 6
β’
(LSpanβπ) =
(LSpanβπ) |
17 | 15, 16, 8, 5 | islsat 37482 |
. . . . 5
β’ (π β LMod β (π β π΄ β βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯}))) |
18 | 3, 17 | syl 17 |
. . . 4
β’ (π β (π β π΄ β βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯}))) |
19 | 6, 18 | mpbid 231 |
. . 3
β’ (π β βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯})) |
20 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β ((Baseβπ) β { 0 })) β π β LVec) |
21 | | eldifi 4091 |
. . . . . . . 8
β’ (π₯ β ((Baseβπ) β { 0 }) β π₯ β (Baseβπ)) |
22 | 21 | adantl 483 |
. . . . . . 7
β’ ((π β§ π₯ β ((Baseβπ) β { 0 })) β π₯ β (Baseβπ)) |
23 | 15, 8, 4, 16, 20, 22 | lspsncv0 20623 |
. . . . . 6
β’ ((π β§ π₯ β ((Baseβπ) β { 0 })) β Β¬
βπ β
(LSubSpβπ)({ 0 } β
π β§ π β ((LSpanβπ)β{π₯}))) |
24 | 23 | ex 414 |
. . . . 5
β’ (π β (π₯ β ((Baseβπ) β { 0 }) β Β¬
βπ β
(LSubSpβπ)({ 0 } β
π β§ π β ((LSpanβπ)β{π₯})))) |
25 | | psseq2 4053 |
. . . . . . . . 9
β’ (π = ((LSpanβπ)β{π₯}) β (π β π β π β ((LSpanβπ)β{π₯}))) |
26 | 25 | anbi2d 630 |
. . . . . . . 8
β’ (π = ((LSpanβπ)β{π₯}) β (({ 0 } β π β§ π β π) β ({ 0 } β π β§ π β ((LSpanβπ)β{π₯})))) |
27 | 26 | rexbidv 3176 |
. . . . . . 7
β’ (π = ((LSpanβπ)β{π₯}) β (βπ β (LSubSpβπ)({ 0 } β π β§ π β π) β βπ β (LSubSpβπ)({ 0 } β π β§ π β ((LSpanβπ)β{π₯})))) |
28 | 27 | notbid 318 |
. . . . . 6
β’ (π = ((LSpanβπ)β{π₯}) β (Β¬ βπ β (LSubSpβπ)({ 0 } β π β§ π β π) β Β¬ βπ β (LSubSpβπ)({ 0 } β π β§ π β ((LSpanβπ)β{π₯})))) |
29 | 28 | biimprcd 250 |
. . . . 5
β’ (Β¬
βπ β
(LSubSpβπ)({ 0 } β
π β§ π β ((LSpanβπ)β{π₯})) β (π = ((LSpanβπ)β{π₯}) β Β¬ βπ β (LSubSpβπ)({ 0 } β π β§ π β π))) |
30 | 24, 29 | syl6 35 |
. . . 4
β’ (π β (π₯ β ((Baseβπ) β { 0 }) β (π = ((LSpanβπ)β{π₯}) β Β¬ βπ β (LSubSpβπ)({ 0 } β π β§ π β π)))) |
31 | 30 | rexlimdv 3151 |
. . 3
β’ (π β (βπ₯ β ((Baseβπ) β { 0 })π = ((LSpanβπ)β{π₯}) β Β¬ βπ β (LSubSpβπ)({ 0 } β π β§ π β π))) |
32 | 19, 31 | mpd 15 |
. 2
β’ (π β Β¬ βπ β (LSubSpβπ)({ 0 } β π β§ π β π)) |
33 | | lsatcv0.c |
. . 3
β’ πΆ = ( βL
βπ) |
34 | 8, 4 | lsssn0 20424 |
. . . 4
β’ (π β LMod β { 0 } β
(LSubSpβπ)) |
35 | 3, 34 | syl 17 |
. . 3
β’ (π β { 0 } β
(LSubSpβπ)) |
36 | 4, 33, 1, 35, 7 | lcvbr 37512 |
. 2
β’ (π β ({ 0 }πΆπ β ({ 0 } β π β§ Β¬ βπ β (LSubSpβπ)({ 0 } β π β§ π β π)))) |
37 | 14, 32, 36 | mpbir2and 712 |
1
β’ (π β { 0 }πΆπ) |