Theorem idhmop

Description: The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	idhmop	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}$$

Proof

Step	Hyp	Ref	Expression
1		hoif	$$⊢I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$
2		f1of	$$⊢I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}\to I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}$$
3	1 2	ax-mp	$$⊢I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}$$
4		hoival	$$⊢x\in \mathscr{H}\to I_{\mathrm{op}}\left(x\right)=x$$
5	4	eqcomd	$$⊢x\in \mathscr{H}\to x=I_{\mathrm{op}}\left(x\right)$$
6		hoival	$$⊢y\in \mathscr{H}\to I_{\mathrm{op}}\left(y\right)=y$$
7	5 6	oveqan12d	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}{I}_{\mathrm{op}}\left(y\right)=I_{\mathrm{op}}\left(x\right){\cdot }_{\mathrm{ih}}y$$
8	7	rgen2	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}{I}_{\mathrm{op}}\left(y\right)=I_{\mathrm{op}}\left(x\right){\cdot }_{\mathrm{ih}}y$$
9		elhmop	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}\leftrightarrow \left(I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}{I}_{\mathrm{op}}\left(y\right)=I_{\mathrm{op}}\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
10	3 8 9	mpbir2an	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}$$