Theorem lcomf

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

	Ref	Expression
Hypotheses	lcomf.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lcomf.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lcomf.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lcomf.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	lcomf.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lcomf.g	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐾 )
	lcomf.h	⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ 𝐵 )
	lcomf.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
Assertion	lcomf	⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐻 ) : 𝐼 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lcomf.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		lcomf.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		lcomf.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		lcomf.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
5		lcomf.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
6		lcomf.g	⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐾 )
7		lcomf.h	⊢ ( 𝜑 → 𝐻 : 𝐼 ⟶ 𝐵 )
8		lcomf.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9	4 1 3 2	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
10	9	3expb	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
11	5 10	sylan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
12		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
13	11 6 7 8 8 12	off	⊢ ( 𝜑 → ( 𝐺 ∘f · 𝐻 ) : 𝐼 ⟶ 𝐵 )