Theorem scaffn

Description: The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	scaffval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	scaffval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	scaffval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	scaffval.a	⊢ ∙ = ( ·sf ‘ 𝑊 )
Assertion	scaffn	⊢ ∙ Fn ( 𝐾 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		scaffval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		scaffval.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		scaffval.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
4		scaffval.a	⊢ ∙ = ( ·sf ‘ 𝑊 )
5		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
6	1 2 3 4 5	scaffval	⊢ ∙ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) )
7		ovex	⊢ ( 𝑥 ( ·𝑠 ‘ 𝑊 ) 𝑦 ) ∈ V
8	6 7	fnmpoi	⊢ ∙ Fn ( 𝐾 × 𝐵 )