Metamath Proof Explorer


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 ) )