:: by Keiichi Miyajima and Takahiro Kato

::

:: Received January 12, 2010

:: Copyright (c) 2010-2017 Association of Mizar Users

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;
:: original: rng

redefine func rng F -> Subset of COMPLEX;

coherence

rng F is Subset of COMPLEX by VALUED_0:def 1;

registration

let D be non empty set ;

let F be Function of COMPLEX,D;

let F1 be complex-valued FinSequence;

coherence

F * F1 is FinSequence-like

end;
let F be Function of COMPLEX,D;

let F1 be complex-valued FinSequence;

coherence

F * F1 is FinSequence-like

proof end;

definition

ex b_{1} being UnOp of COMPLEX st

for c being Complex holds b_{1} . c = c ^2

for b_{1}, b_{2} being UnOp of COMPLEX st ( for c being Complex holds b_{1} . c = c ^2 ) & ( for c being Complex holds b_{2} . c = c ^2 ) holds

b_{1} = b_{2}
end;

func sqrcomplex -> UnOp of COMPLEX means :Def1: :: RVSUM_2:def 1

for c being Complex holds it . c = c ^2 ;

existence for c being Complex holds it . c = c ^2 ;

ex b

for c being Complex holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines sqrcomplex RVSUM_2:def 1 :

for b_{1} being UnOp of COMPLEX holds

( b_{1} = sqrcomplex iff for c being Complex holds b_{1} . c = c ^2 );

for b

( b

Lm1: for c, c1 being Complex holds (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1

proof end;

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

proof end;

definition

let F1, F2 be complex-valued FinSequence;

F1 + F2 is FinSequence of COMPLEX by Lm2;

compatibility

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = F1 + F2 iff b_{1} = addcomplex .: (F1,F2) )

for b_{1} being FinSequence of COMPLEX

for F1, F2 being complex-valued FinSequence st b_{1} = addcomplex .: (F1,F2) holds

b_{1} = addcomplex .: (F2,F1)

end;
:: original: +

redefine func F1 + F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 2

addcomplex .: (F1,F2);

coherence redefine func F1 + F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 2

addcomplex .: (F1,F2);

F1 + F2 is FinSequence of COMPLEX by Lm2;

compatibility

for b

( b

proof end;

commutativity for b

for F1, F2 being complex-valued FinSequence st b

b

proof end;

:: deftheorem defines + RVSUM_2:def 2 :

for F1, F2 being complex-valued FinSequence holds F1 + F2 = addcomplex .: (F1,F2);

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;
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;

theorem :: RVSUM_2:3

for s being set

for i being Nat

for R1, R2 being b_{2} -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)

for i being Nat

for R1, R2 being b

proof end;

definition

let F be complex-valued FinSequence;

coherence

- F is FinSequence of COMPLEX by Lm2;

compatibility

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = - F iff b_{1} = compcomplex * F )

end;
coherence

- F is FinSequence of COMPLEX by Lm2;

compatibility

for b

( b

proof end;

:: deftheorem defines - RVSUM_2:def 3 :

for F being complex-valued FinSequence holds - F = compcomplex * F;

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;
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;

theorem :: RVSUM_2:9

for i being Nat

for R, R1, R2 being b_{1} -element FinSequence of COMPLEX st R1 + R = R2 + R holds

R1 = R2

for R, R1, R2 being b

R1 = R2

proof end;

definition

let F1, F2 be complex-valued FinSequence;

F1 - F2 is FinSequence of COMPLEX by Lm2;

compatibility

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = F1 - F2 iff b_{1} = diffcomplex .: (F1,F2) )

end;
:: original: -

redefine func F1 - F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 4

diffcomplex .: (F1,F2);

coherence redefine func F1 - F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 4

diffcomplex .: (F1,F2);

F1 - F2 is FinSequence of COMPLEX by Lm2;

compatibility

for b

