:: The Sum and Product of Finite Sequences of Complex Numbers
:: by Keiichi Miyajima and Takahiro Kato
::
:: Received January 12, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

definition
let F be complex-valued Relation;
:: original: rng
redefine func rng F -> Subset of COMPLEX;
coherence
rng F is Subset of COMPLEX 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 F1 (#) F -> FinSequence-like ;
coherence
F * F1 is FinSequence-like
proof end;
end;

definition
func sqrcomplex -> UnOp of COMPLEX means :Def1: :: RVSUM_2:def 1
 for c being complex number holds it . c = c ^2 ;
existence
ex b1 being UnOp of COMPLEX st
for c being complex number holds b1 . c = c ^2
proof end;
uniqueness
for b1, b2 being UnOp of COMPLEX st ( for c being complex number holds b1 . c = c ^2 ) & ( for c being complex number holds b2 . c = c ^2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines sqrcomplex RVSUM_2:def 1 :
for b1 being UnOp of COMPLEX holds
( b1 = sqrcomplex iff for c being complex number holds b1 . c = c ^2 );

theorem :: RVSUM_2:1
sqrcomplex is_distributive_wrt multcomplex
proof end;

Lm1: for c, c1 being complex number holds (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1
proof end;

theorem :: RVSUM_2:2
for c being complex number holds c multcomplex is_distributive_wrt addcomplex
proof end;

begin

Lm2: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
proof end;

definition
let F1, F2 be complex-valued FinSequence;
:: original: +
redefine func F1 + F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 2
addcomplex .: (F1,F2);
coherence
F1 + F2 is FinSequence of COMPLEX by Lm2;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = F1 + F2 iff b1 = addcomplex .: (F1,F2) )
proof end;
commutativity
for b1 being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b1 = addcomplex .: (F1,F2) holds
b1 = addcomplex .: (F2,F1)
proof end;
end;

:: deftheorem defines + RVSUM_2:def 2 :
for F1, F2 being complex-valued FinSequence holds F1 + F2 = addcomplex .: (F1,F2);

definition
let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: +
redefine func R1 + R2 -> Element of i -tuples_on COMPLEX;
coherence
R1 + R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;

theorem :: RVSUM_2:3
for s being set
for i being Nat
for R1, R2 being b2 -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)
proof end;

theorem :: RVSUM_2:4
for F being complex-valued FinSequence holds (<*> COMPLEX) + F = <*> COMPLEX
proof end;

theorem :: RVSUM_2:5
for c1, c2 being complex number holds <*c1*> + <*c2*> = <*(c1 + c2)*>
proof end;

theorem :: RVSUM_2:6
for i being Nat
for c1, c2 being complex number holds (i |-> c1) + (i |-> c2) = i |-> (c1 + c2)
proof end;

definition
let F be complex-valued FinSequence;
:: original: -
redefine func - F -> FinSequence of COMPLEX equals :: RVSUM_2:def 3
compcomplex * F;
coherence
- F is FinSequence of COMPLEX by Lm2;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = - F iff b1 = compcomplex * F )
proof end;
end;

:: deftheorem defines - RVSUM_2:def 3 :
for F being complex-valued FinSequence holds - F = compcomplex * F;

definition
let i be Nat;
let R be i -element FinSequence of COMPLEX ;
:: original: -
redefine func - R -> Element of i -tuples_on COMPLEX;
coherence
- R is Element of i -tuples_on COMPLEX by FINSEQ_2:113;
end;

theorem :: RVSUM_2:7
for c being complex number holds - <*c*> = <*(- c)*>
proof end;

theorem Th8: :: RVSUM_2:8
for i being Nat
for c being complex number holds - (i |-> c) = i |-> (- c)
proof end;

theorem :: RVSUM_2:9
for i being Nat
for R1, R, R2 being b1 -element FinSequence of COMPLEX st R1 + R = R2 + R holds
R1 = R2
proof end;

theorem Th10: :: RVSUM_2:10
for F1, F2 being complex-valued FinSequence holds - (F1 + F2) = (- F1) + (- F2)
proof end;

