lmodscaf

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

	Ref	Expression
Hypotheses	scaffval.b	$⊢ B = {Base}_{W}$
	scaffval.f	$⊢ F = Scalar (W)$
	scaffval.k	$⊢ K = {Base}_{F}$
	scaffval.a	$⊢ \underset{˙}{∙} = \cdot_{𝑠𝑓} (W)$
Assertion	lmodscaf	$⊢ W \in LMod \to \underset{˙}{∙} : K \times B ⟶ B$

Step	Hyp	Ref	Expression
1		scaffval.b	$⊢ B = {Base}_{W}$
2		scaffval.f	$⊢ F = Scalar (W)$
3		scaffval.k	$⊢ K = {Base}_{F}$
4		scaffval.a	$⊢ \underset{˙}{∙} = \cdot_{𝑠𝑓} (W)$
5		eqid	$⊢ \cdot_{W} = \cdot_{W}$
6	1 2 5 3	lmodvscl	$⊢ (W \in LMod \land x \in K \land y \in B) \to x \cdot_{W} y \in B$
7	6	3expb	$⊢ (W \in LMod \land (x \in K \land y \in B)) \to x \cdot_{W} y \in B$
8	7	ralrimivva	$⊢ W \in LMod \to \forall x \in K \forall y \in B x \cdot_{W} y \in B$
9	1 2 3 4 5	scaffval	$⊢ \underset{˙}{∙} = (x \in K, y \in B ⟼ x \cdot_{W} y)$
10	9	fmpo	$⊢ \forall x \in K \forall y \in B x \cdot_{W} y \in B \leftrightarrow \underset{˙}{∙} : K \times B ⟶ B$
11	8 10	sylib	$⊢ W \in LMod \to \underset{˙}{∙} : K \times B ⟶ B$

Metamath Proof Explorer