Theorem elcnop

Description: Property defining a continuous Hilbert space operator. (Contributed by NM, 28-Jan-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	elcnop	|- ( T e. ContOp <-> ( T : ~H --> ~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 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	|- ( t = T -> ( t ` w ) = ( T ` w ) )
2		fveq1	|- ( t = T -> ( t ` x ) = ( T ` x ) )
3	1 2	oveq12d	|- ( t = T -> ( ( t ` w ) -h ( t ` x ) ) = ( ( T ` w ) -h ( T ` x ) ) )
4	3	fveq2d	|- ( t = T -> ( normh ` ( ( t ` w ) -h ( t ` x ) ) ) = ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) )
5	4	breq1d	|- ( t = T -> ( ( normh ` ( ( t ` w ) -h ( t ` x ) ) ) < y <-> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < y ) )
6	5	imbi2d	|- ( t = T -> ( ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( t ` w ) -h ( t ` x ) ) ) < y ) <-> ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < y ) ) )
7	6	rexralbidv	|- ( t = T -> ( E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( t ` w ) -h ( t ` x ) ) ) < y ) <-> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( T ` w ) -h ( T ` x ) ) ) < y ) ) )
8	7	2ralbidv	|- ( t = T -> ( 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 ) <-> 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 ) ) )
9		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 ) }
10	8 9	elrab2	|- ( T e. 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 ) ) )
11		ax-hilex	|- ~H e. _V
12	11 11	elmap	|- ( T e. ( ~H ^m ~H ) <-> T : ~H --> ~H )
13	12	anbi1i	|- ( ( 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 ) ) <-> ( T : ~H --> ~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 ) ) )
14	10 13	bitri	|- ( T e. ContOp <-> ( T : ~H --> ~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 ) ) )