Step | Hyp | Ref
| Expression |
1 | | ocvfval.o |
. 2
β’ β₯ =
(ocvβπ) |
2 | | elex 3465 |
. . 3
β’ (π β π β π β V) |
3 | | fveq2 6846 |
. . . . . . 7
β’ (β = π β (Baseββ) = (Baseβπ)) |
4 | | ocvfval.v |
. . . . . . 7
β’ π = (Baseβπ) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . 6
β’ (β = π β (Baseββ) = π) |
6 | 5 | pweqd 4581 |
. . . . 5
β’ (β = π β π« (Baseββ) = π« π) |
7 | | fveq2 6846 |
. . . . . . . . . 10
β’ (β = π β
(Β·πββ) =
(Β·πβπ)) |
8 | | ocvfval.i |
. . . . . . . . . 10
β’ , =
(Β·πβπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . . 9
β’ (β = π β
(Β·πββ) = , ) |
10 | 9 | oveqd 7378 |
. . . . . . . 8
β’ (β = π β (π₯(Β·πββ)π¦) = (π₯ , π¦)) |
11 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (β = π β (Scalarββ) = (Scalarβπ)) |
12 | | ocvfval.f |
. . . . . . . . . . 11
β’ πΉ = (Scalarβπ) |
13 | 11, 12 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (β = π β (Scalarββ) = πΉ) |
14 | 13 | fveq2d 6850 |
. . . . . . . . 9
β’ (β = π β
(0gβ(Scalarββ)) = (0gβπΉ)) |
15 | | ocvfval.z |
. . . . . . . . 9
β’ 0 =
(0gβπΉ) |
16 | 14, 15 | eqtr4di 2791 |
. . . . . . . 8
β’ (β = π β
(0gβ(Scalarββ)) = 0 ) |
17 | 10, 16 | eqeq12d 2749 |
. . . . . . 7
β’ (β = π β ((π₯(Β·πββ)π¦) = (0gβ(Scalarββ)) β (π₯ , π¦) = 0 )) |
18 | 17 | ralbidv 3171 |
. . . . . 6
β’ (β = π β (βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ)) β βπ¦ β π (π₯ , π¦) = 0 )) |
19 | 5, 18 | rabeqbidv 3423 |
. . . . 5
β’ (β = π β {π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))} = {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
20 | 6, 19 | mpteq12dv 5200 |
. . . 4
β’ (β = π β (π β π« (Baseββ) β¦ {π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))}) = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })) |
21 | | df-ocv 21090 |
. . . 4
β’ ocv =
(β β V β¦ (π β π«
(Baseββ) β¦
{π₯ β (Baseββ) β£ βπ¦ β π (π₯(Β·πββ)π¦) = (0gβ(Scalarββ))})) |
22 | | eqid 2733 |
. . . . . 6
β’ (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) |
23 | 4 | fvexi 6860 |
. . . . . . . 8
β’ π β V |
24 | | ssrab2 4041 |
. . . . . . . 8
β’ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } β π |
25 | 23, 24 | elpwi2 5307 |
. . . . . . 7
β’ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } β π« π |
26 | 25 | a1i 11 |
. . . . . 6
β’ (π β π« π β {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 } β π« π) |
27 | 22, 26 | fmpti 7064 |
. . . . 5
β’ (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }):π« πβΆπ« π |
28 | 23 | pwex 5339 |
. . . . 5
β’ π«
π β V |
29 | | fex2 7874 |
. . . . 5
β’ (((π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }):π« πβΆπ« π β§ π« π β V β§ π« π β V) β (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) β
V) |
30 | 27, 28, 28, 29 | mp3an 1462 |
. . . 4
β’ (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 }) β
V |
31 | 20, 21, 30 | fvmpt 6952 |
. . 3
β’ (π β V β
(ocvβπ) = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })) |
32 | 2, 31 | syl 17 |
. 2
β’ (π β π β (ocvβπ) = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })) |
33 | 1, 32 | eqtrid 2785 |
1
β’ (π β π β β₯ = (π β π« π β¦ {π₯ β π β£ βπ¦ β π (π₯ , π¦) = 0 })) |