Metamath Proof Explorer

Theorem asclfval

Description: Function value of the algebra scalar lifting function. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Hypotheses asclfval.a 
|- A = ( algSc ` W )
asclfval.f 
|- F = ( Scalar ` W )
asclfval.k 
|- K = ( Base ` F )
asclfval.s 
|- .x. = ( .s ` W )
asclfval.o 
|- .1. = ( 1r ` W )
Assertion asclfval 
|- A = ( x e. K |-> ( x .x. .1. ) )

Proof

Step Hyp Ref Expression
1 asclfval.a 
 |-  A = ( algSc ` W )
2 asclfval.f 
 |-  F = ( Scalar ` W )
3 asclfval.k 
 |-  K = ( Base ` F )
4 asclfval.s 
 |-  .x. = ( .s ` W )
5 asclfval.o 
 |-  .1. = ( 1r ` 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 -> ( .s ` w ) = ( .s ` W ) )
11 10 4 eqtr4di 
 |-  ( w = W -> ( .s ` w ) = .x. )
12 eqidd 
 |-  ( w = W -> x = x )
13 fveq2 
 |-  ( w = W -> ( 1r ` w ) = ( 1r ` W ) )
14 13 5 eqtr4di 
 |-  ( w = W -> ( 1r ` w ) = .1. )
15 11 12 14 oveq123d 
 |-  ( w = W -> ( x ( .s ` w ) ( 1r ` w ) ) = ( x .x. .1. ) )
16 9 15 mpteq12dv 
 |-  ( w = W -> ( x e. ( Base ` ( Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) = ( x e. K |-> ( x .x. .1. ) ) )
17 df-ascl 
 |-  algSc = ( w e. _V |-> ( x e. ( Base ` ( Scalar ` w ) ) |-> ( x ( .s ` w ) ( 1r ` w ) ) ) )
18 16 17 3 mptfvmpt 
 |-  ( W e. _V -> ( algSc ` W ) = ( x e. K |-> ( x .x. .1. ) ) )
19 fvprc 
 |-  ( -. W e. _V -> ( algSc ` W ) = (/) )
20 mpt0 
 |-  ( x e. (/) |-> ( x .x. .1. ) ) = (/)
21 19 20 eqtr4di 
 |-  ( -. W e. _V -> ( algSc ` W ) = ( x e. (/) |-> ( x .x. .1. ) ) )
22 fvprc 
 |-  ( -. W e. _V -> ( Scalar ` W ) = (/) )
23 2 22 eqtrid 
 |-  ( -. W e. _V -> F = (/) )
24 23 fveq2d 
 |-  ( -. W e. _V -> ( Base ` F ) = ( Base ` (/) ) )
25 base0 
 |-  (/) = ( Base ` (/) )
26 24 25 eqtr4di 
 |-  ( -. W e. _V -> ( Base ` F ) = (/) )
27 3 26 eqtrid 
 |-  ( -. W e. _V -> K = (/) )
28 27 mpteq1d 
 |-  ( -. W e. _V -> ( x e. K |-> ( x .x. .1. ) ) = ( x e. (/) |-> ( x .x. .1. ) ) )
29 21 28 eqtr4d 
 |-  ( -. W e. _V -> ( algSc ` W ) = ( x e. K |-> ( x .x. .1. ) ) )
30 18 29 pm2.61i 
 |-  ( algSc ` W ) = ( x e. K |-> ( x .x. .1. ) )
31 1 30 eqtri 
 |-  A = ( x e. K |-> ( x .x. .1. ) )