let V be VectSp of F_Complex ; :: thesis: for f being hermitan-Form of V
for v, w being Element of V holds (signnorm f,(v + w)) + (signnorm f,(v - w)) = (2 * (signnorm f,v)) + (2 * (signnorm f,w))
let f be hermitan-Form of V; :: thesis: for v, w being Element of V holds (signnorm f,(v + w)) + (signnorm f,(v - w)) = (2 * (signnorm f,v)) + (2 * (signnorm f,w))
let v1, w be Element of V; :: thesis: (signnorm f,(v1 + w)) + (signnorm f,(v1 - w)) = (2 * (signnorm f,v1)) + (2 * (signnorm f,w))
set v3 = f . v1,v1;
set v4 = f . v1,w;
set w1 = f . w,v1;
set w2 = f . w,w;
set vp = f . (v1 + w),(v1 + w);
set vm = f . (v1 - w),(v1 - w);
set s1 = signnorm f,v1;
set s2 = signnorm f,w;
set sp = signnorm f,(v1 + w);
set sm = signnorm f,(v1 - w);
f . (v1 + w),(v1 + w) = ((f . v1,v1) + (f . v1,w)) + ((f . w,v1) + (f . w,w)) by BILINEAR:29;
then A1: (f . (v1 + w),(v1 + w)) + (f . (v1 - w),(v1 - w)) = (((f . v1,v1) + (f . v1,w)) + ((f . w,v1) + (f . w,w))) + (((f . v1,v1) - (f . v1,w)) - ((f . w,v1) - (f . w,w))) by Th39
.= (((f . v1,v1) + (((f . v1,w) + (f . v1,v1)) - (f . v1,w))) + ((f . w,v1) + (f . w,w))) - ((f . w,v1) - (f . w,w))
.= (((f . v1,v1) + (f . v1,v1)) + ((f . w,v1) + (f . w,w))) - ((f . w,v1) - (f . w,w)) by COMPLFLD:41
.= ((f . v1,v1) + (f . v1,v1)) + (((f . w,v1) + (f . w,w)) - ((f . w,v1) - (f . w,w)))
.= ((f . v1,v1) + (f . v1,v1)) + ((((f . w,v1) + (f . w,w)) - (f . w,v1)) + (f . w,w)) by RLVECT_1:43
.= ((f . v1,v1) + (f . v1,v1)) + ((f . w,w) + (f . w,w)) by COMPLFLD:41 ;
thus (signnorm f,(v1 + w)) + (signnorm f,(v1 - w)) = Re ((f . (v1 + w),(v1 + w)) + (f . (v1 - w),(v1 - w))) by HAHNBAN1:16
.= (Re ((f . v1,v1) + (f . v1,v1))) + (Re ((f . w,w) + (f . w,w))) by A1, HAHNBAN1:16
.= ((Re (f . v1,v1)) + (Re (f . v1,v1))) + (Re ((f . w,w) + (f . w,w))) by HAHNBAN1:16
.= (2 * (Re (f . v1,v1))) + ((Re (f . w,w)) + (Re (f . w,w))) by HAHNBAN1:16
.= (2 * (signnorm f,v1)) + (2 * (signnorm f,w)) ; :: thesis: verum