Theorem scafval

Description: The scalar multiplication operation as 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)$$
	scaffval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
Assertion	scafval	$$⊢\left(X\in K\wedge Y\in B\right)\to X\underset{\dot{}}{\bullet }Y=X\underset{\dot{}}{·}Y$$

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		scaffval.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
6		oveq12	$$⊢\left(x=X\wedge y=Y\right)\to x\underset{\dot{}}{·}y=X\underset{\dot{}}{·}Y$$
7	1 2 3 4 5	scaffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,y\in B⟼x\underset{\dot{}}{·}y\right)$$
8		ovex	$$⊢X\underset{\dot{}}{·}Y\in \mathrm{V}$$
9	6 7 8	ovmpoa	$$⊢\left(X\in K\wedge Y\in B\right)\to X\underset{\dot{}}{\bullet }Y=X\underset{\dot{}}{·}Y$$