Metamath Proof Explorer

Theorem ishl2

Description: A Hilbert space is a complete subcomplex pre-Hilbert space over RR or CC . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses hlress.f ⊢ F = Scalar ⁡ W
hlress.k ⊢ K = Base F
Assertion ishl2 ⊢ W ∈ ℂHil ↔ W ∈ CMetSp ∧ W ∈ CPreHil ∧ K ∈ ℝ ℂ

Proof

Step Hyp Ref Expression
1 hlress.f ⊢ F = Scalar ⁡ W
2 hlress.k ⊢ K = Base F
3 ishl ⊢ W ∈ ℂHil ↔ W ∈ Ban ∧ W ∈ CPreHil
4 df-3an ⊢ W ∈ CMetSp ∧ K ∈ ℝ ℂ ∧ W ∈ CPreHil ↔ W ∈ CMetSp ∧ K ∈ ℝ ℂ ∧ W ∈ CPreHil
5 3ancomb ⊢ W ∈ CMetSp ∧ W ∈ CPreHil ∧ K ∈ ℝ ℂ ↔ W ∈ CMetSp ∧ K ∈ ℝ ℂ ∧ W ∈ CPreHil
6 cphnvc ⊢ W ∈ CPreHil → W ∈ NrmVec
7 1 isbn ⊢ W ∈ Ban ↔ W ∈ NrmVec ∧ W ∈ CMetSp ∧ F ∈ CMetSp
8 3anass ⊢ W ∈ NrmVec ∧ W ∈ CMetSp ∧ F ∈ CMetSp ↔ W ∈ NrmVec ∧ W ∈ CMetSp ∧ F ∈ CMetSp
9 7 8 bitri ⊢ W ∈ Ban ↔ W ∈ NrmVec ∧ W ∈ CMetSp ∧ F ∈ CMetSp
10 9 baib ⊢ W ∈ NrmVec → W ∈ Ban ↔ W ∈ CMetSp ∧ F ∈ CMetSp
11 6 10 syl ⊢ W ∈ CPreHil → W ∈ Ban ↔ W ∈ CMetSp ∧ F ∈ CMetSp
12 1 2 cphsca ⊢ W ∈ CPreHil → F = ℂ fld ↾ 𝑠 K
13 12 eleq1d ⊢ W ∈ CPreHil → F ∈ CMetSp ↔ ℂ fld ↾ 𝑠 K ∈ CMetSp
14 1 2 cphsubrg ⊢ W ∈ CPreHil → K ∈ SubRing ⁡ ℂ fld
15 cphlvec ⊢ W ∈ CPreHil → W ∈ LVec
16 1 lvecdrng ⊢ W ∈ LVec → F ∈ DivRing
17 15 16 syl ⊢ W ∈ CPreHil → F ∈ DivRing
18 12 17 eqeltrrd ⊢ W ∈ CPreHil → ℂ fld ↾ 𝑠 K ∈ DivRing
19 eqid ⊢ ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 K
20 19 cncdrg ⊢ K ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 K ∈ DivRing ∧ ℂ fld ↾ 𝑠 K ∈ CMetSp → K ∈ ℝ ℂ
21 20 3expia ⊢ K ∈ SubRing ⁡ ℂ fld ∧ ℂ fld ↾ 𝑠 K ∈ DivRing → ℂ fld ↾ 𝑠 K ∈ CMetSp → K ∈ ℝ ℂ
22 14 18 21 syl2anc ⊢ W ∈ CPreHil → ℂ fld ↾ 𝑠 K ∈ CMetSp → K ∈ ℝ ℂ
23 elpri ⊢ K ∈ ℝ ℂ → K = ℝ ∨ K = ℂ
24 oveq2 ⊢ K = ℝ → ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 ℝ
25 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
26 25 recld2 ⊢ ℝ ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
27 cncms ⊢ ℂ fld ∈ CMetSp
28 ax-resscn ⊢ ℝ ⊆ ℂ
29 eqid ⊢ ℂ fld ↾ 𝑠 ℝ = ℂ fld ↾ 𝑠 ℝ
30 cnfldbas ⊢ ℂ = Base ℂ fld
31 29 30 25 cmsss ⊢ ℂ fld ∈ CMetSp ∧ ℝ ⊆ ℂ → ℂ fld ↾ 𝑠 ℝ ∈ CMetSp ↔ ℝ ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
32 27 28 31 mp2an ⊢ ℂ fld ↾ 𝑠 ℝ ∈ CMetSp ↔ ℝ ∈ Clsd ⁡ TopOpen ⁡ ℂ fld
33 26 32 mpbir ⊢ ℂ fld ↾ 𝑠 ℝ ∈ CMetSp
34 24 33 eqeltrdi ⊢ K = ℝ → ℂ fld ↾ 𝑠 K ∈ CMetSp
35 oveq2 ⊢ K = ℂ → ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 ℂ
36 30 ressid ⊢ ℂ fld ∈ CMetSp → ℂ fld ↾ 𝑠 ℂ = ℂ fld
37 27 36 ax-mp ⊢ ℂ fld ↾ 𝑠 ℂ = ℂ fld
38 37 27 eqeltri ⊢ ℂ fld ↾ 𝑠 ℂ ∈ CMetSp
39 35 38 eqeltrdi ⊢ K = ℂ → ℂ fld ↾ 𝑠 K ∈ CMetSp
40 34 39 jaoi ⊢ K = ℝ ∨ K = ℂ → ℂ fld ↾ 𝑠 K ∈ CMetSp
41 23 40 syl ⊢ K ∈ ℝ ℂ → ℂ fld ↾ 𝑠 K ∈ CMetSp
42 22 41 impbid1 ⊢ W ∈ CPreHil → ℂ fld ↾ 𝑠 K ∈ CMetSp ↔ K ∈ ℝ ℂ
43 13 42 bitrd ⊢ W ∈ CPreHil → F ∈ CMetSp ↔ K ∈ ℝ ℂ
44 43 anbi2d ⊢ W ∈ CPreHil → W ∈ CMetSp ∧ F ∈ CMetSp ↔ W ∈ CMetSp ∧ K ∈ ℝ ℂ
45 11 44 bitrd ⊢ W ∈ CPreHil → W ∈ Ban ↔ W ∈ CMetSp ∧ K ∈ ℝ ℂ
46 45 pm5.32ri ⊢ W ∈ Ban ∧ W ∈ CPreHil ↔ W ∈ CMetSp ∧ K ∈ ℝ ℂ ∧ W ∈ CPreHil
47 4 5 46 3bitr4ri ⊢ W ∈ Ban ∧ W ∈ CPreHil ↔ W ∈ CMetSp ∧ W ∈ CPreHil ∧ K ∈ ℝ ℂ
48 3 47 bitri ⊢ W ∈ ℂHil ↔ W ∈ CMetSp ∧ W ∈ CPreHil ∧ K ∈ ℝ ℂ