This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pjssge0ii

Description: Theorem 4.5(iv)->(v) of Beran p. 112. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 
|- H e. CH
pjidm.2 
|- A e. ~H
pjsslem.1 
|- G e. CH
Assertion pjssge0ii 
|- ( ( ( ( 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 pjidm.1 
 |-  H e. CH
2 pjidm.2 
 |-  A e. ~H
3 pjsslem.1 
 |-  G e. CH
4 1 choccli 
 |-  ( _|_ ` H ) e. CH
5 3 4 chincli 
 |-  ( G i^i ( _|_ ` H ) ) e. CH
6 5 2 pjhclii 
 |-  ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) e. ~H
7 6 normcli 
 |-  ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) e. RR
8 7 sqge0i 
 |-  0 <_ ( ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) ^ 2 )
9 oveq1 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) .ih A ) )
10 5 2 pjinormii 
 |-  ( ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) ^ 2 )
11 9 10 eqtrdi 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( normh ` ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) ) ^ 2 ) )
12 8 11 breqtrrid 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) = ( ( projh ` ( G i^i ( _|_ ` H ) ) ) ` A ) -> 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) )