Theorem asclrhm

Description: The algebra scalar lifting function 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. Ring )
9		assaring	|- ( W e. AssAlg -> W e. Ring )
10		assalmod	|- ( W e. AssAlg -> W e. LMod )
11	1 2 10 9	ascl1	|- ( W e. AssAlg -> ( A ` ( 1r ` F ) ) = ( 1r ` W ) )
12	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 ) ) )
13	12	3expb	|- ( ( W e. AssAlg /\ ( x e. ( Base ` F ) /\ y e. ( Base ` F ) ) ) -> ( A ` ( x ( .r ` F ) y ) ) = ( ( A ` x ) ( .r ` W ) ( A ` y ) ) )
14	1 2 9 10	asclghm	|- ( W e. AssAlg -> A e. ( F GrpHom W ) )
15	3 4 5 6 7 8 9 11 13 14	isrhm2d	|- ( W e. AssAlg -> A e. ( F RingHom W ) )