Metamath Proof Explorer

Theorem normlem7

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 11-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normlem1.1 
|- S e. CC
normlem1.2 
|- F e. ~H
normlem1.3 
|- G e. ~H
normlem7.4 
|- ( abs ` S ) = 1
Assertion normlem7 
|- ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) <_ ( 2 x. ( ( sqrt ` ( G .ih G ) ) x. ( sqrt ` ( F .ih F ) ) ) )

Proof

Step Hyp Ref Expression
1 normlem1.1 
 |-  S e. CC
2 normlem1.2 
 |-  F e. ~H
3 normlem1.3 
 |-  G e. ~H
4 normlem7.4 
 |-  ( abs ` S ) = 1
5 eqid 
 |-  -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
6 1 2 3 5 normlem2 
 |-  -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. RR
7 1 cjcli 
 |-  ( * ` S ) e. CC
8 2 3 hicli 
 |-  ( F .ih G ) e. CC
9 7 8 mulcli 
 |-  ( ( * ` S ) x. ( F .ih G ) ) e. CC
10 3 2 hicli 
 |-  ( G .ih F ) e. CC
11 1 10 mulcli 
 |-  ( S x. ( G .ih F ) ) e. CC
12 9 11 addcli 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. CC
13 12 negrebi 
 |-  ( -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. RR <-> ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. RR )
14 6 13 mpbi 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. RR
15 14 leabsi 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) <_ ( abs ` ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) )
16 12 absnegi 
 |-  ( abs ` -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) = ( abs ` ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) )
17 15 16 breqtrri 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) <_ ( abs ` -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) )
18 eqid 
 |-  ( G .ih G ) = ( G .ih G )
19 eqid 
 |-  ( F .ih F ) = ( F .ih F )
20 1 2 3 5 18 19 4 normlem6 
 |-  ( abs ` -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) <_ ( 2 x. ( ( sqrt ` ( G .ih G ) ) x. ( sqrt ` ( F .ih F ) ) ) )
21 12 negcli 
 |-  -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) e. CC
22 21 abscli 
 |-  ( abs ` -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) e. RR
23 2re 
 |-  2 e. RR
24 hiidge0 
 |-  ( G e. ~H -> 0 <_ ( G .ih G ) )
25 hiidrcl 
 |-  ( G e. ~H -> ( G .ih G ) e. RR )
26 3 25 ax-mp 
 |-  ( G .ih G ) e. RR
27 26 sqrtcli 
 |-  ( 0 <_ ( G .ih G ) -> ( sqrt ` ( G .ih G ) ) e. RR )
28 3 24 27 mp2b 
 |-  ( sqrt ` ( G .ih G ) ) e. RR
29 hiidge0 
 |-  ( F e. ~H -> 0 <_ ( F .ih F ) )
30 hiidrcl 
 |-  ( F e. ~H -> ( F .ih F ) e. RR )
31 2 30 ax-mp 
 |-  ( F .ih F ) e. RR
32 31 sqrtcli 
 |-  ( 0 <_ ( F .ih F ) -> ( sqrt ` ( F .ih F ) ) e. RR )
33 2 29 32 mp2b 
 |-  ( sqrt ` ( F .ih F ) ) e. RR
34 28 33 remulcli 
 |-  ( ( sqrt ` ( G .ih G ) ) x. ( sqrt ` ( F .ih F ) ) ) e. RR
35 23 34 remulcli 
 |-  ( 2 x. ( ( sqrt ` ( G .ih G ) ) x. ( sqrt ` ( F .ih F ) ) ) ) e. RR
36 14 22 35 letri 
 |-  ( ( ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) <_ ( abs ` -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) /\ ( abs ` -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) ) <_ ( 2 x. ( ( sqrt ` ( G .ih G ) ) x. ( sqrt ` ( F .ih F ) ) ) ) ) -> ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) <_ ( 2 x. ( ( sqrt ` ( G .ih G ) ) x. ( sqrt ` ( F .ih F ) ) ) ) )
37 17 20 36 mp2an 
 |-  ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) ) <_ ( 2 x. ( ( sqrt ` ( G .ih G ) ) x. ( sqrt ` ( F .ih F ) ) ) )