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

Metamath Proof Explorer

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 ‘ ( ( 𝑡 ‘ 𝑤 ) − ( 𝑡 ‘ 𝑥 ) ) ) < 𝑦 ) }