Description: Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlhilslem.h | |- H = ( LHyp ` K ) |
|
hlhilslem.e | |- E = ( ( EDRing ` K ) ` W ) |
||
hlhilslem.u | |- U = ( ( HLHil ` K ) ` W ) |
||
hlhilslem.r | |- R = ( Scalar ` U ) |
||
hlhilslem.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
||
hlhilsplus.a | |- .+ = ( +g ` E ) |
||
Assertion | hlhilsplus | |- ( ph -> .+ = ( +g ` R ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlhilslem.h | |- H = ( LHyp ` K ) |
|
2 | hlhilslem.e | |- E = ( ( EDRing ` K ) ` W ) |
|
3 | hlhilslem.u | |- U = ( ( HLHil ` K ) ` W ) |
|
4 | hlhilslem.r | |- R = ( Scalar ` U ) |
|
5 | hlhilslem.k | |- ( ph -> ( K e. HL /\ W e. H ) ) |
|
6 | hlhilsplus.a | |- .+ = ( +g ` E ) |
|
7 | df-plusg | |- +g = Slot 2 |
|
8 | 2nn | |- 2 e. NN |
|
9 | 2lt4 | |- 2 < 4 |
|
10 | 1 2 3 4 5 7 8 9 6 | hlhilslem | |- ( ph -> .+ = ( +g ` R ) ) |