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 → ℚ ⊆ 𝐾 )