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