Theorem asclfn

Description: Unconditional functionality of the algebra scalar lifting function. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	asclfn.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclfn.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclfn.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	asclfn	$$⊢AFnK$$

Proof

Step	Hyp	Ref	Expression
1		asclfn.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclfn.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclfn.k	$$⊢K={\mathrm{Base}}_F$$
4		ovex	$$⊢x{\cdot }_W{1}_W\in \mathrm{V}$$
5		eqid	$$⊢{\cdot }_W={\cdot }_W$$
6		eqid	$$⊢1_W=1_W$$
7	1 2 3 5 6	asclfval	$$⊢A=\left(x\in K⟼x{\cdot }_W{1}_W\right)$$
8	4 7	fnmpti	$$⊢AFnK$$