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

Metamath Proof Explorer

Theorem ipcn

Proof