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
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
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
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; :: 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:12;
then A4: Re ([**r,0**] * (a * (f . (w,v1)))) = r * |.(f . (w,v1)).| by A2, Th10;
(a *') * (f . (v1,w)) = (((a *') * (f . (v1,w))) *') *'
.= (((a *') *') * ((f . (v1,w)) *')) *' by COMPLFLD:54
.= (a * (f . (w,v1))) *' by Def5 ;
then A5: Re ([**r,0**] * ((a *') * (f . (v1,w)))) = r * (Re ((a * (f . (w,v1))) *')) by A3, Th10
.= r * |.(f . (w,v1)).| by A2, COMPLEX1:27 ;
( Re [**(r ^2),0**] = r ^2 & Im [**(r ^2),0**] = 0 ) by COMPLEX1:12;
then A6: Re ([**(r ^2),0**] * (f . (w,w))) = (r ^2) * (signnorm (f,w)) by Th10;
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, Th42;
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:10
.= ((Re ((f . (v1,v1)) - ([**r,0**] * (a * (f . (w,v1)))))) - (r * |.(f . (w,v1)).|)) + ((signnorm (f,w)) * (r ^2)) by A5, Th9
.= (((signnorm (f,v1)) - (r * |.(f . (w,v1)).|)) - (r * |.(f . (w,v1)).|)) + ((signnorm (f,w)) * (r ^2)) by A4, Th9
.= ((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