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{Ring}$$
9		assaring	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{Ring}$$
10		assalmod	$$⊢W\in \mathrm{AssAlg}\to W\in \mathrm{LMod}$$
11	1 2 10 9	ascl1	$$⊢W\in \mathrm{AssAlg}\to A\left(1_F\right)=1_W$$
12	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)$$
13	12	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)$$
14	1 2 9 10	asclghm	$$⊢W\in \mathrm{AssAlg}\to A\in \left(F\mathrm{GrpHom}W\right)$$
15	3 4 5 6 7 8 9 11 13 14	isrhm2d	$$⊢W\in \mathrm{AssAlg}\to A\in \left(F\mathrm{RingHom}W\right)$$