Metamath Proof Explorer

Theorem pjpythi

Description: Pythagorean theorem for projections. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjnorm.1 
|- H e. CH
pjnorm.2 
|- A e. ~H
Assertion pjpythi 
|- ( ( normh ` A ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) )

Proof

Step Hyp Ref Expression
1 pjnorm.1 
 |-  H e. CH
2 pjnorm.2 
 |-  A e. ~H
3 1 2 pjpji 
 |-  A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )
4 3 fveq2i 
 |-  ( normh ` A ) = ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
5 4 oveq1i 
 |-  ( ( normh ` A ) ^ 2 ) = ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) ^ 2 )
6 1 chshii 
 |-  H e. SH
7 shococss 
 |-  ( H e. SH -> H C_ ( _|_ ` ( _|_ ` H ) ) )
8 1 choccli 
 |-  ( _|_ ` H ) e. CH
9 1 8 2 pjopythi 
 |-  ( H C_ ( _|_ ` ( _|_ ` H ) ) -> ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) ) )
10 6 7 9 mp2b 
 |-  ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) )
11 5 10 eqtri 
 |-  ( ( normh ` A ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` ( _|_ ` H ) ) ` A ) ) ^ 2 ) )