Step | Hyp | Ref
| Expression |
1 | | ocvfval.v |
. . . 4
β’ π = (Baseβπ) |
2 | 1 | fvexi 6861 |
. . 3
β’ π β V |
3 | 2 | elpw2 5307 |
. 2
β’ (π β π« π β π β π) |
4 | | ocvfval.i |
. . . . . 6
β’ , =
(Β·πβπ) |
5 | | ocvfval.f |
. . . . . 6
β’ πΉ = (Scalarβπ) |
6 | | ocvfval.z |
. . . . . 6
β’ 0 =
(0gβπΉ) |
7 | | ocvfval.o |
. . . . . 6
β’ β₯ =
(ocvβπ) |
8 | 1, 4, 5, 6, 7 | ocvfval 21086 |
. . . . 5
β’ (π β V β β₯ =
(π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })) |
9 | 8 | fveq1d 6849 |
. . . 4
β’ (π β V β ( β₯
βπ) = ((π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })βπ)) |
10 | | raleq 3312 |
. . . . . 6
β’ (π = π β (βπ¦ β π (π₯ , π¦) = 0 β βπ¦ β π (π₯ , π¦) = 0 )) |
11 | 10 | rabbidv 3418 |
. . . . 5
β’ (π = π β {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
12 | | eqid 2737 |
. . . . 5
β’ (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
13 | 2 | rabex 5294 |
. . . . 5
β’ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } β
V |
14 | 11, 12, 13 | fvmpt 6953 |
. . . 4
β’ (π β π« π β ((π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })βπ) = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
15 | 9, 14 | sylan9eq 2797 |
. . 3
β’ ((π β V β§ π β π« π) β ( β₯ βπ) = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
16 | | 0fv 6891 |
. . . . 5
β’
(β
βπ) =
β
|
17 | | fvprc 6839 |
. . . . . . 7
β’ (Β¬
π β V β
(ocvβπ) =
β
) |
18 | 7, 17 | eqtrid 2789 |
. . . . . 6
β’ (Β¬
π β V β β₯ =
β
) |
19 | 18 | fveq1d 6849 |
. . . . 5
β’ (Β¬
π β V β ( β₯
βπ) =
(β
βπ)) |
20 | | ssrab2 4042 |
. . . . . 6
β’ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } β π |
21 | | fvprc 6839 |
. . . . . . 7
β’ (Β¬
π β V β
(Baseβπ) =
β
) |
22 | 1, 21 | eqtrid 2789 |
. . . . . 6
β’ (Β¬
π β V β π = β
) |
23 | | sseq0 4364 |
. . . . . 6
β’ (({π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } β π β§ π = β
) β {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } =
β
) |
24 | 20, 22, 23 | sylancr 588 |
. . . . 5
β’ (Β¬
π β V β {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } =
β
) |
25 | 16, 19, 24 | 3eqtr4a 2803 |
. . . 4
β’ (Β¬
π β V β ( β₯
βπ) = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
26 | 25 | adantr 482 |
. . 3
β’ ((Β¬
π β V β§ π β π« π) β ( β₯ βπ) = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
27 | 15, 26 | pm2.61ian 811 |
. 2
β’ (π β π« π β ( β₯ βπ) = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
28 | 3, 27 | sylbir 234 |
1
β’ (π β π β ( β₯ βπ) = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |