Theorem idleop

Description: The identity operator is a positive operator. Part of Example 12.2(i) in Young p. 142. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	idleop	$$⊢0_{\mathrm{hop}}{\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$

Proof

Step	Hyp	Ref	Expression
1		0hmop	$$⊢0_{\mathrm{hop}}\in \mathrm{HrmOp}$$
2		idhmop	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}$$
3		leop2	$$⊢\left(0_{\mathrm{hop}}\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}\in \mathrm{HrmOp}\right)\to \left(0_{\mathrm{hop}}{\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow \forall x\in \mathscr{H}{0}_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}x\le I_{\mathrm{op}}\left(x\right){\cdot }_{\mathrm{ih}}x\right)$$
4	1 2 3	mp2an	$$⊢0_{\mathrm{hop}}{\le }_{\mathrm{op}}{I}_{\mathrm{op}}\leftrightarrow \forall x\in \mathscr{H}{0}_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}x\le I_{\mathrm{op}}\left(x\right){\cdot }_{\mathrm{ih}}x$$
5		hiidge0	$$⊢x\in \mathscr{H}\to 0\le x{\cdot }_{\mathrm{ih}}x$$
6		ho0val	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right)=0_{ℎ}$$
7	6	oveq1d	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}x=0_{ℎ}{\cdot }_{\mathrm{ih}}x$$
8		hi01	$$⊢x\in \mathscr{H}\to 0_{ℎ}{\cdot }_{\mathrm{ih}}x=0$$
9	7 8	eqtrd	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}x=0$$
10		hoival	$$⊢x\in \mathscr{H}\to I_{\mathrm{op}}\left(x\right)=x$$
11	10	oveq1d	$$⊢x\in \mathscr{H}\to I_{\mathrm{op}}\left(x\right){\cdot }_{\mathrm{ih}}x=x{\cdot }_{\mathrm{ih}}x$$
12	5 9 11	3brtr4d	$$⊢x\in \mathscr{H}\to 0_{\mathrm{hop}}\left(x\right){\cdot }_{\mathrm{ih}}x\le I_{\mathrm{op}}\left(x\right){\cdot }_{\mathrm{ih}}x$$
13	4 12	mprgbir	$$⊢0_{\mathrm{hop}}{\le }_{\mathrm{op}}{I}_{\mathrm{op}}$$