Metamath Proof Explorer

Theorem cphsubrg

Description: The scalar field of a subcomplex pre-Hilbert space is a subring of CCfld . (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses cphsca.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
cphsca.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
Assertion cphsubrg ( π‘Š ∈ β„‚PreHil β†’ 𝐾 ∈ ( SubRing β€˜ β„‚fld ) )

Proof

Step Hyp Ref Expression
1 cphsca.f ⊒ 𝐹 = ( Scalar β€˜ π‘Š )
2 cphsca.k ⊒ 𝐾 = ( Base β€˜ 𝐹 )
3 1 2 cphsca ⊒ ( π‘Š ∈ β„‚PreHil β†’ 𝐹 = ( β„‚fld β†Ύs 𝐾 ) )
4 cphlvec ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ LVec )
5 1 lvecdrng ⊒ ( π‘Š ∈ LVec β†’ 𝐹 ∈ DivRing )
6 4 5 syl ⊒ ( π‘Š ∈ β„‚PreHil β†’ 𝐹 ∈ DivRing )
7 2 3 6 cphsubrglem ⊒ ( π‘Š ∈ β„‚PreHil β†’ ( 𝐹 = ( β„‚fld β†Ύs 𝐾 ) ∧ 𝐾 = ( 𝐾 ∩ β„‚ ) ∧ 𝐾 ∈ ( SubRing β€˜ β„‚fld ) ) )
8 7 simp3d ⊒ ( π‘Š ∈ β„‚PreHil β†’ 𝐾 ∈ ( SubRing β€˜ β„‚fld ) )