Theorem hlprlem

Description: Lemma for hlpr . (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	hlress.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	hlress.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	hlprlem	⊢ ( 𝑊 ∈ ℂHil → ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐾 ) ∈ DivRing ∧ ( ℂfld ↾s 𝐾 ) ∈ CMetSp ) )

Proof

Step	Hyp	Ref	Expression
1		hlress.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		hlress.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3		hlcph	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil )
4	1 2	cphsubrg	⊢ ( 𝑊 ∈ ℂPreHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
5	3 4	syl	⊢ ( 𝑊 ∈ ℂHil → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
6	1 2	cphsca	⊢ ( 𝑊 ∈ ℂPreHil → 𝐹 = ( ℂfld ↾s 𝐾 ) )
7	3 6	syl	⊢ ( 𝑊 ∈ ℂHil → 𝐹 = ( ℂfld ↾s 𝐾 ) )
8		cphlvec	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LVec )
9	1	lvecdrng	⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
10	3 8 9	3syl	⊢ ( 𝑊 ∈ ℂHil → 𝐹 ∈ DivRing )
11	7 10	eqeltrrd	⊢ ( 𝑊 ∈ ℂHil → ( ℂfld ↾s 𝐾 ) ∈ DivRing )
12		hlbn	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ Ban )
13	1	bnsca	⊢ ( 𝑊 ∈ Ban → 𝐹 ∈ CMetSp )
14	12 13	syl	⊢ ( 𝑊 ∈ ℂHil → 𝐹 ∈ CMetSp )
15	7 14	eqeltrrd	⊢ ( 𝑊 ∈ ℂHil → ( ℂfld ↾s 𝐾 ) ∈ CMetSp )
16	5 11 15	3jca	⊢ ( 𝑊 ∈ ℂHil → ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s 𝐾 ) ∈ DivRing ∧ ( ℂfld ↾s 𝐾 ) ∈ CMetSp ) )