# 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`