This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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