hhcnf

Description: The continuous functionals of Hilbert space. (Contributed by Mario Carneiro, 19-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhcn.1	⊢ 𝐷 = ( norm_ℎ ∘ −_ℎ )
	hhcn.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	hhcn.4	⊢ 𝐾 = ( TopOpen ‘ ℂ_fld )
Assertion	hhcnf	⊢ ContFn = ( 𝐽 Cn 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		hhcn.1	⊢ 𝐷 = ( norm_ℎ ∘ −_ℎ )
2		hhcn.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3		hhcn.4	⊢ 𝐾 = ( TopOpen ‘ ℂ_fld )
4		df-rab	⊢ { 𝑡 ∈ ( ℂ ↑_m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) } = { 𝑡 ∣ ( 𝑡 ∈ ( ℂ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) }
5		df-cnfn	⊢ ContFn = { 𝑡 ∈ ( ℂ ↑_m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }
6	1	hilmetdval	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑥 𝐷 𝑤 ) = ( norm_ℎ ‘ ( 𝑥 −_ℎ 𝑤 ) ) )
7		normsub	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( norm_ℎ ‘ ( 𝑥 −_ℎ 𝑤 ) ) = ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) )
8	6 7	eqtrd	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) → ( 𝑥 𝐷 𝑤 ) = ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) )
9	8	adantll	⊢ ( ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( 𝑥 𝐷 𝑤 ) = ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) )
10	9	breq1d	⊢ ( ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑥 𝐷 𝑤 ) < 𝑧 ↔ ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 ) )
11		ffvelcdm	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) → ( 𝑡 ‘ 𝑥 ) ∈ ℂ )
12		ffvelcdm	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑤 ∈ ℋ ) → ( 𝑡 ‘ 𝑤 ) ∈ ℂ )
13	11 12	anim12dan	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑡 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑡 ‘ 𝑤 ) ∈ ℂ ) )
14		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
15	14	cnmetdval	⊢ ( ( ( 𝑡 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑡 ‘ 𝑤 ) ∈ ℂ ) → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) = ( abs ‘ ( ( 𝑡 ‘ 𝑥 ) − ( 𝑡 ‘ 𝑤 ) ) ) )
16		abssub	⊢ ( ( ( 𝑡 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑡 ‘ 𝑤 ) ∈ ℂ ) → ( abs ‘ ( ( 𝑡 ‘ 𝑥 ) − ( 𝑡 ‘ 𝑤 ) ) ) = ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) )
17	15 16	eqtrd	⊢ ( ( ( 𝑡 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑡 ‘ 𝑤 ) ∈ ℂ ) → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) = ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) )
18	13 17	syl	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ ( 𝑥 ∈ ℋ ∧ 𝑤 ∈ ℋ ) ) → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) = ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) )
19	18	anassrs	⊢ ( ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) = ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) )
20	19	breq1d	⊢ ( ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) )
21	10 20	imbi12d	⊢ ( ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ↔ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
22	21	ralbidva	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
23	22	rexbidv	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) → ( ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
24	23	ralbidv	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ 𝑥 ∈ ℋ ) → ( ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
25	24	ralbidva	⊢ ( 𝑡 : ℋ ⟶ ℂ → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
26	25	pm5.32i	⊢ ( ( 𝑡 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
27	1	hilxmet	⊢ 𝐷 ∈ ( ∞Met ‘ ℋ )
28		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
29	3	cnfldtopn	⊢ 𝐾 = ( MetOpen ‘ ( abs ∘ − ) )
30	2 29	metcn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℋ ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ) → ( 𝑡 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑡 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ) ) )
31	27 28 30	mp2an	⊢ ( 𝑡 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑡 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( 𝑥 𝐷 𝑤 ) < 𝑧 → ( ( 𝑡 ‘ 𝑥 ) ( abs ∘ − ) ( 𝑡 ‘ 𝑤 ) ) < 𝑦 ) ) )
32		cnex	⊢ ℂ ∈ V
33		ax-hilex	⊢ ℋ ∈ V
34	32 33	elmap	⊢ ( 𝑡 ∈ ( ℂ ↑_m ℋ ) ↔ 𝑡 : ℋ ⟶ ℂ )
35	34	anbi1i	⊢ ( ( 𝑡 ∈ ( ℂ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) ↔ ( 𝑡 : ℋ ⟶ ℂ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
36	26 31 35	3bitr4i	⊢ ( 𝑡 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝑡 ∈ ( ℂ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
37	36	eqabi	⊢ ( 𝐽 Cn 𝐾 ) = { 𝑡 ∣ ( 𝑡 ∈ ( ℂ ↑_m ℋ ) ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ ℋ ( ( norm_ℎ ‘ ( 𝑤 −_ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) ) }
38	4 5 37	3eqtr4i	⊢ ContFn = ( 𝐽 Cn 𝐾 )

Metamath Proof Explorer

Theorem hhcnf

Proof