Step | Hyp | Ref
| Expression |
1 | | elfvdm 6883 |
. . . . 5
β’ (π΄ β ( β₯ βπ) β π β dom β₯ ) |
2 | | n0i 4297 |
. . . . . . . . 9
β’ (π΄ β ( β₯ βπ) β Β¬ ( β₯
βπ) =
β
) |
3 | | ocvfval.o |
. . . . . . . . . . . 12
β’ β₯ =
(ocvβπ) |
4 | | fvprc 6838 |
. . . . . . . . . . . 12
β’ (Β¬
π β V β
(ocvβπ) =
β
) |
5 | 3, 4 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (Β¬
π β V β β₯ =
β
) |
6 | 5 | fveq1d 6848 |
. . . . . . . . . 10
β’ (Β¬
π β V β ( β₯
βπ) =
(β
βπ)) |
7 | | 0fv 6890 |
. . . . . . . . . 10
β’
(β
βπ) =
β
|
8 | 6, 7 | eqtrdi 2789 |
. . . . . . . . 9
β’ (Β¬
π β V β ( β₯
βπ) =
β
) |
9 | 2, 8 | nsyl2 141 |
. . . . . . . 8
β’ (π΄ β ( β₯ βπ) β π β V) |
10 | | ocvfval.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
11 | | ocvfval.i |
. . . . . . . . 9
β’ , =
(Β·πβπ) |
12 | | ocvfval.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
13 | | ocvfval.z |
. . . . . . . . 9
β’ 0 =
(0gβπΉ) |
14 | 10, 11, 12, 13, 3 | ocvfval 21093 |
. . . . . . . 8
β’ (π β V β β₯ =
(π β π« π β¦ {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 })) |
15 | 9, 14 | syl 17 |
. . . . . . 7
β’ (π΄ β ( β₯ βπ) β β₯ = (π β π« π β¦ {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 })) |
16 | 15 | dmeqd 5865 |
. . . . . 6
β’ (π΄ β ( β₯ βπ) β dom β₯ = dom (π β π« π β¦ {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 })) |
17 | 10 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
18 | 17 | rabex 5293 |
. . . . . . 7
β’ {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 } β
V |
19 | | eqid 2733 |
. . . . . . 7
β’ (π β π« π β¦ {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 }) = (π β π« π β¦ {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 }) |
20 | 18, 19 | dmmpti 6649 |
. . . . . 6
β’ dom
(π β π« π β¦ {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 }) = π« π |
21 | 16, 20 | eqtrdi 2789 |
. . . . 5
β’ (π΄ β ( β₯ βπ) β dom β₯ = π« π) |
22 | 1, 21 | eleqtrd 2836 |
. . . 4
β’ (π΄ β ( β₯ βπ) β π β π« π) |
23 | 22 | elpwid 4573 |
. . 3
β’ (π΄ β ( β₯ βπ) β π β π) |
24 | 10, 11, 12, 13, 3 | ocvval 21094 |
. . . . 5
β’ (π β π β ( β₯ βπ) = {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 }) |
25 | 24 | eleq2d 2820 |
. . . 4
β’ (π β π β (π΄ β ( β₯ βπ) β π΄ β {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 })) |
26 | | oveq1 7368 |
. . . . . . 7
β’ (π¦ = π΄ β (π¦ , π₯) = (π΄ , π₯)) |
27 | 26 | eqeq1d 2735 |
. . . . . 6
β’ (π¦ = π΄ β ((π¦ , π₯) = 0 β (π΄ , π₯) = 0 )) |
28 | 27 | ralbidv 3171 |
. . . . 5
β’ (π¦ = π΄ β (βπ₯ β π (π¦ , π₯) = 0 β βπ₯ β π (π΄ , π₯) = 0 )) |
29 | 28 | elrab 3649 |
. . . 4
β’ (π΄ β {π¦ β π β£ βπ₯ β π (π¦ , π₯) = 0 } β (π΄ β π β§ βπ₯ β π (π΄ , π₯) = 0 )) |
30 | 25, 29 | bitrdi 287 |
. . 3
β’ (π β π β (π΄ β ( β₯ βπ) β (π΄ β π β§ βπ₯ β π (π΄ , π₯) = 0 ))) |
31 | 23, 30 | biadanii 821 |
. 2
β’ (π΄ β ( β₯ βπ) β (π β π β§ (π΄ β π β§ βπ₯ β π (π΄ , π₯) = 0 ))) |
32 | | 3anass 1096 |
. 2
β’ ((π β π β§ π΄ β π β§ βπ₯ β π (π΄ , π₯) = 0 ) β (π β π β§ (π΄ β π β§ βπ₯ β π (π΄ , π₯) = 0 ))) |
33 | 31, 32 | bitr4i 278 |
1
β’ (π΄ β ( β₯ βπ) β (π β π β§ π΄ β π β§ βπ₯ β π (π΄ , π₯) = 0 )) |