Metamath Proof Explorer


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 HC
pjidm.2 A
pjadj.3 B
Assertion pjadjii projHAihB=AihprojHB

Proof

Step Hyp Ref Expression
1 pjidm.1 HC
2 pjidm.2 A
3 pjadj.3 B
4 3 2 pjorthi HCprojHBihprojHA=0
5 1 4 ax-mp projHBihprojHA=0
6 5 fveq2i projHBihprojHA=0
7 cj0 0=0
8 6 7 eqtri projHBihprojHA=0
9 1 choccli HC
10 9 2 pjhclii projHA
11 1 3 pjhclii projHB
12 10 11 his1i projHAihprojHB=projHBihprojHA
13 2 3 pjorthi HCprojHAihprojHB=0
14 1 13 ax-mp projHAihprojHB=0
15 8 12 14 3eqtr4ri projHAihprojHB=projHAihprojHB
16 15 oveq2i projHAihprojHB+projHAihprojHB=projHAihprojHB+projHAihprojHB
17 1 2 pjhclii projHA
18 9 3 pjhclii projHB
19 his7 projHAprojHBprojHBprojHAihprojHB+projHB=projHAihprojHB+projHAihprojHB
20 17 11 18 19 mp3an projHAihprojHB+projHB=projHAihprojHB+projHAihprojHB
21 ax-his2 projHAprojHAprojHBprojHA+projHAihprojHB=projHAihprojHB+projHAihprojHB
22 17 10 11 21 mp3an projHA+projHAihprojHB=projHAihprojHB+projHAihprojHB
23 16 20 22 3eqtr4i projHAihprojHB+projHB=projHA+projHAihprojHB
24 1 3 pjpji B=projHB+projHB
25 24 oveq2i projHAihB=projHAihprojHB+projHB
26 1 2 pjpji A=projHA+projHA
27 26 oveq1i AihprojHB=projHA+projHAihprojHB
28 23 25 27 3eqtr4i projHAihB=AihprojHB