Description: Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlhilslem.h | ||
hlhilslem.e | |||
hlhilslem.u | |||
hlhilslem.r | |||
hlhilslem.k | |||
hlhilsmul.m | |||
Assertion | hlhilsmul |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlhilslem.h | ||
2 | hlhilslem.e | ||
3 | hlhilslem.u | ||
4 | hlhilslem.r | ||
5 | hlhilslem.k | ||
6 | hlhilsmul.m | ||
7 | df-mulr | ||
8 | 3nn | ||
9 | 3lt4 | ||
10 | 1 2 3 4 5 7 8 9 6 | hlhilslem |