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 e. CPreHil -> QQ C_ K )

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	|- F = ( Scalar ` W )
2		cphsca.k	|- K = ( Base ` F )
3	1 2	cphsubrg	|- ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )
4	1 2	cphsca	|- ( W e. CPreHil -> F = ( CCfld |`s K ) )
5		cphlvec	|- ( W e. CPreHil -> W e. LVec )
6	1	lvecdrng	|- ( W e. LVec -> F e. DivRing )
7	5 6	syl	|- ( W e. CPreHil -> F e. DivRing )
8	4 7	eqeltrrd	|- ( W e. CPreHil -> ( CCfld |`s K ) e. DivRing )
9		qsssubdrg	|- ( ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing ) -> QQ C_ K )
10	3 8 9	syl2anc	|- ( W e. CPreHil -> QQ C_ K )