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:28;
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 Th36
.= (((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:12
.= ((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:29
.= ((f . (v1,v1)) + (f . (v1,v1))) + ((f . (w,w)) + (f . (w,w))) by COMPLFLD:12 ;
thus (signnorm (f,(v1 + w))) + (signnorm (f,(v1 - w))) = Re ((f . ((v1 + w),(v1 + w))) + (f . ((v1 - w),(v1 - w)))) by HAHNBAN1:10
.= (Re ((f . (v1,v1)) + (f . (v1,v1)))) + (Re ((f . (w,w)) + (f . (w,w)))) by A1, HAHNBAN1:10
.= ((Re (f . (v1,v1))) + (Re (f . (v1,v1)))) + (Re ((f . (w,w)) + (f . (w,w)))) by HAHNBAN1:10
.= (2 * (Re (f . (v1,v1)))) + ((Re (f . (w,w))) + (Re (f . (w,w)))) by HAHNBAN1:10
.= (2 * (signnorm (f,v1))) + (2 * (signnorm (f,w))) ; :: thesis: verum