# Metamath Proof Explorer

## Theorem asclrhm

Description: The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Hypotheses asclrhm.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
asclrhm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
Assertion asclrhm ${⊢}{W}\in \mathrm{AssAlg}\to {A}\in \left({F}\mathrm{RingHom}{W}\right)$

### Proof

Step Hyp Ref Expression
1 asclrhm.a ${⊢}{A}=\mathrm{algSc}\left({W}\right)$
2 asclrhm.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
4 eqid ${⊢}{1}_{{F}}={1}_{{F}}$
5 eqid ${⊢}{1}_{{W}}={1}_{{W}}$
6 eqid ${⊢}{\cdot }_{{F}}={\cdot }_{{F}}$
7 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
8 2 assasca ${⊢}{W}\in \mathrm{AssAlg}\to {F}\in \mathrm{CRing}$
9 crngring ${⊢}{F}\in \mathrm{CRing}\to {F}\in \mathrm{Ring}$
10 8 9 syl ${⊢}{W}\in \mathrm{AssAlg}\to {F}\in \mathrm{Ring}$
11 assaring ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{Ring}$
12 3 4 ringidcl ${⊢}{F}\in \mathrm{Ring}\to {1}_{{F}}\in {\mathrm{Base}}_{{F}}$
13 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
14 1 2 3 13 5 asclval ${⊢}{1}_{{F}}\in {\mathrm{Base}}_{{F}}\to {A}\left({1}_{{F}}\right)={1}_{{F}}{\cdot }_{{W}}{1}_{{W}}$
15 10 12 14 3syl ${⊢}{W}\in \mathrm{AssAlg}\to {A}\left({1}_{{F}}\right)={1}_{{F}}{\cdot }_{{W}}{1}_{{W}}$
16 assalmod ${⊢}{W}\in \mathrm{AssAlg}\to {W}\in \mathrm{LMod}$
17 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
18 17 5 ringidcl ${⊢}{W}\in \mathrm{Ring}\to {1}_{{W}}\in {\mathrm{Base}}_{{W}}$
19 11 18 syl ${⊢}{W}\in \mathrm{AssAlg}\to {1}_{{W}}\in {\mathrm{Base}}_{{W}}$
20 17 2 13 4 lmodvs1 ${⊢}\left({W}\in \mathrm{LMod}\wedge {1}_{{W}}\in {\mathrm{Base}}_{{W}}\right)\to {1}_{{F}}{\cdot }_{{W}}{1}_{{W}}={1}_{{W}}$
21 16 19 20 syl2anc ${⊢}{W}\in \mathrm{AssAlg}\to {1}_{{F}}{\cdot }_{{W}}{1}_{{W}}={1}_{{W}}$
22 15 21 eqtrd ${⊢}{W}\in \mathrm{AssAlg}\to {A}\left({1}_{{F}}\right)={1}_{{W}}$
23 1 2 3 7 6 ascldimul ${⊢}\left({W}\in \mathrm{AssAlg}\wedge {x}\in {\mathrm{Base}}_{{F}}\wedge {y}\in {\mathrm{Base}}_{{F}}\right)\to {A}\left({x}{\cdot }_{{F}}{y}\right)={A}\left({x}\right){\cdot }_{{W}}{A}\left({y}\right)$
24 23 3expb ${⊢}\left({W}\in \mathrm{AssAlg}\wedge \left({x}\in {\mathrm{Base}}_{{F}}\wedge {y}\in {\mathrm{Base}}_{{F}}\right)\right)\to {A}\left({x}{\cdot }_{{F}}{y}\right)={A}\left({x}\right){\cdot }_{{W}}{A}\left({y}\right)$
25 1 2 11 16 asclghm ${⊢}{W}\in \mathrm{AssAlg}\to {A}\in \left({F}\mathrm{GrpHom}{W}\right)$
26 3 4 5 6 7 10 11 22 24 25 isrhm2d ${⊢}{W}\in \mathrm{AssAlg}\to {A}\in \left({F}\mathrm{RingHom}{W}\right)$