Metamath Proof Explorer


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 HC
Assertion pjadji ABprojHAihB=AihprojHB

Proof

Step Hyp Ref Expression
1 pjadjt.1 HC
2 fveq2 A=ifAA0projHA=projHifAA0
3 2 oveq1d A=ifAA0projHAihB=projHifAA0ihB
4 oveq1 A=ifAA0AihprojHB=ifAA0ihprojHB
5 3 4 eqeq12d A=ifAA0projHAihB=AihprojHBprojHifAA0ihB=ifAA0ihprojHB
6 oveq2 B=ifBB0projHifAA0ihB=projHifAA0ihifBB0
7 fveq2 B=ifBB0projHB=projHifBB0
8 7 oveq2d B=ifBB0ifAA0ihprojHB=ifAA0ihprojHifBB0
9 6 8 eqeq12d B=ifBB0projHifAA0ihB=ifAA0ihprojHBprojHifAA0ihifBB0=ifAA0ihprojHifBB0
10 ifhvhv0 ifAA0
11 ifhvhv0 ifBB0
12 1 10 11 pjadjii projHifAA0ihifBB0=ifAA0ihprojHifBB0
13 5 9 12 dedth2h ABprojHAihB=AihprojHB