Metamath Proof Explorer

Theorem pjdifnormii

Description: Theorem 4.5(v)<->(vi) 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 pjdifnormii 
|- ( 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) <-> ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` 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 3 2 pjhclii 
 |-  ( ( projh ` G ) ` A ) e. ~H
5 4 normcli 
 |-  ( normh ` ( ( projh ` G ) ` A ) ) e. RR
6 5 resqcli 
 |-  ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) e. RR
7 1 2 pjhclii 
 |-  ( ( projh ` H ) ` A ) e. ~H
8 7 normcli 
 |-  ( normh ` ( ( projh ` H ) ` A ) ) e. RR
9 8 resqcli 
 |-  ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) e. RR
10 6 9 subge0i 
 |-  ( 0 <_ ( ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) - ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) ) <-> ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) <_ ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) )
11 his2sub 
 |-  ( ( ( ( projh ` G ) ` A ) e. ~H /\ ( ( projh ` H ) ` A ) e. ~H /\ A e. ~H ) -> ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( ( projh ` G ) ` A ) .ih A ) - ( ( ( projh ` H ) ` A ) .ih A ) ) )
12 4 7 2 11 mp3an 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( ( projh ` G ) ` A ) .ih A ) - ( ( ( projh ` H ) ` A ) .ih A ) )
13 3 2 pjinormii 
 |-  ( ( ( projh ` G ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 )
14 1 2 pjinormii 
 |-  ( ( ( projh ` H ) ` A ) .ih A ) = ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 )
15 13 14 oveq12i 
 |-  ( ( ( ( projh ` G ) ` A ) .ih A ) - ( ( ( projh ` H ) ` A ) .ih A ) ) = ( ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) - ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) )
16 12 15 eqtri 
 |-  ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) = ( ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) - ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) )
17 16 breq2i 
 |-  ( 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) <-> 0 <_ ( ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) - ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) ) )
18 normge0 
 |-  ( ( ( projh ` H ) ` A ) e. ~H -> 0 <_ ( normh ` ( ( projh ` H ) ` A ) ) )
19 7 18 ax-mp 
 |-  0 <_ ( normh ` ( ( projh ` H ) ` A ) )
20 normge0 
 |-  ( ( ( projh ` G ) ` A ) e. ~H -> 0 <_ ( normh ` ( ( projh ` G ) ` A ) ) )
21 4 20 ax-mp 
 |-  0 <_ ( normh ` ( ( projh ` G ) ` A ) )
22 8 5 le2sqi 
 |-  ( ( 0 <_ ( normh ` ( ( projh ` H ) ` A ) ) /\ 0 <_ ( normh ` ( ( projh ` G ) ` A ) ) ) -> ( ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) <-> ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) <_ ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) ) )
23 19 21 22 mp2an 
 |-  ( ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) <-> ( ( normh ` ( ( projh ` H ) ` A ) ) ^ 2 ) <_ ( ( normh ` ( ( projh ` G ) ` A ) ) ^ 2 ) )
24 10 17 23 3bitr4i 
 |-  ( 0 <_ ( ( ( ( projh ` G ) ` A ) -h ( ( projh ` H ) ` A ) ) .ih A ) <-> ( normh ` ( ( projh ` H ) ` A ) ) <_ ( normh ` ( ( projh ` G ) ` A ) ) )