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	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{UniOp}$$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$
2		f1ofo	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}\to \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{onto}{⟶}\mathscr{H}$$
3	1 2	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{onto}{⟶}\mathscr{H}$$
4		fvresi	$$⊢x\in \mathscr{H}\to \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right)=x$$
5		fvresi	$$⊢y\in \mathscr{H}\to \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(y\right)=y$$
6	4 5	oveqan12d	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right){\cdot }_{\mathrm{ih}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
7	6	rgen2	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right){\cdot }_{\mathrm{ih}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}y$$
8		elunop	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{UniOp}\leftrightarrow \left(\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{onto}{⟶}\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right){\cdot }_{\mathrm{ih}}\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}y\right)$$
9	3 7 8	mpbir2an	$$⊢{\mathrm{I}\upharpoonright }_{\mathscr{H}}\in \mathrm{UniOp}$$