let a be Element of COMPLEX ; 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 ; ( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
reconsider z5 = Re a, z6 = Im a as Element of COMPLEX by XCMPLX_0:def 2;
A1:
len (x *') = len x
by Def1;
len (((1 / 2) * z5) * x) = len x
by Th3;
then A2:
len (((((1 / 2) * <i>) * z6) * x) + (((1 / 2) * z5) * x)) = len ((((1 / 2) * <i>) * z6) * x)
by Th3, Th6;
A3:
len (((1 / 2) * z5) * x) = len x
by Th3;
A4:
( len (z5 * x) = len x & len ((<i> * z6) * x) = len x )
by Th3;
A5: (Re a) * (Re x) =
(z5 * (1 / 2)) * (x + (x *'))
by Th44
.=
(((z5 * 1) / 2) * x) + (((z5 * 1) / 2) * (x *'))
by A1, Th25
;
A6:
( len (Re x) = len x & len ((Re a) * (Re x)) = len (Re x) )
by Th40, RVSUM_1:117;
A7:
( len ((z5 - (z6 * <i>)) * (x *')) = len (x *') & len ((z5 + (<i> * z6)) * x) = len x )
by Th3;
A8:
len (((- ((1 / 2) * <i>)) * z6) * (x *')) = len (x *')
by Th3;
A9: (Im a) * (Im x) =
(z6 * (- ((1 / 2) * <i>))) * (x - (x *'))
by Th44
.=
(((- ((1 / 2) * <i>)) * z6) * x) - (((- ((1 / 2) * <i>)) * z6) * (x *'))
by A1, Th36
;
A10:
len (((- ((1 / 2) * <i>)) * z6) * x) = len x
by Th3;
A11:
( len (z5 * (x *')) = len (x *') & len ((z6 * <i>) * (x *')) = len (x *') )
by Th3;
A12:
( len (((1 / 2) * z5) * (x *')) = len (x *') & len ((((1 / 2) * <i>) * z6) * x) = len x )
by Th3;
A13: Re (a * x) =
(1 / 2) * (((a *') * (x *')) + (a * x))
by Th13
.=
(1 / 2) * (((a *') * (x *')) + ((z5 + (<i> * z6)) * x))
by COMPLEX1:13
.=
(1 / 2) * (((z5 - (z6 * <i>)) * (x *')) + ((z5 + (<i> * z6)) * x))
by COMPLEX1:def 11
.=
((1 / 2) * ((z5 - (z6 * <i>)) * (x *'))) + ((1 / 2) * ((z5 + (<i> * z6)) * x))
by A7, Th25, Def1
.=
((1 / 2) * ((z5 - (z6 * <i>)) * (x *'))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x)))
by Th52
.=
((1 / 2) * ((z5 * (x *')) - ((z6 * <i>) * (x *')))) + ((1 / 2) * ((z5 * x) + ((<i> * z6) * x)))
by Th53
.=
((1 / 2) * ((z5 * (x *')) - ((z6 * <i>) * (x *')))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x)))
by A4, Th25
.=
(((1 / 2) * (z5 * (x *'))) - ((1 / 2) * ((z6 * <i>) * (x *')))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x)))
by A11, Th36
.=
(((1 / 2) * (z5 * (x *'))) - ((1 / 2) * ((<i> * z6) * (x *')))) + (((1 / 2) * (z5 * x)) + (((1 / 2) * (<i> * z6)) * x))
by Th44
.=
(((1 / 2) * (z5 * (x *'))) + (- ((((1 / 2) * <i>) * z6) * (x *')))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x))
by Th44
.=
(((1 / 2) * (z5 * (x *'))) + ((- (((1 / 2) * <i>) * z6)) * (x *'))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x))
by Th45
.=
((((1 / 2) * z5) * (x *')) + (((- ((1 / 2) * <i>)) * z6) * (x *'))) + (((1 / 2) * (z5 * x)) + ((((1 / 2) * <i>) * z6) * x))
by Th44
.=
((((1 / 2) * z5) * x) + ((((1 / 2) * <i>) * z6) * x)) + ((((1 / 2) * z5) * (x *')) + (((- ((1 / 2) * <i>)) * z6) * (x *')))
by Th44
.=
((((((1 / 2) * <i>) * z6) * x) + (((1 / 2) * z5) * x)) + (((1 / 2) * z5) * (x *'))) + (((- ((1 / 2) * <i>)) * z6) * (x *'))
by A1, A8, A12, A2, Th24
.=
(((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *'))) + ((- ((- ((1 / 2) * <i>)) * z6)) * x)) + (((- ((1 / 2) * <i>)) * z6) * (x *'))
by A1, A3, A12, Th24
.=
(((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *'))) - (((- ((1 / 2) * <i>)) * z6) * x)) + (((- ((1 / 2) * <i>)) * z6) * (x *'))
by Th45
.=
((Re a) * (Re x)) - ((Im a) * (Im x))
by A1, A5, A9, A6, A10, A8, Th33
;
A14:
len ((((1 / 2) * <i>) * z5) * (x *')) = len (x *')
by Th3;
A15: (Im a) * (Re x) =
(z6 * (1 / 2)) * (x + (x *'))
by Th44
.=
(((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *'))
by A1, Th25
;
A16:
( len ((<i> * z6) * (x *')) = len (x *') & len ((- z5) * (x *')) = len (x *') )
by Th3;
A17:
len ((1 / 2) * (z6 * x)) = len (z6 * x)
by Th3;
A18:
( len (z6 * (x *')) = len (x *') & len ((1 / 2) * (z6 * (x *'))) = len (z6 * (x *')) )
by Th3;
then A19:
len (((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) = len ((1 / 2) * (z6 * x))
by A1, A17, Th3, Th6;
A20:
len (((- ((1 / 2) * <i>)) * z5) * x) = len x
by Th3;
then A21:
len (((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) = len ((1 / 2) * (z6 * x))
by A17, Th3, Th6;
A22: (Re a) * (Im x) =
(z5 * (- ((1 / 2) * <i>))) * (x - (x *'))
by Th44
.=
(((- ((1 / 2) * <i>)) * z5) * x) - (((- ((1 / 2) * <i>)) * z5) * (x *'))
by A1, Th36
;
A23:
len (z6 * x) = len x
by Th3;
( len ((a * x) *') = len (a * x) & len (- ((a * x) *')) = len ((a * x) *') )
by Def1, Th5;
then Im (a * x) =
((- ((1 / 2) * <i>)) * (- ((a * x) *'))) + ((- ((1 / 2) * <i>)) * (a * x))
by Th25
.=
((- ((1 / 2) * <i>)) * (- ((a *') * (x *')))) + ((- ((1 / 2) * <i>)) * (a * x))
by Th13
.=
((- ((1 / 2) * <i>)) * (- ((a *') * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x))
by COMPLEX1:13
.=
((- ((1 / 2) * <i>)) * (- ((z5 - (z6 * <i>)) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x))
by COMPLEX1:def 11
.=
((- ((1 / 2) * <i>)) * ((- (z5 - (z6 * <i>))) * (x *'))) + ((- ((1 / 2) * <i>)) * ((z5 + (<i> * z6)) * x))
by Th45
.=
((- ((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 Th52
.=
((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + ((- ((1 / 2) * <i>)) * ((z5 * x) + ((<i> * z6) * x)))
by Th52
.=
((- ((1 / 2) * <i>)) * (((- z5) * (x *')) + ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x)))
by A4, Th25
.=
(((- ((1 / 2) * <i>)) * ((- z5) * (x *'))) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x)))
by A16, Th25
.=
((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x)))
by Th44
.=
((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + ((- ((1 / 2) * <i>)) * (<i> * (z6 * (x *'))))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x)))
by Th44
.=
((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + (((- ((1 / 2) * <i>)) * (z5 * x)) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x)))
by Th44
.=
((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((1 / 2) * <i>)) * ((<i> * z6) * x)))
by Th44
.=
((((- ((1 / 2) * <i>)) * (- z5)) * (x *')) + (((- ((1 / 2) * <i>)) * <i>) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((1 / 2) * <i>)) * (<i> * (z6 * x))))
by Th44
.=
(((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) + (((1 / 2) * (z6 * (x *'))) + ((((1 / 2) * <i>) * z5) * (x *')))
by Th44
.=
((((1 / 2) * (z6 * x)) + (((- ((1 / 2) * <i>)) * z5) * x)) + ((1 / 2) * (z6 * (x *')))) + ((((1 / 2) * <i>) * z5) * (x *'))
by A1, A23, A17, A18, A14, A21, Th24
.=
((((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) + (((- ((1 / 2) * <i>)) * z5) * x)) + ((((1 / 2) * <i>) * z5) * (x *'))
by A1, A23, A17, A20, A18, Th24
.=
(((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((((1 / 2) * <i>) * z5) * (x *')))
by A1, A23, A17, A20, A14, A19, Th24
.=
((((1 / 2) * z6) * x) + ((1 / 2) * (z6 * (x *')))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((((1 / 2) * <i>) * z5) * (x *')))
by Th44
.=
((((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *'))) + ((((- ((1 / 2) * <i>)) * z5) * x) + ((- ((- ((1 / 2) * <i>)) * z5)) * (x *')))
by Th44
.=
((Im a) * (Re x)) + ((Re a) * (Im x))
by A15, A22, Th45
;
hence
( Re (a * x) = ((Re a) * (Re x)) - ((Im a) * (Im x)) & Im (a * x) = ((Im a) * (Re x)) + ((Re a) * (Im x)) )
by A13; verum