let V be VectSp of F_Complex ; for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V st signnorm (f,w) = 0 holds
|.(f . (w,v)).| = 0
let v1, w be Vector of V; for f being diagReR+0valued hermitan-Form of V st signnorm (f,w) = 0 holds
|.(f . (w,v1)).| = 0
let f be diagReR+0valued hermitan-Form of V; ( signnorm (f,w) = 0 implies |.(f . (w,v1)).| = 0 )
set w1 = f . (w,v1);
set A = signnorm (f,v1);
set B = |.(f . (w,v1)).|;
set C = signnorm (f,w);
reconsider A = signnorm (f,v1) as Real ;
assume that
A1:
signnorm (f,w) = 0
and
A2:
|.(f . (w,v1)).| <> 0
; contradiction
A3:
ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * (f . (w,v1))) = |.(f . (w,v1)).| & Im (a * (f . (w,v1))) = 0 )
by Th8;
A4:
now not A <> 0 A5:
now not A > 0 assume A6:
A > 0
;
contradiction(A - ((2 * |.(f . (w,v1)).|) * (A / |.(f . (w,v1)).|))) + ((signnorm (f,w)) * ((A / |.(f . (w,v1)).|) ^2)) =
A - ((A * (2 * |.(f . (w,v1)).|)) / |.(f . (w,v1)).|)
by A1, XCMPLX_1:74
.=
A - (((A * 2) * |.(f . (w,v1)).|) / |.(f . (w,v1)).|)
.=
A - (A + A)
by A2, XCMPLX_1:89
.=
- A
;
hence
contradiction
by A3, A6, Th43;
verum end; assume
A <> 0
;
contradictionhence
contradiction
by A7, A5;
verum end;
now not A = 0 assume A9:
A = 0
;
contradictionhence
contradiction
by A2, A10;
verum end;
hence
contradiction
by A4; verum