Theorem pjhmopi

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

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

Proof

Step	Hyp	Ref	Expression
1		pjhmop.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
3	1	pjadji	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)$$
4	3	eqcomd	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
5	4	rgen2	$$⊢\forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
6		elhmop	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{HrmOp}\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}\wedge \forall x\in \mathscr{H}\forall y\in \mathscr{H}x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(y\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
7	2 5 6	mpbir2an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{HrmOp}$$