Theorem lcomf

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

	Ref	Expression
Hypotheses	lcomf.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	lcomf.k	$$⊢K={\mathrm{Base}}_F$$
	lcomf.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	lcomf.b	$$⊢B={\mathrm{Base}}_W$$
	lcomf.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lcomf.g	$$⊢\phi \to G:I⟶K$$
	lcomf.h	$$⊢\phi \to H:I⟶B$$
	lcomf.i	$$⊢\phi \to I\in V$$
Assertion	lcomf	$$⊢\phi \to \left(G{\underset{\dot{}}{·}}_{f}H\right):I⟶B$$

Proof

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