# Metamath Proof Explorer

## Theorem pjssge0i

Description: Theorem 4.5(iv)->(v) 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 pjssge0i
`|- ( A e. ~H -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih 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 fveq2
` |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` if ( A e. ~H , A , 0h ) ) )`
7 5 6 eqeq12d
` |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) <-> ( ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) -h ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` if ( A e. ~H , A , 0h ) ) ) )`
8 id
` |-  ( A = if ( A e. ~H , A , 0h ) -> A = if ( A e. ~H , A , 0h ) )`
9 5 8 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 ) ) )`
10 9 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 ) ) ) )`
11 7 10 imbi12d
` |-  ( A = if ( A e. ~H , A , 0h ) -> ( ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> 0 <_ ( ( ( ( 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 ) ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` if ( A e. ~H , A , 0h ) ) -> 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 ) ) ) ) )`
12 ifhvhv0
` |-  if ( A e. ~H , A , 0h ) e. ~H`
13 2 12 1 pjssge0ii
` |-  ( ( ( ( projh ` G ) ` if ( A e. ~H , A , 0h ) ) -h ( ( projh ` H ) ` if ( A e. ~H , A , 0h ) ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` if ( A e. ~H , A , 0h ) ) -> 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 ) ) )`
14 11 13 dedth
` |-  ( A e. ~H -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) ) )`