definition
let F1, F2 be complex-valued FinSequence;
:: original: -
redefine func F1 - F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 4
diffcomplex .: (F1,F2);
coherence
F1 - F2 is FinSequence of COMPLEX by Lm2;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = F1 - F2 iff b1 = diffcomplex .: (F1,F2) )
proof end;
end;

:: deftheorem defines - RVSUM_2:def 4 :
for F1, F2 being complex-valued FinSequence holds F1 - F2 = diffcomplex .: (F1,F2);

definition
let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: -
redefine func R1 - R2 -> Element of i -tuples_on COMPLEX;
coherence
R1 - R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;

theorem :: RVSUM_2:11
for s being set
for i being Nat
for R1, R2 being b2 -element FinSequence of COMPLEX holds (R1 - R2) . s = (R1 . s) - (R2 . s)
proof end;

theorem :: RVSUM_2:12
for F being complex-valued FinSequence holds
( (<*> COMPLEX) - F = <*> COMPLEX & F - (<*> COMPLEX) = <*> COMPLEX )
proof end;

theorem :: RVSUM_2:13
for c1, c2 being complex number holds <*c1*> - <*c2*> = <*(c1 - c2)*>
proof end;

theorem :: RVSUM_2:14
for i being Nat
for c1, c2 being complex number holds (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)
proof end;

theorem :: RVSUM_2:15
for i being Nat
for R being b1 -element FinSequence of COMPLEX holds R - (i |-> 0c) = R
proof end;

theorem :: RVSUM_2:16
for F1, F2 being complex-valued FinSequence holds - (F1 - F2) = F2 - F1
proof end;

theorem :: RVSUM_2:17
for F1, F2 being complex-valued FinSequence holds - (F1 - F2) = (- F1) + F2
proof end;

theorem :: RVSUM_2:18
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX st R1 - R2 = i |-> 0c holds
R1 = R2
proof end;

theorem :: RVSUM_2:19
for i being Nat
for R1, R being b1 -element FinSequence of COMPLEX holds R1 = (R1 + R) - R
proof end;

theorem :: RVSUM_2:20
for i being Nat
for R1, R being b1 -element FinSequence of COMPLEX holds R1 = (R1 - R) + R
proof end;

notation
let F be complex-valued FinSequence;
let c be complex number ;
synonym c * F for c (#) F;
end;

definition
let F be complex-valued FinSequence;
let c be complex number ;
:: original: *
redefine func c * F -> FinSequence of COMPLEX equals :: RVSUM_2:def 5
(c multcomplex) * F;
coherence
c * F is FinSequence of COMPLEX by Lm2;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = c * F iff b1 = (c multcomplex) * F )
proof end;
end;

:: deftheorem defines * RVSUM_2:def 5 :
for F being complex-valued FinSequence
for c being complex number holds c * F = (c multcomplex) * F;

definition
let i be Nat;
let R be i -element FinSequence of COMPLEX ;
let c be complex number ;
:: original: *
redefine func c * R -> Element of i -tuples_on COMPLEX;
coherence
c * R is Element of i -tuples_on COMPLEX by FINSEQ_2:113;
end;

theorem :: RVSUM_2:21
for c, c1 being complex number holds c * <*c1*> = <*(c * c1)*>
proof end;

theorem Th22: :: RVSUM_2:22
for i being Nat
for c1, c2 being complex number holds c1 * (i |-> c2) = i |-> (c1 * c2)
proof end;

theorem :: RVSUM_2:23
for c1, c2 being complex number
for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)
proof end;

theorem :: RVSUM_2:24
for i being Nat
for R being b1 -element FinSequence of COMPLEX holds 0c * R = i |-> 0c
proof end;

notation
let F1, F2 be complex-valued FinSequence;
synonym mlt (F1,F2) for F1 (#) F2;
end;

definition
let F1, F2 be complex-valued FinSequence;
:: original: mlt
redefine func mlt (F1,F2) -> FinSequence of COMPLEX equals :: RVSUM_2:def 6
multcomplex .: (F1,F2);
coherence
mlt (F1,F2) is FinSequence of COMPLEX by Lm2;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = mlt (F1,F2) iff b1 = multcomplex .: (F1,F2) )
proof end;
commutativity
for b1 being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b1 = multcomplex .: (F1,F2) holds
b1 = multcomplex .: (F2,F1)
proof end;
end;

