Step | Hyp | Ref
| Expression |
1 | | cobs 21124 |
. 2
class
OBasis |
2 | | vh |
. . 3
setvar β |
3 | | cphl 21044 |
. . 3
class
PreHil |
4 | | vx |
. . . . . . . . . 10
setvar π₯ |
5 | 4 | cv 1541 |
. . . . . . . . 9
class π₯ |
6 | | vy |
. . . . . . . . . 10
setvar π¦ |
7 | 6 | cv 1541 |
. . . . . . . . 9
class π¦ |
8 | 2 | cv 1541 |
. . . . . . . . . 10
class β |
9 | | cip 17143 |
. . . . . . . . . 10
class
Β·π |
10 | 8, 9 | cfv 6497 |
. . . . . . . . 9
class
(Β·πββ) |
11 | 5, 7, 10 | co 7358 |
. . . . . . . 8
class (π₯(Β·πββ)π¦) |
12 | 4, 6 | weq 1967 |
. . . . . . . . 9
wff π₯ = π¦ |
13 | | csca 17141 |
. . . . . . . . . . 11
class
Scalar |
14 | 8, 13 | cfv 6497 |
. . . . . . . . . 10
class
(Scalarββ) |
15 | | cur 19918 |
. . . . . . . . . 10
class
1r |
16 | 14, 15 | cfv 6497 |
. . . . . . . . 9
class
(1rβ(Scalarββ)) |
17 | | c0g 17326 |
. . . . . . . . . 10
class
0g |
18 | 14, 17 | cfv 6497 |
. . . . . . . . 9
class
(0gβ(Scalarββ)) |
19 | 12, 16, 18 | cif 4487 |
. . . . . . . 8
class if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) |
20 | 11, 19 | wceq 1542 |
. . . . . . 7
wff (π₯(Β·πββ)π¦) = if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) |
21 | | vb |
. . . . . . . 8
setvar π |
22 | 21 | cv 1541 |
. . . . . . 7
class π |
23 | 20, 6, 22 | wral 3061 |
. . . . . 6
wff
βπ¦ β
π (π₯(Β·πββ)π¦) = if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) |
24 | 23, 4, 22 | wral 3061 |
. . . . 5
wff
βπ₯ β
π βπ¦ β π (π₯(Β·πββ)π¦) = if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) |
25 | | cocv 21080 |
. . . . . . . 8
class
ocv |
26 | 8, 25 | cfv 6497 |
. . . . . . 7
class
(ocvββ) |
27 | 22, 26 | cfv 6497 |
. . . . . 6
class
((ocvββ)βπ) |
28 | 8, 17 | cfv 6497 |
. . . . . . 7
class
(0gββ) |
29 | 28 | csn 4587 |
. . . . . 6
class
{(0gββ)} |
30 | 27, 29 | wceq 1542 |
. . . . 5
wff
((ocvββ)βπ) = {(0gββ)} |
31 | 24, 30 | wa 397 |
. . . 4
wff
(βπ₯ β
π βπ¦ β π (π₯(Β·πββ)π¦) = if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) β§ ((ocvββ)βπ) = {(0gββ)}) |
32 | | cbs 17088 |
. . . . . 6
class
Base |
33 | 8, 32 | cfv 6497 |
. . . . 5
class
(Baseββ) |
34 | 33 | cpw 4561 |
. . . 4
class π«
(Baseββ) |
35 | 31, 21, 34 | crab 3406 |
. . 3
class {π β π«
(Baseββ) β£
(βπ₯ β π βπ¦ β π (π₯(Β·πββ)π¦) = if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) β§ ((ocvββ)βπ) = {(0gββ)})} |
36 | 2, 3, 35 | cmpt 5189 |
. 2
class (β β PreHil β¦ {π β π«
(Baseββ) β£
(βπ₯ β π βπ¦ β π (π₯(Β·πββ)π¦) = if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) β§ ((ocvββ)βπ) = {(0gββ)})}) |
37 | 1, 36 | wceq 1542 |
1
wff OBasis =
(β β PreHil β¦
{π β π«
(Baseββ) β£
(βπ₯ β π βπ¦ β π (π₯(Β·πββ)π¦) = if(π₯ = π¦, (1rβ(Scalarββ)),
(0gβ(Scalarββ))) β§ ((ocvββ)βπ) = {(0gββ)})}) |