Theorem hlpr

Description: The scalar field of a subcomplex Hilbert space is either RR or CC . (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	hlress.f	|- F = ( Scalar ` W )
	hlress.k	|- K = ( Base ` F )
Assertion	hlpr	|- ( W e. CHil -> K e. { RR , CC } )

Proof

Step	Hyp	Ref	Expression
1		hlress.f	|- F = ( Scalar ` W )
2		hlress.k	|- K = ( Base ` F )
3	1 2	hlprlem	|- ( W e. CHil -> ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing /\ ( CCfld |`s K ) e. CMetSp ) )
4		eqid	|- ( CCfld |`s K ) = ( CCfld |`s K )
5	4	cncdrg	|- ( ( K e. ( SubRing ` CCfld ) /\ ( CCfld |`s K ) e. DivRing /\ ( CCfld |`s K ) e. CMetSp ) -> K e. { RR , CC } )
6	3 5	syl	|- ( W e. CHil -> K e. { RR , CC } )