:: CSSPACE semantic presentation

definition

func the_set_of_ComplexSequences -> non empty set means :Def1: :: CSSPACE:def 1
for x being set holds
( x in it iff x is Complex_Sequence );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_ComplexSequences CSSPACE:def 1 :

definition

let z be set ;
assume A1: z in the_set_of_ComplexSequences ;
func seq_id z -> Complex_Sequence equals :Def2: :: CSSPACE:def 2
z;
coherence by A1, Def1;

end;

:: deftheorem Def2 defines seq_id CSSPACE:def 2 :

definition

let z be set ;
assume A1: z in COMPLEX ;
func C_id z -> Complex equals :Def3: :: CSSPACE:def 3
z;
coherence by A1;

end;

:: deftheorem Def3 defines C_id CSSPACE:def 3 :

theorem Th1: :: CSSPACE:1

ex ADD being BinOp of the_set_of_ComplexSequences st
( ( for a, b being Element of the_set_of_ComplexSequences holds ADD . a,b = (seq_id a) + (seq_id b) ) & ADD is commutative & ADD is associative )

proof end;

theorem Th2: :: CSSPACE:2

ex f being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences st
for r, x being set st r in COMPLEX & x in the_set_of_ComplexSequences holds
f . [r,x] = (C_id r) (#) (seq_id x)

proof end;

definition

func l_add -> BinOp of the_set_of_ComplexSequences means :Def4: :: CSSPACE:def 4
for a, b being Element of the_set_of_ComplexSequences holds it . a,b = (seq_id a) + (seq_id b);
existence by Th1;
uniqueness

proof end;

end;

:: deftheorem Def4 defines l_add CSSPACE:def 4 :

definition

func l_mult -> Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences means :Def5: :: CSSPACE:def 5
for z, x being set st z in COMPLEX & x in the_set_of_ComplexSequences holds
it . [z,x] = (C_id z) (#) (seq_id x);
existence by Th2;
uniqueness

proof end;

end;

:: deftheorem Def5 defines l_mult CSSPACE:def 5 :

definition

func CZeroseq -> Element of the_set_of_ComplexSequences means :Def6: :: CSSPACE:def 6
for n being Nat holds (seq_id it) . n = 0c ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines CZeroseq CSSPACE:def 6 :

theorem Th3: :: CSSPACE:3

for x being Complex_Sequence holds seq_id x = x

proof end;

theorem Th4: :: CSSPACE:4

for v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds v + w = (seq_id v) + (seq_id w)

proof end;

theorem Th5: :: CSSPACE:5

for z being Complex
for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds z * v = z (#) (seq_id v)

proof end;

registration

cluster CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) -> Abelian ;
coherence

proof end;

end;

Lm1: for u, v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds u + v = v + u
;

theorem Th6: :: CSSPACE:6

for u, v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (u + v) + w = u + (v + w)

proof end;

theorem Th7: :: CSSPACE:7

for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds v + (0. CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #)) = v

proof end;

theorem Th8: :: CSSPACE:8

for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) ex w being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) st v + w = 0. CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #)

proof end;

theorem Th9: :: CSSPACE:9

for z being Complex
for v, w being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds z * (v + w) = (z * v) + (z * w)

proof end;

theorem Th10: :: CSSPACE:10

for z1, z2 being Complex
for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (z1 + z2) * v = (z1 * v) + (z2 * v)

proof end;

theorem Th11: :: CSSPACE:11

for z1, z2 being Complex
for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds (z1 * z2) * v = z1 * (z2 * v)

proof end;

theorem Th12: :: CSSPACE:12

for v being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds 1r * v = v

proof end;

definition

func Linear_Space_of_ComplexSequences -> ComplexLinearSpace equals :: CSSPACE:def 7
CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #);
correctness by Lm1, Th6, Th7, Th8, Th9, Th10, Th11, Th12, CLVECT_1:1;

end;

:: deftheorem defines Linear_Space_of_ComplexSequences CSSPACE:def 7 :

definition

let X be ComplexLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Add_ X1,X -> BinOp of X1 equals :Def8: :: CSSPACE:def 8
the add of X || X1;
correctness

proof end;

end;

:: deftheorem Def8 defines Add_ CSSPACE:def 8 :

definition

let X be ComplexLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Mult_ X1,X -> Function of [:COMPLEX ,X1:],X1 equals :Def9: :: CSSPACE:def 9
the Mult of X | [:COMPLEX ,X1:];
correctness

proof end;

end;

:: deftheorem Def9 defines Mult_ CSSPACE:def 9 :

definition

let X be ComplexLinearSpace;
let X1 be Subset of X;
assume A1: ( X1 is lineary-closed & not X1 is empty ) ;
func Zero_ X1,X -> Element of X1 equals :Def10: :: CSSPACE:def 10
0. X;
correctness

proof end;

end;

:: deftheorem Def10 defines Zero_ CSSPACE:def 10 :

theorem Th13: :: CSSPACE:13

for V being ComplexLinearSpace
for V1 being Subset of V st V1 is lineary-closed & not V1 is empty holds
CLSStruct(# V1,(Zero_ V1,V),(Add_ V1,V),(Mult_ V1,V) #) is Subspace of V

proof end;

definition

func the_set_of_l2ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :Def11: :: CSSPACE:def 11
( not it is empty & ( for x being set holds
( x in it iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :

theorem Th14: :: CSSPACE:14

( the_set_of_l2ComplexSequences is lineary-closed & not the_set_of_l2ComplexSequences is empty )

proof end;

theorem :: CSSPACE:15

CLSStruct(# the_set_of_l2ComplexSequences ,(Zero_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Add_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ),(Mult_ the_set_of_l2ComplexSequences ,Linear_Space_of_ComplexSequences ) #) is Subspace of Linear_Space_of_ComplexSequences by Th13, Th14;

theorem Th16: :: CSSPACE:16

theorem :: CSSPACE:17

( the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & ( for x being set holds
( x is Element of Linear_Space_of_ComplexSequences iff x is Complex_Sequence ) ) & ( for x being set holds
( x is VECTOR of Linear_Space_of_ComplexSequences iff x is Complex_Sequence ) ) & ( for u being VECTOR of Linear_Space_of_ComplexSequences holds u = seq_id u ) & ( for u, v being VECTOR of Linear_Space_of_ComplexSequences holds u + v = (seq_id u) + (seq_id v) ) & ( for z being Complex
for u being VECTOR of Linear_Space_of_ComplexSequences holds z * u = z (#) (seq_id u) ) ) by Def1, Def2, Th4, Th5;

definition

attr c₁ is strict;
struct CUNITSTR -> CLSStruct ;
aggr CUNITSTR(# carrier, Zero, add, Mult, scalar #) -> CUNITSTR ;
sel scalar c₁ -> Function of [:the carrier of c₁,the carrier of c₁:], COMPLEX ;

end;

registration

cluster non empty strict CUNITSTR ;
existence

proof end;

end;

registration

let D be non empty set ;
let Z be Element of D;
let a be BinOp of D;
let m be Function of [:COMPLEX ,D:],D;
let s be Function of [:D,D:], COMPLEX ;
cluster CUNITSTR(# D,Z,a,m,s #) -> non empty ;
coherence

proof end;

end;

deffunc H₁( CUNITSTR ) -> Element of the carrier of $1 = 0. $1;

definition

let X be non empty CUNITSTR ;
let x, y be Point of X;
func x .|. y -> Complex equals :: CSSPACE:def 12
the scalar of X . [x,y];
correctness ;

end;

:: deftheorem defines .|. CSSPACE:def 12 :

consider V0 being ComplexLinearSpace;

Lm2: the carrier of ((0). V0) = {(0. V0)}
by CLVECT_1:def 5;

reconsider nilfunc = [:the carrier of ((0). V0),the carrier of ((0). V0):] --> 0c as Function of [:the carrier of ((0). V0),the carrier of ((0). V0):], COMPLEX by FUNCOP_1:57;

Lm3: for x, y being VECTOR of ((0). V0) holds nilfunc . [x,y] = 0c
by FUNCOP_1:13;

0. V0 in the carrier of ((0). V0)
by Lm2, TARSKI:def 1;

then Lm4: nilfunc . [(0. V0),(0. V0)] = 0c
by Lm3;

Lm5: for u being VECTOR of ((0). V0) holds
( 0 <= Re (nilfunc . [u,u]) & Im (nilfunc . [u,u]) = 0 )

proof end;

Lm6: for u, v being VECTOR of ((0). V0) holds nilfunc . [u,v] = (nilfunc . [v,u]) *'

proof end;

Lm7: for u, v, w being VECTOR of ((0). V0) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])

proof end;

Lm8: for u, v being VECTOR of ((0). V0)
for a being Complex holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])

proof end;

set X0 = CUNITSTR(# the carrier of ((0). V0),the Zero of ((0). V0),the add of ((0). V0),the Mult of ((0). V0),nilfunc #);

Lm9: now

let x, y, z be Point of CUNITSTR(# the carrier of ((0). V0),the Zero of ((0). V0),the add of ((0). V0),the Mult of ((0). V0),nilfunc #); :: thesis:
let a be Complex; :: thesis:
thus ( x .|. x = 0c iff x = H₁( CUNITSTR(# the carrier of ((0). V0),the Zero of ((0). V0),the add of ((0). V0),the Mult of ((0). V0),nilfunc #)) ) :: thesis:

proof

H₁( CUNITSTR(# the carrier of ((0). V0),the Zero of ((0). V0),the add of ((0). V0),the Mult of ((0). V0),nilfunc #)) = the Zero of CUNITSTR(# the carrier of ((0). V0),the Zero of ((0). V0),the add of ((0). V0),the Mult of ((0). V0),nilfunc #)
.= 0. ((0). V0)
.= 0. V0 by CLVECT_1:31 ;
hence ( x .|. x = 0c iff x = H₁( CUNITSTR(# the carrier of ((0). V0),the Zero of ((0). V0),the add of ((0). V0),the Mult of ((0). V0),nilfunc #)) ) by Lm2, Lm4, TARSKI:def 1; :: thesis:

end;

proof

end;

thus (a * x) .|. y = a * (x .|. y) :: thesis:

proof

reconsider u = x, v = y as VECTOR of ((0). V0) ;
( (a * x) .|. y = nilfunc . [(a * u),v] & x .|. y = nilfunc . [u,v] ) ;
hence (a * x) .|. y = a * (x .|. y) by Lm8; :: thesis:

end;

definition

let IT be non empty CUNITSTR ;
attr IT is ComplexUnitarySpace-like means :Def13: :: CSSPACE:def 13
for x, y, w being Point of IT
for a being Complex holds
( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. w = (x .|. w) + (y .|. w) & (a * x) .|. y = a * (x .|. y) );

end;

:: deftheorem Def13 defines ComplexUnitarySpace-like CSSPACE:def 13 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like strict ComplexUnitarySpace-like CUNITSTR ;
existence

proof end;

end;

definition

mode ComplexUnitarySpace is non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexUnitarySpace-like CUNITSTR ;

end;

theorem :: CSSPACE:18

for X being ComplexUnitarySpace holds (0. X) .|. (0. X) = 0 by Def13;

theorem Th19: :: CSSPACE:19

for X being ComplexUnitarySpace
for x, y, z being Point of X holds x .|. (y + z) = (x .|. y) + (x .|. z)

proof end;

theorem Th20: :: CSSPACE:20

for a being Complex
for X being ComplexUnitarySpace
for x, y being Point of X holds x .|. (a * y) = (a *' ) * (x .|. y)

proof end;

theorem Th21: :: CSSPACE:21

for a being Complex
for X being ComplexUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. ((a *' ) * y)

proof end;

theorem Th22: :: CSSPACE:22

for a, b being Complex
for X being ComplexUnitarySpace
for x, y, z being Point of X holds ((a * x) + (b * y)) .|. z = (a * (x .|. z)) + (b * (y .|. z))

proof end;

theorem Th23: :: CSSPACE:23

for a, b being Complex
for X being ComplexUnitarySpace
for x, y, z being Point of X holds x .|. ((a * y) + (b * z)) = ((a *' ) * (x .|. y)) + ((b *' ) * (x .|. z))

proof end;

theorem Th24: :: CSSPACE:24

for X being ComplexUnitarySpace
for x, y being Point of X holds (- x) .|. y = x .|. (- y)

proof end;

theorem Th25: :: CSSPACE:25

for X being ComplexUnitarySpace
for x, y being Point of X holds (- x) .|. y = - (x .|. y)

proof end;

theorem Th26: :: CSSPACE:26

for X being ComplexUnitarySpace
for x, y being Point of X holds x .|. (- y) = - (x .|. y)

proof end;

theorem Th27: :: CSSPACE:27

for X being ComplexUnitarySpace
for x, y being Point of X holds (- x) .|. (- y) = x .|. y

proof end;

theorem Th28: :: CSSPACE:28

for X being ComplexUnitarySpace
for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)

proof end;

theorem Th29: :: CSSPACE:29

for X being ComplexUnitarySpace
for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)

proof end;

theorem :: CSSPACE:30

for X being ComplexUnitarySpace
for x, y, u, v being Point of X holds (x - y) .|. (u - v) = (((x .|. u) - (x .|. v)) - (y .|. u)) + (y .|. v)

proof end;

theorem Th31: :: CSSPACE:31

for X being ComplexUnitarySpace
for x being Point of X holds (0. X) .|. x = 0

proof end;

theorem Th32: :: CSSPACE:32

for X being ComplexUnitarySpace
for x being Point of X holds x .|. (0. X) = 0

proof end;

theorem Th33: :: CSSPACE:33

for X being ComplexUnitarySpace
for x, y being Point of X holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)

proof end;

theorem :: CSSPACE:34

for X being ComplexUnitarySpace
for x, y being Point of X holds (x + y) .|. (x - y) = (((x .|. x) - (x .|. y)) + (y .|. x)) - (y .|. y)

proof end;

theorem Th35: :: CSSPACE:35

for X being ComplexUnitarySpace
for x, y being Point of X holds (x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y)

proof end;

Lm10: for X being ComplexUnitarySpace
for p, q being Complex
for x, y being Point of X holds ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *' )) * (x .|. x)) + ((p * (q *' )) * (x .|. y))) + (((p *' ) * q) * (y .|. x))) + ((q * (q *' )) * (y .|. y))

proof end;

theorem Th36: :: CSSPACE:36

for X being ComplexUnitarySpace
for x being Point of X holds |.(x .|. x).| = Re (x .|. x)

proof end;

theorem Th37: :: CSSPACE:37

for X being ComplexUnitarySpace
for x, y being Point of X holds |.(x .|. y).| <= (sqrt |.(x .|. x).|) * (sqrt |.(y .|. y).|)

proof end;

definition

let X be ComplexUnitarySpace;
let x, y be Point of X;
pred x,y are_orthogonal means :Def14: :: CSSPACE:def 14
x .|. y = 0;
symmetry by Def13, COMPLEX1:113;

end;

:: deftheorem Def14 defines are_orthogonal CSSPACE:def 14 :

theorem :: CSSPACE:38

for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
x, - y are_orthogonal

proof end;

theorem :: CSSPACE:39

for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x,y are_orthogonal

proof end;

theorem :: CSSPACE:40

for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x, - y are_orthogonal

proof end;

theorem :: CSSPACE:41

for X being ComplexUnitarySpace
for x being Point of X holds x, 0. X are_orthogonal

proof end;

theorem :: CSSPACE:42

for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
(x + y) .|. (x + y) = (x .|. x) + (y .|. y)

proof end;

theorem :: CSSPACE:43

for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
(x - y) .|. (x - y) = (x .|. x) + (y .|. y)

proof end;

definition

let X be ComplexUnitarySpace;
let x be Point of X;
func ||.x.|| -> Real equals :: CSSPACE:def 15
sqrt |.(x .|. x).|;
correctness ;

end;

:: deftheorem defines ||. CSSPACE:def 15 :

theorem Th44: :: CSSPACE:44

for X being ComplexUnitarySpace
for x being Point of X holds
( ||.x.|| = 0 iff x = 0. X )

proof end;

theorem Th45: :: CSSPACE:45

for a being Complex
for X being ComplexUnitarySpace
for x being Point of X holds ||.(a * x).|| = |.a.| * ||.x.||

proof end;

theorem Th46: :: CSSPACE:46

for X being ComplexUnitarySpace
for x being Point of X holds 0 <= ||.x.||

proof end;

theorem Th47: :: CSSPACE:47

for X being ComplexUnitarySpace
for x, y being Point of X holds |.(x .|. y).| <= ||.x.|| * ||.y.|| by Th37;

theorem Th48: :: CSSPACE:48

for X being ComplexUnitarySpace
for x, y being Point of X holds ||.(x + y).|| <= ||.x.|| + ||.y.||

proof end;

theorem Th49: :: CSSPACE:49

for X being ComplexUnitarySpace
for x being Point of X holds ||.(- x).|| = ||.x.||

proof end;

theorem Th50: :: CSSPACE:50

for X being ComplexUnitarySpace
for x, y being Point of X holds ||.x.|| - ||.y.|| <= ||.(x - y).||

proof end;

theorem :: CSSPACE:51

for X being ComplexUnitarySpace
for x, y being Point of X holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||

proof end;

definition

let X be ComplexUnitarySpace;
let x, y be Point of X;
func dist x,y -> Real equals :: CSSPACE:def 16
||.(x - y).||;
correctness ;

end;

:: deftheorem defines dist CSSPACE:def 16 :

theorem Th52: :: CSSPACE:52

for X being ComplexUnitarySpace
for x, y being Point of X holds dist x,y = dist y,x

proof end;

definition

let X be ComplexUnitarySpace;
let x, y be Point of X;
:: original: dist
redefine func dist x,y -> Real;
commutativity by Th52;

end;

theorem Th53: :: CSSPACE:53

for X being ComplexUnitarySpace
for x being Point of X holds dist x,x = 0

proof end;

theorem :: CSSPACE:54

for X being ComplexUnitarySpace
for x, z, y being Point of X holds dist x,z <= (dist x,y) + (dist y,z)

proof end;

theorem Th55: :: CSSPACE:55

for X being ComplexUnitarySpace
for x, y being Point of X holds
( x <> y iff dist x,y <> 0 )

proof end;

theorem Th56: :: CSSPACE:56

for X being ComplexUnitarySpace
for x, y being Point of X holds dist x,y >= 0 by Th46;

theorem :: CSSPACE:57

for X being ComplexUnitarySpace
for x, y being Point of X holds
( x <> y iff dist x,y > 0 )

proof end;

theorem :: CSSPACE:58

for X being ComplexUnitarySpace
for x, y being Point of X holds dist x,y = sqrt |.((x - y) .|. (x - y)).| ;

theorem :: CSSPACE:59

for X being ComplexUnitarySpace
for x, y, u, v being Point of X holds dist (x + y),(u + v) <= (dist x,u) + (dist y,v)

proof end;

theorem :: CSSPACE:60

for X being ComplexUnitarySpace
for x, y, u, v being Point of X holds dist (x - y),(u - v) <= (dist x,u) + (dist y,v)

proof end;

theorem :: CSSPACE:61

for X being ComplexUnitarySpace
for x, z, y being Point of X holds dist (x - z),(y - z) = dist x,y

proof end;

theorem :: CSSPACE:62

for X being ComplexUnitarySpace
for x, z, y being Point of X holds dist (x - z),(y - z) <= (dist z,x) + (dist z,y)

proof end;

definition

let X be ComplexUnitarySpace;
let seq be sequence of X;
func - seq -> sequence of X means :Def17: :: CSSPACE:def 17
for n being Nat holds it . n = - (seq . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines - CSSPACE:def 17 :

definition

let X be ComplexUnitarySpace;
let seq be sequence of X;
let x be Point of X;
func seq + x -> sequence of X means :Def18: :: CSSPACE:def 18
for n being Nat holds it . n = (seq . n) + x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines + CSSPACE:def 18 :

theorem Th63: :: CSSPACE:63

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1

proof end;

definition

let X be ComplexUnitarySpace;
let seq1, seq2 be sequence of X;
:: original: +
redefine func seq1 + seq2 -> M6( NAT ,the carrier of X);
commutativity by Th63;

end;

theorem :: CSSPACE:64

for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3

proof end;

theorem :: CSSPACE:65

for X being ComplexUnitarySpace
for seq1, seq2, seq being sequence of X st seq1 is V67 & seq2 is V67 & seq = seq1 + seq2 holds
seq is V67

proof end;

theorem :: CSSPACE:66

for X being ComplexUnitarySpace
for seq1, seq2, seq being sequence of X st seq1 is V67 & seq2 is V67 & seq = seq1 - seq2 holds
seq is V67

proof end;

theorem :: CSSPACE:67

for a being Complex
for X being ComplexUnitarySpace
for seq1, seq being sequence of X st seq1 is V67 & seq = a * seq1 holds
seq is V67

proof end;

theorem Th68: :: CSSPACE:68

for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is V67 iff for n being Nat holds seq . n = seq . (n + 1) )

proof end;

theorem Th69: :: CSSPACE:69

for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is V67 iff for n, k being Nat holds seq . n = seq . (n + k) )

proof end;

theorem :: CSSPACE:70

for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is V67 iff for n, m being Nat holds seq . n = seq . m )

proof end;

theorem :: CSSPACE:71

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2)

proof end;

theorem :: CSSPACE:72

for X being ComplexUnitarySpace
for seq being sequence of X holds seq = seq + (0. X)

proof end;

theorem :: CSSPACE:73

for a being Complex
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 + seq2) = (a * seq1) + (a * seq2)

proof end;

theorem :: CSSPACE:74

for a, b being Complex
for X being ComplexUnitarySpace
for seq being sequence of X holds (a + b) * seq = (a * seq) + (b * seq)

proof end;

theorem :: CSSPACE:75

for a, b being Complex
for X being ComplexUnitarySpace
for seq being sequence of X holds (a * b) * seq = a * (b * seq)

proof end;

theorem :: CSSPACE:76

for X being ComplexUnitarySpace
for seq being sequence of X holds 1r * seq = seq

proof end;

theorem :: CSSPACE:77

for X being ComplexUnitarySpace
for seq being sequence of X holds (- 1r ) * seq = - seq

proof end;

theorem :: CSSPACE:78

for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X holds seq - x = seq + (- x)

proof end;

theorem :: CSSPACE:79

for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1)

proof end;

theorem :: CSSPACE:80

for X being ComplexUnitarySpace
for seq being sequence of X holds seq = seq - (0. X)

proof end;

theorem :: CSSPACE:81

for X being ComplexUnitarySpace
for seq being sequence of X holds seq = - (- seq)

proof end;

theorem :: CSSPACE:82

for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3

proof end;

theorem :: CSSPACE:83

for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)

proof end;

theorem :: CSSPACE:84

for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3

proof end;

theorem :: CSSPACE:85

for a being Complex
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds a * (seq1 - seq2) = (a * seq1) - (a * seq2)

proof end;

theorem Th86: :: CSSPACE:86

ex f being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX st
for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
f . [x,y] = Sum ((seq_id x) (#) ((seq_id y) *' ))

proof end;

definition

func cl_scalar -> Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX means :: CSSPACE:def 19
for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
it . [x,y] = Sum ((seq_id x) (#) ((seq_id y) *' ));
existence by Th86;
uniqueness

proof end;

end;

:: deftheorem defines cl_scalar CSSPACE:def 19 :

registration end;

definition end;

:: deftheorem defines Complex_l2_Space CSSPACE:def 20 :

theorem Th87: :: CSSPACE:87

for l being CUNITSTR st CLSStruct(# the carrier of l,the Zero of l,the add of l,the Mult of l #) is ComplexLinearSpace holds
l is ComplexLinearSpace

proof end;

theorem :: CSSPACE:88

for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds
( seq is summable & Sum seq = 0c )

proof end;

registration end;