let V be VectSp of F_Complex ; :: thesis: for v, w being Vector of V
for f being diagReR+0valued hermitan-Form of V
for r being real number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v)) = |.(f . w,v).| holds
( Re (f . (v - (([**r,0 **] * a) * w)),(v - (([**r,0 **] * a) * w))) = ((signnorm f,v) - ((2 * |.(f . w,v).|) * r)) + ((signnorm f,w) * (r ^2 )) & 0 <= ((signnorm f,v) - ((2 * |.(f . w,v).|) * r)) + ((signnorm f,w) * (r ^2 )) )
let v1, w be Vector of V; :: thesis: for f being diagReR+0valued hermitan-Form of V
for r being real number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| holds
( Re (f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w))) = ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) & 0 <= ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) )
let f be diagReR+0valued hermitan-Form of V; :: thesis: for r being real number
for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| holds
( Re (f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w))) = ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) & 0 <= ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) )
let r be real number ; :: thesis: for a being Element of F_Complex st |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| holds
( Re (f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w))) = ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) & 0 <= ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) )
let a be Element of F_Complex ; :: thesis: ( |.a.| = 1 & Re (a * (f . w,v1)) = |.(f . w,v1).| implies ( Re (f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w))) = ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) & 0 <= ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) ) )
assume that
A1: |.a.| = 1 and
A2: Re (a * (f . w,v1)) = |.(f . w,v1).| ; :: thesis: ( Re (f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w))) = ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) & 0 <= ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) )
set v3 = f . v1,v1;
set v4 = f . v1,w;
set w1 = f . w,v1;
set w2 = f . w,w;
set A = signnorm f,v1;
set B = |.(f . w,v1).|;
set C = signnorm f,w;
A3: ( Re [**r,0 **] = r & Im [**r,0 **] = 0 ) by COMPLEX1:28;
then A4: Re ([**r,0 **] * (a * (f . w,v1))) = r * |.(f . w,v1).| by A2, Th11;
(a *' ) * (f . v1,w) = (((a *' ) * (f . v1,w)) *' ) *'
.= (((a *' ) *' ) * ((f . v1,w) *' )) *' by COMPLFLD:90
.= (a * (f . w,v1)) *' by Def5 ;
then A5: Re ([**r,0 **] * ((a *' ) * (f . v1,w))) = r * (Re ((a * (f . w,v1)) *' )) by A3, Th11
.= r * |.(f . w,v1).| by A2, COMPLEX1:112 ;
( Re [**(r ^2 ),0 **] = r ^2 & Im [**(r ^2 ),0 **] = 0 ) by COMPLEX1:28;
then A6: Re ([**(r ^2 ),0 **] * (f . w,w)) = (r ^2 ) * (signnorm f,w) by Th11;
f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w)) = (((f . v1,v1) - ([**r,0 **] * (a * (f . w,v1)))) - ([**r,0 **] * ((a *' ) * (f . v1,w)))) + ([**(r ^2 ),0 **] * (f . w,w)) by A1, Th45;
then Re (f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w))) = (Re (((f . v1,v1) - ([**r,0 **] * (a * (f . w,v1)))) - ([**r,0 **] * ((a *' ) * (f . v1,w))))) + ((signnorm f,w) * (r ^2 )) by A6, HAHNBAN1:16
.= ((Re ((f . v1,v1) - ([**r,0 **] * (a * (f . w,v1))))) - (r * |.(f . w,v1).|)) + ((signnorm f,w) * (r ^2 )) by A5, Th10
.= (((signnorm f,v1) - (r * |.(f . w,v1).|)) - (r * |.(f . w,v1).|)) + ((signnorm f,w) * (r ^2 )) by A4, Th10
.= ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) ;
hence ( Re (f . (v1 - (([**r,0 **] * a) * w)),(v1 - (([**r,0 **] * a) * w))) = ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) & 0 <= ((signnorm f,v1) - ((2 * |.(f . w,v1).|) * r)) + ((signnorm f,w) * (r ^2 )) ) by Def7; :: thesis: verum