Metamath Proof Explorer


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 } )