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

Metamath Proof Explorer

Theorem pjopyth

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

Ref Expression
Assertion pjopyth 
|- ( ( H e. CH /\ G e. CH /\ A e. ~H ) -> ( H C_ ( _|_ ` G ) -> ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( H C_ ( _|_ ` G ) <-> if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) ) )
2 fveq2 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( projh ` H ) = ( projh ` if ( H e. CH , H , ~H ) ) )
3 2 fveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( projh ` H ) ` A ) = ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) )
4 3 oveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) )
5 4 fveq2d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) = ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) )
6 5 oveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) )
7 3 fveq2d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( normh ` ( ( projh ` H ) ` A ) ) = ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) )
8 7 oveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) = ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) )
9 8 oveq1d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) )
10 6 9 eqeq12d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) <-> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) ) )
11 1 10 imbi12d 
 |-  ( H = if ( H e. CH , H , ~H ) -> ( ( H C_ ( _|_ ` G ) -> ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) ) <-> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) ) ) )
12 fveq2 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( _|_ ` G ) = ( _|_ ` if ( G e. CH , G , ~H ) ) )
13 12 sseq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) <-> if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) ) )
14 fveq2 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( projh ` G ) = ( projh ` if ( G e. CH , G , ~H ) ) )
15 14 fveq1d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( projh ` G ) ` A ) = ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) )
16 15 oveq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) )
17 16 fveq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) = ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) )
18 17 oveq1d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) ^ 2 ) )
19 15 fveq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( normh ` ( ( projh ` G ) ` A ) ) = ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) )
20 19 oveq1d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) = ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) )
21 20 oveq2d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) ) )
22 18 21 eqeq12d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) <-> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) ) ) )
23 13 22 imbi12d 
 |-  ( G = if ( G e. CH , G , ~H ) -> ( ( if ( H e. CH , H , ~H ) C_ ( _|_ ` G ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) ) <-> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) ) ) ) )
24 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) = ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) )
25 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) = ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) )
26 24 25 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) = ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) )
27 26 fveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) = ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ) )
28 27 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) ^ 2 ) = ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ) ^ 2 ) )
29 24 fveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) = ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) )
30 29 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) = ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) )
31 25 fveq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) = ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) )
32 31 oveq1d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) = ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) )
33 30 32 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) ) )
34 28 33 eqeq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) ) <-> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) ) ) )
35 34 imbi2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` A ) ) ^ 2 ) ) ) <-> ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) ) ) ) )
36 ifchhv 
 |-  if ( H e. CH , H , ~H ) e. CH
37 ifchhv 
 |-  if ( G e. CH , G , ~H ) e. CH
38 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
39 36 37 38 pjopythi 
 |-  ( if ( H e. CH , H , ~H ) C_ ( _|_ ` if ( G e. CH , G , ~H ) ) -> ( ( normh ` ( ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) +h ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` if ( H e. CH , H , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) + ( ( normh ` ( ( projh ` if ( G e. CH , G , ~H ) ) ` if ( A e. ~H , A , 0h ) ) ) ^ 2 ) ) )
40 11 23 35 39 dedth3h 
 |-  ( ( H e. CH /\ G e. CH /\ A e. ~H ) -> ( H C_ ( _|_ ` G ) -> ( ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` G ) ` A ) ) ) ^ 2 ) = ( ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) + ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) ) )