This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idunop

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

Ref Expression
Assertion idunop 
|- ( _I |` ~H ) e. UniOp

Proof

Step Hyp Ref Expression
1 f1oi 
 |-  ( _I |` ~H ) : ~H -1-1-onto-> ~H
2 f1ofo 
 |-  ( ( _I |` ~H ) : ~H -1-1-onto-> ~H -> ( _I |` ~H ) : ~H -onto-> ~H )
3 1 2 ax-mp 
 |-  ( _I |` ~H ) : ~H -onto-> ~H
4 fvresi 
 |-  ( x e. ~H -> ( ( _I |` ~H ) ` x ) = x )
5 fvresi 
 |-  ( y e. ~H -> ( ( _I |` ~H ) ` y ) = y )
6 4 5 oveqan12d 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( ( ( _I |` ~H ) ` x ) .ih ( ( _I |` ~H ) ` y ) ) = ( x .ih y ) )
7 6 rgen2 
 |-  A. x e. ~H A. y e. ~H ( ( ( _I |` ~H ) ` x ) .ih ( ( _I |` ~H ) ` y ) ) = ( x .ih y )
8 elunop 
 |-  ( ( _I |` ~H ) e. UniOp <-> ( ( _I |` ~H ) : ~H -onto-> ~H /\ A. x e. ~H A. y e. ~H ( ( ( _I |` ~H ) ` x ) .ih ( ( _I |` ~H ) ` y ) ) = ( x .ih y ) ) )
9 3 7 8 mpbir2an 
 |-  ( _I |` ~H ) e. UniOp