let a be Element of COMPLEX ; :: thesis: for x being FinSequence of COMPLEX holds
( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
let x be FinSequence of COMPLEX ; :: thesis: ( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
A1: len (x *' ) = len x by Def1;
A2: len (Re x) = len x by Th48;
reconsider z5 = Re a, z6 = Im a as Element of COMPLEX by XCMPLX_0:def 2;
A3: len (((1 / 2) * z5) * x) = len x by Th3;
A4: (Re a) * (Re x) = (z5 * (1 / 2)) * (x + (x *' )) by Th53
.= (((z5 * 1) / 2) * x) + (((z5 * 1) / 2) * (x *' )) by A1, Th30 ;
A5: (Im a) * (Im x) = (z6 * (- ((1 / 2) * <i> ))) * (x - (x *' )) by Th53
.= (((- ((1 / 2) * <i> )) * z6) * x) - (((- ((1 / 2) * <i> )) * z6) * (x *' )) by A1, Th43 ;
A6: len (((1 / 2) * z5) * x) = len x by Th3;
A7: len (((1 / 2) * z5) * (x *' )) = len (x *' ) by Th3;
A8: len ((Re a) * (Re x)) = len (Re x) by EUCLID_2:8;
A9: len (((- ((1 / 2) * <i> )) * z6) * x) = len x by Th3;
A10: len (((- ((1 / 2) * <i> )) * z6) * (x *' )) = len (x *' ) by Th3;
A11: len ((((1 / 2) * <i> ) * z6) * x) = len x by Th3;
A12: len (((((1 / 2) * <i> ) * z6) * x) + (((1 / 2) * z5) * x)) = len ((((1 / 2) * <i> ) * z6) * x) by A6, Th3, Th6;
A13: len ((z5 - (z6 * <i> )) * (x *' )) = len (x *' ) by Th3;
A14: len ((z5 + (<i> * z6)) * x) = len x by Th3;
A15: len (z5 * x) = len x by Th3;
A16: len ((<i> * z6) * x) = len x by Th3;
A17: len (z5 * (x *' )) = len (x *' ) by Th3;
A18: len ((z6 * <i> ) * (x *' )) = len (x *' ) by Th3;
A19: len ((<i> * z6) * (x *' )) = len (x *' ) by Th3;
A20: len ((a * x) *' ) = len (a * x) by Def1;
A21: len (z6 * (x *' )) = len (x *' ) by Th3;
A22: len ((- z5) * (x *' )) = len (x *' ) by Th3;
A23: len (z6 * x) = len x by Th3;
A24: len ((1 / 2) * (z6 * x)) = len (z6 * x) by Th3;
A25: len (((- ((1 / 2) * <i> )) * z5) * x) = len x by Th3;
A26: len ((1 / 2) * (z6 * (x *' ))) = len (z6 * (x *' )) by Th3;
A27: len ((((1 / 2) * <i> ) * z5) * (x *' )) = len (x *' ) by Th3;
A28: len (((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i> )) * z5) * x)) = len ((1 / 2) * (z6 * x)) by A24, A25, Th3, Th6;
A29: len (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *' )))) = len ((1 / 2) * (z6 * x)) by A1, A21, A24, A26, Th3, Th6;
A30: len (- ((a * x) *' )) = len ((a * x) *' ) by Th5;
A31: Re (a * x) = (1 / 2) * (((a *' ) * (x *' )) + (a * x)) by Th17
.= (1 / 2) * (((a *' ) * (x *' )) + ((z5 + (<i> * z6)) * x)) by COMPLEX1:29
.= (1 / 2) * (((z5 - (z6 * <i> )) * (x *' )) + ((z5 + (<i> * z6)) * x)) by COMPLEX1:def 15
.= ((1 / 2) * ((z5 - (z6 * <i> )) * (x *' ))) + ((1 / 2) * ((z5 + (<i> * z6)) * x)) by A1, A13, A14, Th30
.= ((1 / 2) * ((z5 - (z6 * <i> )) * (x *' ))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x))) by Th63
.= ((1 / 2) * ((z5 * (x *' )) - ((z6 * <i> ) * (x *' )))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x))) by Th64
.= ((1 / 2) * ((z5 * (x *' )) - ((z6 * <i> ) * (x *' )))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x))) by A15, A16, Th30
.= (((1 / 2) * (z5 * (x *' ))) - ((1 / 2) * ((z6 * <i> ) * (x *' )))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x))) by A17, A18, Th43
.= (((1 / 2) * (z5 * (x *' ))) - ((1 / 2) * ((<i> * z6) * (x *' )))) + (((1 / 2) * (z5 * x)) + (((1 / 2) * (<i> * z6)) * x)) by Th53
.= (((1 / 2) * (z5 * (x *' ))) + (- ((((1 / 2) * <i> ) * z6) * (x *' )))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i> ) * z6) * x)) by Th53
.= (((1 / 2) * (z5 * (x *' ))) + ((- (((1 / 2) * <i> ) * z6)) * (x *' ))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i> ) * z6) * x)) by Th54
.= ((((1 / 2) * z5) * (x *' )) + (((- ((1 / 2) * <i> )) * z6) * (x *' ))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i> ) * z6) * x)) by Th53
.= ((((1 / 2) * z5) * x) + ((((1 / 2) * <i> ) * z6) * x)) + ((((1 / 2) * z5) * (x *' )) + (((- ((1 / 2) * <i> )) * z6) * (x *' ))) by Th53
.= ((((((1 / 2) * <i> ) * z6) * x) + (((1 / 2) * z5) * x)) + (((1 / 2) * z5) * (x *' ))) + (((- ((1 / 2) * <i> )) * z6) * (x *' )) by A1, A7, A10, A11, A12, Th28
.= (((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *' ))) + ((- ((- ((1 / 2) * <i> )) * z6)) * x)) + (((- ((1 / 2) * <i> )) * z6) * (x *' )) by A1, A3, A7, A11, Th28
.= (((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *' ))) - (((- ((1 / 2) * <i> )) * z6) * x)) + (((- ((1 / 2) * <i> )) * z6) * (x *' )) by Th54
.= ((Re a) * (Re x)) - ((Im a) * (Im x)) by A1, A2, A4, A8, A9, A10, Th40, A5 ;
A32: (Im a) * (Re x) = (z6 * (1 / 2)) * (x + (x *' )) by Th53
.= (((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *' )) by A1, Th30 ;
A33: (Re a) * (Im x) = (z5 * (- ((1 / 2) * <i> ))) * (x - (x *' )) by Th53
.= (((- ((1 / 2) * <i> )) * z5) * x) - (((- ((1 / 2) * <i> )) * z5) * (x *' )) by A1, Th43 ;
Im (a * x) = ((- ((1 / 2) * <i> )) * (- ((a * x) *' ))) + ((- ((1 / 2) * <i> )) * (a * x)) by A20, A30, Th30
.= ((- ((1 / 2) * <i> )) * (- ((a *' ) * (x *' )))) + ((- ((1 / 2) * <i> )) * (a * x)) by Th17
.= ((- ((1 / 2) * <i> )) * (- ((a *' ) * (x *' )))) + ((- ((1 / 2) * <i> )) * ((z5 + (<i> * z6)) * x)) by COMPLEX1:29
.= ((- ((1 / 2) * <i> )) * (- ((z5 - (z6 * <i> )) * (x *' )))) + ((- ((1 / 2) * <i> )) * ((z5 + (<i> * z6)) * x)) by COMPLEX1:def 15
.= ((- ((1 / 2) * <i> )) * ((- (z5 - (z6 * <i> ))) * (x *' ))) + ((- ((1 / 2) * <i> )) * ((z5 + (<i> * z6)) * x)) by Th54
.= ((- ((1 / 2) * <i> )) * (((- z5) + (z6 * <i> )) * (x *' ))) + ((- ((1 / 2) * <i> )) * ((z5 + (<i> * z6)) * x))
.= ((- ((1 / 2) * <i> )) * (((- z5) * (x *' )) + ((<i> * z6) * (x *' )))) + ((- ((1 / 2) * <i> )) * ((z5 + (<i> * z6)) * x)) by Th63
.= ((- ((1 / 2) * <i> )) * (((- z5) * (x *' )) + ((<i> * z6) * (x *' )))) + ((- ((1 / 2) * <i> )) * ((z5 * x) + ((<i> * z6) * x))) by Th63
.= ((- ((1 / 2) * <i> )) * (((- z5) * (x *' )) + ((<i> * z6) * (x *' )))) + (((- ((1 / 2) * <i> )) * (z5 * x)) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * x))) by A15, A16, Th30
.= (((- ((1 / 2) * <i> )) * ((- z5) * (x *' ))) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * (x *' )))) + (((- ((1 / 2) * <i> )) * (z5 * x)) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * x))) by A19, A22, Th30
.= ((((- ((1 / 2) * <i> )) * (- z5)) * (x *' )) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * (x *' )))) + (((- ((1 / 2) * <i> )) * (z5 * x)) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i> )) * (- z5)) * (x *' )) + ((- ((1 / 2) * <i> )) * (<i> * (z6 * (x *' ))))) + (((- ((1 / 2) * <i> )) * (z5 * x)) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i> )) * (- z5)) * (x *' )) + (((- ((1 / 2) * <i> )) * <i> ) * (z6 * (x *' )))) + (((- ((1 / 2) * <i> )) * (z5 * x)) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i> )) * (- z5)) * (x *' )) + (((- ((1 / 2) * <i> )) * <i> ) * (z6 * (x *' )))) + ((((- ((1 / 2) * <i> )) * z5) * x) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * x))) by Th53
.= ((((- ((1 / 2) * <i> )) * (- z5)) * (x *' )) + (((- ((1 / 2) * <i> )) * <i> ) * (z6 * (x *' )))) + ((((- ((1 / 2) * <i> )) * z5) * x) + ((- ((1 / 2) * <i> )) * (<i> * (z6 * x)))) by Th53
.= (((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i> )) * z5) * x)) + (((1 / 2) * (z6 * (x *' ))) + ((((1 / 2) * <i> ) * z5) * (x *' ))) by Th53
.= ((((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i> )) * z5) * x)) + ((1 / 2) * (z6 * (x *' )))) + ((((1 / 2) * <i> ) * z5) * (x *' )) by A1, A21, A23, A24, A26, A27, A28, Th28
.= ((((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *' )))) + (((- ((1 / 2) * <i> )) * z5) * x)) + ((((1 / 2) * <i> ) * z5) * (x *' )) by A1, A21, A23, A24, A25, A26, Th28
.= (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *' )))) + ((((- ((1 / 2) * <i> )) * z5) * x) + ((((1 / 2) * <i> ) * z5) * (x *' ))) by A1, A23, A24, A25, A27, A29, Th28
.= ((((1 / 2) * z6) * x) + ((1 / 2) * (z6 * (x *' )))) + ((((- ((1 / 2) * <i> )) * z5) * x) + ((((1 / 2) * <i> ) * z5) * (x *' ))) by Th53
.= ((((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *' ))) + ((((- ((1 / 2) * <i> )) * z5) * x) + ((- ((- ((1 / 2) * <i> )) * z5)) * (x *' ))) by Th53
.= ((Im a) * (Re x)) + ((Re a) * (Im x)) by Th54, A32, A33 ;
hence ( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) ) by A31; :: thesis: verum