let V be VectSp of F_Complex ; :: thesis: for v, w being Vector of V

for f being diagReR+0valued hermitan-Form of V holds |.(f . (v,w)).| ^2 <= (signnorm (f,v)) * (signnorm (f,w))

let v1, w be Vector of V; :: thesis: for f being diagReR+0valued hermitan-Form of V holds |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w))

let f be diagReR+0valued hermitan-Form of V; :: thesis: |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w))

set v4 = f . (v1,w);

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), B = |.(f . (w,v1)).|, C = signnorm (f,w) as Real ;

A1: ( C = 0 ^2 implies B ^2 <= A * C ) by Th44;

A2: 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;

A3: ( C > 0 implies B ^2 <= A * C )

.= |.(f . (v1,w)).| by COMPLEX1:53 ;

hence |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w)) by A1, A3, Def7; :: thesis: verum

for f being diagReR+0valued hermitan-Form of V holds |.(f . (v,w)).| ^2 <= (signnorm (f,v)) * (signnorm (f,w))

let v1, w be Vector of V; :: thesis: for f being diagReR+0valued hermitan-Form of V holds |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w))

let f be diagReR+0valued hermitan-Form of V; :: thesis: |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w))

set v4 = f . (v1,w);

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), B = |.(f . (w,v1)).|, C = signnorm (f,w) as Real ;

A1: ( C = 0 ^2 implies B ^2 <= A * C ) by Th44;

A2: 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;

A3: ( C > 0 implies B ^2 <= A * C )

proof

B =
|.((f . (v1,w)) *').|
by Def5
assume A4:
C > 0
; :: thesis: B ^2 <= A * C

(A - ((2 * B) * (B / C))) + (C * ((B / C) ^2)) = (A - ((B * (2 * B)) / C)) + (C * ((B / C) ^2)) by XCMPLX_1:74

.= (A - (((B ^2) * 2) / C)) + (C * ((B / C) ^2))

.= (A - (2 * ((B ^2) / C))) + (C * ((B / C) ^2)) by XCMPLX_1:74

.= (A - (2 * ((B ^2) / C))) + (C * ((B ^2) / (C * C))) by XCMPLX_1:76

.= (A - (2 * ((B ^2) / C))) + ((C * (B ^2)) / (C * C)) by XCMPLX_1:74

.= (A - (2 * ((B ^2) / C))) + ((B ^2) / C) by A4, XCMPLX_1:91

.= A - ((B ^2) / C)

.= ((A * C) - (B ^2)) / C by A4, XCMPLX_1:127 ;

then 0 <= (A * C) - (B ^2) by A2, A4, Th43;

then 0 + (B ^2) <= ((A * C) - (B ^2)) + (B ^2) by XREAL_1:6;

hence B ^2 <= A * C ; :: thesis: verum

end;(A - ((2 * B) * (B / C))) + (C * ((B / C) ^2)) = (A - ((B * (2 * B)) / C)) + (C * ((B / C) ^2)) by XCMPLX_1:74

.= (A - (((B ^2) * 2) / C)) + (C * ((B / C) ^2))

.= (A - (2 * ((B ^2) / C))) + (C * ((B / C) ^2)) by XCMPLX_1:74

.= (A - (2 * ((B ^2) / C))) + (C * ((B ^2) / (C * C))) by XCMPLX_1:76

.= (A - (2 * ((B ^2) / C))) + ((C * (B ^2)) / (C * C)) by XCMPLX_1:74

.= (A - (2 * ((B ^2) / C))) + ((B ^2) / C) by A4, XCMPLX_1:91

.= A - ((B ^2) / C)

.= ((A * C) - (B ^2)) / C by A4, XCMPLX_1:127 ;

then 0 <= (A * C) - (B ^2) by A2, A4, Th43;

then 0 + (B ^2) <= ((A * C) - (B ^2)) + (B ^2) by XREAL_1:6;

hence B ^2 <= A * C ; :: thesis: verum

.= |.(f . (v1,w)).| by COMPLEX1:53 ;

hence |.(f . (v1,w)).| ^2 <= (signnorm (f,v1)) * (signnorm (f,w)) by A1, A3, Def7; :: thesis: verum