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