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

Metamath Proof Explorer

Theorem ipcn

Description: The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ipcn.f ⊢ , = ( ·if ‘ 𝑊 )
ipcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
ipcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
Assertion ipcn ( 𝑊 ∈ ℂPreHil → , ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 ipcn.f ⊢ , = ( ·if ‘ 𝑊 )
2 ipcn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3 ipcn.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
4 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
8 5 1 6 7 phlipf ⊢ ( 𝑊 ∈ PreHil → , : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
9 4 8 syl ⊢ ( 𝑊 ∈ ℂPreHil → , : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
10 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
11 6 7 clmsscn ⊢ ( 𝑊 ∈ ℂMod → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ℂ )
12 10 11 syl ⊢ ( 𝑊 ∈ ℂPreHil → ( Base ‘ ( Scalar ‘ 𝑊 ) ) ⊆ ℂ )
13 9 12 fssd ⊢ ( 𝑊 ∈ ℂPreHil → , : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ℂ )
14 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
15 eqid ⊢ ( dist ‘ 𝑊 ) = ( dist ‘ 𝑊 )
16 eqid ⊢ ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
17 eqid ⊢ ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑥 ) + 1 ) ) = ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑥 ) + 1 ) )
18 eqid ⊢ ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) + ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑥 ) + 1 ) ) ) ) = ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑦 ) + ( ( 𝑟 / 2 ) / ( ( ( norm ‘ 𝑊 ) ‘ 𝑥 ) + 1 ) ) ) )
19 simpll ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑊 ∈ ℂPreHil )
20 simplrl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
21 simplrr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
22 simpr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
23 5 14 15 16 17 18 19 20 21 22 ipcnlem1 ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) < 𝑟 ) )
24 23 ralrimiva ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) < 𝑟 ) )
25 simplrl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑊 ) )
26 simprl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
27 25 26 ovresd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) = ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) )
28 27 breq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ↔ ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ) )
29 simplrr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
30 simprr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → 𝑤 ∈ ( Base ‘ 𝑊 ) )
31 29 30 ovresd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) = ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) )
32 31 breq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ↔ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) )
33 28 32 anbi12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) ↔ ( ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) ) )
34 13 ad2antrr ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → , : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ℂ )
35 34 25 29 fovcdmd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 , 𝑦 ) ∈ ℂ )
36 34 26 30 fovcdmd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑧 , 𝑤 ) ∈ ℂ )
37 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
38 37 cnmetdval ⊢ ( ( ( 𝑥 , 𝑦 ) ∈ ℂ ∧ ( 𝑧 , 𝑤 ) ∈ ℂ ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) = ( abs ‘ ( ( 𝑥 , 𝑦 ) − ( 𝑧 , 𝑤 ) ) ) )
39 35 36 38 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) = ( abs ‘ ( ( 𝑥 , 𝑦 ) − ( 𝑧 , 𝑤 ) ) ) )
40 5 14 1 ipfval ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 , 𝑦 ) = ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) )
41 25 29 40 syl2anc ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑥 , 𝑦 ) = ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) )
42 5 14 1 ipfval ⊢ ( ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑧 , 𝑤 ) = ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) )
43 42 adantl ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( 𝑧 , 𝑤 ) = ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) )
44 41 43 oveq12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 , 𝑦 ) − ( 𝑧 , 𝑤 ) ) = ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) )
45 44 fveq2d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( abs ‘ ( ( 𝑥 , 𝑦 ) − ( 𝑧 , 𝑤 ) ) ) = ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) )
46 39 45 eqtrd ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) = ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) )
47 46 breq1d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ↔ ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) < 𝑟 ) )
48 33 47 imbi12d ⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) ∧ ( 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ 𝑤 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) ↔ ( ( ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) < 𝑟 ) ) )
49 48 2ralbidva ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) < 𝑟 ) ) )
50 49 rexbidv ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) ↔ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) < 𝑟 ) ) )
51 50 ralbidv ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( dist ‘ 𝑊 ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( dist ‘ 𝑊 ) 𝑤 ) < 𝑠 ) → ( abs ‘ ( ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑦 ) − ( 𝑧 ( ·𝑖 ‘ 𝑊 ) 𝑤 ) ) ) < 𝑟 ) ) )
52 24 51 mpbird ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) )
53 52 ralrimivva ⊢ ( 𝑊 ∈ ℂPreHil → ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) )
54 cphngp ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ NrmGrp )
55 ngpms ⊢ ( 𝑊 ∈ NrmGrp → 𝑊 ∈ MetSp )
56 54 55 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ MetSp )
57 msxms ⊢ ( 𝑊 ∈ MetSp → 𝑊 ∈ ∞MetSp )
58 56 57 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ∞MetSp )
59 eqid ⊢ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) = ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) )
60 5 59 xmsxmet ⊢ ( 𝑊 ∈ ∞MetSp → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) )
61 58 60 syl ⊢ ( 𝑊 ∈ ℂPreHil → ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) )
62 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
63 62 a1i ⊢ ( 𝑊 ∈ ℂPreHil → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
64 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) )
65 3 cnfldtopn ⊢ 𝐾 = ( MetOpen ‘ ( abs ∘ − ) )
66 64 64 65 txmetcn ⊢ ( ( ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) ∧ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝑊 ) ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) → ( , ∈ ( ( ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn 𝐾 ) ↔ ( , : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) ) ) )
67 61 61 63 66 syl3anc ⊢ ( 𝑊 ∈ ℂPreHil → ( , ∈ ( ( ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn 𝐾 ) ↔ ( , : ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ⟶ ℂ ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑊 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑧 ∈ ( Base ‘ 𝑊 ) ∀ 𝑤 ∈ ( Base ‘ 𝑊 ) ( ( ( 𝑥 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑧 ) < 𝑠 ∧ ( 𝑦 ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) 𝑤 ) < 𝑠 ) → ( ( 𝑥 , 𝑦 ) ( abs ∘ − ) ( 𝑧 , 𝑤 ) ) < 𝑟 ) ) ) )
68 13 53 67 mpbir2and ⊢ ( 𝑊 ∈ ℂPreHil → , ∈ ( ( ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn 𝐾 ) )
69 2 5 59 mstopn ⊢ ( 𝑊 ∈ MetSp → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) )
70 56 69 syl ⊢ ( 𝑊 ∈ ℂPreHil → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) )
71 70 70 oveq12d ⊢ ( 𝑊 ∈ ℂPreHil → ( 𝐽 ×t 𝐽 ) = ( ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) )
72 71 oveq1d ⊢ ( 𝑊 ∈ ℂPreHil → ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) = ( ( ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ×t ( MetOpen ‘ ( ( dist ‘ 𝑊 ) ↾ ( ( Base ‘ 𝑊 ) × ( Base ‘ 𝑊 ) ) ) ) ) Cn 𝐾 ) )
73 68 72 eleqtrrd ⊢ ( 𝑊 ∈ ℂPreHil → , ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐾 ) )