Metamath Proof Explorer

Theorem phlsrng

Description: The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypothesis phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
Assertion phlsrng ${⊢}{W}\in \mathrm{PreHil}\to {F}\in \mathrm{*-Ring}$

Proof

Step Hyp Ref Expression
1 phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
3 eqid ${⊢}{\cdot }_{𝑖}\left({W}\right)={\cdot }_{𝑖}\left({W}\right)$
4 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
5 eqid ${⊢}{*}_{{F}}={*}_{{F}}$
6 eqid ${⊢}{0}_{{F}}={0}_{{F}}$
7 2 1 3 4 5 6 isphl ${⊢}{W}\in \mathrm{PreHil}↔\left({W}\in \mathrm{LVec}\wedge {F}\in \mathrm{*-Ring}\wedge \forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {\mathrm{Base}}_{{W}}⟼{y}{\cdot }_{𝑖}\left({W}\right){x}\right)\in \left({W}\mathrm{LMHom}\mathrm{ringLMod}\left({F}\right)\right)\wedge \left({x}{\cdot }_{𝑖}\left({W}\right){x}={0}_{{F}}\to {x}={0}_{{W}}\right)\wedge \forall {y}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}{\left({x}{\cdot }_{𝑖}\left({W}\right){y}\right)}^{{*}_{{F}}}={y}{\cdot }_{𝑖}\left({W}\right){x}\right)\right)$
8 7 simp2bi ${⊢}{W}\in \mathrm{PreHil}\to {F}\in \mathrm{*-Ring}$