Theorem asclfn

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

	Ref	Expression
Hypotheses	asclfn.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	asclfn.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	asclfn.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	asclfn	⊢ 𝐴 Fn 𝐾

Proof

Step	Hyp	Ref	Expression
1		asclfn.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		asclfn.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		asclfn.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
4		ovex	⊢ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) ∈ V
5		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
6		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
7	1 2 3 5 6	asclfval	⊢ 𝐴 = ( 𝑥 ∈ 𝐾 ↦ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
8	4 7	fnmpti	⊢ 𝐴 Fn 𝐾