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 e. CH
	pjnorm.2	|- A e. ~H
Assertion	pjnormi	|- ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` A )

Proof

Step	Hyp	Ref	Expression
1		pjnorm.1	|- H e. CH
2		pjnorm.2	|- A e. ~H
3	1 2	pjhclii	|- ( ( projh ` H ) ` A ) e. ~H
4	1	choccli	|- ( _|_ ` H ) e. CH
5	4 2	pjhclii	|- ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H
6	3 5	pm3.2i	|- ( ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H )
7	2 2	pjorthi	|- ( H e. CH -> ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 )
8	1 7	ax-mp	|- ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0
9		normpyc	|- ( ( ( ( projh ` H ) ` A ) e. ~H /\ ( ( projh ` ( _|_ ` H ) ) ` A ) e. ~H ) -> ( ( ( ( projh ` H ) ` A ) .ih ( ( projh ` ( _|_ ` H ) ) ` A ) ) = 0 -> ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) ) ) )
10	6 8 9	mp2	|- ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
11	1 2	pjpji	|- A = ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) )
12	11	fveq2i	|- ( normh ` A ) = ( normh ` ( ( ( projh ` H ) ` A ) +h ( ( projh ` ( _|_ ` H ) ) ` A ) ) )
13	10 12	breqtrri	|- ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` A )