Metamath Proof Explorer

Theorem scaffval

Description: The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses scaffval.b 
|- B = ( Base ` W )
scaffval.f 
|- F = ( Scalar ` W )
scaffval.k 
|- K = ( Base ` F )
scaffval.a 
|- .xb = ( .sf ` W )
scaffval.s 
|- .x. = ( .s ` W )
Assertion scaffval 
|- .xb = ( x e. K , y e. B |-> ( x .x. y ) )

Proof

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 eqtrid 
 |-  ( -. 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 ) )