Theorem pjhmop

Description: A projection is a Hermitian operator. (Contributed by NM, 24-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjhmop	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{HrmOp}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)$$
2	1	eleq1d	$$⊢H=if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{HrmOp}\leftrightarrow {\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\in \mathrm{HrmOp}\right)$$
3		h0elch	$$⊢0_{\mathscr{H}}\in {\mathbf{C}}_{\mathscr{H}}$$
4	3	elimel	$$⊢if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
5	4	pjhmopi	$$⊢{\mathrm{proj}}_{ℎ}\left(if\left(H\in {\mathbf{C}}_{\mathscr{H}},H,0_{\mathscr{H}}\right)\right)\in \mathrm{HrmOp}$$
6	2 5	dedth	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{HrmOp}$$