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