Theorem cphsubrg

Description: The scalar field of a subcomplex pre-Hilbert space is a subring of CCfld . (Contributed by Mario Carneiro, 8-Oct-2015)

	Ref	Expression
Hypotheses	cphsca.f	|- F = ( Scalar ` W )
	cphsca.k	|- K = ( Base ` F )
Assertion	cphsubrg	|- ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )

Proof

Step	Hyp	Ref	Expression
1		cphsca.f	|- F = ( Scalar ` W )
2		cphsca.k	|- K = ( Base ` F )
3	1 2	cphsca	|- ( W e. CPreHil -> F = ( CCfld |`s K ) )
4		cphlvec	|- ( W e. CPreHil -> W e. LVec )
5	1	lvecdrng	|- ( W e. LVec -> F e. DivRing )
6	4 5	syl	|- ( W e. CPreHil -> F e. DivRing )
7	2 3 6	cphsubrglem	|- ( W e. CPreHil -> ( F = ( CCfld |`s K ) /\ K = ( K i^i CC ) /\ K e. ( SubRing ` CCfld ) ) )
8	7	simp3d	|- ( W e. CPreHil -> K e. ( SubRing ` CCfld ) )