Definition df-cnfn

Description: Define the set of continuous functionals on Hilbert space. For every "epsilon" ( y ) there is a "delta" ( z ) such that... (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-cnfn	⊢ ContFn = { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnfn	⊢ ContFn
1		vt	⊢ 𝑡
2		cc	⊢ ℂ
3		cmap	⊢ ↑m
4		chba	⊢ ℋ
5	2 4 3	co	⊢ ( ℂ ↑m ℋ )
6		vx	⊢ 𝑥
7		vy	⊢ 𝑦
8		crp	⊢ ℝ+
9		vz	⊢ 𝑧
10		vw	⊢ 𝑤
11		cno	⊢ normℎ
12	10	cv	⊢ 𝑤
13		cmv	⊢ −ℎ
14	6	cv	⊢ 𝑥
15	12 14 13	co	⊢ ( 𝑤 −ℎ 𝑥 )
16	15 11	cfv	⊢ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) )
17		clt	⊢ <
18	9	cv	⊢ 𝑧
19	16 18 17	wbr	⊢ ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧
20		cabs	⊢ abs
21	1	cv	⊢ 𝑡
22	12 21	cfv	⊢ ( 𝑡 ‘ 𝑤 )
23		cmin	⊢ −
24	14 21	cfv	⊢ ( 𝑡 ‘ 𝑥 )
25	22 24 23	co	⊢ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) )
26	25 20	cfv	⊢ ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) )
27	7	cv	⊢ 𝑦
28	26 27 17	wbr	⊢ ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦
29	19 28	wi	⊢ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
30	29 10 4	wral	⊢ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
31	30 9 8	wrex	⊢ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
32	31 7 8	wral	⊢ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
33	32 6 4	wral	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 )
34	33 1 5	crab	⊢ { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }
35	0 34	wceq	⊢ ContFn = { 𝑡 ∈ ( ℂ ↑m ℋ ) ∣ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℋ ( ( normℎ ‘ ( 𝑤 −ℎ 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }