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 ⊢ F = Scalar ⁡ W
cphsca.k ⊢ K = Base F
Assertion cphqss ⊢ W ∈ CPreHil → ℚ ⊆ K

Proof

Step Hyp Ref Expression
1 cphsca.f ⊢ F = Scalar ⁡ W
2 cphsca.k ⊢ K = Base F
3 1 2 cphsubrg ⊢ W ∈ CPreHil → K ∈ SubRing ⁡ ℂ fld
4 1 2 cphsca ⊢ W ∈ CPreHil → F = ℂ fld ↾ 𝑠 K
5 cphlvec ⊢ W ∈ CPreHil → W ∈ LVec
6 1 lvecdrng ⊢ W ∈ LVec → F ∈ DivRing
7 5 6 syl ⊢ W ∈ CPreHil → F ∈ DivRing
8 4 7 eqeltrrd ⊢ W ∈ CPreHil → ℂ fld ↾ 𝑠 K ∈ DivRing
9 qsssubdrg ⊢ K ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 K ∈ DivRing → ℚ ⊆ K
10 3 8 9 syl2anc ⊢ W ∈ CPreHil → ℚ ⊆ K