# Metamath Proof Explorer

## Theorem hlhilsplus

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}=\mathrm{LHyp}\left({K}\right)$
hlhilslem.e ${⊢}{E}=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
hlhilslem.u ${⊢}{U}=\mathrm{HLHil}\left({K}\right)\left({W}\right)$
hlhilslem.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hlhilslem.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hlhilsplus.a
Assertion hlhilsplus

### Proof

Step Hyp Ref Expression
1 hlhilslem.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hlhilslem.e ${⊢}{E}=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
3 hlhilslem.u ${⊢}{U}=\mathrm{HLHil}\left({K}\right)\left({W}\right)$
4 hlhilslem.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
5 hlhilslem.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
6 hlhilsplus.a
7 df-plusg ${⊢}{+}_{𝑔}=\mathrm{Slot}2$
8 2nn ${⊢}2\in ℕ$
9 2lt4 ${⊢}2<4$
10 1 2 3 4 5 7 8 9 6 hlhilslem