Metamath Proof Explorer


Theorem pjopi

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

Ref Expression
Hypotheses pjop.1 H C
pjop.2 A
Assertion pjopi proj H A = A - proj H A

Proof

Step Hyp Ref Expression
1 pjop.1 H C
2 pjop.2 A
3 pjop H C A proj H A = A - proj H A
4 1 2 3 mp2an proj H A = A - proj H A