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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	hlress.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	hlpr	⊢ ( 𝑊 ∈ ℂHil → 𝐾 ∈ { ℝ , ℂ } )

Proof

Step	Hyp	Ref	Expression
1		hlress.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		hlress.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	hlprlem	⊢ ( 𝑊 ∈ ℂHil → ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐾 ) ∈ DivRing ∧ ( ℂfld ↾s 𝐾 ) ∈ CMetSp ) )
4		eqid	⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
5	4	cncdrg	⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐾 ) ∈ DivRing ∧ ( ℂfld ↾s 𝐾 ) ∈ CMetSp ) → 𝐾 ∈ { ℝ , ℂ } )
6	3 5	syl	⊢ ( 𝑊 ∈ ℂHil → 𝐾 ∈ { ℝ , ℂ } )