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 ) ) ) )