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

Metamath Proof Explorer

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