Metamath Proof Explorer

Theorem 0cnop

Description: The identically zero function is a continuous Hilbert space operator. (Contributed by NM, 7-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion 0cnop 
|- 0hop e. ContOp

Proof

Step Hyp Ref Expression
1 ho0f 
 |-  0hop : ~H --> ~H
2 1rp 
 |-  1 e. RR+
3 ho0val 
 |-  ( w e. ~H -> ( 0hop ` w ) = 0h )
4 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
5 3 4 oveqan12rd 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( ( 0hop ` w ) -h ( 0hop ` x ) ) = ( 0h -h 0h ) )
6 5 adantlr 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( ( 0hop ` w ) -h ( 0hop ` x ) ) = ( 0h -h 0h ) )
7 ax-hv0cl 
 |-  0h e. ~H
8 hvsubid 
 |-  ( 0h e. ~H -> ( 0h -h 0h ) = 0h )
9 7 8 ax-mp 
 |-  ( 0h -h 0h ) = 0h
10 6 9 eqtrdi 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( ( 0hop ` w ) -h ( 0hop ` x ) ) = 0h )
11 10 fveq2d 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) = ( normh ` 0h ) )
12 norm0 
 |-  ( normh ` 0h ) = 0
13 11 12 eqtrdi 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) = 0 )
14 rpgt0 
 |-  ( y e. RR+ -> 0 < y )
15 14 ad2antlr 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> 0 < y )
16 13 15 eqbrtrd 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y )
17 16 a1d 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( ( normh ` ( w -h x ) ) < 1 -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y ) )
18 17 ralrimiva 
 |-  ( ( x e. ~H /\ y e. RR+ ) -> A. w e. ~H ( ( normh ` ( w -h x ) ) < 1 -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y ) )
19 breq2 
 |-  ( z = 1 -> ( ( normh ` ( w -h x ) ) < z <-> ( normh ` ( w -h x ) ) < 1 ) )
20 19 rspceaimv 
 |-  ( ( 1 e. RR+ /\ A. w e. ~H ( ( normh ` ( w -h x ) ) < 1 -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y ) ) -> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y ) )
21 2 18 20 sylancr 
 |-  ( ( x e. ~H /\ y e. RR+ ) -> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y ) )
22 21 rgen2 
 |-  A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y )
23 elcnop 
 |-  ( 0hop e. ContOp <-> ( 0hop : ~H --> ~H /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( 0hop ` w ) -h ( 0hop ` x ) ) ) < y ) ) )
24 1 22 23 mpbir2an 
 |-  0hop e. ContOp