Metamath Proof Explorer


Theorem pjorthi

Description: Projection components on orthocomplemented subspaces are orthogonal. (Contributed by NM, 26-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjorth.1 A
pjorth.2 B
Assertion pjorthi H C proj H A ih proj H B = 0

Proof

Step Hyp Ref Expression
1 pjorth.1 A
2 pjorth.2 B
3 chsh H C H S
4 axpjcl H C A proj H A H
5 1 4 mpan2 H C proj H A H
6 choccl H C H C
7 axpjcl H C B proj H B H
8 6 2 7 sylancl H C proj H B H
9 5 8 jca H C proj H A H proj H B H
10 shocorth H S proj H A H proj H B H proj H A ih proj H B = 0
11 3 9 10 sylc H C proj H A ih proj H B = 0