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 F=ScalarW
lcomf.k K=BaseF
lcomf.s ·˙=W
lcomf.b B=BaseW
lcomf.w φWLMod
lcomf.g φG:IK
lcomf.h φH:IB
lcomf.i φIV
Assertion lcomf φG·˙fH:IB

Proof

Step Hyp Ref Expression
1 lcomf.f F=ScalarW
2 lcomf.k K=BaseF
3 lcomf.s ·˙=W
4 lcomf.b B=BaseW
5 lcomf.w φWLMod
6 lcomf.g φG:IK
7 lcomf.h φH:IB
8 lcomf.i φIV
9 4 1 3 2 lmodvscl WLModxKyBx·˙yB
10 9 3expb WLModxKyBx·˙yB
11 5 10 sylan φxKyBx·˙yB
12 inidm II=I
13 11 6 7 8 8 12 off φG·˙fH:IB