# Metamath Proof Explorer

## Theorem hlhils1N

Description: The scalar ring unity for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hlhilsbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hlhilsbase.l ${⊢}{L}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hlhilsbase.s ${⊢}{S}=\mathrm{Scalar}\left({L}\right)$
hlhilsbase.u ${⊢}{U}=\mathrm{HLHil}\left({K}\right)\left({W}\right)$
hlhilsbase.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hlhilsbase.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hlhils1.t
Assertion hlhils1N

### Proof

Step Hyp Ref Expression
1 hlhilsbase.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hlhilsbase.l ${⊢}{L}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hlhilsbase.s ${⊢}{S}=\mathrm{Scalar}\left({L}\right)$
4 hlhilsbase.u ${⊢}{U}=\mathrm{HLHil}\left({K}\right)\left({W}\right)$
5 hlhilsbase.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
6 hlhilsbase.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 hlhils1.t
8 eqidd ${⊢}{\phi }\to {\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
9 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
10 1 2 3 4 5 6 9 hlhilsbase2 ${⊢}{\phi }\to {\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{R}}$
11 eqid ${⊢}{\cdot }_{{S}}={\cdot }_{{S}}$
12 1 2 3 4 5 6 11 hlhilsmul2 ${⊢}{\phi }\to {\cdot }_{{S}}={\cdot }_{{R}}$
13 12 oveqdr ${⊢}\left({\phi }\wedge \left({x}\in {\mathrm{Base}}_{{S}}\wedge {y}\in {\mathrm{Base}}_{{S}}\right)\right)\to {x}{\cdot }_{{S}}{y}={x}{\cdot }_{{R}}{y}$
14 8 10 13 rngidpropd ${⊢}{\phi }\to {1}_{{S}}={1}_{{R}}$
15 7 14 syl5eq