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

Metamath Proof Explorer

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