Metamath Proof Explorer

Theorem cphqss

Description: The scalar field of a subcomplex pre-Hilbert space contains the rational numbers. (Contributed by Mario Carneiro, 15-Oct-2015)

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

Proof

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