# Metamath Proof Explorer

## Theorem asclfval

Description: Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Hypotheses asclfval.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
asclfval.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
asclfval.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
asclfval.s
asclfval.o
Assertion asclfval

### Proof

Step Hyp Ref Expression
1 asclfval.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 asclfval.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 asclfval.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
4 asclfval.s
5 asclfval.o
6 fveq2 ${⊢}{w}={W}\to \mathrm{Scalar}\left({w}\right)=\mathrm{Scalar}\left({W}\right)$
7 6 2 eqtr4di ${⊢}{w}={W}\to \mathrm{Scalar}\left({w}\right)={F}$
8 7 fveq2d ${⊢}{w}={W}\to {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}={\mathrm{Base}}_{{F}}$
9 8 3 eqtr4di ${⊢}{w}={W}\to {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}={K}$
10 fveq2 ${⊢}{w}={W}\to {\cdot }_{{w}}={\cdot }_{{W}}$
11 10 4 eqtr4di
12 eqidd ${⊢}{w}={W}\to {x}={x}$
13 fveq2 ${⊢}{w}={W}\to {1}_{{w}}={1}_{{W}}$
14 13 5 eqtr4di
15 11 12 14 oveq123d
16 9 15 mpteq12dv
17 df-ascl ${⊢}\mathrm{algSc}=\left({w}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({w}\right)}⟼{x}{\cdot }_{{w}}{1}_{{w}}\right)\right)$
18 16 17 3 mptfvmpt
19 fvprc ${⊢}¬{W}\in \mathrm{V}\to \mathrm{algSc}\left({W}\right)=\varnothing$
20 mpt0
21 19 20 eqtr4di
22 fvprc ${⊢}¬{W}\in \mathrm{V}\to \mathrm{Scalar}\left({W}\right)=\varnothing$
23 2 22 syl5eq ${⊢}¬{W}\in \mathrm{V}\to {F}=\varnothing$
24 23 fveq2d ${⊢}¬{W}\in \mathrm{V}\to {\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\varnothing }$
25 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
26 24 25 eqtr4di ${⊢}¬{W}\in \mathrm{V}\to {\mathrm{Base}}_{{F}}=\varnothing$
27 3 26 syl5eq ${⊢}¬{W}\in \mathrm{V}\to {K}=\varnothing$
28 27 mpteq1d
29 21 28 eqtr4d
30 18 29 pm2.61i
31 1 30 eqtri