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 )