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