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=\mathrm{Scalar}\left(W\right)$$
	cphsca.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	cphqss	$$⊢W\in \mathrm{CPreHil}\to \mathbb{Q}\subseteq K$$

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		cphsca.k	$$⊢K={\mathrm{Base}}_F$$
3	1 2	cphsubrg	$$⊢W\in \mathrm{CPreHil}\to K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
4	1 2	cphsca	$$⊢W\in \mathrm{CPreHil}\to F={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K$$
5		cphlvec	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{LVec}$$
6	1	lvecdrng	$$⊢W\in \mathrm{LVec}\to F\in \mathrm{DivRing}$$
7	5 6	syl	$$⊢W\in \mathrm{CPreHil}\to F\in \mathrm{DivRing}$$
8	4 7	eqeltrrd	$$⊢W\in \mathrm{CPreHil}\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\in \mathrm{DivRing}$$
9		qsssubdrg	$$⊢\left(K\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}K\in \mathrm{DivRing}\right)\to \mathbb{Q}\subseteq K$$
10	3 8 9	syl2anc	$$⊢W\in \mathrm{CPreHil}\to \mathbb{Q}\subseteq K$$