Metamath Proof Explorer


Theorem pjop

Description: Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999) (New usage is discouraged.)

Ref Expression
Assertion pjop H C A proj H A = A - proj H A

Proof

Step Hyp Ref Expression
1 axpjpj H C A A = proj H A + proj H A
2 1 eqcomd H C A proj H A + proj H A = A
3 simpr H C A A
4 pjhcl H C A proj H A
5 choccl H C H C
6 pjhcl H C A proj H A
7 5 6 sylan H C A proj H A
8 hvsubadd A proj H A proj H A A - proj H A = proj H A proj H A + proj H A = A
9 3 4 7 8 syl3anc H C A A - proj H A = proj H A proj H A + proj H A = A
10 2 9 mpbird H C A A - proj H A = proj H A
11 10 eqcomd H C A proj H A = A - proj H A