Theorem dfiop2

Description: Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	dfiop2	$$⊢I_{\mathrm{op}}={\mathrm{I}\upharpoonright }_{\mathscr{H}}$$

Proof

Step	Hyp	Ref	Expression
1		df-iop	$$⊢I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
2		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
3	2	pjfni	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)Fn\mathscr{H}$$
4		fnresi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)Fn\mathscr{H}$$
5		pjch1	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)=x$$
6		fvresi	$$⊢x\in \mathscr{H}\to \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right)=x$$
7	5 6	eqtr4d	$$⊢x\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)=\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right)$$
8	7	rgen	$$⊢\forall x\in \mathscr{H}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)=\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right)$$
9		eqfnfv	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)Fn\mathscr{H}\wedge \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)Fn\mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)={\mathrm{I}\upharpoonright }_{\mathscr{H}}\leftrightarrow \forall x\in \mathscr{H}{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\left(x\right)=\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)\left(x\right)\right)$$
10	8 9	mpbiri	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)Fn\mathscr{H}\wedge \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right)Fn\mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)={\mathrm{I}\upharpoonright }_{\mathscr{H}}$$
11	3 4 10	mp2an	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)={\mathrm{I}\upharpoonright }_{\mathscr{H}}$$
12	1 11	eqtri	$$⊢I_{\mathrm{op}}={\mathrm{I}\upharpoonright }_{\mathscr{H}}$$