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 Th53
.=
(((z5 * 1) / 2) * x) + (((z5 * 1) / 2) * (x *' ))
by A1, Th30
;
A6:
( len (Re x) = len x & len ((Re a) * (Re x)) = len (Re x) )
by Th48, RVSUM_1:147;
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 Th53
.=
(((- ((1 / 2) * <i> )) * z6) * x) - (((- ((1 / 2) * <i> )) * z6) * (x *' ))
by A1, Th43
;
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 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, A7, 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 A4, Th30
.=
(((1 / 2) * (z5 * (x *' ))) - ((1 / 2) * ((z6 * <i> ) * (x *' )))) + (((1 / 2) * (z5 * x)) + ((1 / 2) * ((<i> * z6) * x)))
by A11, 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, A8, A12, A2, Th28
.=
(((((1 / 2) * z5) * x) + (((1 / 2) * z5) * (x *' ))) + ((- ((- ((1 / 2) * <i> )) * z6)) * x)) + (((- ((1 / 2) * <i> )) * z6) * (x *' ))
by A1, A3, A12, 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, A5, A9, A6, A10, A8, Th40
;
A14:
len ((((1 / 2) * <i> ) * z5) * (x *' )) = len (x *' )
by Th3;
A15: (Im a) * (Re x) =
(z6 * (1 / 2)) * (x + (x *' ))
by Th53
.=
(((1 / 2) * z6) * x) + (((1 / 2) * z6) * (x *' ))
by A1, Th30
;
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 Th53
.=
(((- ((1 / 2) * <i> )) * z5) * x) - (((- ((1 / 2) * <i> )) * z5) * (x *' ))
by A1, Th43
;
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 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 A4, Th30
.=
(((- ((1 / 2) * <i> )) * ((- z5) * (x *' ))) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * (x *' )))) + (((- ((1 / 2) * <i> )) * (z5 * x)) + ((- ((1 / 2) * <i> )) * ((<i> * z6) * x)))
by 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 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, A23, A17, A18, A14, A21, Th28
.=
((((1 / 2) * (z6 * x)) + ((1 / 2) * (z6 * (x *' )))) + (((- ((1 / 2) * <i> )) * z5) * x)) + ((((1 / 2) * <i> ) * z5) * (x *' ))
by A1, A23, A17, A20, A18, Th28
.=
(((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, 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 A15, A22, Th54
;
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