Metamath Proof Explorer

Theorem pjdifnormi

Description: Theorem 4.5(v)<->(vi) of Beran p. 112. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjdifnormi 
|- ( A e. ~H -> ( 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) <-> ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` G ) ` A ) = ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) )
4 fveq2 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` H ) ` A ) = ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) )
5 3 4 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) -h ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) )
6 id 
 |-  ( A = if ( A e. ~H , A , 0h ) -> A = if ( A e. ~H , A , 0h ) )
7 5 6 oveq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) -h ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) .ih if ( A e. ~H , A , 0h ) ) )
8 7 breq2d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) <-> 0 <_ ( ( ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) -h ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) .ih if ( A e. ~H , A , 0h ) ) ) )
9 2fveq3 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( ( projh ` H ) ` A ) ) = ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) )
10 2fveq3 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( normh ` ( ( projh ` G ) ` A ) ) = ( normh ` ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) ) )
11 9 10 breq12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) <-> ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) <_ ( normh ` ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) ) ) )
12 8 11 bibi12d 
 |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) <-> ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) ) <-> ( 0 <_ ( ( ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) -h ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) .ih if ( A e. ~H , A , 0h ) ) <-> ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) <_ ( normh ` ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) ) ) ) )
13 ifhvhv0 
 |-  if ( A e. ~H , A , 0h ) e. ~H
14 2 13 1 pjdifnormii 
 |-  ( 0 <_ ( ( ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) -h ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) .ih if ( A e. ~H , A , 0h ) ) <-> ( normh ` ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) <_ ( normh ` ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) ) )
15 12 14 dedth 
 |-  ( A e. ~H -> ( 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) <-> ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) ) )