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 )