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

Metamath Proof Explorer

Theorem normlem5

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

Ref Expression
Hypotheses normlem1.1 
|- S e. CC
normlem1.2 
|- F e. ~H
normlem1.3 
|- G e. ~H
normlem2.4 
|- B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
normlem3.5 
|- A = ( G .ih G )
normlem3.6 
|- C = ( F .ih F )
normlem4.7 
|- R e. RR
normlem4.8 
|- ( abs ` S ) = 1
Assertion normlem5 
|- 0 <_ ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C )

Proof

Step Hyp Ref Expression
1 normlem1.1 
 |-  S e. CC
2 normlem1.2 
 |-  F e. ~H
3 normlem1.3 
 |-  G e. ~H
4 normlem2.4 
 |-  B = -u ( ( ( * ` S ) x. ( F .ih G ) ) + ( S x. ( G .ih F ) ) )
5 normlem3.5 
 |-  A = ( G .ih G )
6 normlem3.6 
 |-  C = ( F .ih F )
7 normlem4.7 
 |-  R e. RR
8 normlem4.8 
 |-  ( abs ` S ) = 1
9 7 recni 
 |-  R e. CC
10 1 9 mulcli 
 |-  ( S x. R ) e. CC
11 10 3 hvmulcli 
 |-  ( ( S x. R ) .h G ) e. ~H
12 2 11 hvsubcli 
 |-  ( F -h ( ( S x. R ) .h G ) ) e. ~H
13 hiidge0 
 |-  ( ( F -h ( ( S x. R ) .h G ) ) e. ~H -> 0 <_ ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) ) )
14 12 13 ax-mp 
 |-  0 <_ ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) )
15 1 2 3 4 5 6 7 8 normlem4 
 |-  ( ( F -h ( ( S x. R ) .h G ) ) .ih ( F -h ( ( S x. R ) .h G ) ) ) = ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C )
16 14 15 breqtri 
 |-  0 <_ ( ( ( A x. ( R ^ 2 ) ) + ( B x. R ) ) + C )