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

Metamath Proof Explorer

Definition df-cnop

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

Ref Expression
Assertion df-cnop 
|- ContOp = { t e. ( ~H ^m ~H ) | A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( t ` w ) -h ( t ` x ) ) ) < y ) }

Detailed syntax breakdown

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