Theorem lmodscaf

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	lmodscaf	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{\bullet }:K\times B⟶B$$

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 5 3	lmodvscl	$$⊢\left(W\in \mathrm{LMod}\wedge x\in K\wedge y\in B\right)\to x{\cdot }_{W}y\in B$$
7	6	3expb	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in K\wedge y\in B\right)\right)\to x{\cdot }_{W}y\in B$$
8	7	ralrimivva	$$⊢W\in \mathrm{LMod}\to \forall x\in K\forall y\in Bx{\cdot }_{W}y\in B$$
9	1 2 3 4 5	scaffval	$$⊢\underset{\dot{}}{\bullet }=\left(x\in K,y\in B⟼x{\cdot }_{W}y\right)$$
10	9	fmpo	$$⊢\forall x\in K\forall y\in Bx{\cdot }_{W}y\in B\leftrightarrow \underset{\dot{}}{\bullet }:K\times B⟶B$$
11	8 10	sylib	$$⊢W\in \mathrm{LMod}\to \underset{\dot{}}{\bullet }:K\times B⟶B$$