let V be VectSp of F_Complex ; :: thesis: for v, w being Vector of V
for f being hermitan-Form of V holds (((f . v,w) + (f . v,w)) + (f . v,w)) + (f . v,w) = (((f . (v + w),(v + w)) - (f . (v - w),(v - w))) + (i_FC * (f . (v + (i_FC * w)),(v + (i_FC * w))))) - (i_FC * (f . (v - (i_FC * w)),(v - (i_FC * w))))
let v1, w be Vector of V; :: thesis: for f being hermitan-Form of V holds (((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w) = (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w))))
let f be hermitan-Form of V; :: thesis: (((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w) = (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w))))
set v3 = f . v1,v1;
set v4 = f . v1,w;
set w2 = f . w,w;
set w1 = f . w,v1;
A1: f . (v1 + w),(v1 + w) = ((f . v1,v1) + (f . v1,w)) + ((f . w,v1) + (f . w,w)) by BILINEAR:29;
f . (v1 - w),(v1 - w) = ((f . v1,v1) - (f . v1,w)) - ((f . w,v1) - (f . w,w)) by Th39;
then A2: (f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w)) = (((f . v1,v1) + (f . v1,w)) - (((f . v1,v1) - (f . v1,w)) - ((f . w,v1) - (f . w,w)))) + ((f . w,v1) + (f . w,w)) by A1
.= ((((f . v1,v1) + (f . v1,w)) - ((f . v1,v1) - (f . v1,w))) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w)) by RLVECT_1:43
.= ((((f . v1,v1) - ((f . v1,v1) - (f . v1,w))) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w))
.= (((((f . v1,v1) - (f . v1,v1)) + (f . v1,w)) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w)) by RLVECT_1:43
.= ((((0. F_Complex ) + (f . v1,w)) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w)) by RLVECT_1:28
.= (((f . v1,w) + (f . v1,w)) + ((f . w,v1) - (f . w,w))) + ((f . w,v1) + (f . w,w)) by RLVECT_1:def 7
.= ((f . v1,w) + (f . v1,w)) + ((((f . w,v1) - (f . w,w)) + (f . w,w)) + (f . w,v1))
.= ((f . v1,w) + (f . v1,w)) + (((f . w,v1) - ((f . w,w) - (f . w,w))) + (f . w,v1)) by RLVECT_1:43
.= ((f . v1,w) + (f . v1,w)) + (((f . w,v1) - (0. F_Complex )) + (f . w,v1)) by RLVECT_1:28
.= ((f . v1,w) + (f . v1,w)) + ((f . w,v1) + (f . w,v1)) by RLVECT_1:26 ;
f . (v1 + (i_FC * w)),(v1 + (i_FC * w)) = ((f . v1,v1) + ((i_FC *' ) * (f . v1,w))) + ((i_FC * (f . w,v1)) + (i_FC * ((i_FC *' ) * (f . w,w)))) by Th40
.= ((f . v1,v1) + ((i_FC *' ) * (f . v1,w))) + (i_FC * ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) ;
then A3: i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))) = (i_FC * ((f . v1,v1) + ((i_FC *' ) * (f . v1,w)))) + ((i_FC * i_FC ) * ((f . w,v1) + ((i_FC *' ) * (f . w,w))))
.= ((i_FC * (f . v1,v1)) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w))) by COMPLEX1:17, HAHNBAN1:8, VECTSP_6:81 ;
f . (v1 - (i_FC * w)),(v1 - (i_FC * w)) = (f . v1,(v1 - (i_FC * w))) - (f . (i_FC * w),(v1 - (i_FC * w))) by BILINEAR:36
.= ((f . v1,v1) - (f . v1,(i_FC * w))) - (f . (i_FC * w),(v1 - (i_FC * w))) by Th38
.= ((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (f . (i_FC * w),(v1 - (i_FC * w))) by Th30
.= ((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (i_FC * (f . w,(v1 - (i_FC * w)))) by BILINEAR:32
.= ((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (i_FC * ((f . w,v1) - (f . w,(i_FC * w)))) by Th38
.= ((f . v1,v1) - ((i_FC *' ) * (f . v1,w))) - (i_FC * ((f . w,v1) - ((i_FC *' ) * (f . w,w)))) by Th30 ;
then i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w))) = (i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) - (i_FC * (i_FC * ((f . w,v1) - ((i_FC *' ) * (f . w,w))))) by VECTSP_1:43
.= (i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) - ((i_FC * i_FC ) * ((f . w,v1) - ((i_FC *' ) * (f . w,w))))
.= (i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) - (- ((f . w,v1) - ((i_FC *' ) * (f . w,w)))) by HAHNBAN1:8, VECTSP_6:81
.= (i_FC * ((f . v1,v1) - ((i_FC *' ) * (f . v1,w)))) + ((f . w,v1) - ((i_FC *' ) * (f . w,w))) by COMPLFLD:35
.= ((i_FC * (f . v1,v1)) - (i_FC * ((i_FC *' ) * (f . v1,w)))) + ((f . w,v1) - ((i_FC *' ) * (f . w,w))) by VECTSP_1:43
.= ((i_FC * (f . v1,v1)) - (f . v1,w)) + ((f . w,v1) - ((i_FC *' ) * (f . w,w))) by COMPLEX1:17 ;
then (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w)))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w)))) = ((((i_FC * (f . v1,v1)) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((i_FC * (f . v1,v1)) - (f . v1,w))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w))) by A3, RLVECT_1:41
.= ((((i_FC * (f . v1,v1)) + (f . v1,w)) - ((i_FC * (f . v1,v1)) - (f . v1,w))) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
.= (((((f . v1,w) + (i_FC * (f . v1,v1))) - (i_FC * (f . v1,v1))) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w))) by RLVECT_1:43
.= ((((f . v1,w) + ((i_FC * (f . v1,v1)) - (i_FC * (f . v1,v1)))) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w)))
.= ((((f . v1,w) + (0. F_Complex )) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w))) by RLVECT_1:28
.= (((f . v1,w) + (f . v1,w)) - ((f . w,v1) + ((i_FC *' ) * (f . w,w)))) - ((f . w,v1) - ((i_FC *' ) * (f . w,w))) by RLVECT_1:def 7
.= ((f . v1,w) + (f . v1,w)) - (((f . w,v1) + ((i_FC *' ) * (f . w,w))) + ((f . w,v1) - ((i_FC *' ) * (f . w,w)))) by RLVECT_1:41
.= ((f . v1,w) + (f . v1,w)) - (((f . w,v1) + (f . w,v1)) + (((i_FC *' ) * (f . w,w)) - ((i_FC *' ) * (f . w,w))))
.= ((f . v1,w) + (f . v1,w)) - (((f . w,v1) + (f . w,v1)) + (0. F_Complex )) by RLVECT_1:28
.= ((f . v1,w) + (f . v1,w)) - ((f . w,v1) + (f . w,v1)) by RLVECT_1:def 7 ;
then (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w)))) = ((f . v1,w) + (f . v1,w)) + ((((f . w,v1) + (f . w,v1)) + ((f . v1,w) + (f . v1,w))) - ((f . w,v1) + (f . w,v1))) by A2
.= ((f . v1,w) + (f . v1,w)) + ((f . v1,w) + (f . v1,w)) by COMPLFLD:41
.= (((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w) ;
hence (((f . v1,w) + (f . v1,w)) + (f . v1,w)) + (f . v1,w) = (((f . (v1 + w),(v1 + w)) - (f . (v1 - w),(v1 - w))) + (i_FC * (f . (v1 + (i_FC * w)),(v1 + (i_FC * w))))) - (i_FC * (f . (v1 - (i_FC * w)),(v1 - (i_FC * w)))) ; :: thesis: verum