Description: A linear-combination sum is a function. (Contributed by Stefan O'Rear, 28-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lcomf.f | |
|
lcomf.k | |
||
lcomf.s | |
||
lcomf.b | |
||
lcomf.w | |
||
lcomf.g | |
||
lcomf.h | |
||
lcomf.i | |
||
Assertion | lcomf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcomf.f | |
|
2 | lcomf.k | |
|
3 | lcomf.s | |
|
4 | lcomf.b | |
|
5 | lcomf.w | |
|
6 | lcomf.g | |
|
7 | lcomf.h | |
|
8 | lcomf.i | |
|
9 | 4 1 3 2 | lmodvscl | |
10 | 9 | 3expb | |
11 | 5 10 | sylan | |
12 | inidm | |
|
13 | 11 6 7 8 8 12 | off | |