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 = { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnfn 
 |-  ContFn
1 vt 
 |-  t
2 cc 
 |-  CC
3 cmap 
 |-  ^m
4 chba 
 |-  ~H
5 2 4 3 co 
 |-  ( CC ^m ~H )
6 vx 
 |-  x
7 vy 
 |-  y
8 crp 
 |-  RR+
9 vz 
 |-  z
10 vw 
 |-  w
11 cno 
 |-  normh
12 10 cv 
 |-  w
13 cmv 
 |-  -h
14 6 cv 
 |-  x
15 12 14 13 co 
 |-  ( w -h x )
16 15 11 cfv 
 |-  ( normh ` ( w -h x ) )
17 clt 
 |-  <
18 9 cv 
 |-  z
19 16 18 17 wbr 
 |-  ( normh ` ( w -h x ) ) < z
20 cabs 
 |-  abs
21 1 cv 
 |-  t
22 12 21 cfv 
 |-  ( t ` w )
23 cmin 
 |-  -
24 14 21 cfv 
 |-  ( t ` x )
25 22 24 23 co 
 |-  ( ( t ` w ) - ( t ` x ) )
26 25 20 cfv 
 |-  ( abs ` ( ( t ` w ) - ( t ` x ) ) )
27 7 cv 
 |-  y
28 26 27 17 wbr 
 |-  ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y
29 19 28 wi 
 |-  ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
30 29 10 4 wral 
 |-  A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
31 30 9 8 wrex 
 |-  E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
32 31 7 8 wral 
 |-  A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
33 32 6 4 wral 
 |-  A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y )
34 33 1 5 crab 
 |-  { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }
35 0 34 wceq 
 |-  ContFn = { t e. ( CC ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( t ` w ) - ( t ` x ) ) ) < y ) }