Metamath Proof Explorer

Theorem idcnop

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

Ref Expression
Assertion idcnop 
|- ( _I |` ~H ) e. ContOp

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` ~H ) : ~H -1-1-onto-> ~H
2 f1of 
 |-  ( ( _I |` ~H ) : ~H -1-1-onto-> ~H -> ( _I |` ~H ) : ~H --> ~H )
3 1 2 ax-mp 
 |-  ( _I |` ~H ) : ~H --> ~H
4 id 
 |-  ( y e. RR+ -> y e. RR+ )
5 fvresi 
 |-  ( w e. ~H -> ( ( _I |` ~H ) ` w ) = w )
6 fvresi 
 |-  ( x e. ~H -> ( ( _I |` ~H ) ` x ) = x )
7 5 6 oveqan12rd 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) = ( w -h x ) )
8 7 fveq2d 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) = ( normh ` ( w -h x ) ) )
9 8 breq1d 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y <-> ( normh ` ( w -h x ) ) < y ) )
10 9 biimprd 
 |-  ( ( x e. ~H /\ w e. ~H ) -> ( ( normh ` ( w -h x ) ) < y -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y ) )
11 10 ralrimiva 
 |-  ( x e. ~H -> A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y ) )
12 breq2 
 |-  ( z = y -> ( ( normh ` ( w -h x ) ) < z <-> ( normh ` ( w -h x ) ) < y ) )
13 12 rspceaimv 
 |-  ( ( y e. RR+ /\ A. w e. ~H ( ( normh ` ( w -h x ) ) < y -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y ) ) -> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y ) )
14 4 11 13 syl2anr 
 |-  ( ( x e. ~H /\ y e. RR+ ) -> E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y ) )
15 14 rgen2 
 |-  A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y )
16 elcnop 
 |-  ( ( _I |` ~H ) e. ContOp <-> ( ( _I |` ~H ) : ~H --> ~H /\ A. x e. ~H A. y e. RR+ E. z e. RR+ A. w e. ~H ( ( normh ` ( w -h x ) ) < z -> ( normh ` ( ( ( _I |` ~H ) ` w ) -h ( ( _I |` ~H ) ` x ) ) ) < y ) ) )
17 3 15 16 mpbir2an 
 |-  ( _I |` ~H ) e. ContOp