:: deftheorem defines mlt RVSUM_2:def 6 :
for F1, F2 being complex-valued FinSequence holds mlt (F1,F2) = multcomplex .: (F1,F2);

definition
let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: mlt
redefine func mlt (R1,R2) -> Element of i -tuples_on COMPLEX;
coherence
mlt (R1,R2) is Element of i -tuples_on COMPLEX by FINSEQ_2:120;
end;

theorem :: RVSUM_2:25
for F being complex-valued FinSequence holds mlt ((<*> COMPLEX),F) = <*> COMPLEX
proof end;

theorem :: RVSUM_2:26
for c1, c2 being complex number holds mlt (<*c1*>,<*c2*>) = <*(c1 * c2)*>
proof end;

theorem Th27: :: RVSUM_2:27
for i being Nat
for c being complex number
for R being b1 -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R
proof end;

theorem :: RVSUM_2:28
for i being Nat
for c1, c2 being complex number holds mlt ((i |-> c1),(i |-> c2)) = i |-> (c1 * c2)
proof end;

begin

theorem Th29: :: RVSUM_2:29
Sum (<*> COMPLEX) = 0c by BINOP_2:1, FINSOP_1:10;

theorem :: RVSUM_2:30
for c being complex number holds Sum <*c*> = c
proof end;

theorem Th31: :: RVSUM_2:31
for c being complex number
for F being complex-valued FinSequence holds Sum (F ^ <*c*>) = (Sum F) + c
proof end;

theorem Th32: :: RVSUM_2:32
for F1, F2 being complex-valued FinSequence holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
proof end;

theorem :: RVSUM_2:33
for c being complex number
for F being complex-valued FinSequence holds Sum (<*c*> ^ F) = c + (Sum F)
proof end;

theorem Th34: :: RVSUM_2:34
for c1, c2 being complex number holds Sum <*c1,c2*> = c1 + c2
proof end;

theorem :: RVSUM_2:35
for c1, c2, c3 being complex number holds Sum <*c1,c2,c3*> = (c1 + c2) + c3
proof end;

theorem Th36: :: RVSUM_2:36
for i being Nat
for c being complex number holds Sum (i |-> c) = i * c
proof end;

theorem :: RVSUM_2:37
for i being Nat holds Sum (i |-> 0c) = 0c
proof end;

theorem :: RVSUM_2:38
for c being complex number
for F being complex-valued FinSequence holds Sum (c * F) = c * (Sum F)
proof end;

theorem Th39: :: RVSUM_2:39
for F being complex-valued FinSequence holds Sum (- F) = - (Sum F)
proof end;

theorem Th40: :: RVSUM_2:40
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds Sum (R1 + R2) = (Sum R1) + (Sum R2)
proof end;

theorem :: RVSUM_2:41
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
proof end;

begin

Lm3: for F being empty FinSequence holds Product F = 1
proof end;

theorem :: RVSUM_2:42
Product (<*> COMPLEX) = 1 by Lm3;

theorem :: RVSUM_2:43
for c being complex number
for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)
proof end;

theorem :: RVSUM_2:44
for R being Element of 0 -tuples_on COMPLEX holds Product R = 1 by Lm3;

theorem :: RVSUM_2:45
for i, j being Nat
for c being complex number holds Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))
proof end;

theorem :: RVSUM_2:46
for i, j being Nat
for c being complex number holds Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))
proof end;

theorem :: RVSUM_2:47
for i being Nat
for c1, c2 being complex number holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))
proof end;

theorem Th48: :: RVSUM_2:48
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)
proof end;

theorem :: RVSUM_2:49
for i being Nat
for c being complex number
for R being b1 -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)
proof end;

begin

theorem :: RVSUM_2:50
for x being complex-valued FinSequence holds len (- x) = len x
proof end;

theorem :: RVSUM_2:51
for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 + x2) = len x1
proof end;

theorem :: RVSUM_2:52
for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 - x2) = len x1
proof end;

theorem :: RVSUM_2:53
for a being real number
for x being complex-valued FinSequence holds len (a * x) = len x
proof end;

theorem :: RVSUM_2:54
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 end;