Theorem pjpythi

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

	Ref	Expression
Hypotheses	pjnorm.1	⊢ 𝐻 ∈ Cℋ
	pjnorm.2	⊢ 𝐴 ∈ ℋ
Assertion	pjpythi	⊢ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) )

Proof

Step	Hyp	Ref	Expression
1		pjnorm.1	⊢ 𝐻 ∈ Cℋ
2		pjnorm.2	⊢ 𝐴 ∈ ℋ
3	1 2	pjpji	⊢ 𝐴 = ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) )
4	3	fveq2i	⊢ ( normℎ ‘ 𝐴 ) = ( normℎ ‘ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) )
5	4	oveq1i	⊢ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( normℎ ‘ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) ↑ 2 )
6	1	chshii	⊢ 𝐻 ∈ Sℋ
7		shococss	⊢ ( 𝐻 ∈ Sℋ → 𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) )
8	1	choccli	⊢ ( ⊥ ‘ 𝐻 ) ∈ Cℋ
9	1 8 2	pjopythi	⊢ ( 𝐻 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐻 ) ) → ( ( normℎ ‘ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) ) )
10	6 7 9	mp2b	⊢ ( ( normℎ ‘ ( ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) +ℎ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) )
11	5 10	eqtri	⊢ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( ( ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ↑ 2 ) + ( ( normℎ ‘ ( ( projℎ ‘ ( ⊥ ‘ 𝐻 ) ) ‘ 𝐴 ) ) ↑ 2 ) )