Theorem scaffn

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

	Ref	Expression
Hypotheses	scaffval.b	$$⊢B={\mathrm{Base}}_W$$
	scaffval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	scaffval.k	$$⊢K={\mathrm{Base}}_F$$
	scaffval.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
Assertion	scaffn	$$⊢\underset{\dot{}}{\bullet }Fn\left(K\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		scaffval.b	$$⊢B={\mathrm{Base}}_W$$
2		scaffval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		scaffval.k	$$⊢K={\mathrm{Base}}_F$$
4		scaffval.a	$$⊢\underset{\dot{}}{\bullet }={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
5		eqid	$$⊢{\cdot }_W={\cdot }_W$$
6	1 2 3 4 5	scaffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,y\in B⟼x{\cdot }_{W}y\right)$$
7		ovex	$$⊢x{\cdot }_{W}y\in \mathrm{V}$$
8	6 7	fnmpoi	$$⊢\underset{\dot{}}{\bullet }Fn\left(K\times B\right)$$