Theorem pjadji

Description: A projection is self-adjoint. Property (i) of Beran p. 109. (Contributed by NM, 6-Oct-2000) (New usage is discouraged.)

	Ref	Expression
Hypothesis	pjadjt.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjadji	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjadjt.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		fveq2	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right)$$
3	2	oveq1d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}B={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}B$$
4		oveq1	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
5	3 4	eqeq12d	$$⊢A=if\left(A\in \mathscr{H},A,0_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}B=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
6		oveq2	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}B={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(B\in \mathscr{H},B,0_{ℎ}\right)$$
7		fveq2	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
8	7	oveq2d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
9	6 8	eqeq12d	$$⊢B=if\left(B\in \mathscr{H},B,0_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}B=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\leftrightarrow {\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(B\in \mathscr{H},B,0_{ℎ}\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)\right)$$
10		ifhvhv0	$$⊢if\left(A\in \mathscr{H},A,0_{ℎ}\right)\in \mathscr{H}$$
11		ifhvhv0	$$⊢if\left(B\in \mathscr{H},B,0_{ℎ}\right)\in \mathscr{H}$$
12	1 10 11	pjadjii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(A\in \mathscr{H},A,0_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left(B\in \mathscr{H},B,0_{ℎ}\right)=if\left(A\in \mathscr{H},A,0_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(if\left(B\in \mathscr{H},B,0_{ℎ}\right)\right)$$
13	5 9 12	dedth2h	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$