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

Proof

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