:: The Inner Product and Conjugate of Finite Sequences of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 25, 2005
:: Copyright (c) 2005-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, ARYTM_3, NAT_1, XXREAL_0,
FUNCT_1, RELAT_1, TARSKI, BINOP_2, FUNCOP_1, ARYTM_1, XCMPLX_0, CARD_1,
COMPLEX1, RVSUM_1, REAL_1, ZFMISC_1, VALUED_0;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, PARTFUN1, BINOP_1, FUNCOP_1,
FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, SEQ_4, COMPLEX1, RVSUM_1,
FINSEQ_2, BINOP_2, MATRIX_5, XXREAL_0, COMSEQ_2;
constructors SETWISEO, REAL_1, BINOP_2, FINSEQOP, SEQ_4, MATRIX_5, BINOP_1,
RVSUM_1, RELSET_1, COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
BINOP_2, MEMBERED, FINSEQ_2, VALUED_0, VALUED_1, XREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
equalities VALUED_1, ORDINAL1;
expansions FINSEQ_1;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, FINSEQOP, RELAT_1,
BINOP_2, COMPLEX1, XCMPLX_0, FINSEQ_3, RVSUM_1, ORDINAL1, VALUED_0,
VALUED_1, SEQ_4, CARD_1, XREAL_0, COMSEQ_2;
begin :: Preliminaries
reserve i,j for Element of NAT,
x,y,z for FinSequence of COMPLEX,
c for Element of COMPLEX,
R,R1,R2 for Element of i-tuples_on COMPLEX;
definition let z be FinSequence of COMPLEX;
redefine func z*' -> FinSequence of COMPLEX means :Def1:
len it = len z & for i being Nat st 1<=i & i<=len z holds it.i = (z.i)*';
coherence
proof
set f = z*';
A1: dom f = dom z by COMSEQ_2:def 1;
ex n being Nat st dom z = Seg n by FINSEQ_1:def 2;
then
A2: f is FinSequence by A1,FINSEQ_1:def 2;
rng f c= COMPLEX
proof
let y be object;
thus thesis by XCMPLX_0:def 2;
end;
hence thesis by A2, FINSEQ_1:def 4;
end;
compatibility
proof
let IT be FinSequence of COMPLEX;
thus IT = z*' implies
len IT = len z & for i being Nat st 1<=i & i<=len z holds IT.i = (z.i)*'
proof
assume
A3: IT = z*';
then dom IT = dom z by COMSEQ_2:def 1;
hence thesis by A3,COMSEQ_2:def 1,FINSEQ_3:25,29;
end;
assume that
A4: len IT = len z and
A5: for i being Nat st 1<=i & i<=len z holds IT.i = (z.i)*';
A6: dom IT = dom z by A4,FINSEQ_3:29;
now
let i be set;
assume
A7: i in dom IT;
then reconsider j = i as Nat;
1 <= j & j <= len z by A4,A7,FINSEQ_3:25;
hence IT.i = (z.i)*' by A5;
end;
hence IT = z*' by A6,COMSEQ_2:def 1;
end;
end;
Lm1: c*x = (multcomplex[;](c,id COMPLEX))*x
proof
c multcomplex = multcomplex[;](c,id COMPLEX) by SEQ_4:def 4;
hence thesis by SEQ_4:def 9;
end;
theorem
i in dom (x+y) implies (x+y).i = x.i + y.i by VALUED_1:def 1;
theorem
i in dom (x-y) implies (x-y).i = x.i - y.i by VALUED_1:13;
definition let i,R1,R2;
redefine func R1 - R2 -> Element of i-tuples_on COMPLEX;
coherence
proof
R1 - R2 = diffcomplex.:(R1,R2) by SEQ_4:def 7;
hence thesis by FINSEQ_2:120;
end;
end;
definition let i,R1,R2;
redefine func R1 + R2 -> Element of i-tuples_on COMPLEX;
coherence
proof
R1 + R2 = addcomplex.:(R1,R2) by SEQ_4:def 6;
hence thesis by FINSEQ_2:120;
end;
end;
definition let i, R;
let r be Complex;
redefine func r*R -> Element of i-tuples_on COMPLEX;
coherence
proof
reconsider q = r as Element of COMPLEX by XCMPLX_0:def 2;
q*R = (multcomplex[;](q,id COMPLEX))*R by Lm1;
hence thesis by FINSEQ_2:113;
end;
end;
theorem Th3:
for a being Complex, x being FinSequence of COMPLEX holds
len (a*x)=len x
proof
let a be Complex, x be FinSequence of COMPLEX;
set n=len x;
reconsider z=x as Element of n-tuples_on COMPLEX by FINSEQ_2:92;
reconsider a9 = a as Element of COMPLEX by XCMPLX_0:def 2;
len (a9*z)=n by CARD_1:def 7;
hence thesis;
end;
theorem
for x being complex-valued FinSequence holds dom x = dom -x by VALUED_1:8;
theorem Th5:
for x being complex-valued FinSequence holds len (-x)=len x
proof
let x be complex-valued FinSequence;
dom (-x)=dom x by VALUED_1:8;
hence thesis by FINSEQ_3:29;
end;
Lm2: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
proof
let F be complex-valued FinSequence;
rng F c= COMPLEX by VALUED_0:def 1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th6:
for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
len (x1+x2)=len x1
proof
let x1,x2 be complex-valued FinSequence;
set n=len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
x1 is FinSequence of COMPLEX by Lm2; then
reconsider z1=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
assume len x1=len x2; then
reconsider z2=x2 as Element of n-tuples_on COMPLEX by A1,FINSEQ_2:92;
dom (z1+z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th7:
for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
len (x1-x2)=len x1
proof
let x1,x2 be complex-valued FinSequence;
set n=len x1;
A1: x2 is FinSequence of COMPLEX by Lm2;
x1 is FinSequence of COMPLEX by Lm2; then
reconsider z1=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
assume len x1=len x2; then
reconsider z2=x2 as Element of n-tuples_on COMPLEX by A1,FINSEQ_2:92;
dom (z1-z2)=Seg n by FINSEQ_2:124;
hence thesis by FINSEQ_1:def 3;
end;
theorem
for f being complex-valued FinSequence holds f is Element of COMPLEX len f
proof
let f be complex-valued FinSequence;
f is FinSequence of COMPLEX by Lm2; then
f is Element of COMPLEX* by FINSEQ_1:def 11;
then f in { s where s is Element of COMPLEX*: len s = len f };
then f in ((len f)-tuples_on COMPLEX) by FINSEQ_2:def 4;
hence thesis by SEQ_4:def 11;
end;
::$CT 4
theorem Th9:
for x being FinSequence of COMPLEX holds (-x).i = -x.i
proof
let x be FinSequence of COMPLEX;
per cases;
suppose
A1: not i in dom -x; then
A2: not i in dom x by VALUED_1:8;
thus (-x).i = -0 by A1,FUNCT_1:def 2
.= -x.i by A2,FUNCT_1:def 2;
end;
suppose
A3: i in dom -x;
set r = x.i;
-x = compcomplex*x by SEQ_4:def 8;
then (-x).i = compcomplex.r by A3,FUNCT_1:12;
hence thesis by BINOP_2:def 1;
end;
end;
definition let i,R;
redefine func -R -> Element of i-tuples_on COMPLEX;
coherence
proof
-R = compcomplex*R by SEQ_4:def 8;
hence thesis by FINSEQ_2:113;
end;
end;
theorem
c = R.j implies (-R).j = -c by Th9;
theorem Th11:
for a being Complex holds dom(a*x) = dom x
proof
let a be Complex;
dom(a multcomplex) = COMPLEX by FUNCT_2:def 1;
then rng x c= dom(a multcomplex) by FINSEQ_1:def 4;
hence dom x = dom((a multcomplex)*x) by RELAT_1:27
.= dom(a*x) by SEQ_4:def 9;
end;
theorem Th12:
for i being Nat, a being Complex holds (a*x).i = a*(x.i)
proof
let i be Nat, a be Complex;
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
per cases;
suppose
A1: not i in dom (a*x); then
A2: not i in dom x by Th11;
thus (a*x).i = a*0 by A1,FUNCT_1:def 2
.= a*(x.i) by A2,FUNCT_1:def 2;
end;
suppose
A3: i in dom (a*x);
set a9 = x.i;
A4: a*x = (multcomplex[;](aa,id COMPLEX))*x by Lm1; then
A5: a9 in dom(multcomplex[;](aa,id COMPLEX)) by A3,FUNCT_1:11;
thus (a*x).i = (multcomplex[;](aa,id COMPLEX)).a9 by A3,A4,FUNCT_1:12
.= multcomplex.(a,(id COMPLEX).a9) by A5,FUNCOP_1:32
.= a*(x.i) by BINOP_2:def 5;
end;
end;
theorem Th13:
for a being Complex holds (a*x)*' = a*'*(x*')
proof
let a be Complex;
reconsider aa = a as Element of COMPLEX by XCMPLX_0:def 2;
len (a*'*(x*')) = len (x*') by Th3; then
A1: len (a*'*(x*')) = len x by Def1;
A2: len (a*x) = len x by Th3;
A3: now
let i be Nat;
assume that
A4: 1 <= i and
A5: i <= len ((a*x)*');
A6: i <= len (a*x) by A5,Def1;
hence (a*x)*'.i = (((a*x).i)*') by A4,Def1
.= (aa*(x.i))*' by Th12
.= aa*'*(x.i)*' by COMPLEX1:35
.= a*'*((x*').i) by A2,A4,A6,Def1
.= (a*'*(x*')).i by Th12;
end;
len ((a*x)*') = len (a*x) by Def1;
hence thesis by A1,A3,Th3;
end;
theorem Th14:
(R1+R2).j = R1.j + R2.j
proof
per cases;
suppose
A1: not j in Seg i; then
A2: not j in dom R2 by FINSEQ_2:124;
A3: not j in dom R1 by A1,FINSEQ_2:124;
not j in dom(R1+R2) by A1,FINSEQ_2:124;
hence (R1+R2).j = 0+0 by FUNCT_1:def 2
.= R1.j + 0 by A3,FUNCT_1:def 2
.= R1.j + R2.j by A2,FUNCT_1:def 2;
end;
suppose j in Seg i;
then j in dom (R1 + R2) by FINSEQ_2:124;
hence thesis by VALUED_1:def 1;
end;
end;
theorem Th15:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
(x1 + x2)*' = x1*' + x2*'
proof
let x1,x2 be FinSequence of COMPLEX;
reconsider x9=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=x2 as Element of (len x2)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x3=x1*' as Element of (len (x1*'))-tuples_on COMPLEX by
FINSEQ_2:92;
reconsider x4=x2*' as Element of (len (x2*'))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A1: len x1=len x2; then
A2: len (x1 + x2) = len x1 by Th6;
A3: len x1=len (x1*') & len x2=len (x2*') by Def1;
A4: now
let i be Nat;
A5: i in NAT by ORDINAL1:def 12;
assume that
A6: 1 <= i and
A7: i <= len ((x1 + x2)*');
A8: i <= len (x1 + x2) by A7,Def1;
hence (x1 + x2)*'.i = (((x1 + x2).i)*') by A6,Def1
.= (x9.i + y9.i)*' by A1,A5,Th14
.= (x1.i)*'+(x2.i)*' by COMPLEX1:32
.= ((x1*').i)+(x2.i)*' by A2,A6,A8,Def1
.= ((x1*').i)+((x2*').i) by A1,A2,A6,A8,Def1
.= (x3+x4).i by A1,A3,A5,Th14;
end;
len (x1*' + x2*') = len x1 by A1,A3,Th6;
hence thesis by A4,A2,Def1;
end;
theorem Th16:
(R1-R2).j = R1.j - R2.j
proof
per cases;
suppose
A1: not j in Seg i; then
A2: not j in dom R2 by FINSEQ_2:124;
A3: not j in dom R1 by A1,FINSEQ_2:124;
not j in dom(R1-R2) by A1,FINSEQ_2:124;
hence (R1-R2).j = 0-0 by FUNCT_1:def 2
.= R1.j - 0 by A3,FUNCT_1:def 2
.= R1.j - R2.j by A2,FUNCT_1:def 2;
end;
suppose
j in Seg i;
then j in dom (R1 - R2) by FINSEQ_2:124;
hence thesis by VALUED_1:13;
end;
end;
theorem Th17:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
(x1 - x2)*' = x1*' - x2*'
proof
let x1,x2 be FinSequence of COMPLEX;
reconsider x9=x1 as Element of (len x1)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=x2 as Element of (len x2)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x3=x1*' as Element of (len (x1*'))-tuples_on COMPLEX by
FINSEQ_2:92;
reconsider x4=x2*' as Element of (len (x2*'))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A1: len x1=len x2; then
A2: len (x1 - x2) = len x1 by Th7;
A3: len x1=len (x1*') & len x2=len (x2*') by Def1;
A4: now
let i be Nat;
A5: i in NAT by ORDINAL1:def 12;
assume that
A6: 1 <= i and
A7: i <= len ((x1 - x2)*');
A8: i <= len (x1 - x2) by A7,Def1;
hence (x1 - x2)*'.i = (((x1 - x2).i)*') by A6,Def1
.= (x9.i - y9.i)*' by A1,A5,Th16
.= (x1.i)*'-(x2.i)*' by COMPLEX1:34
.= ((x1*').i)-(x2.i)*' by A2,A6,A8,Def1
.= ((x1*').i)-((x2*').i) by A1,A2,A6,A8,Def1
.= (x3-x4).i by A1,A3,A5,Th16;
end;
len (x1*' - x2*') = len x1 by A1,A3,Th7;
hence thesis by A4,A2,Def1;
end;
theorem
for z being FinSequence of COMPLEX holds (z*')*' = z;
theorem
for z being FinSequence of COMPLEX holds (-z)*' = -(z*')
proof
let z be FinSequence of COMPLEX;
thus (-z)*'= ((-1r)*')*(z*') by Th13,COMPLEX1:def 4
.= -z*' by COMPLEX1:30,33,def 4;
end;
theorem Th20:
for z being Complex holds z+z*' = 2*(Re z)
proof
let z be Complex;
z+z*'=Re z + Re (z*')+(Im z + Im (z*'))** by COMPLEX1:81
.=Re z + Re (z*')+(Im z + -Im z)*** by COMPLEX1:27
.=Re z + Re z by COMPLEX1:27
.=2*(Re z);
hence thesis;
end;
theorem Th21:
for x,y being complex-valued FinSequence st len x=len y holds
(x-y).i = x.i - y.i
proof
let x,y be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & y is FinSequence of COMPLEX by Lm2; then
reconsider x2=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y2=y as Element of (len y)-tuples_on COMPLEX by A1,FINSEQ_2:92;
reconsider y29=(x2 - y2) as Element of (len (x2 - y2))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A2: len x=len y; then
A3: len (x - y) = len x by Th7;
per cases;
suppose
A4: not i in Seg (len x); then
A5: not i in dom x2 by FINSEQ_2:124;
A6: not i in dom y2 by A2,A4,FINSEQ_2:124;
not i in dom(y29) by A3,A4,FINSEQ_2:124;
then (x2-y2).i = 0-0 by FUNCT_1:def 2
.= x2.i - 0 by A5,FUNCT_1:def 2
.= x2.i - y2.i by A6,FUNCT_1:def 2;
hence thesis;
end;
suppose i in Seg (len x);
then i in dom (y29) by A3,FINSEQ_2:124;
hence thesis by VALUED_1:13;
end;
end;
theorem Th22:
for x,y being complex-valued FinSequence st len x=len y holds
(x+y).i = x.i + y.i
proof
let x,y be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & y is FinSequence of COMPLEX by Lm2; then
reconsider x2=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y2=y as Element of (len y)-tuples_on COMPLEX by A1,FINSEQ_2:92;
reconsider y29=(x2 + y2) as Element of (len (x2 + y2))-tuples_on COMPLEX by
FINSEQ_2:92;
assume
A2: len x=len y; then
A3: len (x + y) = len x by Th6;
per cases;
suppose
A4: not i in Seg len x; then
A5: not i in dom x2 by FINSEQ_2:124;
A6: not i in dom y2 by A2,A4,FINSEQ_2:124;
not i in dom(y29) by A3,A4,FINSEQ_2:124;
then (x2+y2).i = 0+0 by FUNCT_1:def 2
.= x2.i + 0 by A5,FUNCT_1:def 2
.= x2.i + y2.i by A6,FUNCT_1:def 2;
hence thesis;
end;
suppose i in Seg len x;
then i in dom y29 by A3,FINSEQ_2:124;
hence thesis by VALUED_1:def 1;
end;
end;
definition let z be FinSequence of COMPLEX;
func Re z -> FinSequence of REAL equals
1/2*(z+z*');
coherence
proof
A1: len z = len (z*') by Def1;
A2: len (1/2*(z+z*')) = len (z+z*') by Th3
.= len z by A1,Th6;
rng (1/2*(z+z*')) c= REAL
proof
let w be object;
assume w in rng (1/2*(z+z*'));
then consider x being object such that
A3: x in dom (1/2*(z+z*')) and
A4: w=(1/2*(z+z*')).x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A3;
x in Seg len (1/2*(z+z*')) by A3,FINSEQ_1:def 3; then
A5: 1<=i & i<=len z by A2,FINSEQ_1:1;
(1/2*(z+z*')).i = 1/2*((z+z*').i) by Th12
.=1/2*((z.i)+(z*').i) by A1,Th22
.=1/2*((z.i)+(z.i)*') by A5,Def1
.=(1/2)*(2*(Re (z.i))) by Th20;
hence thesis by A4;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
theorem Th23:
for z being Complex holds z-z*' = 2*(Im z) * **
proof
let z be Complex;
z-z*'= Re z - Re (z*') + (Im z - Im (z*'))*** by COMPLEX1:84
.= Re z - Re (z*')+(Im z - -Im z)*** by COMPLEX1:27
.= Re z - Re z + (Im z - -Im z)*** by COMPLEX1:27
.= 2*(Im z)***;
hence thesis;
end;
definition
let z be FinSequence of COMPLEX;
func Im z -> FinSequence of REAL equals
(-1/2***)*(z-z*');
coherence
proof
A1: len z = len (z*') by Def1;
A2: len ((-1/2***)*(z-z*')) = len (z-z*') by Th3
.= len z by A1,Th7;
rng ((-1/2***)*(z-z*')) c= REAL
proof
let w be object;
assume w in rng ((-1/2***)*(z-z*'));
then consider x being object such that
A3: x in dom ((-1/2***)*(z-z*')) and
A4: w=((-1/2***)*(z-z*')).x by FUNCT_1:def 3;
reconsider i=x as Element of NAT by A3;
x in Seg len ((-1/2***)*(z-z*')) by A3,FINSEQ_1:def 3; then
A5: 1<=i & i<=len z by A2,FINSEQ_1:1;
((-1/2***)*(z-z*')).i =(-1/2***)*((z-z*').i) by Th12
.=(-1/2***)*((z.i)-(z*').i) by A1,Th21
.=(-1/2***)*((z.i)-(z.i)*') by A5,Def1
.=(-1/2***)*((2*(Im (z.i))) * **) by Th23;
hence thesis by A4;
end;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let x,y be FinSequence of COMPLEX;
func |( x,y )| -> Element of COMPLEX equals
|(Re x,Re y)| - ***(|(Re x,Im y)|) + ***(|(Im x,Re y)|) + |(Im x,Im y)|;
coherence by XCMPLX_0:def 2;
end;
theorem Th24:
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x + (y + z) = x + y + z
proof
let x,y,z be complex-valued FinSequence;
reconsider x1=x, y1 = y, z1 = z as FinSequence of COMPLEX by Lm2;
assume
A1: len x=len y & len y=len z;
reconsider z9=z1 as Element of (len z)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=y1 as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9=x1 as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
x + (y + z) = addcomplex.:(x1,y1+z1) by SEQ_4:def 6
.= addcomplex.:(x1,addcomplex.:(y1,z1)) by SEQ_4:def 6
.= addcomplex.:(addcomplex.:(x9,y9),z9) by A1,FINSEQOP:28
.= addcomplex.:(x1+y1,z1) by SEQ_4:def 6
.= x + y + z by SEQ_4:def 6;
hence thesis;
end;
::$CT
theorem Th25:
for c being Complex, x,y being FinSequence of COMPLEX st
len x=len y holds c*(x+y) = c*x + c*y
proof
let c be Complex, x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
set cM = c multcomplex;
reconsider y9=y as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
A2: c is Element of COMPLEX by XCMPLX_0:def 2;
c*(x+y) = cM*(x + y) by SEQ_4:def 9
.= cM*(addcomplex.:(x,y)) by SEQ_4:def 6
.= addcomplex.:(cM*x9,cM*y9) by A1,A2,FINSEQOP:51,SEQ_4:56
.= cM*x + cM*y by SEQ_4:def 6
.= c*x + cM*y by SEQ_4:def 9
.= c*x + c*y by SEQ_4:def 9;
hence thesis;
end;
::$CT
theorem Th26:
for x,y being complex-valued FinSequence st len x=len y & x + y = 0c
(len x) holds x = -y & y = -x
proof
let x,y be complex-valued FinSequence;
assume that
A1: len x=len y and
A2: x + y = 0c (len x);
reconsider x1=x, y1 = y as FinSequence of COMPLEX by Lm2;
reconsider x9=x1 as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider y9=y1 as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
A3: x + y = addcomplex.:(x1,y1) & -y = compcomplex*y1 by SEQ_4:def 6,def 8;
x + y = (len x) |-> 0c by A2,SEQ_4:def 12;
then x9 = -y9 by A1,A3,BINOP_2:1,FINSEQOP:74,SEQ_4:51,52;
hence thesis;
end;
theorem Th27:
for x being complex-valued FinSequence holds x + 0c (len x) = x
proof
let x be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX by Lm2; then
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
x + 0c (len x) = x+(len x) |-> 0c by SEQ_4:def 12
.= addcomplex.:(x,(len x) |-> 0c) by A1,SEQ_4:def 6
.= x9 by BINOP_2:1,FINSEQOP:56;
hence thesis;
end;
theorem Th28:
for x being complex-valued FinSequence holds x + -x = 0c (len x)
proof
let x be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & -x is FinSequence of COMPLEX by Lm2; then
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
x + -x = addcomplex.:(x,-x) by A1,SEQ_4:def 6
.= addcomplex.:(x,compcomplex*x) by A1,SEQ_4:def 8
.= (len x9) |-> 0c by BINOP_2:1,FINSEQOP:73,SEQ_4:51,52
.= 0c (len x9) by SEQ_4:def 12;
hence thesis;
end;
theorem Th29:
for x,y being complex-valued FinSequence st len x=len y holds
-(x + y) = -x + -y
proof
let x,y be complex-valued FinSequence;
assume
A1: len x=len y;
A2: len (-y) = len y by Th5; then
A3: len (-x + -y) = len (-x) by A1,Th5,Th6;
A4: len (-x) = len x by Th5;
A5: len (x + y) = len x by A1,Th6;
then (x + y) + (-x + -y) = y + x + -x + -y by A1,A2,A4,Th24
.= y + (x + -x) + -y by A1,A4,Th24
.= y + 0c (len x) + -y by Th28
.= y + -y by A1,Th27
.= 0c (len y) by Th28;
hence thesis by A1,A4,A5,A3,Th26;
end;
theorem Th30:
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x - y - z = x - (y + z)
proof
let x,y,z be complex-valued FinSequence;
assume that
A1: len x=len y and
A2: len y=len z;
len (-y) = len y & len (-z) = len z by Th5;
then x - y - z = x + (- y + - z) by A1,A2,Th24
.= x - (y + z) by A2,Th29;
hence thesis;
end;
theorem Th31:
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x + (y - z) = x + y - z
proof
let x,y,z be complex-valued FinSequence;
assume
A1: len x=len y & len y=len z;
len (-z) = len z by Th5;
hence thesis by A1,Th24;
end;
::$CT
theorem Th32:
for x,y being complex-valued FinSequence st len x=len y holds
-(x - y) = -x + y
proof
let x,y be complex-valued FinSequence;
assume
A1: len x=len y;
len (-y) = len y by Th5;
then -(x - y) = -x +--y by A1,Th29
.= -x + y;
hence thesis;
end;
theorem Th33:
for x,y,z being complex-valued FinSequence st
len x=len y & len y=len z holds x - (y - z) = x - y + z
proof
let x,y,z be complex-valued FinSequence;
assume that
A1: len x=len y and
A2: len y=len z;
A3: len (-y) = len y by Th5;
x - (y - z) = x + (- y + z) by A2,Th32
.= x - y + z by A1,A2,A3,Th24;
hence thesis;
end;
theorem Th34:
for c being Complex holds c*(0c (len x)) = 0c (len x)
proof
let c be Complex;
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;
A1: rng (0c (len x)) c= COMPLEX by FINSEQ_1:def 4;
c*(0c (len x)) = multcomplex[;](cc,id COMPLEX)*(0c (len x)) by Lm1
.= multcomplex[;](cc,(id COMPLEX)*(0c (len x))) by FUNCOP_1:34
.= multcomplex[;](cc,(0c (len x))) by A1,RELAT_1:53
.= multcomplex[;](cc,(len x |-> 0c)) by SEQ_4:def 12
.= (len x) |->(multcomplex.(cc,0c)) by FINSEQOP:18
.= (len x) |->(cc*0c) by BINOP_2:def 5
.= (0c (len x)) by SEQ_4:def 12;
hence thesis;
end;
theorem Th35:
for c being Complex holds -c*x = c*(-x)
proof
let c be Complex;
A1: len (c*(-x))=len (-x) & len (c*x)=len x by Th3;
A2: len x=len (-x) by Th5;
then c*(-x) + c*x = c*(x+-x) by Th25
.= c*(0c (len x)) by Th28
.= 0c (len x) by Th34;
hence thesis by A2,A1,Th26;
end;
theorem Th36:
for c being Complex, x,y being FinSequence of COMPLEX st
len x=len y holds c*(x-y) = c*x - c*y
proof
let c be Complex, x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider y9=y as Element of (len y)-tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9=x as Element of (len x)-tuples_on COMPLEX by FINSEQ_2:92;
set cM = cc multcomplex;
c*(x-y) = cM*(x +(- y)) by SEQ_4:def 9
.= cM*(addcomplex.:(x,(-y))) by SEQ_4:def 6
.= addcomplex.:(cM*x9,cM*(-y9)) by A1,FINSEQOP:51,SEQ_4:56
.= cM*x + cM*(-y) by SEQ_4:def 6
.= c*x + cM*(-y) by SEQ_4:def 9
.= c*x + c*(-y) by SEQ_4:def 9
.= c*x - c*y by Th35;
hence thesis;
end;
theorem
for x1,y1 being Element of COMPLEX
for x2,y2 being Real st x1 = x2 &
y1 = y2 holds addcomplex.(x1,y1) = addreal.(x2,y2)
proof
let x1,y1 be Element of COMPLEX;
let x2,y2 be Real;
A1: addcomplex.(x1,y1)= x1+y1 by BINOP_2:def 3;
assume x1 = x2 & y1 = y2;
hence thesis by A1,BINOP_2:def 9;
end;
reserve C for Function of [:COMPLEX,COMPLEX:],COMPLEX;
reserve G for Function of [:REAL,REAL:],REAL;
theorem Th38:
for x1,y1 being FinSequence of COMPLEX for x2,y2 being
FinSequence of REAL st x1 = x2 & y1 = y2 & len x1=len y2 & (for i st i in dom
x1 holds C.(x1.i,y1.i)=G.(x2.i,y2.i)) holds C.:(x1,y1)=G.:(x2,y2)
proof
let x1,y1 be FinSequence of COMPLEX;
let x2,y2 be FinSequence of REAL;
assume that
A1: x1 = x2 and
A2: y1 = y2 and
A3: len x1=len y2 and
A4: for i st i in dom x1 holds C.(x1.i,y1.i)=G.(x2.i,y2.i);
A5: len (G.:(x2,y2)) = len x1 by A1,A3,FINSEQ_2:72;
now
let i be Nat;
assume that
A6: 1 <= i and
A7: i <= len (C.:(x1,y1));
A8: i <= len x1 by A2,A3,A7,FINSEQ_2:72; then
A9: i in dom x1 by A6,FINSEQ_3:25;
A10: i in dom (G.:(x2,y2)) by A5,A6,A8,FINSEQ_3:25;
i in dom (C.:(x1,y1)) by A6,A7,FINSEQ_3:25;
hence (C.:(x1,y1)).i = C.(x1.i,y1.i) by FUNCOP_1:22
.= G.(x2.i,y2.i) by A4,A9
.= (G.:(x2,y2)).i by A10,FUNCOP_1:22;
end;
hence thesis by A5,A2,A3,FINSEQ_2:72;
end;
theorem
for x1,y1 being FinSequence of COMPLEX for x2,y2 being FinSequence of
REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds addcomplex.:(x1,y1) = addreal.:
(x2,y2)
proof
let x1,y1 be FinSequence of COMPLEX;
let x2,y2 be FinSequence of REAL;
assume that
A1: x1 = x2 & y1 = y2 and
A2: len x1=len y2;
for i st i in dom x1 holds addcomplex.(x1.i,y1.i)=addreal.(x2.i,y2.i)
proof
let i;
x1.i + y1.i = addcomplex.(x1.i,y1.i) by BINOP_2:def 3;
hence thesis by A1,BINOP_2:def 9;
end;
hence thesis by A1,A2,Th38;
end;
::$CT
theorem Th40:
for x being FinSequence of COMPLEX holds len (Re x)=len x & len (Im x)=len x
proof
let x be FinSequence of COMPLEX;
A1: len x=len (x*') by Def1;
A2: len (Im x) =len (x-x*') by Th3
.=len x by A1,Th7;
len (Re x) =len (x+x*') by Th3
.=len x by A1,Th6;
hence thesis by A2;
end;
theorem Th41:
for x,y being FinSequence of COMPLEX st len x=len y holds Re (x+
y) = Re x + Re y & Im(x + y) = Im x + Im y
proof
let x,y be FinSequence of COMPLEX;
A1: len (-x*')=len (x*') by Th5;
assume
A2: len x=len y;
then
A3: len (x+y)=len x by Th6;
A4: len y=len (y*') by Def1;
then
A5: len (y+(y*'))=len y by Th6;
A6: len x=len (x*') by Def1;
then
A7: len (x+(x*'))=len x by Th6;
A8: len (x-(x*'))=len x by A6,Th7;
A9: len (y-(y*'))=len y by A4,Th7;
thus Re (x+y)=1/2*((x+y)+(x*'+y*')) by A2,Th15
.=1/2*((x+y+x*')+y*') by A2,A4,A6,A3,Th24
.=1/2*((x+x*'+y)+y*') by A2,A6,Th24
.=1/2*((x+x*')+(y+y*')) by A2,A4,A7,Th24
.= Re x + Re y by A2,A7,A5,Th25;
thus Im (x+y)=(-1/2***)*((x+y)-(x*'+y*')) by A2,Th15
.=(-1/2***)*((x+y)-x*'-y*') by A2,A4,A6,A3,Th30
.=(-1/2***)*(x+-x*'+y-y*') by A2,A6,A1,Th24
.=(-1/2***)*((x-x*')+(y-y*')) by A2,A4,A8,Th31
.=Im x + Im y by A2,A8,A9,Th25;
end;
theorem
for x1,y1 being FinSequence of COMPLEX for x2,y2 being FinSequence of
REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds diffcomplex.:(x1,y1) = diffreal
.:(x2,y2)
proof
let x1,y1 be FinSequence of COMPLEX, x2,y2 be FinSequence of REAL;
assume that
A1: x1 = x2 & y1 = y2 and
A2: len x1=len y2;
for i st i in dom x1 holds diffcomplex.(x1.i,y1.i)=diffreal.(x2.i,y2.i)
proof
let i;
x1.i - y1.i = diffcomplex.(x1.i,y1.i) by BINOP_2:def 4;
hence thesis by A1,BINOP_2:def 10;
end;
hence thesis by A1,A2,Th38;
end;
::$CT
theorem Th43:
for x,y being FinSequence of COMPLEX st len x=len y holds
Re(x - y) = Re x - Re y & Im(x - y) = Im x - Im y
proof
let x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
then
A2: len (x-y)=len x by Th7;
A3: len x=len (x*') by Def1;
then
A4: len (x+(x*'))=len x by Th6;
A5: len y=len (y*') by Def1;
then
A6: len (y+(y*'))=len y by Th6;
thus Re (x-y)=(1/2)*((x-y)+(x*'-y*')) by A1,Th17
.=(1/2)*(x*'+(x-y)-y*') by A1,A5,A3,A2,Th31
.=(1/2)*(x*'+((x-y)-y*')) by A1,A5,A3,A2,Th31
.=(1/2)*(x*'+(x-(y+y*'))) by A1,A5,Th30
.=(1/2)*(x+x*'-(y+y*')) by A1,A3,A6,Th31
.= Re x - Re y by A1,A4,A6,Th36;
A7: len (x-(x*'))=len x by A3,Th7;
A8: len (y-(y*'))=len y by A5,Th7;
thus Im (x-y)=(-1/2***)*((x-y)-(x*'-y*')) by A1,Th17
.=(-1/2***)*((x-y)-x*'+y*') by A1,A5,A3,A2,Th33
.=(-1/2***)*(x-(x*'+y)+y*') by A1,A3,Th30
.=(-1/2***)*(x-x*'-y+y*') by A1,A3,Th30
.=(-1/2***)*((x-x*')-(y-y*')) by A1,A5,A7,Th33
.=Im x - Im y by A1,A7,A8,Th36;
end;
theorem Th44:
for a, b being Complex holds a*(b*z) = (a*b)*z
proof
let a, b be Complex;
reconsider aa = a, bb = b, ab=a*b as Element of COMPLEX by XCMPLX_0:def 2;
thus (a*b)*z = (multcomplex[;](ab,id COMPLEX))*z by Lm1
.= multcomplex[;](multcomplex.(aa,bb),id COMPLEX)*z by BINOP_2:def 5
.= multcomplex[;](aa,multcomplex[;](bb,id COMPLEX))*z by FUNCOP_1:62
.= (multcomplex[;](aa,id COMPLEX)*multcomplex[;](bb,id COMPLEX))*z by
FUNCOP_1:55
.= (multcomplex[;](aa,id COMPLEX))*(multcomplex[;](bb,id COMPLEX)*z) by
RELAT_1:36
.= (multcomplex[;](aa,id COMPLEX))*(b*z) by Lm1
.= a*(b*z) by Lm1;
end;
Lm3: -(0c (len x)) = 0c (len x)
proof
-(0c (len x)) = -((len x) |-> 0c) by SEQ_4:def 12
.= compcomplex*((len x) |-> 0c) by SEQ_4:def 8
.= len x |->(compcomplex.0c) by FINSEQOP:16
.= (len x) |-> -0c by BINOP_2:def 1
.= (0c (len x)) by SEQ_4:def 12;
hence thesis;
end;
theorem Th45:
for c being Complex holds (-c)*x = -(c*x)
proof
let c be Complex;
A1: len ((-c)*x)=len x by Th3;
A2: len (c*x)=len x by Th3;
(-c)*x + c*x = (-1)*c*x + c*x .= -(c*x)+ c*x by Th44
.= -(c*x - c*x) by A2,Th32
.= -(0c (len x)) by A2,Th28
.= 0c (len x) by Lm3;
hence thesis by A1,A2,Th26;
end;
reserve h for Function of COMPLEX,COMPLEX,
g for Function of REAL,REAL;
theorem Th46:
for y1 being FinSequence of COMPLEX for y2 being FinSequence of
REAL st len y1=len y2 & (for i st i in dom y1 holds h.(y1.i)=g.(y2.i)) holds h*
y1 = g*y2
proof
let y1 be FinSequence of COMPLEX;
let y2 be FinSequence of REAL;
assume that
A1: len y1=len y2 and
A2: for i st i in dom y1 holds h.(y1.i)=g.(y2.i);
A3: len (g*y2) = len y1 by A1,FINSEQ_2:33;
now
let i be Nat;
assume that
A4: 1 <= i and
A5: i <= len (h*y1);
A6: i <= len y1 by A5,FINSEQ_2:33;
then
A7: i in dom y1 by A4,FINSEQ_3:25;
A8: i in dom (g*y2) by A3,A4,A6,FINSEQ_3:25;
i in dom (h*y1) by A4,A5,FINSEQ_3:25;
hence (h*y1).i = h.(y1.i) by FUNCT_1:12
.= g.(y2.i) by A2,A7
.= (g*y2).i by A8,FUNCT_1:12;
end;
hence thesis by A3,FINSEQ_2:33;
end;
theorem
for y1 being FinSequence of COMPLEX for y2 being FinSequence of REAL
st y1 = y2 & len y1=len y2 holds compcomplex*y1 = compreal*y2
proof
let y1 be FinSequence of COMPLEX;
let y2 be FinSequence of REAL;
assume that
A1: y1 = y2 and
A2: len y1=len y2;
for i st i in dom y1 holds compcomplex.(y1.i)=compreal.(y2.i)
proof
let i;
assume i in dom y1;
- y1.i = compcomplex.(y1.i) by BINOP_2:def 1;
hence thesis by A1,BINOP_2:def 7;
end;
hence thesis by A2,Th46;
end;
::$CT
theorem Th48:
for x being FinSequence of COMPLEX holds Re (***x) = -(Im x) &
Im (***x) = Re x
proof
let x be FinSequence of COMPLEX;
A1: len (x*') = len x by Def1;
A2: Im (***x) =(((-1/2)***))*(***x-((-**)*(x*'))) by Th13,COMPLEX1:31
.=(((-1/2)***))*(***x+-(-(***x*'))) by Th45
.=(((-1/2)***))*(***(x+x*')) by A1,Th25
.=(((-1/2)***)***)*(x+x*') by Th44
.=Re x;
Re (***x) =(1/2)*(***x+((-**)*(x*'))) by Th13,COMPLEX1:31
.=(1/2)*(***x-(***((x*')))) by Th45
.=(1/2)*(***(x-(x*'))) by A1,Th36
.=(1/2***)*(x-x*') by Th44
.=((-1)*((-1/2)***))*(x-x*')
.=-(Im x) by Th44;
hence thesis by A2;
end;
theorem Th49:
for x,y being FinSequence of COMPLEX st len x=len y holds
|(***x,y)| = ***(|(x,y)|)
proof
let x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
A2: len (Im y) = len y by Th40;
A3: len (Re y) = len y by Th40;
A4: len (Im x) = len x by Th40;
|(***x,y)| =|(-(Im x),Re y)| - ***(|(Re (***x),Im y)|) + ***(|(Im (
***x),Re y)|) + |(Im (***x),Im y)| by Th48
.=|(-(Im x),Re y)| - ***(|(-(Im x),Im y)|) + ***(|(Im (***x),Re y)|)
+ |(Im (***x),Im y)| by Th48
.=|(-(Im x),Re y)| - ***(|(-(Im x),Im y)|) + ***(|(Re x,Re y)|) + |(Im
(***x),Im y)| by Th48
.=|(-(Im x),Re y)| - ***(|(-(Im x),Im y)|) + ***(|(Re x,Re y)|) + |(Re
x,Im y)| by Th48
.=-|((Im x),Re y)| - ***(|(-(Im x),Im y)|) + ***(|(Re x,Re y)|) + |(Re
x,Im y)| by A1,A3,A4,RVSUM_1:122
.=-|((Im x),Re y)| - ***(-|((Im x),Im y)|) + ***(|(Re x,Re y)|) + |(Re
x,Im y)| by A1,A4,A2,RVSUM_1:122
.=***(|(x,y)|);
hence thesis;
end;
theorem Th50:
for x,y being FinSequence of COMPLEX st len x=len y holds |(x,
***y)| = -***(|(x,y)|)
proof
let x,y be FinSequence of COMPLEX;
assume
A1: len x=len y;
A2: len (Im x) = len x by Th40;
A3: len (Re x) = len x by Th40;
A4: len (Im y) = len y by Th40;
|(x,***y)| =|(Re x,-(Im y))| - ***(|(Re x,Im (***y))|) + ***(|(Im x,
Re (***y))|) + |(Im x,Im (***y))| by Th48
.=|(Re x,-(Im y))| - ***(|(Re x,Re y)|) + ***(|(Im x,Re (***y))|) +
|(Im x,Im (***y))| by Th48
.=|(Re x,-(Im y))| - ***(|(Re x,Re y)|) + ***(|(Im x,-Im y)|) + |(Im x
,Im (***y))| by Th48
.=|(Re x,-(Im y))| - ***(|(Re x,Re y)|) + ***(|(Im x,-Im y)|) + |(Im x
,Re y)| by Th48
.=-|(Re x,Im y)| - ***(|(Re x,Re y)|) + ***(|(Im x,-Im y)|) + |(Im x,
Re y)| by A1,A3,A4,RVSUM_1:122
.=-|(Re x,Im y)| - ***(|(Re x,Re y)|) + ***(-(|(Im x,Im y)|)) + |(Im x
,Re y)| by A1,A2,A4,RVSUM_1:122
.=-***(|(x,y)|);
hence thesis;
end;
theorem
for a1 being Element of COMPLEX,y1 being FinSequence of COMPLEX for a2
being Element of REAL,y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len
y1=len y2 holds (a1 multcomplex)*y1 = (a2 multreal)*y2
proof
let a1 be Element of COMPLEX,y1 be FinSequence of COMPLEX;
let a2 be Element of REAL,y2 be FinSequence of REAL;
assume that
A1: a1=a2 & y1 = y2 and
A2: len y1=len y2;
for i st i in dom y1 holds (a1 multcomplex).(y1.i)=(a2 multreal).(y2.i)
proof
let i;
reconsider y2i = y2.i as Element of REAL by XREAL_0:def 1;
assume i in dom y1;
A3: (a2*y2).i = a2*(y2.i) by RVSUM_1:44
.= multreal.(a2,(id REAL).(y2i)) by BINOP_2:def 11
.= (multreal[;](a2,id REAL)).(y2i) by FUNCOP_1:53
.= (a2 multreal).(y2.i) by RVSUM_1:def 3;
(a1*y1).i = a1*(y1.i) by Th12
.= multcomplex.(a1,(id COMPLEX).(y1.i)) by BINOP_2:def 5
.= (multcomplex[;](a1,id COMPLEX)).(y1.i) by FUNCOP_1:53
.= (a1 multcomplex).(y1.i) by SEQ_4:def 4;
hence thesis by A1,A3;
end;
hence thesis by A2,Th46;
end;
::$CT
theorem Th52:
for a, b being Complex holds (a+b)*z = a*z + b*z
proof
let a, b be Complex;
reconsider aa = a, bb = b, ab=a+b as Element of COMPLEX by XCMPLX_0:def 2;
set c1M = multcomplex[;](aa,id COMPLEX), c2M = multcomplex[;](bb,id COMPLEX);
thus (a + b)*z = (multcomplex[;](ab,id COMPLEX))*z by Lm1
.= multcomplex[;](addcomplex.(aa,bb),id COMPLEX)*z by BINOP_2:def 3
.= addcomplex.:(c1M,c2M)*z by FINSEQOP:35,SEQ_4:54
.= addcomplex.:(c1M*z,c2M*z) by FUNCOP_1:25
.= c1M*z + c2M*z by SEQ_4:def 6
.= a*z + c2M*z by Lm1
.= a*z + b*z by Lm1;
end;
theorem Th53:
for a, b being Complex holds (a-b)*z = a*z - b*z
proof
let a, b be Complex;
reconsider aa = a, bb = b as Element of COMPLEX by XCMPLX_0:def 2;
(a - b)*z=(a+(-b))*z .= aa*z +(-bb)*z by Th52
.= a*z - b*z by Th45;
hence thesis;
end;
theorem Th54:
for a being Element of COMPLEX,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
proof
let a be Element of COMPLEX, x be FinSequence of COMPLEX;
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***)*z6*x+1/2*z5*x) =len ((1/2***)*z6*x) by Th3,Th6;
A3: len (1/2*z5*x) = len x by Th3;
A4: len (z5*x) = len x & len ((***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***)*x*') = len (x*') & len ((z5 + ***z6)*x) = len x by Th3;
A8: len (((-1/2***)*z6)*(x*')) = len (x*') by Th3;
A9: Im a * Im x =(z6 * (-1/2***))*(x-x*') by Th44
.=((-1/2***)*z6)*x -((-1/2***)*z6)*(x*') by A1,Th36;
A10: len (((-1/2***)*z6)*x) = len x by Th3;
A11: len (z5*(x*')) = len (x*') & len ((z6***)*(x*')) = len (x*') by Th3;
A12: len (1/2*z5*(x*')) = len (x*') & len (((1/2***)*z6)*x) = len x by Th3;
A13: Re (a*x) = (1/2)*((a*'*x*')+a*x) by Th13
.= (1/2)*((a*'*x*')+((z5) + ***z6)*x) by COMPLEX1:13
.= (1/2)*(((z5-z6***)*x*')+(z5 + ***z6)*x) by COMPLEX1:def 11
.= (1/2)*((z5-z6***)*x*')+(1/2)*((z5 + ***z6)*x) by A7,Th25,Def1
.= (1/2)*((z5-z6***)*x*')+(1/2)*(z5*x + (***z6)*x) by Th52
.= (1/2)*(z5*(x*')-(z6***)*(x*'))+(1/2)*(z5*x + (***z6)*x) by Th53
.= 1/2*(z5*(x*')-(z6***)*(x*')) +(1/2*(z5*x) + 1/2*((***z6)*x)) by A4
,Th25
.= ((1/2*(z5*(x*'))-1/2*((z6***)*(x*')))) +(1/2*(z5*x) + 1/2*((***z6)*
x)) by A11,Th36
.= 1/2*(z5*(x*'))-1/2*((***z6)*(x*')) +(1/2*(z5*x) + 1/2*(***z6)*x) by
Th44
.= (1/2*(z5*(x*'))+(-(1/2***)*z6*(x*'))) +((1/2*(z5*x) + (1/2***)*z6*x
)) by Th44
.= (1/2*(z5*(x*'))+((-1/2****z6)*(x*'))) +((1/2*(z5*x) + (1/2***)*z6*x
)) by Th45
.= ((1/2*z5)*(x*')+((-1/2***)*z6)*(x*')) +((1/2*(z5*x) + (1/2***)*z6*x
)) by Th44
.= (1/2*z5*x + (1/2***)*z6*x) + (1/2*z5*(x*') + (-1/2***)*z6*(x*')) by
Th44
.= ((1/2***)*z6*x+1/2*z5*x) + 1/2*z5*(x*') + (-1/2***)*z6*(x*') by A1,A8
,A12,A2,Th24
.= (1/2*z5*x+1/2*z5*(x*')) +((-(-1/2***)*z6)*x) +((-1/2***)*z6*(x*'))
by A1,A3,A12,Th24
.= (1/2*z5*x+1/2*z5*(x*')) -((-1/2***)*z6*x) +((-1/2***)*z6*(x*')) by
Th45
.= Re a * Re x - Im a * Im x by A1,A5,A9,A6,A10,A8,Th33;
A14: len (((1/2***)*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 ((***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***)*z5)*x) = len x by Th3;
then
A21: len ((1/2)*(z6*x)+((-1/2***)*z5)*x) = len ((1/2)*(z6*x)) by A17,Th3,Th6;
A22: Re a * Im x = (z5 * (-1/2***))*(x-x*') by Th44
.= ((-1/2***)*z5)*x-((-1/2***)*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***)*((-((a*x)*')))+(-1/2***)*(a*x) by Th25
.= (-1/2***)*(-((a*')*(x*')))+(-1/2***)*(a*x) by Th13
.= (-1/2***)*(-((a*')*(x*'))) +(-1/2***)*((z5 + ***z6)*x) by COMPLEX1:13
.= (-1/2***)*(-((z5-z6***)*x*')) +(-1/2***)*((z5 + ***z6)*x) by
COMPLEX1:def 11
.= (-1/2***)*((-(z5-z6***))*x*') +(-1/2***)*((z5 + ***z6)*x) by Th45
.= (-1/2***)*((-z5+z6***)*(x*')) +(-1/2***)*((z5 + ***z6)*x)
.= (-1/2***)*((-z5)*(x*')+(***z6)*(x*')) +(-1/2***)*((z5 + ***z6)*x)
by Th52
.= (-1/2***)*((-z5)*(x*')+(***z6)*(x*')) +(-1/2***)*(z5*x + (***z6)*
x) by Th52
.= (-1/2***)*((-z5)*(x*')+(***z6)*(x*')) +((-1/2***)*(z5*x) + (-1/2*
**)*((***z6)*x)) by A4,Th25
.= (-1/2***)*((-z5)*(x*'))+(-1/2***)*((***z6)*(x*')) +((-1/2***)*(z5
*x) + (-1/2***)*((***z6)*x)) by A16,Th25
.= ((-1/2***)*(-z5))*(x*')+(-1/2***)*((***z6)*(x*')) +((-1/2***)*(z5
*x) + (-1/2***)*((***z6)*x)) by Th44
.= ((-1/2***)*(-z5))*(x*')+(-1/2***)*(***(z6*(x*'))) +((-1/2***)*(z5
*x) + (-1/2***)*((***z6)*x)) by Th44
.= ((-1/2***)*(-z5))*(x*')+((-1/2***)***)*(z6*(x*')) +((-1/2***)*(z5
*x) + (-1/2***)*((***z6)*x)) by Th44
.= ((-1/2***)*(-z5))*(x*')+((-1/2***)***)*(z6*(x*')) +(((-1/2***)*z5
)*x + (-1/2***)*((***z6)*x)) by Th44
.= ((-1/2***)*(-z5))*(x*')+((-1/2***)***)*(z6*(x*')) +(((-1/2***)*z5
)*x + (-1/2***)*(***(z6*x))) by Th44
.= (1/2)*(z6*x)+((-1/2***)*z5)*x +((1/2)*(z6*(x*'))+((1/2***)*z5)*(x*'
)) by Th44
.= (1/2)*(z6*x)+(((-1/2***)*z5)*x) +(1/2)*(z6*(x*'))+((1/2***)*z5)*(x
*') by A1,A23,A17,A18,A14,A21,Th24
.= (1/2)*(z6*x)+(1/2)*(z6*(x*')) + (((-1/2***)*z5)*x)+((1/2***)*z5)*(x
*') by A1,A23,A17,A20,A18,Th24
.= (1/2*(z6*x)+(1/2)*(z6*(x*')))+((((-1/2***)*z5)*x)+((1/2***)*z5)*(x
*')) by A1,A23,A17,A20,A14,A19,Th24
.= (1/2*z6)*x+(1/2)*(z6*(x*')) +((((-1/2***)*z5)*x)+((1/2***)*z5)*(x*'
)) by Th44
.= (1/2*z6)*x+(1/2*z6)*(x*') +(((-1/2***)*z5)*x+((-((-1/2***)*z5))*(x
*'))) by Th44
.= Im a * Re x + Re a * Im x by A15,A22,Th45;
hence thesis by A13;
end;
begin :: The Inner Product and Conjugate of Finite Sequences
theorem Th55:
for x1,x2,y being FinSequence of COMPLEX st len x1=len x2 & len
x2=len y holds |((x1+x2),y)| = |(x1,y)| + |(x2,y)|
proof
let x1,x2,y be FinSequence of COMPLEX;
assume that
A1: len x1=len x2 and
A2: len x2=len y;
A3: len (Re x1) = len x1 & len (Re x2) = len x2 by Th40;
A4: len (Im y) = len y by Th40;
A5: len (Im x1) = len x1 & len (Im x2) = len x2 by Th40;
A6: len (Re y) = len y by Th40;
|((x1+x2),y)| = |((Re x1+ Re x2),Re y)| - ***(|(Re (x1+x2),Im y)|) +
***(|(Im (x1+x2),Re y)|) + |(Im (x1+x2),Im y)| by A1,Th41
.= |((Re x1+ Re x2),Re y)| - ***(|((Re x1+Re x2),Im y)|) + ***(|(Im (
x1+x2),Re y)|) + |(Im (x1+x2),Im y)| by A1,Th41
.= |((Re x1+ Re x2),Re y)| - ***(|((Re x1+Re x2),Im y)|) + ***(|((Im
x1+ Im x2),Re y)|) + |(Im (x1+x2),Im y)| by A1,Th41
.= |((Re x1+ Re x2),Re y)| - ***(|((Re x1+Re x2),Im y)|) + ***(|((Im
x1+ Im x2),Re y)|) + |((Im x1+ Im x2),Im y)| by A1,Th41
.= |(Re x1,Re y)|+ |(Re x2,Re y)| - ***(|((Re x1+Re x2),Im y)|) + ***(
|((Im x1+ Im x2),Re y)|) + |((Im x1+ Im x2),Im y)| by A1,A2,A3,A6,RVSUM_1:120
.= |(Re x1,Re y)|+ |(Re x2,Re y)| - ***(|(Re x1,Im y)| + |(Re x2,Im y)|
) + ***(|((Im x1+ Im x2),Re y)|) + |((Im x1+ Im x2),Im y)| by A1,A2,A3,A4,
RVSUM_1:120
.= |(Re x1,Re y)|+ |(Re x2,Re y)| - ***(|(Re x1,Im y)| + |(Re x2,Im y)|
) + ***(|(Im x1,Re y)|+ |(Im x2,Re y)|) + |((Im x1+ Im x2),Im y)| by A1,A2,A6
,A5,RVSUM_1:120
.= |(Re x1,Re y)| + |(Re x2,Re y)| - ***(|(Re x1,Im y)| + |(Re x2,Im y
)|) + ***(|(Im x1,Re y)| + |(Im x2,Re y)|) + (|(Im x1,Im y)|+ |(Im x2,Im y)|)
by A1,A2,A5,A4,RVSUM_1:120
.= |(x1,y)| + |(x2,y)|;
hence thesis;
end;
theorem Th56:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(-x1, x2)| = -|(x1, x2)|
proof
let x1,x2 be FinSequence of COMPLEX;
assume
A1: len x1=len x2;
A2: len (***x1)=len x1 by Th3;
|(-x1, x2)| = |(******x1, x2)| .= |(***(***x1), x2)| by Th44
.= ***(|(***x1, x2)|) by A1,A2,Th49
.= ***(***(|(x1, x2)|)) by A1,Th49
.= (-1)*|(x1, x2)|;
hence thesis;
end;
theorem Th57:
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(x1, -x2)| = -|(x1, x2)|
proof
let x1,x2 be FinSequence of COMPLEX;
assume
A1: len x1=len x2;
A2: len (***x2)=len x2 by Th3;
|(x1, -x2)| = |(x1, ******x2)| .= |(x1, ***(***x2))| by Th44
.= -***(|(x1, *