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

Metamath Proof Explorer

Theorem pjnormi

Description: The norm of the projection is less than or equal to the norm. (Contributed by NM, 27-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses pjnorm.1 ⊢ H ∈ C ℋ
pjnorm.2 ⊢ A ∈ ℋ
Assertion pjnormi ⊢ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A ≤ norm ℎ ⁡ A

Proof

Step Hyp Ref Expression
1 pjnorm.1 ⊢ H ∈ C ℋ
2 pjnorm.2 ⊢ A ∈ ℋ
3 1 2 pjhclii ⊢ proj ℎ ⁡ H ⁡ A ∈ ℋ
4 1 choccli ⊢ ⊥ ⁡ H ∈ C ℋ
5 4 2 pjhclii ⊢ proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ℋ
6 3 5 pm3.2i ⊢ proj ℎ ⁡ H ⁡ A ∈ ℋ ∧ proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ℋ
7 2 2 pjorthi ⊢ H ∈ C ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0
8 1 7 ax-mp ⊢ proj ℎ ⁡ H ⁡ A ⋅ ih proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0
9 normpyc ⊢ proj ℎ ⁡ H ⁡ A ∈ ℋ ∧ proj ℎ ⁡ ⊥ ⁡ H ⁡ A ∈ ℋ → proj ℎ ⁡ H ⁡ A ⋅ ih proj ℎ ⁡ ⊥ ⁡ H ⁡ A = 0 → norm ℎ ⁡ proj ℎ ⁡ H ⁡ A ≤ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A
10 6 8 9 mp2 ⊢ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A ≤ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A
11 1 2 pjpji ⊢ A = proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A
12 11 fveq2i ⊢ norm ℎ ⁡ A = norm ℎ ⁡ proj ℎ ⁡ H ⁡ A + ℎ proj ℎ ⁡ ⊥ ⁡ H ⁡ A
13 10 12 breqtrri ⊢ norm ℎ ⁡ proj ℎ ⁡ H ⁡ A ≤ norm ℎ ⁡ A