Theorem hmopidmpj

Description: An idempotent Hermitian operator is a projection operator. Theorem 26.4 of Halmos p. 44. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hmopidmpj	$$⊢\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\to T={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)$$
2		rneq	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \mathrm{ran}T=\mathrm{ran}if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)$$
3	2	fveq2d	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to {\mathrm{proj}}_{ℎ}\left(\mathrm{ran}T\right)={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)$$
4	1 3	eqeq12d	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \left(T={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}T\right)\leftrightarrow if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)\right)$$
5		eleq1	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \left(T\in \mathrm{HrmOp}\leftrightarrow if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\in \mathrm{HrmOp}\right)$$
6	1 1	coeq12d	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to T\circ T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)$$
7	6 1	eqeq12d	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \left(T\circ T=T\leftrightarrow if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)$$
8	5 7	anbi12d	$$⊢T=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\leftrightarrow \left(if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\in \mathrm{HrmOp}\wedge if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)\right)$$
9		eleq1	$$⊢I_{\mathrm{op}}=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \left(I_{\mathrm{op}}\in \mathrm{HrmOp}\leftrightarrow if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\in \mathrm{HrmOp}\right)$$
10		id	$$⊢I_{\mathrm{op}}=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to I_{\mathrm{op}}=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)$$
11	10 10	coeq12d	$$⊢I_{\mathrm{op}}=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to I_{\mathrm{op}}\circ I_{\mathrm{op}}=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)$$
12	11 10	eqeq12d	$$⊢I_{\mathrm{op}}=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \left(I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}\leftrightarrow if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)$$
13	9 12	anbi12d	$$⊢I_{\mathrm{op}}=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\to \left(\left(I_{\mathrm{op}}\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}\right)\leftrightarrow \left(if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\in \mathrm{HrmOp}\wedge if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)\right)$$
14		idhmop	$$⊢I_{\mathrm{op}}\in \mathrm{HrmOp}$$
15		hoif	$$⊢I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$
16		f1of	$$⊢I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}\to I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}$$
17	15 16	ax-mp	$$⊢I_{\mathrm{op}}:\mathscr{H}⟶\mathscr{H}$$
18	17	hoid1i	$$⊢I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}$$
19	14 18	pm3.2i	$$⊢\left(I_{\mathrm{op}}\in \mathrm{HrmOp}\wedge I_{\mathrm{op}}\circ I_{\mathrm{op}}=I_{\mathrm{op}}\right)$$
20	8 13 19	elimhyp	$$⊢\left(if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\in \mathrm{HrmOp}\wedge if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)$$
21	20	simpli	$$⊢if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\in \mathrm{HrmOp}$$
22	20	simpri	$$⊢if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\circ if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)=if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)$$
23	21 22	hmopidmpji	$$⊢if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}if\left(\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right),T,I_{\mathrm{op}}\right)\right)$$
24	4 23	dedth	$$⊢\left(T\in \mathrm{HrmOp}\wedge T\circ T=T\right)\to T={\mathrm{proj}}_{ℎ}\left(\mathrm{ran}T\right)$$