Step | Hyp | Ref
| Expression |
1 | | ssdif0 4327 |
. . 3
β’ (π β
{(0gβπ)}
β (π β
{(0gβπ)})
= β
) |
2 | | lspprat.w |
. . . . . . . 8
β’ (π β π β LVec) |
3 | | lveclmod 20611 |
. . . . . . . 8
β’ (π β LVec β π β LMod) |
4 | 2, 3 | syl 17 |
. . . . . . 7
β’ (π β π β LMod) |
5 | | lspprat.v |
. . . . . . . 8
β’ π = (Baseβπ) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
7 | 5, 6 | lmod0vcl 20395 |
. . . . . . 7
β’ (π β LMod β
(0gβπ)
β π) |
8 | 4, 7 | syl 17 |
. . . . . 6
β’ (π β (0gβπ) β π) |
9 | 8 | adantr 482 |
. . . . 5
β’ ((π β§ π β {(0gβπ)}) β
(0gβπ)
β π) |
10 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β {(0gβπ)}) β π β {(0gβπ)}) |
11 | | lspprat.u |
. . . . . . . . 9
β’ (π β π β π) |
12 | | lspprat.s |
. . . . . . . . . 10
β’ π = (LSubSpβπ) |
13 | 6, 12 | lss0ss 20453 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π) β {(0gβπ)} β π) |
14 | 4, 11, 13 | syl2anc 585 |
. . . . . . . 8
β’ (π β
{(0gβπ)}
β π) |
15 | 14 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β {(0gβπ)}) β
{(0gβπ)}
β π) |
16 | 10, 15 | eqssd 3965 |
. . . . . 6
β’ ((π β§ π β {(0gβπ)}) β π = {(0gβπ)}) |
17 | | lspprat.n |
. . . . . . . . 9
β’ π = (LSpanβπ) |
18 | 6, 17 | lspsn0 20513 |
. . . . . . . 8
β’ (π β LMod β (πβ{(0gβπ)}) =
{(0gβπ)}) |
19 | 4, 18 | syl 17 |
. . . . . . 7
β’ (π β (πβ{(0gβπ)}) =
{(0gβπ)}) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ π β {(0gβπ)}) β (πβ{(0gβπ)}) =
{(0gβπ)}) |
21 | 16, 20 | eqtr4d 2776 |
. . . . 5
β’ ((π β§ π β {(0gβπ)}) β π = (πβ{(0gβπ)})) |
22 | | sneq 4600 |
. . . . . . 7
β’ (π§ = (0gβπ) β {π§} = {(0gβπ)}) |
23 | 22 | fveq2d 6850 |
. . . . . 6
β’ (π§ = (0gβπ) β (πβ{π§}) = (πβ{(0gβπ)})) |
24 | 23 | rspceeqv 3599 |
. . . . 5
β’
(((0gβπ) β π β§ π = (πβ{(0gβπ)})) β βπ§ β π π = (πβ{π§})) |
25 | 9, 21, 24 | syl2anc 585 |
. . . 4
β’ ((π β§ π β {(0gβπ)}) β βπ§ β π π = (πβ{π§})) |
26 | 25 | ex 414 |
. . 3
β’ (π β (π β {(0gβπ)} β βπ§ β π π = (πβ{π§}))) |
27 | 1, 26 | biimtrrid 242 |
. 2
β’ (π β ((π β {(0gβπ)}) = β
β
βπ§ β π π = (πβ{π§}))) |
28 | 5, 12 | lssss 20441 |
. . . . . . . 8
β’ (π β π β π β π) |
29 | 11, 28 | syl 17 |
. . . . . . 7
β’ (π β π β π) |
30 | 29 | ssdifssd 4106 |
. . . . . 6
β’ (π β (π β {(0gβπ)}) β π) |
31 | 30 | sseld 3947 |
. . . . 5
β’ (π β (π§ β (π β {(0gβπ)}) β π§ β π)) |
32 | | lspprat.x |
. . . . . 6
β’ (π β π β π) |
33 | | lspprat.y |
. . . . . 6
β’ (π β π β π) |
34 | | lspprat.p |
. . . . . 6
β’ (π β π β (πβ{π, π})) |
35 | 5, 12, 17, 2, 11, 32, 33, 34, 6 | lsppratlem6 20658 |
. . . . 5
β’ (π β (π§ β (π β {(0gβπ)}) β π = (πβ{π§}))) |
36 | 31, 35 | jcad 514 |
. . . 4
β’ (π β (π§ β (π β {(0gβπ)}) β (π§ β π β§ π = (πβ{π§})))) |
37 | 36 | eximdv 1921 |
. . 3
β’ (π β (βπ§ π§ β (π β {(0gβπ)}) β βπ§(π§ β π β§ π = (πβ{π§})))) |
38 | | n0 4310 |
. . 3
β’ ((π β
{(0gβπ)})
β β
β βπ§ π§ β (π β {(0gβπ)})) |
39 | | df-rex 3071 |
. . 3
β’
(βπ§ β
π π = (πβ{π§}) β βπ§(π§ β π β§ π = (πβ{π§}))) |
40 | 37, 38, 39 | 3imtr4g 296 |
. 2
β’ (π β ((π β {(0gβπ)}) β β
β
βπ§ β π π = (πβ{π§}))) |
41 | 27, 40 | pm2.61dne 3028 |
1
β’ (π β βπ§ β π π = (πβ{π§})) |