Theorem asclf

Description: The algebra scalar lifting function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	asclf.a	|- A = ( algSc ` W )
	asclf.f	|- F = ( Scalar ` W )
	asclf.r	|- ( ph -> W e. Ring )
	asclf.l	|- ( ph -> W e. LMod )
	asclf.k	|- K = ( Base ` F )
	asclf.b	|- B = ( Base ` W )
Assertion	asclf	|- ( ph -> A : K --> B )

Proof

Step	Hyp	Ref	Expression
1		asclf.a	|- A = ( algSc ` W )
2		asclf.f	|- F = ( Scalar ` W )
3		asclf.r	|- ( ph -> W e. Ring )
4		asclf.l	|- ( ph -> W e. LMod )
5		asclf.k	|- K = ( Base ` F )
6		asclf.b	|- B = ( Base ` W )
7	4	adantr	|- ( ( ph /\ x e. K ) -> W e. LMod )
8		simpr	|- ( ( ph /\ x e. K ) -> x e. K )
9		eqid	|- ( 1r ` W ) = ( 1r ` W )
10	6 9	ringidcl	|- ( W e. Ring -> ( 1r ` W ) e. B )
11	3 10	syl	|- ( ph -> ( 1r ` W ) e. B )
12	11	adantr	|- ( ( ph /\ x e. K ) -> ( 1r ` W ) e. B )
13		eqid	|- ( .s ` W ) = ( .s ` W )
14	6 2 13 5	lmodvscl	|- ( ( W e. LMod /\ x e. K /\ ( 1r ` W ) e. B ) -> ( x ( .s ` W ) ( 1r ` W ) ) e. B )
15	7 8 12 14	syl3anc	|- ( ( ph /\ x e. K ) -> ( x ( .s ` W ) ( 1r ` W ) ) e. B )
16	1 2 5 13 9	asclfval	|- A = ( x e. K |-> ( x ( .s ` W ) ( 1r ` W ) ) )
17	15 16	fmptd	|- ( ph -> A : K --> B )