lcomf

Description: A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015)

Step	Hyp	Ref	Expression
1		lcomf.f	$⊢ F = Scalar (W)$
2		lcomf.k	$⊢ K = {Base}_{F}$
3		lcomf.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lcomf.b	$⊢ B = {Base}_{W}$
5		lcomf.w	$⊢ φ \to W \in LMod$
6		lcomf.g	$⊢ φ \to G : I ⟶ K$
7		lcomf.h	$⊢ φ \to H : I ⟶ B$
8		lcomf.i	$⊢ φ \to I \in V$
9	4 1 3 2	lmodvscl	$⊢ (W \in LMod \land x \in K \land y \in B) \to x \underset{˙}{\cdot} y \in B$
10	9	3expb	$⊢ (W \in LMod \land (x \in K \land y \in B)) \to x \underset{˙}{\cdot} y \in B$
11	5 10	sylan	$⊢ (φ \land (x \in K \land y \in B)) \to x \underset{˙}{\cdot} y \in B$
12		inidm	$⊢ I \cap I = I$
13	11 6 7 8 8 12	off	$⊢ φ \to (G {\underset{˙}{\cdot}}_{f} H) : I ⟶ B$

Metamath Proof Explorer