Step |
Hyp |
Ref |
Expression |
0 |
|
cprjsp |
|- PrjSp |
1 |
|
vv |
|- v |
2 |
|
clvec |
|- LVec |
3 |
|
cbs |
|- Base |
4 |
1
|
cv |
|- v |
5 |
4 3
|
cfv |
|- ( Base ` v ) |
6 |
|
c0g |
|- 0g |
7 |
4 6
|
cfv |
|- ( 0g ` v ) |
8 |
7
|
csn |
|- { ( 0g ` v ) } |
9 |
5 8
|
cdif |
|- ( ( Base ` v ) \ { ( 0g ` v ) } ) |
10 |
|
vb |
|- b |
11 |
10
|
cv |
|- b |
12 |
|
vx |
|- x |
13 |
|
vy |
|- y |
14 |
12
|
cv |
|- x |
15 |
14 11
|
wcel |
|- x e. b |
16 |
13
|
cv |
|- y |
17 |
16 11
|
wcel |
|- y e. b |
18 |
15 17
|
wa |
|- ( x e. b /\ y e. b ) |
19 |
|
vl |
|- l |
20 |
|
csca |
|- Scalar |
21 |
4 20
|
cfv |
|- ( Scalar ` v ) |
22 |
21 3
|
cfv |
|- ( Base ` ( Scalar ` v ) ) |
23 |
19
|
cv |
|- l |
24 |
|
cvsca |
|- .s |
25 |
4 24
|
cfv |
|- ( .s ` v ) |
26 |
23 16 25
|
co |
|- ( l ( .s ` v ) y ) |
27 |
14 26
|
wceq |
|- x = ( l ( .s ` v ) y ) |
28 |
27 19 22
|
wrex |
|- E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) |
29 |
18 28
|
wa |
|- ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) |
30 |
29 12 13
|
copab |
|- { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } |
31 |
11 30
|
cqs |
|- ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) |
32 |
10 9 31
|
csb |
|- [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) |
33 |
1 2 32
|
cmpt |
|- ( v e. LVec |-> [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) ) |
34 |
0 33
|
wceq |
|- PrjSp = ( v e. LVec |-> [_ ( ( Base ` v ) \ { ( 0g ` v ) } ) / b ]_ ( b /. { <. x , y >. | ( ( x e. b /\ y e. b ) /\ E. l e. ( Base ` ( Scalar ` v ) ) x = ( l ( .s ` v ) y ) ) } ) ) |