( b

proof end;

:: deftheorem defines - RVSUM_2:def 4 :

for F1, F2 being complex-valued FinSequence holds F1 - F2 = diffcomplex .: (F1,F2);

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;
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;

theorem :: RVSUM_2:11

for s being set

for i being Nat

for R1, R2 being b_{2} -element FinSequence of COMPLEX holds (R1 - R2) . s = (R1 . s) - (R2 . s)

for i being Nat

for R1, R2 being b

proof end;

theorem :: RVSUM_2:12

for F being complex-valued FinSequence holds

( (<*> COMPLEX) - F = <*> COMPLEX & F - (<*> COMPLEX) = <*> COMPLEX )

( (<*> COMPLEX) - F = <*> COMPLEX & F - (<*> COMPLEX) = <*> COMPLEX )

proof end;

theorem :: RVSUM_2:18

for i being Nat

for R1, R2 being b_{1} -element FinSequence of COMPLEX st R1 - R2 = i |-> 0c holds

R1 = R2

for R1, R2 being b

R1 = R2

proof end;

definition

let F be complex-valued FinSequence;

let c be Complex;

c * F is FinSequence of COMPLEX by Lm2;

compatibility

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = c * F iff b_{1} = (c multcomplex) * F )

end;
let c be Complex;

:: original: *

redefine func c * F -> FinSequence of COMPLEX equals :: RVSUM_2:def 5

(c multcomplex) * F;

coherence redefine func c * F -> FinSequence of COMPLEX equals :: RVSUM_2:def 5

(c multcomplex) * F;

c * F is FinSequence of COMPLEX by Lm2;

compatibility

for b

( b

proof end;

:: deftheorem defines * RVSUM_2:def 5 :

for F being complex-valued FinSequence

for c being Complex holds c * F = (c multcomplex) * F;

for F being complex-valued FinSequence

for c being Complex holds c * F = (c multcomplex) * F;

definition

let i be Nat;

let R be i -element FinSequence of COMPLEX ;

let c be Complex;

:: 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;
let R be i -element FinSequence of COMPLEX ;

let c be Complex;

:: 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;

theorem :: RVSUM_2:23

for c1, c2 being Complex

for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)

for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)

proof end;

definition

let F1, F2 be complex-valued FinSequence;

mlt (F1,F2) is FinSequence of COMPLEX by Lm2;

compatibility

for b_{1} being FinSequence of COMPLEX holds

( b_{1} = mlt (F1,F2) iff b_{1} = multcomplex .: (F1,F2) )

for b_{1} being FinSequence of COMPLEX

for F1, F2 being complex-valued FinSequence st b_{1} = multcomplex .: (F1,F2) holds

b_{1} = multcomplex .: (F2,F1)

end;
:: original: mlt

redefine func mlt (F1,F2) -> FinSequence of COMPLEX equals :: RVSUM_2:def 6

multcomplex .: (F1,F2);

coherence redefine func mlt (F1,F2) -> FinSequence of COMPLEX equals :: RVSUM_2:def 6

multcomplex .: (F1,F2);

mlt (F1,F2) is FinSequence of COMPLEX by Lm2;

compatibility

for b

( b

proof end;

commutativity for b

for F1, F2 being complex-valued FinSequence st b

b

proof end;

:: deftheorem defines mlt RVSUM_2:def 6 :

for F1, F2 being complex-valued FinSequence holds mlt (F1,F2) = multcomplex .: (F1,F2);

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;
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;

theorem Th27: :: RVSUM_2:27

for i being Nat

for c being Complex

for R being b_{1} -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R

for c being Complex

for R being b

proof end;

theorem Th40: :: RVSUM_2:40

for i being Nat

for R1, R2 being b_{1} -element FinSequence of COMPLEX holds Sum (R1 + R2) = (Sum R1) + (Sum R2)

for R1, R2 being b

proof end;

theorem :: RVSUM_2:41

for i being Nat

for R1, R2 being b_{1} -element FinSequence of COMPLEX holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

for R1, R2 being b

proof end;

Lm3: for F being empty FinSequence holds Product F = 1

proof end;

theorem :: RVSUM_2:43

for c being Complex

for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)

for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)

proof end;

theorem :: RVSUM_2:45

for i, j being Nat

for c being Complex holds Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))

for c being Complex 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 holds Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))

for c being Complex 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 holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))

for c1, c2 being Complex 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 b_{1} -element FinSequence of COMPLEX holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)

for R1, R2 being b

proof end;

theorem :: RVSUM_2:49

for i being Nat

for c being Complex

for R being b_{1} -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)

for c being Complex

for R being b

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))

mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))

proof end;