# Metamath Proof Explorer

## Theorem asclf

Description: The algebra scalars function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses asclf.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
asclf.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
asclf.r ${⊢}{\phi }\to {W}\in \mathrm{Ring}$
asclf.l ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
asclf.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
asclf.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
Assertion asclf ${⊢}{\phi }\to {A}:{K}⟶{B}$

### Proof

Step Hyp Ref Expression
1 asclf.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 asclf.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 asclf.r ${⊢}{\phi }\to {W}\in \mathrm{Ring}$
4 asclf.l ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
5 asclf.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
6 asclf.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
7 4 adantr ${⊢}\left({\phi }\wedge {x}\in {K}\right)\to {W}\in \mathrm{LMod}$
8 simpr ${⊢}\left({\phi }\wedge {x}\in {K}\right)\to {x}\in {K}$
9 eqid ${⊢}{1}_{{W}}={1}_{{W}}$
10 6 9 ringidcl ${⊢}{W}\in \mathrm{Ring}\to {1}_{{W}}\in {B}$
11 3 10 syl ${⊢}{\phi }\to {1}_{{W}}\in {B}$
12 11 adantr ${⊢}\left({\phi }\wedge {x}\in {K}\right)\to {1}_{{W}}\in {B}$
13 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
14 6 2 13 5 lmodvscl ${⊢}\left({W}\in \mathrm{LMod}\wedge {x}\in {K}\wedge {1}_{{W}}\in {B}\right)\to {x}{\cdot }_{{W}}{1}_{{W}}\in {B}$
15 7 8 12 14 syl3anc ${⊢}\left({\phi }\wedge {x}\in {K}\right)\to {x}{\cdot }_{{W}}{1}_{{W}}\in {B}$
16 1 2 5 13 9 asclfval ${⊢}{A}=\left({x}\in {K}⟼{x}{\cdot }_{{W}}{1}_{{W}}\right)$
17 15 16 fmptd ${⊢}{\phi }\to {A}:{K}⟶{B}$