This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- G e. CH
pjoi0.2 
|- H e. CH
pjoi0.3 
|- A e. ~H
Assertion pjopythi 
|- ( G C_ ( _|_ ` H ) -> ( ( normh ` ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 pjoi0.1 
 |-  G e. CH
2 pjoi0.2 
 |-  H e. CH
3 pjoi0.3 
 |-  A e. ~H
4 1 2 3 pjoi0i 
 |-  ( G C_ ( _|_ ` H ) -> ( ( ( projh ` G ) ` A ) .ih ( ( projh ` H ) ` A ) ) = 0 )
5 1 3 pjhclii 
 |-  ( ( projh ` G ) ` A ) e. ~H
6 2 3 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
7 5 6 normpythi 
 |-  ( ( ( ( projh ` G ) ` A ) .ih ( ( projh ` H ) ` A ) ) = 0 -> ( ( normh ` ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) ) )
8 4 7 syl 
 |-  ( G C_ ( _|_ ` H ) -> ( ( normh ` ( ( ( projh ` G ) ` A ) +h ( ( projh ` H ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) ) )