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