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;

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

hence contradiction by A7, A5; :: thesis: verum

end;

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;(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

A7: now :: thesis: not A < 0

assume
A <> 0
; :: thesis: contradictionassume 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;0 <= (A - ((2 * |.(f . (w,v1)).|) * 0)) + ((signnorm (f,w)) * (0 ^2)) by A3, Th43;

hence contradiction by A8; :: thesis: verum

hence contradiction by A7, A5; :: thesis: verum

now :: thesis: not A = 0

hence
contradiction
by A4; :: thesis: verumassume A9:
A = 0
; :: thesis: contradiction

end;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;0 <= (A - ((2 * |.(f . (w,v1)).|) * 1)) + ((signnorm (f,w)) * (1 ^2)) by A3, Th43;

hence contradiction by A1, A9, A11; :: thesis: verum

now :: thesis: not |.(f . (w,v1)).| < 0

hence
contradiction
by A2, A10; :: thesis: verumassume 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;0 <= (A - ((2 * |.(f . (w,v1)).|) * (- 1))) + ((signnorm (f,w)) * ((- 1) ^2)) by A3, Th43;

hence contradiction by A1, A9, A12; :: thesis: verum