Theorem pjadjii

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

	Ref	Expression
Hypotheses	pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
	pjidm.2	$$⊢A\in \mathscr{H}$$
	pjadj.3	$$⊢B\in \mathscr{H}$$
Assertion	pjadjii	$$⊢{\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		pjidm.1	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjidm.2	$$⊢A\in \mathscr{H}$$
3		pjadj.3	$$⊢B\in \mathscr{H}$$
4	3 2	pjorthi	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0$$
5	1 4	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)=0$$
6	5	fveq2i	$$⊢\overline{{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)}=\bar{0}$$
7		cj0	$$⊢\bar{0}=0$$
8	6 7	eqtri	$$⊢\overline{{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)}=0$$
9	1	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10	9 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}$$
11	1 3	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in \mathscr{H}$$
12	10 11	his1i	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=\overline{{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)}$$
13	2 3	pjorthi	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)=0$$
14	1 13	ax-mp	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)=0$$
15	8 12 14	3eqtr4ri	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
16	15	oveq2i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)+\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)+\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
17	1 2	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
18	9 3	pjhclii	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \mathscr{H}$$
19		his7	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)+\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)$$
20	17 11 18 19	mp3an	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)+\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)$$
21		ax-his2	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\in \mathscr{H}\wedge {\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\in \mathscr{H}\right)\to \left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)+\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
22	17 10 11 21	mp3an	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)+\left({\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)\right)$$
23	16 20 22	3eqtr4i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
24	1 3	pjpji	$$⊢B={\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)$$
25	24	oveq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}B={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(B\right)\right)$$
26	1 2	pjpji	$$⊢A={\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)$$
27	26	oveq1i	$$⊢A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){+}_{ℎ}{\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\left(A\right)\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$
28	23 25 27	3eqtr4i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right){\cdot }_{\mathrm{ih}}B=A{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(H\right)\left(B\right)$$