Step |
Hyp |
Ref |
Expression |
1 |
|
scaffval.b |
|- B = ( Base ` W ) |
2 |
|
scaffval.f |
|- F = ( Scalar ` W ) |
3 |
|
scaffval.k |
|- K = ( Base ` F ) |
4 |
|
scaffval.a |
|- .xb = ( .sf ` W ) |
5 |
|
scaffval.s |
|- .x. = ( .s ` W ) |
6 |
|
fveq2 |
|- ( w = W -> ( Scalar ` w ) = ( Scalar ` W ) ) |
7 |
6 2
|
eqtr4di |
|- ( w = W -> ( Scalar ` w ) = F ) |
8 |
7
|
fveq2d |
|- ( w = W -> ( Base ` ( Scalar ` w ) ) = ( Base ` F ) ) |
9 |
8 3
|
eqtr4di |
|- ( w = W -> ( Base ` ( Scalar ` w ) ) = K ) |
10 |
|
fveq2 |
|- ( w = W -> ( Base ` w ) = ( Base ` W ) ) |
11 |
10 1
|
eqtr4di |
|- ( w = W -> ( Base ` w ) = B ) |
12 |
|
fveq2 |
|- ( w = W -> ( .s ` w ) = ( .s ` W ) ) |
13 |
12 5
|
eqtr4di |
|- ( w = W -> ( .s ` w ) = .x. ) |
14 |
13
|
oveqd |
|- ( w = W -> ( x ( .s ` w ) y ) = ( x .x. y ) ) |
15 |
9 11 14
|
mpoeq123dv |
|- ( w = W -> ( x e. ( Base ` ( Scalar ` w ) ) , y e. ( Base ` w ) |-> ( x ( .s ` w ) y ) ) = ( x e. K , y e. B |-> ( x .x. y ) ) ) |
16 |
|
df-scaf |
|- .sf = ( w e. _V |-> ( x e. ( Base ` ( Scalar ` w ) ) , y e. ( Base ` w ) |-> ( x ( .s ` w ) y ) ) ) |
17 |
3
|
fvexi |
|- K e. _V |
18 |
1
|
fvexi |
|- B e. _V |
19 |
5
|
fvexi |
|- .x. e. _V |
20 |
19
|
rnex |
|- ran .x. e. _V |
21 |
|
p0ex |
|- { (/) } e. _V |
22 |
20 21
|
unex |
|- ( ran .x. u. { (/) } ) e. _V |
23 |
|
df-ov |
|- ( x .x. y ) = ( .x. ` <. x , y >. ) |
24 |
|
fvrn0 |
|- ( .x. ` <. x , y >. ) e. ( ran .x. u. { (/) } ) |
25 |
23 24
|
eqeltri |
|- ( x .x. y ) e. ( ran .x. u. { (/) } ) |
26 |
25
|
rgen2w |
|- A. x e. K A. y e. B ( x .x. y ) e. ( ran .x. u. { (/) } ) |
27 |
17 18 22 26
|
mpoexw |
|- ( x e. K , y e. B |-> ( x .x. y ) ) e. _V |
28 |
15 16 27
|
fvmpt |
|- ( W e. _V -> ( .sf ` W ) = ( x e. K , y e. B |-> ( x .x. y ) ) ) |
29 |
|
fvprc |
|- ( -. W e. _V -> ( .sf ` W ) = (/) ) |
30 |
|
fvprc |
|- ( -. W e. _V -> ( Base ` W ) = (/) ) |
31 |
1 30
|
syl5eq |
|- ( -. W e. _V -> B = (/) ) |
32 |
31
|
olcd |
|- ( -. W e. _V -> ( K = (/) \/ B = (/) ) ) |
33 |
|
0mpo0 |
|- ( ( K = (/) \/ B = (/) ) -> ( x e. K , y e. B |-> ( x .x. y ) ) = (/) ) |
34 |
32 33
|
syl |
|- ( -. W e. _V -> ( x e. K , y e. B |-> ( x .x. y ) ) = (/) ) |
35 |
29 34
|
eqtr4d |
|- ( -. W e. _V -> ( .sf ` W ) = ( x e. K , y e. B |-> ( x .x. y ) ) ) |
36 |
28 35
|
pm2.61i |
|- ( .sf ` W ) = ( x e. K , y e. B |-> ( x .x. y ) ) |
37 |
4 36
|
eqtri |
|- .xb = ( x e. K , y e. B |-> ( x .x. y ) ) |