This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 · 𝐻 ) : 𝐼 ⟶ 𝐵 )