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 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 ) )