Theorem cnopc

Description: Basic continuity property of a continuous Hilbert space operator. (Contributed by NM, 2-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	cnopc	|- ( ( T e. ContOp /\ A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) )

Proof

Step	Hyp	Ref	Expression
1		elcnop	|- ( T e. ContOp <-> ( T : ~H --> ~H /\ A. z e. ~H A. w e. RR+ E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` z ) ) ) < w ) ) )
2	1	simprbi	|- ( T e. ContOp -> A. z e. ~H A. w e. RR+ E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` z ) ) ) < w ) )
3		oveq2	|- ( z = A -> ( y -h z ) = ( y -h A ) )
4	3	fveq2d	|- ( z = A -> ( normh ` ( y -h z ) ) = ( normh ` ( y -h A ) ) )
5	4	breq1d	|- ( z = A -> ( ( normh ` ( y -h z ) ) < x <-> ( normh ` ( y -h A ) ) < x ) )
6		fveq2	|- ( z = A -> ( T ` z ) = ( T ` A ) )
7	6	oveq2d	|- ( z = A -> ( ( T ` y ) -h ( T ` z ) ) = ( ( T ` y ) -h ( T ` A ) ) )
8	7	fveq2d	|- ( z = A -> ( normh ` ( ( T ` y ) -h ( T ` z ) ) ) = ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) )
9	8	breq1d	|- ( z = A -> ( ( normh ` ( ( T ` y ) -h ( T ` z ) ) ) < w <-> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < w ) )
10	5 9	imbi12d	|- ( z = A -> ( ( ( normh ` ( y -h z ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` z ) ) ) < w ) <-> ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < w ) ) )
11	10	rexralbidv	|- ( z = A -> ( E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` z ) ) ) < w ) <-> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < w ) ) )
12		breq2	|- ( w = B -> ( ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < w <-> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) )
13	12	imbi2d	|- ( w = B -> ( ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < w ) <-> ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) ) )
14	13	rexralbidv	|- ( w = B -> ( E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < w ) <-> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) ) )
15	11 14	rspc2v	|- ( ( A e. ~H /\ B e. RR+ ) -> ( A. z e. ~H A. w e. RR+ E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h z ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` z ) ) ) < w ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) ) )
16	2 15	syl5com	|- ( T e. ContOp -> ( ( A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) ) )
17	16	3impib	|- ( ( T e. ContOp /\ A e. ~H /\ B e. RR+ ) -> E. x e. RR+ A. y e. ~H ( ( normh ` ( y -h A ) ) < x -> ( normh ` ( ( T ` y ) -h ( T ` A ) ) ) < B ) )