Metamath Proof Explorer

Theorem hlprlem

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

Ref Expression
Hypotheses hlress.f ⊢ F = Scalar ⁡ W
hlress.k ⊢ K = Base F
Assertion hlprlem ⊢ W ∈ ℂHil → K ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 K ∈ DivRing ∧ ℂ fld ↾ 𝑠 K ∈ CMetSp

Proof

Step Hyp Ref Expression
1 hlress.f ⊢ F = Scalar ⁡ W
2 hlress.k ⊢ K = Base F
3 hlcph ⊢ W ∈ ℂHil → W ∈ CPreHil
4 1 2 cphsubrg ⊢ W ∈ CPreHil → K ∈ SubRing ⁡ ℂ fld
5 3 4 syl ⊢ W ∈ ℂHil → K ∈ SubRing ⁡ ℂ fld
6 1 2 cphsca ⊢ W ∈ CPreHil → F = ℂ fld ↾ 𝑠 K
7 3 6 syl ⊢ W ∈ ℂHil → F = ℂ fld ↾ 𝑠 K
8 cphlvec ⊢ W ∈ CPreHil → W ∈ LVec
9 1 lvecdrng ⊢ W ∈ LVec → F ∈ DivRing
10 3 8 9 3syl ⊢ W ∈ ℂHil → F ∈ DivRing
11 7 10 eqeltrrd ⊢ W ∈ ℂHil → ℂ fld ↾ 𝑠 K ∈ DivRing
12 hlbn ⊢ W ∈ ℂHil → W ∈ Ban
13 1 bnsca ⊢ W ∈ Ban → F ∈ CMetSp
14 12 13 syl ⊢ W ∈ ℂHil → F ∈ CMetSp
15 7 14 eqeltrrd ⊢ W ∈ ℂHil → ℂ fld ↾ 𝑠 K ∈ CMetSp
16 5 11 15 3jca ⊢ W ∈ ℂHil → K ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 K ∈ DivRing ∧ ℂ fld ↾ 𝑠 K ∈ CMetSp