Theorem pjadj3

Description: A projector is self-adjoint. Property (i) of Beran p. 109. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	pjadj3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjmfn	$$⊢{\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}$$
2		fnfvelrn	$$⊢\left({\mathrm{proj}}_{ℎ}Fn{\mathbf{C}}_{\mathscr{H}}\wedge H\in {\mathbf{C}}_{\mathscr{H}}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
3	1 2	mpan	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}$$
4		pjadj2	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\in \mathrm{ran}{\mathrm{proj}}_{ℎ}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$
5	3 4	syl	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {adj}_h\left({\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(H\right)$$