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 ⊢ H ∈ C ℋ
pjnorm.2 ⊢ A ∈ ℋ
Assertion pjpythi ⊢ norm ℎ ⁡ A 2 = norm ℎ ⁡ proj ℎ ⁡ H ⁡ A 2 + norm ℎ ⁡ proj ℎ ⁡ ⊥ ⁡ H ⁡ A 2

Proof

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