Theorem asclrhm

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

	Ref	Expression
Hypotheses	asclrhm.a	|- A = ( algSc ` W )
	asclrhm.f	|- F = ( Scalar ` W )
Assertion	asclrhm	|- ( W e. AssAlg -> A e. ( F RingHom W ) )

Proof

Step	Hyp	Ref	Expression
1		asclrhm.a	|- A = ( algSc ` W )
2		asclrhm.f	|- F = ( Scalar ` W )
3		eqid	|- ( Base ` F ) = ( Base ` F )
4		eqid	|- ( 1r ` F ) = ( 1r ` F )
5		eqid	|- ( 1r ` W ) = ( 1r ` W )
6		eqid	|- ( .r ` F ) = ( .r ` F )
7		eqid	|- ( .r ` W ) = ( .r ` W )
8	2	assasca	|- ( W e. AssAlg -> F e. CRing )
9	8	crngringd	|- ( W e. AssAlg -> F e. Ring )
10		assaring	|- ( W e. AssAlg -> W e. Ring )
11		assalmod	|- ( W e. AssAlg -> W e. LMod )
12	1 2 11 10	ascl1	|- ( W e. AssAlg -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) )
13	1 2 3 7 6	ascldimul	|- ( ( W e. AssAlg /\ x e. ( Base ` F ) /\ y e. ( Base ` F ) ) -> ( A ` ( x ( .r ` F ) y ) ) = ( ( A ` x ) ( .r ` W ) ( A ` y ) ) )
14	13	3expb	|- ( ( W e. AssAlg /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( A ` ( x ( .r ` F ) y ) ) = ( ( A ` x ) ( .r ` W ) ( A ` y ) ) )
15	1 2 10 11	asclghm	|- ( W e. AssAlg -> A e. ( F GrpHom W ) )
16	3 4 5 6 7 9 10 12 14 15	isrhm2d	|- ( W e. AssAlg -> A e. ( F RingHom W ) )