# Metamath Proof Explorer

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}}_{ℋ}$
pjidm.2 ${⊢}{A}\in ℋ$
pjadj.3 ${⊢}{B}\in ℋ$
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}}_{ℋ}$
2 pjidm.2 ${⊢}{A}\in ℋ$
3 pjadj.3 ${⊢}{B}\in ℋ$
4 3 2 pjorthi ${⊢}{H}\in {\mathbf{C}}_{ℋ}\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 ${⊢}\stackrel{‾}{{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right)}=\stackrel{‾}{0}$
7 cj0 ${⊢}\stackrel{‾}{0}=0$
8 6 7 eqtri ${⊢}\stackrel{‾}{{\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}}_{ℋ}$
10 9 2 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right)\in ℋ$
11 1 3 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)\in ℋ$
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)=\stackrel{‾}{{\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}}_{ℋ}\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 ℋ$
18 9 3 pjhclii ${⊢}{\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({B}\right)\in ℋ$
19 his7 ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({B}\right)\in ℋ\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 ℋ\wedge {\mathrm{proj}}_{ℎ}\left(\perp \left({H}\right)\right)\left({A}\right)\in ℋ\wedge {\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)\in ℋ\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)$