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	⊢ 𝐺 ∈ Cℋ
	pjoi0.2	⊢ 𝐻 ∈ Cℋ
	pjoi0.3	⊢ 𝐴 ∈ ℋ
Assertion	pjopythi	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( normℎ ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pjoi0.1	⊢ 𝐺 ∈ Cℋ
2		pjoi0.2	⊢ 𝐻 ∈ Cℋ
3		pjoi0.3	⊢ 𝐴 ∈ ℋ
4	1 2 3	pjoi0i	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 0 )
5	1 3	pjhclii	⊢ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ℋ
6	2 3	pjhclii	⊢ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ∈ ℋ
7	5 6	normpythi	⊢ ( ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ·ih ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) = 0 → ( ( normℎ ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) )
8	4 7	syl	⊢ ( 𝐺 ⊆ ( ⊥ ‘ 𝐻 ) → ( ( normℎ ‘ ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) ) )