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=\mathrm{algSc}\left(W\right)$$
	asclf.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclf.r	$$⊢\phi \to W\in \mathrm{Ring}$$
	asclf.l	$$⊢\phi \to W\in \mathrm{LMod}$$
	asclf.k	$$⊢K={\mathrm{Base}}_F$$
	asclf.b	$$⊢B={\mathrm{Base}}_W$$
Assertion	asclf	$$⊢\phi \to A:K⟶B$$

Proof

Step	Hyp	Ref	Expression
1		asclf.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclf.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclf.r	$$⊢\phi \to W\in \mathrm{Ring}$$
4		asclf.l	$$⊢\phi \to W\in \mathrm{LMod}$$
5		asclf.k	$$⊢K={\mathrm{Base}}_F$$
6		asclf.b	$$⊢B={\mathrm{Base}}_W$$
7	4	adantr	$$⊢\left(\phi \wedge x\in K\right)\to W\in \mathrm{LMod}$$
8		simpr	$$⊢\left(\phi \wedge x\in K\right)\to x\in K$$
9		eqid	$$⊢1_W=1_W$$
10	6 9	ringidcl	$$⊢W\in \mathrm{Ring}\to 1_W\in B$$
11	3 10	syl	$$⊢\phi \to 1_W\in B$$
12	11	adantr	$$⊢\left(\phi \wedge x\in K\right)\to 1_W\in B$$
13		eqid	$$⊢{\cdot }_W={\cdot }_W$$
14	6 2 13 5	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge x\in K\wedge 1_W\in B\right)\to x{\cdot }_W{1}_W\in B$$
15	7 8 12 14	syl3anc	$$⊢\left(\phi \wedge x\in K\right)\to x{\cdot }_W{1}_W\in B$$
16	1 2 5 13 9	asclfval	$$⊢A=\left(x\in K⟼x{\cdot }_W{1}_W\right)$$
17	15 16	fmptd	$$⊢\phi \to A:K⟶B$$