Step | Hyp | Ref
| Expression |
1 | | cprjsp 41030 |
. 2
class
βπ£π π |
2 | | vv |
. . 3
setvar π£ |
3 | | clvec 20635 |
. . 3
class
LVec |
4 | | vb |
. . . 4
setvar π |
5 | 2 | cv 1540 |
. . . . . 6
class π£ |
6 | | cbs 17109 |
. . . . . 6
class
Base |
7 | 5, 6 | cfv 6516 |
. . . . 5
class
(Baseβπ£) |
8 | | c0g 17350 |
. . . . . . 7
class
0g |
9 | 5, 8 | cfv 6516 |
. . . . . 6
class
(0gβπ£) |
10 | 9 | csn 4606 |
. . . . 5
class
{(0gβπ£)} |
11 | 7, 10 | cdif 3925 |
. . . 4
class
((Baseβπ£)
β {(0gβπ£)}) |
12 | 4 | cv 1540 |
. . . . 5
class π |
13 | | vx |
. . . . . . . . 9
setvar π₯ |
14 | 13, 4 | wel 2107 |
. . . . . . . 8
wff π₯ β π |
15 | | vy |
. . . . . . . . 9
setvar π¦ |
16 | 15, 4 | wel 2107 |
. . . . . . . 8
wff π¦ β π |
17 | 14, 16 | wa 396 |
. . . . . . 7
wff (π₯ β π β§ π¦ β π) |
18 | 13 | cv 1540 |
. . . . . . . . 9
class π₯ |
19 | | vl |
. . . . . . . . . . 11
setvar π |
20 | 19 | cv 1540 |
. . . . . . . . . 10
class π |
21 | 15 | cv 1540 |
. . . . . . . . . 10
class π¦ |
22 | | cvsca 17166 |
. . . . . . . . . . 11
class
Β·π |
23 | 5, 22 | cfv 6516 |
. . . . . . . . . 10
class (
Β·π βπ£) |
24 | 20, 21, 23 | co 7377 |
. . . . . . . . 9
class (π(
Β·π βπ£)π¦) |
25 | 18, 24 | wceq 1541 |
. . . . . . . 8
wff π₯ = (π( Β·π
βπ£)π¦) |
26 | | csca 17165 |
. . . . . . . . . 10
class
Scalar |
27 | 5, 26 | cfv 6516 |
. . . . . . . . 9
class
(Scalarβπ£) |
28 | 27, 6 | cfv 6516 |
. . . . . . . 8
class
(Baseβ(Scalarβπ£)) |
29 | 25, 19, 28 | wrex 3069 |
. . . . . . 7
wff
βπ β
(Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦) |
30 | 17, 29 | wa 396 |
. . . . . 6
wff ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦)) |
31 | 30, 13, 15 | copab 5187 |
. . . . 5
class
{β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))} |
32 | 12, 31 | cqs 8669 |
. . . 4
class (π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))}) |
33 | 4, 11, 32 | csb 3873 |
. . 3
class
β¦((Baseβπ£) β {(0gβπ£)}) / πβ¦(π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))}) |
34 | 2, 3, 33 | cmpt 5208 |
. 2
class (π£ β LVec β¦
β¦((Baseβπ£) β {(0gβπ£)}) / πβ¦(π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))})) |
35 | 1, 34 | wceq 1541 |
1
wff
βπ£π π = (π£ β LVec β¦
β¦((Baseβπ£) β {(0gβπ£)}) / πβ¦(π / {β¨π₯, π¦β© β£ ((π₯ β π β§ π¦ β π) β§ βπ β (Baseβ(Scalarβπ£))π₯ = (π( Β·π
βπ£)π¦))})) |