Metamath Proof Explorer

Theorem 0cnfn

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

Ref Expression
Assertion 0cnfn 
|- ( ~H X. { 0 } ) e. ContFn

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 1 fconst6 
 |-  ( ~H X. { 0 } ) : ~H --> CC
3 1rp 
 |-  1 e. RR+
4 c0ex 
 |-  0 e. _V
5 4 fvconst2 
 |-  ( w e. ~H -> ( ( ~H X. { 0 } ) ` w ) = 0 )
6 4 fvconst2 
 |-  ( x e. ~H -> ( ( ~H X. { 0 } ) ` x ) = 0 )
7 5 6 oveqan12rd 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) = ( 0 - 0 ) )
8 7 adantlr 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) = ( 0 - 0 ) )
9 0m0e0 
 |-  ( 0 - 0 ) = 0
10 8 9 eqtrdi 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) = 0 )
11 10 fveq2d 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) ) = ( abs ` 0 ) )
12 abs0 
 |-  ( abs ` 0 ) = 0
13 11 12 eqtrdi 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` 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 ) -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) ) < y )
17 16 a1d 
 |-  ( ( ( x e. ~H /\ y e. RR+ ) /\ w e. ~H ) -> ( ( normh ` ( w -h x ) ) < 1 -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) ) < y ) )
18 17 ralrimiva 
 |-  ( ( x e. ~H /\ y e. RR+ ) -> A. w e. ~H ( ( normh ` ( w -h x ) ) < 1 -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` 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 -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) ) < y ) ) -> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) ) < y ) )
21 3 18 20 sylancr 
 |-  ( ( x e. ~H /\ y e. RR+ ) -> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` 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 -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) ) < y )
23 elcnfn 
 |-  ( ( ~H X. { 0 } ) e. ContFn <-> ( ( ~H X. { 0 } ) : ~H --> CC /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( abs ` ( ( ( ~H X. { 0 } ) ` w ) - ( ( ~H X. { 0 } ) ` x ) ) ) < y ) ) )
24 2 22 23 mpbir2an 
 |-  ( ~H X. { 0 } ) e. ContFn