# Metamath Proof Explorer

## Theorem ascldimul

Description: The algebra scalars function distributes over multiplication. (Contributed by Mario Carneiro, 8-Mar-2015) (Proof shortened by SN, 5-Nov-2023)

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

### Proof

Step Hyp Ref Expression
1 ascldimul.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 ascldimul.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 ascldimul.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
4 ascldimul.t
5 ascldimul.s
6 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
7 6 3ad2ant1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {W}\in \mathrm{LMod}$
8 simp2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {R}\in {K}$
9 simp3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {S}\in {K}$
10 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
11 10 3ad2ant1 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {W}\in \mathrm{Ring}$
12 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
13 eqid ${⊢}{1}_{{W}}={1}_{{W}}$
14 12 13 ringidcl ${⊢}{W}\in \mathrm{Ring}\to {1}_{{W}}\in {\mathrm{Base}}_{{W}}$
15 11 14 syl ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {1}_{{W}}\in {\mathrm{Base}}_{{W}}$
16 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
17 12 2 16 3 5 lmodvsass
18 7 8 9 15 17 syl13anc
19 2 lmodring ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Ring}$
20 6 19 syl ${⊢}{W}\in \mathrm{AssAlg}\to {F}\in \mathrm{Ring}$
21 3 5 ringcl
22 20 21 syl3an1
23 1 2 3 16 13 asclval
24 22 23 syl
25 1 2 10 6 3 12 asclf ${⊢}{W}\in \mathrm{AssAlg}\to {A}:{K}⟶{\mathrm{Base}}_{{W}}$
26 25 ffvelrnda ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {S}\in {K}\right)\to {A}\left({S}\right)\in {\mathrm{Base}}_{{W}}$
27 26 3adant2 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {A}\left({S}\right)\in {\mathrm{Base}}_{{W}}$
28 1 2 3 12 4 16 asclmul1
29 27 28 syld3an3
30 1 2 3 16 13 asclval ${⊢}{S}\in {K}\to {A}\left({S}\right)={S}{\cdot }_{{W}}{1}_{{W}}$
31 30 3ad2ant3 ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {A}\left({S}\right)={S}{\cdot }_{{W}}{1}_{{W}}$
32 31 oveq2d ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {R}\in {K}\wedge {S}\in {K}\right)\to {R}{\cdot }_{{W}}{A}\left({S}\right)={R}{\cdot }_{{W}}\left({S}{\cdot }_{{W}}{1}_{{W}}\right)$
33 29 32 eqtrd
34 18 24 33 3eqtr4d