let V be VectSp of F_Complex ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 :: thesis: not A <> 0
A5: now :: thesis: not A > 0
assume A6: A > 0 ; :: thesis: 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; :: thesis: verum
end;
A7: now :: thesis: not A < 0
assume A8: A < 0 ; :: thesis: contradiction
0 <= (A - ((2 * |.(f . (w,v1)).|) * 0)) + ((signnorm (f,w)) * (0 ^2)) by A3, Th43;
hence contradiction by A8; :: thesis: verum
end;
assume A <> 0 ; :: thesis: contradiction
hence contradiction by A7, A5; :: thesis: verum
end;
now :: thesis: not A = 0
assume A9: A = 0 ; :: thesis: contradiction
A10: now :: thesis: not 0 < |.(f . (w,v1)).|
assume A11: 0 < |.(f . (w,v1)).| ; :: thesis: contradiction
0 <= (A - ((2 * |.(f . (w,v1)).|) * 1)) + ((signnorm (f,w)) * (1 ^2)) by A3, Th43;
hence contradiction by A1, A9, A11; :: thesis: verum
end;
now :: thesis: not |.(f . (w,v1)).| < 0
assume A12: |.(f . (w,v1)).| < 0 ; :: thesis: contradiction
0 <= (A - ((2 * |.(f . (w,v1)).|) * (- 1))) + ((signnorm (f,w)) * ((- 1) ^2)) by A3, Th43;
hence contradiction by A1, A9, A12; :: thesis: verum
end;
hence contradiction by A2, A10; :: thesis: verum
end;
hence contradiction by A4; :: thesis: verum