| Step | Hyp | Ref
| Expression |
|---|
| 1 | | sneq 4633 |
. . . . . 6
β’ (π = 0 β {π} = { 0 }) |
| 2 | 1 | fveq2d 6889 |
. . . . 5
β’ (π = 0 β (πβ{π}) = (πβ{ 0 })) |
| 3 | | lspdisj2.w |
. . . . . . 7
β’ (π β π β LVec) |
| 4 | | lveclmod 20954 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
| 5 | 3, 4 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
| 6 | | lspdisj2.o |
. . . . . . 7
β’ 0 =
(0gβπ) |
| 7 | | lspdisj2.n |
. . . . . . 7
β’ π = (LSpanβπ) |
| 8 | 6, 7 | lspsn0 20855 |
. . . . . 6
β’ (π β LMod β (πβ{ 0 }) = { 0 }) |
| 9 | 5, 8 | syl 17 |
. . . . 5
β’ (π β (πβ{ 0 }) = { 0 }) |
| 10 | 2, 9 | sylan9eqr 2788 |
. . . 4
β’ ((π β§ π = 0 ) β (πβ{π}) = { 0 }) |
| 11 | 10 | ineq1d 4206 |
. . 3
β’ ((π β§ π = 0 ) β ((πβ{π}) β© (πβ{π})) = ({ 0 } β© (πβ{π}))) |
| 12 | | lspdisj2.y |
. . . . . . 7
β’ (π β π β π) |
| 13 | | lspdisj2.v |
. . . . . . . 8
β’ π = (Baseβπ) |
| 14 | | eqid 2726 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
| 15 | 13, 14, 7 | lspsncl 20824 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
| 16 | 5, 12, 15 | syl2anc 583 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
| 17 | 6, 14 | lss0ss 20796 |
. . . . . 6
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ)) β { 0 } β (πβ{π})) |
| 18 | 5, 16, 17 | syl2anc 583 |
. . . . 5
β’ (π β { 0 } β (πβ{π})) |
| 19 | | df-ss 3960 |
. . . . 5
β’ ({ 0 } β
(πβ{π}) β ({ 0 } β© (πβ{π})) = { 0 }) |
| 20 | 18, 19 | sylib 217 |
. . . 4
β’ (π β ({ 0 } β© (πβ{π})) = { 0 }) |
| 21 | 20 | adantr 480 |
. . 3
β’ ((π β§ π = 0 ) β ({ 0 } β©
(πβ{π})) = { 0 }) |
| 22 | 11, 21 | eqtrd 2766 |
. 2
β’ ((π β§ π = 0 ) β ((πβ{π}) β© (πβ{π})) = { 0 }) |
| 23 | 3 | adantr 480 |
. . 3
β’ ((π β§ π β 0 ) β π β LVec) |
| 24 | 16 | adantr 480 |
. . 3
β’ ((π β§ π β 0 ) β (πβ{π}) β (LSubSpβπ)) |
| 25 | | lspdisj2.x |
. . . 4
β’ (π β π β π) |
| 26 | 25 | adantr 480 |
. . 3
β’ ((π β§ π β 0 ) β π β π) |
| 27 | | lspdisj2.q |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
| 28 | 27 | adantr 480 |
. . . 4
β’ ((π β§ π β 0 ) β (πβ{π}) β (πβ{π})) |
| 29 | 23 | adantr 480 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β LVec) |
| 30 | 12 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π β 0 ) β π β π) |
| 31 | 30 | adantr 480 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β π) |
| 32 | | simpr 484 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β (πβ{π})) |
| 33 | | simplr 766 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β 0 ) |
| 34 | 13, 6, 7, 29, 31, 32, 33 | lspsneleq 20966 |
. . . . . 6
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β (πβ{π}) = (πβ{π})) |
| 35 | 34 | ex 412 |
. . . . 5
β’ ((π β§ π β 0 ) β (π β (πβ{π}) β (πβ{π}) = (πβ{π}))) |
| 36 | 35 | necon3ad 2947 |
. . . 4
β’ ((π β§ π β 0 ) β ((πβ{π}) β (πβ{π}) β Β¬ π β (πβ{π}))) |
| 37 | 28, 36 | mpd 15 |
. . 3
β’ ((π β§ π β 0 ) β Β¬ π β (πβ{π})) |
| 38 | 13, 6, 7, 14, 23, 24, 26, 37 | lspdisj 20976 |
. 2
β’ ((π β§ π β 0 ) β ((πβ{π}) β© (πβ{π})) = { 0 }) |
| 39 | 22, 38 | pm2.61dane 3023 |
1
β’ (π β ((πβ{π}) β© (πβ{π})) = { 0 }) |
