# Metamath Proof Explorer

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}}_{ℋ}$
Assertion pjadji ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\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}}_{ℋ}$
2 fveq2 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right)$
3 2 oveq1d ${⊢}{A}=if\left({A}\in ℋ,{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 ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}$
4 oveq1 ${⊢}{A}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\to {A}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)$
5 3 4 eqeq12d ${⊢}{A}=if\left({A}\in ℋ,{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)↔{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)\right)$
6 oveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)$
7 fveq2 ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
8 7 oveq2d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
9 6 8 eqeq12d ${⊢}{B}=if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}{B}=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({B}\right)↔{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)\right)$
10 ifhvhv0 ${⊢}if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\in ℋ$
11 ifhvhv0 ${⊢}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\in ℋ$
12 1 10 11 pjadjii ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({A}\in ℋ,{A},{0}_{ℎ}\right)\right){\cdot }_{\mathrm{ih}}if\left({B}\in ℋ,{B},{0}_{ℎ}\right)=if\left({A}\in ℋ,{A},{0}_{ℎ}\right){\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(if\left({B}\in ℋ,{B},{0}_{ℎ}\right)\right)$
13 5 9 12 dedth2h ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\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)$