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	⊢ 𝐻 ∈ Cℋ
	pjnorm.2	⊢ 𝐴 ∈ ℋ
Assertion	pjnormi	⊢ ( normℎ ‘ ( ( projℎ ‘ 𝐻 ) ‘ 𝐴 ) ) ≤ ( normℎ ‘ 𝐴 )

Proof

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