:: The Sum and Product of Finite Sequences of Complex Numbers
:: by Keiichi Miyajima and Takahiro Kato
::
:: Received January 12, 2010
:: Copyright (c) 2010-2026 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 FINSEQ_1, FINSEQ_2, ARYTM_1, FUNCT_1, RELAT_1, BINOP_1, SETWISEO,
SQUARE_1, FUNCOP_1, RVSUM_1, RVSUM_2, CARD_3, XBOOLE_0, COMPLEX1,
XCMPLX_0, VALUED_0, BINOP_2, ZFMISC_1, NUMBERS, SUBSET_1, NAT_1, TARSKI,
ORDINAL4, ARYTM_3, CARD_1, VALUED_1, REAL_1, XXREAL_0;
notations TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, CARD_1, NUMBERS, VALUED_0,
XBOOLE_0,
XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1,
PARTFUN1, BINOP_2, FUNCT_2, BINOP_1, FUNCOP_1, FINSEQ_1, FINSEQ_2,
VALUED_1, SEQ_4, FINSEQOP, SETWOP_2, RVSUM_1;
constructors BINOP_1, COMPLEX1, SETWISEO, SQUARE_1, BINOP_2, FINSEQOP,
FINSOP_1, RELSET_1, RVSUM_1, SEQ_4, CARD_1, CARD_3;
registrations FUNCT_1, FUNCT_2, FUNCOP_1, NUMBERS, XREAL_0, BINOP_2, MEMBERED,
FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, RELAT_1, RVSUM_1, CARD_1,
XCMPLX_0, NAT_1;
requirements NUMERALS, SUBSET, ARITHM;
definitions BINOP_1, FINSEQ_1;
equalities FINSEQ_1, SQUARE_1, VALUED_1, XCMPLX_0, RVSUM_1, XBOOLE_0, SEQ_4;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, FINSEQ_2, FINSEQOP, SETWOP_2,
RELAT_1, FINSOP_1, ZFMISC_1, XCMPLX_0, BINOP_2, FINSEQ_3, VALUED_0,
VALUED_1, RFUNCT_1, RVSUM_1, SEQ_4, CARD_1, XBOOLE_1;
schemes NAT_1, FUNCT_2;
begin :: Auxiliary theorems
definition let F be complex-valued Relation;
redefine func rng F -> Subset of COMPLEX; :: redefines rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence by VALUED_0:def 1;
end;
registration
let D be non empty set;
let F be Function of COMPLEX,D;
let F1 be complex-valued FinSequence;
cluster F*F1 -> FinSequence-like;
coherence
proof
consider n1 being Nat such that
A1: dom F1 = Seg n1 by FINSEQ_1:def 2;
take n1;
dom F = COMPLEX & rng F1 c= COMPLEX by FUNCT_2:def 1;
hence thesis by A1,RELAT_1:27;
end;
end;
reserve s for set,
i,j for Nat,
c,c1,c2,c3 for Complex,
F,F1,F2 for complex-valued FinSequence,
R,R1,R2 for i-element complex-valued FinSequence;
definition
func sqrcomplex -> UnOp of COMPLEX means :Def1:
for c holds it.c = c^2;
existence
proof
deffunc F(Element of COMPLEX) = $1^2;
consider G being Function of COMPLEX,COMPLEX such that
A1: for x being Element of COMPLEX holds G.x = F(x) from FUNCT_2:sch 4;
take G;
let c;
c in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
uniqueness
proof
let G1,G2 be UnOp of COMPLEX such that
A2: for c holds G1.c = c^2 and
A3: for c holds G2.c = c^2;
now let x be Element of COMPLEX;
G1.(x) = (x)^2 by A2;
hence G1.x = G2.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
sqrcomplex is_distributive_wrt multcomplex
proof
let x1,x2 be Element of COMPLEX;
thus sqrcomplex.(multcomplex.(x1,x2)) = sqrcomplex.(x1*x2) by BINOP_2:def 5
.= (x1*x2)^2 by Def1
.= x1^2*x2^2
.= multcomplex.(x1^2,x2^2) by BINOP_2:def 5
.= multcomplex.(sqrcomplex.x1,x2^2) by Def1
.= multcomplex.(sqrcomplex.x1,sqrcomplex.x2) by Def1;
end;
Lm1: (multcomplex[;](c,id COMPLEX)).c1 = c*c1
proof
reconsider a=c, s=c1 as Element of COMPLEX by XCMPLX_0:def 2;
thus (multcomplex[;](c,id COMPLEX)).c1 = multcomplex.(a,(id COMPLEX).s)
by FUNCOP_1:53
.= multcomplex.(a,s)
.= c*c1 by BINOP_2:def 5;
end;
theorem ::: generalized COMPLSP1:17
c multcomplex is_distributive_wrt addcomplex
proof
c in COMPLEX by XCMPLX_0:def 2;
hence thesis by FINSEQOP:54,SEQ_4:54;
end;
begin :: Some Functors on the i-tuples on Complex
Lm2: F is FinSequence of COMPLEX
proof
thus rng F c= COMPLEX;
end;
definition let F1,F2;
redefine func F1 + F2 -> FinSequence of COMPLEX equals :: redefines + (VALUED_1, definition)
addcomplex.:(F1,F2);
coherence by Lm2;
compatibility
proof
reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX;
dom addcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
[:rng F3, rng F4:] c= dom addcomplex by ZFMISC_1:96; then
A1: dom(addcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69;
A2: dom (F1+F2) = dom F1 /\ dom F2 by VALUED_1:def 1;
thus F = F1+F2 implies F = addcomplex.:(F1,F2)
proof
assume A3: F = F1+F2;
for z being set st z in dom(addcomplex.:(F1,F2)) holds
F.z = addcomplex.(F1.z,F2.z)
proof
let z be set;
assume z in dom(addcomplex.:(F1,F2));
hence F.z = F1.z + F2.z by A2,A1,A3,VALUED_1:def 1
.= addcomplex.(F1.z,F2.z) by BINOP_2:def 3;
end;
hence thesis by A2,A1,A3,FUNCOP_1:21;
end;
assume A4: F = addcomplex.:(F1,F2);
now let c be object;
assume c in dom F;
hence F.c = addcomplex.(F1.c,F2.c) by A4,FUNCOP_1:22
.= F1.c + F2.c by BINOP_2:def 3;
end;
hence thesis by A1,A4,VALUED_1:def 1;
end;
commutativity
proof
let F be FinSequence of COMPLEX;
let F1,F2;
assume
A5: F = addcomplex.:(F1,F2);
reconsider F1,F2 as FinSequence of COMPLEX by Lm2;
A6: dom addcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
A7: [:rng F2, rng F1:] c= dom addcomplex by ZFMISC_1:96;
[:rng F1, rng F2:] c= dom addcomplex by A6,ZFMISC_1:96; then
A8: dom(addcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69
.= dom(addcomplex.:(F2,F1)) by A7,FUNCOP_1:69;
for z being set st z in dom(addcomplex.:(F2,F1))
holds F.z = addcomplex.(F2.z,F1.z)
proof
let z be set;
assume z in dom(addcomplex.:(F2,F1));
hence F.z = addcomplex.(F1.z,F2.z) by A5,A8,FUNCOP_1:22
.= F1.z + F2.z by BINOP_2:def 3
.= addcomplex.(F2.z,F1.z) by BINOP_2:def 3;
end;
hence thesis by A5,A8,FUNCOP_1:21;
end;
end;
definition let i,R1,R2;
redefine func R1 + R2 -> Element of i-tuples_on COMPLEX; :: redefines + (VALUED_1, definition)
coherence
proof
R1 is i-element FinSequence of COMPLEX &
R2 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
hence thesis by FINSEQ_2:120;
end;
end;
theorem
(R1+R2).s = R1.s + R2.s
proof
A0: R2 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
per cases;
suppose
A1: not s in Seg i; then
A2: not s in dom R2 by A0,FINSEQ_2:124;
R1 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
then
A3: not s in dom R1 by A1,FINSEQ_2:124;
not s in dom(R1+R2) by A1,FINSEQ_2:124;
hence (R1+R2).s = 0+0 by FUNCT_1:def 2
.= R1.s + 0 by A3,FUNCT_1:def 2
.= R1.s + R2.s by A2,FUNCT_1:def 2;
end;
suppose s in Seg i; then
s in dom (R1 + R2) by FINSEQ_2:124;
hence thesis by VALUED_1:def 1;
end;
end;
theorem
<*>COMPLEX + F = <*>COMPLEX
proof
F is FinSequence of COMPLEX by Lm2;
hence thesis by FINSEQ_2:73;
end;
theorem
<*c1*> + <*c2*> = <*c1+c2*>
proof
reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
<*s1*> + <*s2*> = <*addcomplex.(s1,s2)*> by FINSEQ_2:74
.= <*c1+c2*> by BINOP_2:def 3;
hence thesis;
end;
theorem
(i|->c1) + (i|->c2) = i|->(c1+c2)
proof
reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
(i|->s1) + (i|->s2) = i|->(addcomplex.(s1,s2)) by FINSEQOP:17
.= i|->(c1+c2) by BINOP_2:def 3;
hence thesis;
end;
definition let F;
redefine func -F -> FinSequence of COMPLEX equals :: redefines - (VALUED_1, definition)
compcomplex*F;
coherence by Lm2;
compatibility
proof
let F1 be FinSequence of COMPLEX;
A1: dom(-F) = dom F by VALUED_1:8;
A2: rng F c= COMPLEX & dom compcomplex = COMPLEX by FUNCT_2:def 1; then
A3: dom(compcomplex*F) = dom F by RELAT_1:27;
thus F1 = -F implies F1 = compcomplex*F
proof
assume A4: F1 = -F;
now
let c be object;
assume A5: c in dom F1;
thus F1.c = -(F.c) by A4,VALUED_1:8
.= compcomplex.(F.c) by BINOP_2:def 1
.= (compcomplex*F).c by A1,A4,A5,FUNCT_1:13;
end;
hence thesis by A3,A4,FUNCT_1:2,VALUED_1:8;
end;
assume A6: F1 = compcomplex*F;
now
let c be object;
assume A7: c in dom F1;
thus (-F).c = -(F.c) by VALUED_1:8
.= compcomplex.(F.c) by BINOP_2:def 1
.= (compcomplex*F).c by A6,A7,FUNCT_1:12;
end;
hence thesis by A1,A2,A6,FUNCT_1:2,RELAT_1:27;
end;
end;
definition let i,R;
redefine func -R -> Element of i-tuples_on COMPLEX; :: redefines - (VALUED_1, definition)
coherence
proof
R is i-element FinSequence of COMPLEX by FINSEQ_1:102;
hence thesis by FINSEQ_2:113;
end;
end;
theorem
-<*c*> = <*-c*>
proof
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
-<*s*> = <*compcomplex.s*> by FINSEQ_2:35
.= <*-c*> by BINOP_2:def 1;
hence thesis;
end;
theorem Th8:
-(i|->c) = i|->-c
proof
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
-(i|->s) = i|->(compcomplex.s) by FINSEQOP:16
.= i|->-c by BINOP_2:def 1;
hence thesis;
end;
theorem
R1 + R = R2 + R implies R1 = R2
proof
A0: R is i-element FinSequence of COMPLEX &
R1 is i-element FinSequence of COMPLEX &
R2 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
assume R1 + R = R2 + R; then
R1 + (R + -R)= (R2 + R)+-R by A0,FINSEQOP:28; then
A1: R1 + (R + -R)= R2 + (R + -R) by A0,FINSEQOP:28;
R + -R = i|->0c by A0,BINOP_2:1,FINSEQOP:73,SEQ_4:51,52; then
R1 = R2 + (i|->0c) by A0,A1,BINOP_2:1,FINSEQOP:56;
hence thesis by A0,BINOP_2:1,FINSEQOP:56;
end;
theorem Th10:
-(F1 + F2) = -F1 + -F2
proof
A1: dom -(F1 + F2) = dom(F1+F2) by VALUED_1:8;
A2: dom(F1+F2) = dom F1 /\ dom F2 by VALUED_1:def 1;
A3: dom (-F1 + -F2) = dom (-F1) /\ dom -F2 by VALUED_1:def 1
.= dom F1 /\ dom -F2 by VALUED_1:8
.= dom F1 /\ dom F2 by VALUED_1:8;
now
let i;
assume A4: i in dom -(F1+F2);
thus (-(F1 + F2)).i = -((F1+F2).i) by VALUED_1:8
.= -(F1.i+F2.i) by A1,A4,VALUED_1:def 1
.= -(F1.i)+-(F2.i)
.= -(F1.i) + (-F2).i by VALUED_1:8
.= (-F1).i + (-F2).i by VALUED_1:8
.= (-F1 + -F2).i by A1,A2,A3,A4,VALUED_1:def 1;
end;
hence thesis by A2,A3,FINSEQ_1:13,VALUED_1:8;
end;
definition let F1,F2;
redefine func F1 - F2 -> FinSequence of COMPLEX equals :: redefines - (VALUED_1, definition)
diffcomplex.:(F1,F2);
coherence by Lm2;
compatibility
proof
reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX;
A1: dom (F1-F2) = dom F1 /\ dom F2 by VALUED_1:12;
dom diffcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
A2: [:rng F3, rng F4:] c= dom diffcomplex by ZFMISC_1:96; then
A3: dom(diffcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69;
thus F = F1-F2 implies F = diffcomplex.:(F1,F2)
proof
assume A4: F = F1-F2;
for z being set st z in dom(diffcomplex.:(F1,F2))
holds F.z = diffcomplex.(F1.z,F2.z)
proof
let z be set;
assume z in dom(diffcomplex.:(F1,F2));
hence F.z = F1.z - F2.z by A1,A3,A4,VALUED_1:13
.= diffcomplex.(F1.z,F2.z) by BINOP_2:def 4;
end;
hence thesis by A1,A3,A4,FUNCOP_1:21;
end;
assume A5: F = diffcomplex.:(F1,F2);
now
let c be object;
assume c in dom F;
hence F.c = diffcomplex.(F1.c,F2.c) by A5,FUNCOP_1:22
.= F1.c - F2.c by BINOP_2:def 4;
end;
hence thesis by A1,A2,A5,FUNCOP_1:69,VALUED_1:14;
end;
end;
definition let i,R1,R2;
redefine func R1 - R2 -> Element of i-tuples_on COMPLEX; :: redefines - (VALUED_1, definition)
coherence
proof
R1 is i-element FinSequence of COMPLEX &
R2 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
hence thesis by FINSEQ_2:120;
end;
end;
theorem
(R1-R2).s = R1.s - R2.s
proof
A0: R2 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
per cases;
suppose
A1: not s in Seg i; then
A2: not s in dom R2 by A0,FINSEQ_2:124;
R1 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
then
A3: not s in dom R1 by A1,FINSEQ_2:124;
not s in dom(R1-R2) by A1,FINSEQ_2:124;
hence (R1-R2).s = 0-0 by FUNCT_1:def 2
.= R1.s - 0 by A3,FUNCT_1:def 2
.= R1.s - R2.s by A2,FUNCT_1:def 2;
end;
suppose s in Seg i; then
s in dom (R1 - R2) by FINSEQ_2:124;
hence thesis by VALUED_1:13;
end;
end;
theorem
<*>COMPLEX - F = <*>COMPLEX & F - <*>COMPLEX = <*>COMPLEX
proof
F is FinSequence of COMPLEX by Lm2;
hence thesis by FINSEQ_2:73;
end;
theorem
<*c1*> - <*c2*> = <*c1-c2*>
proof
reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
<*s1*> - <*s2*> = <*diffcomplex.(s1,s2)*> by FINSEQ_2:74
.= <*c1-c2*> by BINOP_2:def 4;
hence thesis;
end;
theorem
(i|->c1) - (i|->c2) = i|->(c1-c2)
proof
reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
(i|->s1) - (i|->s2) = i|->(diffcomplex.(s1,s2)) by FINSEQOP:17
.= i|->(c1-c2) by BINOP_2:def 4;
hence thesis;
end;
theorem
R - (i|-> 0c) = R
proof
A1: R is i-element FinSequence of COMPLEX by FINSEQ_1:102;
thus R - (i|-> 0c) = R + (i|->(-0)) by Th8
.= R by A1,BINOP_2:1,FINSEQOP:56;
end;
theorem
-(F1 - F2) = F2 - F1
proof
thus -(F1 - F2) = -F1 + --F2 by Th10
.= F2 - F1;
end;
theorem
-(F1 - F2) = -F1 + F2
proof
thus -(F1 - F2) = -F1 +--F2 by Th10
.= -F1 + F2;
end;
theorem
R1 - R2 = i|->0c implies R1 = R2
proof
A1: R1 is i-element FinSequence of COMPLEX &
R2 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
assume R1 - R2 = i|->0c; then
R1 = --R2 by A1,BINOP_2:1,FINSEQOP:74,SEQ_4:51,52;
hence thesis;
end;
theorem
i <= j implies
for R1 being i-element complex-valued FinSequence
for R being j-element complex-valued FinSequence holds
R1 = R1 + R - R
proof
assume
A1: i <= j;
let R1 be i-element complex-valued FinSequence;
let R be j-element complex-valued FinSequence;
A2: len R1 = i & len R = j by CARD_1:def 7;
A4: dom(R1+R) = dom R1 /\ dom R by VALUED_1:def 1
.= dom R1 by A2,XBOOLE_1:28,A1,FINSEQ_3:30;
A5: dom(R1+R-R) = dom(R1+R) /\ dom R by VALUED_1:12
.= dom R1 by A2,A4,XBOOLE_1:28,A1,FINSEQ_3:30;
now
let x be object;
assume
A6: x in dom R1;
hence (R1+R-R).x = (R1+R).x-R.x by A5,VALUED_1:13
.= R1.x+R.x-R.x by A4,A6,VALUED_1:def 1
.= R1.x;
end;
hence thesis by A5,FUNCT_1:def 11;
end;
theorem
i <= j implies
for R1 being i-element complex-valued FinSequence
for R being j-element complex-valued FinSequence holds
R1 = R1 - R + R
proof
assume
A1: i <= j;
let R1 be i-element complex-valued FinSequence;
let R be j-element complex-valued FinSequence;
A2: len R1 = i & len R = j by CARD_1:def 7;
A4: dom(R1-R) = dom R1 /\ dom R by VALUED_1:12
.= dom R1 by A2,XBOOLE_1:28,A1,FINSEQ_3:30;
A5: dom(R1-R+R) = dom(R1-R) /\ dom R by VALUED_1:def 1
.= dom R1 by A2,A4,XBOOLE_1:28,A1,FINSEQ_3:30;
now
let x be object;
assume
A6: x in dom R1;
hence (R1-R+R).x = (R1-R).x+R.x by A5,VALUED_1:def 1
.= R1.x-R.x+R.x by A4,A6,VALUED_1:13
.= R1.x;
end;
hence thesis by A5,FUNCT_1:def 11;
end;
notation let F,c;
synonym c*F for c(#)F;
end;
definition let F,c;
redefine func c*F -> FinSequence of COMPLEX equals :: redefines * (RVSUM_2, synonym) → (#) (VALUED_1, definition)
(c multcomplex)*F;
coherence by Lm2;
compatibility
proof
let F1 be FinSequence of COMPLEX;
A1: dom(c*F) = dom F by VALUED_1:def 5;
A2: rng F c= COMPLEX & dom(c multcomplex) = COMPLEX by FUNCT_2:def 1; then
A3: dom((c multcomplex)*F) = dom F by RELAT_1:27;
thus F1 = c*F implies F1 = (c multcomplex)*F
proof
assume A4: F1 = c*F;
now
let s be object;
assume A5: s in dom F1;
hence F1.s = c*(F.s) by A4,VALUED_1:def 5
.= (c multcomplex).(F.s) by Lm1
.= ((c multcomplex)*F).s by A1,A4,A5,FUNCT_1:13;
end;
hence thesis by A1,A3,A4,FUNCT_1:2;
end;
assume A6: F1 = (c multcomplex)*F;
now
let s be object;
assume A7: s in dom F1;
thus (c*F).s = c*(F.s) by VALUED_1:6
.= (c multcomplex).(F.s) by Lm1
.= ((c multcomplex)*F).s by A6,A7,FUNCT_1:12;
end;
hence thesis by A1,A2,A6,FUNCT_1:2,RELAT_1:27;
end;
end;
definition let i,R,c;
redefine func c*R -> Element of i-tuples_on COMPLEX; :: redefines * (RVSUM_2, synonym) → (#) (VALUED_1, definition)
coherence
proof
R is i-element FinSequence of COMPLEX by FINSEQ_1:102;
hence thesis by FINSEQ_2:113;
end;
end;
theorem
c*<*c1*> = <*c*c1*>
proof
reconsider s=c, s1=c1 as Element of COMPLEX by XCMPLX_0:def 2;
s*<*s1*> = <*(multcomplex[;](s,id COMPLEX)).s1*> by FINSEQ_2:35
.= <*c*c1*> by Lm1;
hence thesis;
end;
theorem Th22:
c1*(i|->c2) = i|->(c1*c2)
proof
reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
s1*(i|->s2) = i|->((multcomplex[;](s1,id COMPLEX)).s2) by FINSEQOP:16
.= i|->(c1*c2) by Lm1;
hence thesis;
end;
theorem
(c1 + c2)*F = c1*F + c2*F
proof
A1: dom ((c1 + c2)*F) = dom F by VALUED_1:def 5;
A2: dom (c1*F + c2*F) = dom (c1*F) /\ dom (c2*F) by VALUED_1:def 1;
A3: dom (c1*F) = dom F by VALUED_1:def 5;
A4: dom (c2*F) = dom F by VALUED_1:def 5;
now
let i;
assume A5: i in dom ((c1+c2)*F);
thus ((c1+c2)*F).i = (c1+c2)*(F.i) by VALUED_1:6
.= c1*(F.i) + c2*(F.i)
.= c1*(F.i) + (c2*F).i by VALUED_1:6
.= (c1*F).i + (c2*F).i by VALUED_1:6
.= (c1*F+c2*F).i by A1,A2,A3,A4,A5,VALUED_1:def 1;
end;
hence thesis by A1,A2,A3,A4,FINSEQ_1:13;
end;
theorem
0c*R = i|->0c
proof
A1: rng R c= COMPLEX;
A2: R is i-element FinSequence of COMPLEX by FINSEQ_1:102;
thus 0c*R = multcomplex[;](0c,(id COMPLEX)*R) by FUNCOP_1:34
.= multcomplex[;](0c,R) by A1,RELAT_1:53
.= i|->0c by A2,BINOP_2:1,FINSEQOP:76,SEQ_4:51,54;
end;
notation let F1,F2;
synonym mlt(F1,F2) for F1(#)F2;
end;
definition let F1,F2;
redefine func mlt(F1,F2) -> FinSequence of COMPLEX equals :: redefines mlt (RVSUM_2, synonym) → (#) (VALUED_1, definition)
multcomplex.:(F1,F2);
coherence by Lm2;
compatibility
proof
reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX;
dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
[:rng F3, rng F4:] c= dom multcomplex by ZFMISC_1:96; then
A1: dom(multcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69;
A2: dom mlt(F1,F2) = dom F1 /\ dom F2 by VALUED_1:def 4;
thus F = mlt(F1,F2) implies F = multcomplex.:(F1,F2)
proof
assume A3: F = mlt(F1,F2);
for z being set st z in dom(multcomplex.:(F1,F2))
holds F.z = multcomplex.(F1.z,F2.z)
proof
let z be set;
assume z in dom(multcomplex.:(F1,F2));
thus F.z = F1.z * F2.z by A3,VALUED_1:5
.= multcomplex.(F1.z,F2.z) by BINOP_2:def 5;
end;
hence thesis by A1,A2,A3,FUNCOP_1:21;
end;
assume A4: F = multcomplex.:(F1,F2);
now
let c be object;
assume c in dom F;
hence F.c = multcomplex.(F1.c,F2.c) by A4,FUNCOP_1:22
.= F1.c * F2.c by BINOP_2:def 5;
end;
hence thesis by A1,A4,VALUED_1:def 4;
end;
commutativity
proof
let F be FinSequence of COMPLEX;
let F1,F2;
reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
A5: dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1; then
A6: [:rng F4, rng F3:] c= dom multcomplex by ZFMISC_1:96;
[:rng F3, rng F4:] c= dom multcomplex by A5,ZFMISC_1:96; then
A7: dom(multcomplex.:(F1,F2)) = dom F1 /\ dom F2 by FUNCOP_1:69
.= dom(multcomplex.:(F2,F1)) by A6,FUNCOP_1:69;
assume A8: F = multcomplex.:(F1,F2);
for z being set st z in dom(multcomplex.:(F2,F1))
holds F.z = multcomplex.(F2.z,F1.z)
proof
let z be set such that
A9: z in dom(multcomplex.:(F2,F1));
set F1z = F1.z, F2z =F2.z;
thus F.z = multcomplex.(F1.z,F2.z) by A8,A7,A9,FUNCOP_1:22
.= F1z * F2z by BINOP_2:def 5
.= multcomplex.(F2.z,F1.z) by BINOP_2:def 5;
end;
hence thesis by A8,A7,FUNCOP_1:21;
end;
end;
definition let i,R1,R2;
redefine func mlt(R1,R2) -> Element of i-tuples_on COMPLEX; :: redefines mlt (RVSUM_2, synonym) → (#) (VALUED_1, definition)
coherence
proof
R1 is i-element FinSequence of COMPLEX &
R2 is i-element FinSequence of COMPLEX by FINSEQ_1:102;
hence thesis by FINSEQ_2:120;
end;
end;
theorem
mlt(<*>COMPLEX,F) = <*>COMPLEX
proof
F is FinSequence of COMPLEX by Lm2;
hence thesis by FINSEQ_2:73;
end;
theorem
mlt(<*c1*>,<*c2*>) = <*c1*c2*>
proof
reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
mlt(<*s1*>,<*s2*>) = <*multcomplex.(s1,s2)*> by FINSEQ_2:74
.= <*c1*c2*> by BINOP_2:def 5;
hence thesis;
end;
theorem Th27:
mlt(i|->c,R) = c*R
proof
A1: R is i-element FinSequence of COMPLEX by FINSEQ_1:102;
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
mlt(i|->s,R) = multcomplex[;](s,R) by A1,FINSEQOP:20
.= c*R by A1,FINSEQOP:22;
hence thesis;
end;
theorem
mlt(i|->c1,i|->c2) = i|->(c1*c2)
proof
reconsider s1=c1, s2=c2 as Element of COMPLEX by XCMPLX_0:def 2;
mlt(i|->s1,i|->s2) = s1*(i|->s2) by Th27
.= i|->(c1*c2) by Th22;
hence thesis;
end;
begin :: Finite Sum of Finite Sequence of Complex Numbers
theorem Th29:
Sum(<*> COMPLEX) = 0c by BINOP_2:1,FINSOP_1:10;
registration let f be empty FinSequence;
cluster Sum f -> zero;
coherence by Th29;
end;
theorem
Sum <*c*> = c
proof
reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
Sum <*c*> = c by FINSOP_1:11;
hence thesis;
end;
theorem Th31:
Sum(F^<*c*>) = Sum F + c
proof
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider F1=F as FinSequence of COMPLEX by Lm2;
thus Sum(F^<*c*>) = Sum(F1^<*s*>)
.= addcomplex.(addcomplex $$ F1,s) by FINSOP_1:4
.= Sum F1 + c by BINOP_2:def 3
.= Sum F + c;
end;
theorem Th32:
Sum(F1^F2) = Sum F1 + Sum F2
proof
reconsider F3=F1,F4=F2 as FinSequence of COMPLEX by Lm2;
thus Sum(F1^F2) = Sum(F3^F4)
.= addcomplex.(addcomplex $$ F3,addcomplex $$ F4) by FINSOP_1:5
.= Sum F3 + Sum F4 by BINOP_2:def 3
.= Sum F1 + Sum F2;
end;
theorem
Sum(<*c*>^F) = c + Sum F
proof
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum(<*c*>^F) = Sum <*s*> + Sum F by Th32
.= c + Sum F by FINSOP_1:11;
end;
theorem Th34:
Sum<*c1,c2*> = c1 + c2
proof
reconsider s1=c1 as Element of COMPLEX by XCMPLX_0:def 2;
thus Sum<*c1,c2*> = Sum<*s1*> + c2 by Th31
.= c1 + c2 by FINSOP_1:11;
end;
theorem
Sum<*c1,c2,c3*> = c1 + c2 + c3
proof
thus Sum<*c1,c2,c3*> = Sum<*c1,c2*> + c3 by Th31
.= c1 + c2 + c3 by Th34;
end;
theorem Th36:
Sum(i |-> c) = i*c
proof
reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
defpred P[Nat] means Sum($1 |->c) = $1*c;
A1: for i st P[i] holds P[(i+1)]
proof
let i such that
A2: Sum(i |-> c) = i*c;
thus Sum((i+1) |-> c) = Sum((i |-> c)^<*c*>) by FINSEQ_2:60
.= i*c + 1*c by A2,Th31
.= (i+1)*c;
end;
A3: P[0];
for i holds P[i] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
Sum(i |-> 0c) = 0c
proof
thus Sum(i |-> 0c) = i*0 by Th36
.= 0c;
end;
theorem
Sum(c*F) = c*(Sum F)
proof
reconsider F1=F as FinSequence of COMPLEX by Lm2;
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
set cM = multcomplex[;](s,id COMPLEX);
thus Sum (c*F) = cM.(addcomplex $$ F1) by SEQ_4:51,54,SETWOP_2:30
.= c*(Sum F1) by Lm1
.= c*(Sum F);
end;
theorem Th39:
Sum -F = -(Sum F)
proof
reconsider F1=F as FinSequence of COMPLEX by Lm2;
thus Sum -F = compcomplex.(addcomplex $$ F1) by SEQ_4:51,52,SETWOP_2:31
.= -(Sum F1) by BINOP_2:def 1
.= -(Sum F);
end;
theorem Th40:
Sum(R1 + R2) = Sum R1 + Sum R2
proof
reconsider R1,R2 as i-element FinSequence of COMPLEX by FINSEQ_1:102;
reconsider T1=R1, T2=R2 as Element of i-tuples_on COMPLEX by FINSEQ_2:131;
Sum(R1 + R2) = addcomplex.(addcomplex$$T1,addcomplex$$T2) by SETWOP_2:35
.= Sum R1 + Sum R2 by BINOP_2:def 3;
hence thesis;
end;
theorem
Sum(R1 - R2) = Sum R1 - Sum R2
proof
thus Sum(R1 - R2) = Sum R1 + Sum -R2 by Th40
.= Sum R1 - Sum R2 by Th39;
end;
begin :: The Product of Finite Sequences of Complex Numbers
Lm3: for F being empty FinSequence holds Product F = 1
proof
Product <*>COMPLEX = 1 by BINOP_2:6,FINSOP_1:10;
hence thesis;
end;
theorem
Product <*>COMPLEX = 1 by Lm3;
registration let f be empty FinSequence;
reduce 1 * (Product f) to 1;
reducibility by Lm3;
end;
theorem
Product (<*c*>^F) = c * Product F
proof
thus Product (<*c*>^F) = Product <*c*> * Product F by RVSUM_1:97
.= c * Product F;
end;
theorem
for R being Element of 0-tuples_on COMPLEX holds Product R = 1 by Lm3;
theorem
Product ((i+j) |->c) = (Product (i|->c))*(Product (j|->c))
proof
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
Product ((i+j) |->s) =
multcomplex.(multcomplex$$(i|->s),multcomplex$$(j|->s)) by SETWOP_2:26
.= (Product (i|->s))*(Product (j|->s)) by BINOP_2:def 5;
hence thesis;
end;
theorem
Product ((i*j) |->c) = Product (j |-> (Product (i|->c)))
proof
reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
Product ((i*j) |->c) = Product (j |-> (Product (i|->c))) by SETWOP_2:27;
hence thesis;
end;
theorem
Product (i|->(c1*c2)) = (Product (i|->c1))*(Product (i|->c2))
proof
reconsider s1=c1, s2=c2, ss = c1*c2 as Element of COMPLEX by XCMPLX_0:def 2;
Product (i|->(ss)) = multcomplex$$(i|->multcomplex.(s1,s2))
by BINOP_2:def 5
.= multcomplex.(multcomplex$$(i|->s1),multcomplex$$(i|->s2)) by SETWOP_2:36
.= (Product (i|->s1))*(Product (i|->s2)) by BINOP_2:def 5;
hence thesis;
end;
theorem Th48:
Product mlt(R1,R2) = Product R1 * Product R2
proof
reconsider R1,R2 as i-element FinSequence of COMPLEX by FINSEQ_1:102;
reconsider T1=R1, T2=R2 as Element of i-tuples_on COMPLEX
by FINSEQ_2:131;
Product (mlt(R1,R2)) = multcomplex.(multcomplex$$T1,multcomplex$$T2)
by SETWOP_2:35
.= Product R1 * Product R2 by BINOP_2:def 5;
hence thesis;
end;
theorem
Product (c*R) = Product (i|->c) * Product R
proof
reconsider s=c as Element of COMPLEX by XCMPLX_0:def 2;
thus Product (c*R) = Product mlt(i|->s,R) by Th27
.= Product (i|->c) * Product R by Th48;
end;
begin :: from EUCLID_2 (partially modified)
theorem
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;
theorem
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;
assume len x1<=len x2;
then
A2: dom x1 c= dom x2 by FINSEQ_3:30;
dom(x1+x2) = dom x1 /\ dom x2 by VALUED_1:def 1;
hence thesis by A2,XBOOLE_1:28,FINSEQ_3:29;
end;
theorem
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;
assume len x1<=len x2;
then
A2: dom x1 c= dom x2 by FINSEQ_3:30;
dom(x1-x2) = dom x1 /\ dom x2 by VALUED_1:12;
hence thesis by A2,XBOOLE_1:28,FINSEQ_3:29;
end;
theorem
for a being Complex, x being complex-valued FinSequence
holds len (a*x) = len x
proof
let a be Complex, x be complex-valued FinSequence;
dom(a*x) = dom x by VALUED_1:def 5;
hence thesis by FINSEQ_3:29;
end;
theorem
for x,y,z being complex-valued FinSequence st len x = len y & len y = len z
holds mlt(x+y,z) = mlt(x,z) + mlt(y,z)
proof
let x,y,z be complex-valued FinSequence;
A1:x is FinSequence of COMPLEX & y is FinSequence of COMPLEX &
z is FinSequence of COMPLEX by Lm2;
assume len x=len y & len y=len z; then
reconsider x2=x, y2=y, z2=z as Element of (len x)-tuples_on COMPLEX
by A1,FINSEQ_2:92;
A2: dom (mlt(x+y,z))=Seg len(mlt(x2+y2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.=dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
A3: dom (mlt(x,z))=Seg len(mlt(x2,z2)) by FINSEQ_1:def 3
.=Seg len x by CARD_1:def 7
.=Seg len (mlt(x2,z2)+mlt(y2,z2)) by CARD_1:def 7
.=dom (mlt(x2,z2)+mlt(y2,z2)) by FINSEQ_1:def 3;
for i being Nat st i in dom (mlt(x+y,z)) holds mlt(x+y,z).i=(mlt(x,z)+
mlt(y,z)).i
proof
let i be Nat;
assume A4: i in dom mlt(x+y,z);
set a=x.i, b=y.i, d=(x+y).i, e=z.i;
len (x2+y2)=len x by CARD_1:def 7; then
dom (x2+y2)=Seg len x by FINSEQ_1:def 3
.=Seg len(mlt(x2,z2)) by CARD_1:def 7
.=dom (mlt(x,z)) by FINSEQ_1:def 3; then
A5: d=a+b by A2,A3,A4,VALUED_1:def 1;
thus mlt(x+y,z).i=d*e by VALUED_1:5
.=a*e+b*e by A5
.=mlt(x,z).i +b*e by VALUED_1:5
.=mlt(x,z).i +mlt(y,z).i by VALUED_1:5
.=(mlt(x,z)+mlt(y,z)).i by A2,A4,VALUED_1:def 1;
end;
hence thesis by A2,FINSEQ_1:13;
end;