Metamath Proof Explorer


Theorem pjopythi

Description: Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjoi0.1 GC
pjoi0.2 HC
pjoi0.3 A
Assertion pjopythi GHnormprojGA+projHA2=normprojGA2+normprojHA2

Proof

Step Hyp Ref Expression
1 pjoi0.1 GC
2 pjoi0.2 HC
3 pjoi0.3 A
4 1 2 3 pjoi0i GHprojGAihprojHA=0
5 1 3 pjhclii projGA
6 2 3 pjhclii projHA
7 5 6 normpythi projGAihprojHA=0normprojGA+projHA2=normprojGA2+normprojHA2
8 4 7 syl GHnormprojGA+projHA2=normprojGA2+normprojHA2