Step | Hyp | Ref
| Expression |
1 | | sneq 4597 |
. . . . . 6
β’ (π = 0 β {π} = { 0 }) |
2 | 1 | fveq2d 6847 |
. . . . 5
β’ (π = 0 β (πβ{π}) = (πβ{ 0 })) |
3 | | lspdisj2.w |
. . . . . . 7
β’ (π β π β LVec) |
4 | | lveclmod 20582 |
. . . . . . 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 20484 |
. . . . . 6
β’ (π β LMod β (πβ{ 0 }) = { 0 }) |
9 | 5, 8 | syl 17 |
. . . . 5
β’ (π β (πβ{ 0 }) = { 0 }) |
10 | 2, 9 | sylan9eqr 2795 |
. . . 4
β’ ((π β§ π = 0 ) β (πβ{π}) = { 0 }) |
11 | 10 | ineq1d 4172 |
. . 3
β’ ((π β§ π = 0 ) β ((πβ{π}) β© (πβ{π})) = ({ 0 } β© (πβ{π}))) |
12 | | lspdisj2.y |
. . . . . . 7
β’ (π β π β π) |
13 | | lspdisj2.v |
. . . . . . . 8
β’ π = (Baseβπ) |
14 | | eqid 2733 |
. . . . . . . 8
β’
(LSubSpβπ) =
(LSubSpβπ) |
15 | 13, 14, 7 | lspsncl 20453 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
16 | 5, 12, 15 | syl2anc 585 |
. . . . . 6
β’ (π β (πβ{π}) β (LSubSpβπ)) |
17 | 6, 14 | lss0ss 20424 |
. . . . . 6
β’ ((π β LMod β§ (πβ{π}) β (LSubSpβπ)) β { 0 } β (πβ{π})) |
18 | 5, 16, 17 | syl2anc 585 |
. . . . 5
β’ (π β { 0 } β (πβ{π})) |
19 | | df-ss 3928 |
. . . . 5
β’ ({ 0 } β
(πβ{π}) β ({ 0 } β© (πβ{π})) = { 0 }) |
20 | 18, 19 | sylib 217 |
. . . 4
β’ (π β ({ 0 } β© (πβ{π})) = { 0 }) |
21 | 20 | adantr 482 |
. . 3
β’ ((π β§ π = 0 ) β ({ 0 } β©
(πβ{π})) = { 0 }) |
22 | 11, 21 | eqtrd 2773 |
. 2
β’ ((π β§ π = 0 ) β ((πβ{π}) β© (πβ{π})) = { 0 }) |
23 | 3 | adantr 482 |
. . 3
β’ ((π β§ π β 0 ) β π β LVec) |
24 | 16 | adantr 482 |
. . 3
β’ ((π β§ π β 0 ) β (πβ{π}) β (LSubSpβπ)) |
25 | | lspdisj2.x |
. . . 4
β’ (π β π β π) |
26 | 25 | adantr 482 |
. . 3
β’ ((π β§ π β 0 ) β π β π) |
27 | | lspdisj2.q |
. . . . 5
β’ (π β (πβ{π}) β (πβ{π})) |
28 | 27 | adantr 482 |
. . . 4
β’ ((π β§ π β 0 ) β (πβ{π}) β (πβ{π})) |
29 | 23 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β LVec) |
30 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β 0 ) β π β π) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β π) |
32 | | simpr 486 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β (πβ{π})) |
33 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β π β 0 ) |
34 | 13, 6, 7, 29, 31, 32, 33 | lspsneleq 20592 |
. . . . . 6
β’ (((π β§ π β 0 ) β§ π β (πβ{π})) β (πβ{π}) = (πβ{π})) |
35 | 34 | ex 414 |
. . . . 5
β’ ((π β§ π β 0 ) β (π β (πβ{π}) β (πβ{π}) = (πβ{π}))) |
36 | 35 | necon3ad 2953 |
. . . 4
β’ ((π β§ π β 0 ) β ((πβ{π}) β (πβ{π}) β Β¬ π β (πβ{π}))) |
37 | 28, 36 | mpd 15 |
. . 3
β’ ((π β§ π β 0 ) β Β¬ π β (πβ{π})) |
38 | 13, 6, 7, 14, 23, 24, 26, 37 | lspdisj 20602 |
. 2
β’ ((π β§ π β 0 ) β ((πβ{π}) β© (πβ{π})) = { 0 }) |
39 | 22, 38 | pm2.61dane 3029 |
1
β’ (π β ((πβ{π}) β© (πβ{π})) = { 0 }) |