Theorem asclfn

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

	Ref	Expression
Hypotheses	asclfn.a	|- A = ( algSc ` W )
	asclfn.f	|- F = ( Scalar ` W )
	asclfn.k	|- K = ( Base ` F )
Assertion	asclfn	|- A Fn K

Proof

Step	Hyp	Ref	Expression
1		asclfn.a	|- A = ( algSc ` W )
2		asclfn.f	|- F = ( Scalar ` W )
3		asclfn.k	|- K = ( Base ` F )
4		ovex	|- ( x ( .s ` W ) ( 1r ` W ) ) e. _V
5		eqid	|- ( .s ` W ) = ( .s ` W )
6		eqid	|- ( 1r ` W ) = ( 1r ` W )
7	1 2 3 5 6	asclfval	|- A = ( x e. K |-> ( x ( .s ` W ) ( 1r ` W ) ) )
8	4 7	fnmpti	|- A Fn K