Metamath Proof Explorer

Theorem pjs14i

Description: Theorem S-14 of Watanabe, p. 486. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjs14.1 
|- G e. CH
pjs14.2 
|- H e. CH
Assertion pjs14i 
|- ( A e. ~H -> ( normh ` ( ( ( projh ` H ) o. ( projh ` G ) ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) )

Proof

Step Hyp Ref Expression
1 pjs14.1 
 |-  G e. CH
2 pjs14.2 
 |-  H e. CH
3 2 1 pjcoi 
 |-  ( A e. ~H -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` A ) = ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) )
4 3 fveq2d 
 |-  ( A e. ~H -> ( normh ` ( ( ( projh ` H ) o. ( projh ` G ) ) ` A ) ) = ( normh ` ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) ) )
5 1 pjhcli 
 |-  ( A e. ~H -> ( ( projh ` G ) ` A ) e. ~H )
6 pjnorm 
 |-  ( ( H e. CH /\ ( ( projh ` G ) ` A ) e. ~H ) -> ( normh ` ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) )
7 2 5 6 sylancr 
 |-  ( A e. ~H -> ( normh ` ( ( projh ` H ) ` ( ( projh ` G ) ` A ) ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) )
8 4 7 eqbrtrd 
 |-  ( A e. ~H -> ( normh ` ( ( ( projh ` H ) o. ( projh ` G ) ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) )