Theorem lcomf

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

	Ref	Expression
Hypotheses	lcomf.f	|- F = ( Scalar ` W )
	lcomf.k	|- K = ( Base ` F )
	lcomf.s	|- .x. = ( .s ` W )
	lcomf.b	|- B = ( Base ` W )
	lcomf.w	|- ( ph -> W e. LMod )
	lcomf.g	|- ( ph -> G : I --> K )
	lcomf.h	|- ( ph -> H : I --> B )
	lcomf.i	|- ( ph -> I e. V )
Assertion	lcomf	|- ( ph -> ( G oF .x. H ) : I --> B )

Proof

Step	Hyp	Ref	Expression
1		lcomf.f	|- F = ( Scalar ` W )
2		lcomf.k	|- K = ( Base ` F )
3		lcomf.s	|- .x. = ( .s ` W )
4		lcomf.b	|- B = ( Base ` W )
5		lcomf.w	|- ( ph -> W e. LMod )
6		lcomf.g	|- ( ph -> G : I --> K )
7		lcomf.h	|- ( ph -> H : I --> B )
8		lcomf.i	|- ( ph -> I e. V )
9	4 1 3 2	lmodvscl	|- ( ( W e. LMod /\ x e. K /\ y e. B ) -> ( x .x. y ) e. B )
10	9	3expb	|- ( ( W e. LMod /\ ( x e. K /\ y e. B ) ) -> ( x .x. y ) e. B )
11	5 10	sylan	|- ( ( ph /\ ( x e. K /\ y e. B ) ) -> ( x .x. y ) e. B )
12		inidm	|- ( I i^i I ) = I
13	11 6 7 8 8 12	off	|- ( ph -> ( G oF .x. H ) : I --> B )