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 ) |