:: Complex Linear Space of Complex Sequences
:: by Noboru Endou
::
:: Copyright (c) 2004-2019 Association of Mizar Users

definition
coherence
Funcs (NAT,COMPLEX) is non empty set
;
end;

:: deftheorem defines the_set_of_ComplexSequences CSSPACE:def 1 :

definition
let z be object ;
assume A1: z in the_set_of_ComplexSequences ;
func seq_id z -> Complex_Sequence equals :Def2: :: CSSPACE:def 2
z;
coherence by ;
end;

:: deftheorem Def2 defines seq_id CSSPACE:def 2 :
for z being object st z in the_set_of_ComplexSequences holds
seq_id z = z;

registration
let z be Element of the_set_of_ComplexSequences ;
reduce seq_id z to z;
reducibility
seq_id z = z
by Def2;
end;

definition
let z be object ;
assume A1: z is Complex ;
func C_id z -> Complex equals :Def3: :: CSSPACE:def 3
z;
coherence
z is Complex
by A1;
end;

:: deftheorem Def3 defines C_id CSSPACE:def 3 :
for z being object st z is Complex holds
C_id z = z;

registration
let z be Complex;
reduce C_id z to z;
reducibility
C_id z = z
by Def3;
end;

definition
::$CD 2 coherence by FUNCT_2:8; end; :: deftheorem CSSPACE:def 4 : canceled; :: deftheorem CSSPACE:def 5 : canceled; :: deftheorem defines CZeroseq CSSPACE:def 6 : registration let x be Complex_Sequence; reduce seq_id x to x; reducibility seq_id x = x proof end; end; theorem :: CSSPACE:1 for x being Complex_Sequence holds seq_id x = x ; definition coherence ; end; :: deftheorem defines Linear_Space_of_ComplexSequences CSSPACE:def 7 : registration end; registration let z be VECTOR of Linear_Space_of_ComplexSequences; reduce seq_id z to z; reducibility seq_id z = z by Def2; end; theorem Th2: :: CSSPACE:2 for v, w being VECTOR of Linear_Space_of_ComplexSequences holds v + w = () + () proof end; theorem Th3: :: CSSPACE:3 for z being Complex for v being VECTOR of Linear_Space_of_ComplexSequences holds z * v = z (#) () proof end; theorem Th4: :: CSSPACE:4 for n being object holds . n = 0 proof end; theorem :: CSSPACE:5 for f being Element of the_set_of_ComplexSequences st ( for n being Nat holds () . n = 0 ) holds f = CZeroseq proof end; theorem :: CSSPACE:6 canceled; theorem :: CSSPACE:7 canceled; theorem :: CSSPACE:8 canceled; theorem :: CSSPACE:9 canceled; theorem :: CSSPACE:10 canceled; ::$CT 5
definition
let X be ComplexLinearSpace;
let X1 be Subset of X;
assume A1: X1 is linearly-closed ;
func Add_ (X1,X) -> BinOp of X1 equals :Def6: :: CSSPACE:def 8
the addF of X || X1;
correctness
coherence
the addF of X || X1 is BinOp of X1
;
proof end;
end;

:: deftheorem Def6 defines Add_ CSSPACE:def 8 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed holds

definition
let X be ComplexLinearSpace;
let X1 be Subset of X;
assume A1: X1 is linearly-closed ;
func Mult_ (X1,X) -> Function of [:COMPLEX,X1:],X1 equals :Def7: :: CSSPACE:def 9
the Mult of X | [:COMPLEX,X1:];
correctness
coherence
the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1
;
proof end;
end;

:: deftheorem Def7 defines Mult_ CSSPACE:def 9 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed holds
Mult_ (X1,X) = the Mult of X | [:COMPLEX,X1:];

definition
let X be ComplexLinearSpace;
let X1 be Subset of X;
assume that
A1: X1 is linearly-closed and
A2: not X1 is empty ;
func Zero_ (X1,X) -> Element of X1 equals :Def8: :: CSSPACE:def 10
0. X;
correctness
coherence
0. X is Element of X1
;
proof end;
end;

:: deftheorem Def8 defines Zero_ CSSPACE:def 10 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Zero_ (X1,X) = 0. X;

theorem Th6: :: CSSPACE:11
for V being ComplexLinearSpace
for V1 being Subset of V st V1 is linearly-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 :Def9: :: CSSPACE:def 11
for x being object holds
( x in it iff ( x in the_set_of_ComplexSequences & |.().| (#) |.().| is summable ) );
existence
ex b1 being Subset of Linear_Space_of_ComplexSequences st
for x being object holds
( x in b1 iff ( x in the_set_of_ComplexSequences & |.().| (#) |.().| is summable ) )
proof end;
uniqueness
for b1, b2 being Subset of Linear_Space_of_ComplexSequences st ( for x being object holds
( x in b1 iff ( x in the_set_of_ComplexSequences & |.().| (#) |.().| is summable ) ) ) & ( for x being object holds
( x in b2 iff ( x in the_set_of_ComplexSequences & |.().| (#) |.().| is summable ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :
for b1 being Subset of Linear_Space_of_ComplexSequences holds
( b1 = the_set_of_l2ComplexSequences iff for x being object holds
( x in b1 iff ( x in the_set_of_ComplexSequences & |.().| (#) |.().| is summable ) ) );

Lm1:
proof end;

registration
coherence
proof end;
end;

theorem Th7: :: CSSPACE:12
proof end;

registration end;

registration
let z be Element of the_set_of_l2ComplexSequences ;
reduce seq_id z to z;
reducibility
seq_id z = z
;
end;

theorem :: CSSPACE:15
( the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & ( 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 = () + () ) & ( for z being Complex
for u being VECTOR of Linear_Space_of_ComplexSequences holds z * u = z (#) () ) ) by ;

definition
attr c1 is strict ;
struct CUNITSTR -> CLSStruct ;
aggr CUNITSTR(# carrier, ZeroF, addF, Mult, scalar #) -> CUNITSTR ;
sel scalar c1 -> Function of [: the carrier of c1, the carrier of c1:],COMPLEX;
end;

registration
cluster non empty strict for CUNITSTR ;
existence
ex b1 being CUNITSTR st
( not b1 is empty & b1 is strict )
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 ,D;
let s be Function of [:D,D:],COMPLEX;
cluster CUNITSTR(# D,Z,a,m,s #) -> non empty ;
coherence
not CUNITSTR(# D,Z,a,m,s #) is empty
;
end;

deffunc H1( 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
coherence
the scalar of X . (x,y) is Complex
;
;
end;

:: deftheorem defines .|. CSSPACE:def 12 :
for X being non empty CUNITSTR
for x, y being Point of X holds x .|. y = the scalar of X . (x,y);

set V0 = the ComplexLinearSpace;

Lm2: the carrier of () = {()}
by CLVECT_1:def 9;

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

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

0. the ComplexLinearSpace in the carrier of ()
by ;

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

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

by ;

Lm6: for u, v being VECTOR of () holds nilfunc . [u,v] = (nilfunc . [v,u]) *'
proof end;

Lm7: for u, v, w being VECTOR of () holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
proof end;

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

proof end;

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

Lm9: now :: thesis: for x, y, z being Point of CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)
for a being Complex holds
( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
let x, y, z be Point of CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #); :: thesis: for a being Complex holds
( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

let a be Complex; :: thesis: ( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) = 0. the ComplexLinearSpace by CLVECT_1:30;
hence ( x .|. x = 0c iff x = H1( CUNITSTR(# the carrier of (),(0. ()), the addF of (), the Mult of (),nilfunc #)) ) by ; :: thesis: ( 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
thus ( 0 <= Re (x .|. x) & 0 = Im (x .|. x) ) by Lm5; :: thesis: ( x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
thus x .|. y = (y .|. x) *' by Lm6; :: thesis: ( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
thus (x + y) .|. z = (x .|. z) + (y .|. z) :: thesis: (a * x) .|. y = a * (x .|. y)
proof
reconsider u = x, v = y, w = z as VECTOR of () ;
(x + y) .|. z = nilfunc . [(u + v),w] ;
hence (x + y) .|. z = (x .|. z) + (y .|. z) by Lm7; :: thesis: verum
end;
thus (a * x) .|. y = a * (x .|. y) :: thesis: verum
proof
reconsider u = x, v = y as VECTOR of () ;
(a * x) .|. y = nilfunc . [(a * u),v] ;
hence (a * x) .|. y = a * (x .|. y) by Lm8; :: thesis: verum
end;
end;

definition
let IT be non empty CUNITSTR ;
attr IT is ComplexUnitarySpace-like means :Def11: :: 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 Def11 defines ComplexUnitarySpace-like CSSPACE:def 13 :
for IT being non empty CUNITSTR holds
( IT is ComplexUnitarySpace-like iff 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) ) );

registration
existence
ex b1 being non empty CUNITSTR st
( b1 is ComplexUnitarySpace-like & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is strict )
proof end;
end;

definition end;

theorem :: CSSPACE:16
for X being ComplexUnitarySpace holds (0. X) .|. (0. X) = 0 by Def11;

theorem Th12: :: CSSPACE:17
for X being ComplexUnitarySpace
for x, y, z being Point of X holds x .|. (y + z) = (x .|. y) + (x .|. z)
proof end;

theorem Th13: :: CSSPACE:18
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 Th14: :: CSSPACE:19
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 Th15: :: CSSPACE:20
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 Th16: :: CSSPACE:21
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 Th17: :: CSSPACE:22
for X being ComplexUnitarySpace
for x, y being Point of X holds (- x) .|. y = x .|. (- y)
proof end;

theorem Th18: :: CSSPACE:23
for X being ComplexUnitarySpace
for x, y being Point of X holds (- x) .|. y = - (x .|. y)
proof end;

theorem Th19: :: CSSPACE:24
for X being ComplexUnitarySpace
for x, y being Point of X holds x .|. (- y) = - (x .|. y)
proof end;

theorem Th20: :: CSSPACE:25
for X being ComplexUnitarySpace
for x, y being Point of X holds (- x) .|. (- y) = x .|. y
proof end;

theorem Th21: :: CSSPACE:26
for X being ComplexUnitarySpace
for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)
proof end;

theorem Th22: :: CSSPACE:27
for X being ComplexUnitarySpace
for x, y, z being Point of X holds x .|. (y - z) = (x .|. y) - (x .|. z)
proof end;

theorem :: CSSPACE:28
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 Th24: :: CSSPACE:29
for X being ComplexUnitarySpace
for x being Point of X holds (0. X) .|. x = 0
proof end;

theorem Th25: :: CSSPACE:30
for X being ComplexUnitarySpace
for x being Point of X holds x .|. (0. X) = 0
proof end;

theorem Th26: :: CSSPACE:31
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:32
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 Th28: :: 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;

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 Th29: :: CSSPACE:34
for X being ComplexUnitarySpace
for x being Point of X holds |.(x .|. x).| = Re (x .|. x)
proof end;

theorem Th30: :: CSSPACE:35
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 :Def12: :: CSSPACE:def 14
x .|. y = 0 ;
symmetry
for x, y being Point of X st x .|. y = 0 holds
y .|. x = 0
by ;
end;

:: deftheorem Def12 defines are_orthogonal CSSPACE:def 14 :
for X being ComplexUnitarySpace
for x, y being Point of X holds
( x,y are_orthogonal iff x .|. y = 0 );

theorem :: CSSPACE:36
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:37
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:38
for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
- x, - y are_orthogonal by Th20;

theorem :: CSSPACE:39
for X being ComplexUnitarySpace
for x being Point of X holds x, 0. X 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) .|. (x + y) = (x .|. x) + (y .|. y)
proof end;

theorem :: CSSPACE:41
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 -> Real equals :: CSSPACE:def 15
sqrt |.(x .|. x).|;
correctness
coherence
sqrt |.(x .|. x).| is Real
;
;
end;

:: deftheorem defines ||. CSSPACE:def 15 :
for X being ComplexUnitarySpace
for x being Point of X holds = sqrt |.(x .|. x).|;

theorem Th37: :: CSSPACE:42
for X being ComplexUnitarySpace
for x being Point of X holds
( = 0 iff x = 0. X )
proof end;

theorem Th38: :: CSSPACE:43
for a being Complex
for X being ComplexUnitarySpace
for x being Point of X holds ||.(a * x).|| = |.a.| *
proof end;

theorem Th39: :: CSSPACE:44
for X being ComplexUnitarySpace
for x being Point of X holds 0 <=
proof end;

theorem :: CSSPACE:45
for X being ComplexUnitarySpace
for x, y being Point of X holds |.(x .|. y).| <= * by Th30;

theorem Th41: :: CSSPACE:46
for X being ComplexUnitarySpace
for x, y being Point of X holds ||.(x + y).|| <= +
proof end;

theorem Th42: :: CSSPACE:47
for X being ComplexUnitarySpace
for x being Point of X holds ||.(- x).|| =
proof end;

theorem Th43: :: CSSPACE:48
for X being ComplexUnitarySpace
for x, y being Point of X holds - <= ||.(x - y).||
proof end;

theorem :: CSSPACE:49
for X being ComplexUnitarySpace
for x, y being Point of X holds |.().| <= ||.(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
coherence
||.(x - y).|| is Real
;
;
end;

:: deftheorem defines dist CSSPACE:def 16 :
for X being ComplexUnitarySpace
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;

definition
let X be ComplexUnitarySpace;
let x, y be Point of X;
:: original: dist
redefine func dist (x,y) -> Real;
commutativity
for x, y being Point of X holds dist (x,y) = dist (y,x)
proof end;
end;

theorem Th45: :: CSSPACE:50
for X being ComplexUnitarySpace
for x being Point of X holds dist (x,x) = 0
proof end;

theorem :: CSSPACE:51
for X being ComplexUnitarySpace
for x, y, z being Point of X holds dist (x,z) <= (dist (x,y)) + (dist (y,z))
proof end;

theorem Th47: :: CSSPACE:52
for X being ComplexUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) <> 0 )
proof end;

theorem :: CSSPACE:53
for X being ComplexUnitarySpace
for x, y being Point of X holds dist (x,y) >= 0 by Th39;

theorem :: CSSPACE:54
for X being ComplexUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) > 0 )
proof end;

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

theorem :: CSSPACE:56
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:57
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:58
for X being ComplexUnitarySpace
for x, y, z being Point of X holds dist ((x - z),(y - z)) = dist (x,y)
proof end;

theorem :: CSSPACE:59
for X being ComplexUnitarySpace
for x, y, z being Point of X holds dist ((x - z),(y - z)) <= (dist (z,x)) + (dist (z,y))
proof end;

definition
let X be ComplexUnitarySpace;
let seq1, seq2 be sequence of X;
:: original: +
redefine func seq1 + seq2 -> Element of bool [:NAT, the carrier of X:];
commutativity
for seq1, seq2 being sequence of X holds seq1 + seq2 = seq2 + seq1
proof end;
end;

theorem :: CSSPACE:60
for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3
proof end;

theorem :: CSSPACE:61
for X being ComplexUnitarySpace
for seq, seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 + seq2 holds
seq is constant
proof end;

theorem :: CSSPACE:62
for X being ComplexUnitarySpace
for seq, seq1, seq2 being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 - seq2 holds
seq is constant
proof end;

theorem :: CSSPACE:63
for a being Complex
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq1 is constant & seq = a * seq1 holds
seq is constant
proof end;

theorem :: CSSPACE:64
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = seq1 + (- seq2)
proof end;

theorem :: CSSPACE:65
for X being ComplexUnitarySpace
for seq being sequence of X holds seq = seq + (0. X)
proof end;

theorem :: CSSPACE:66
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:67
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:68
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:69
for X being ComplexUnitarySpace
for seq being sequence of X holds 1r * seq = seq
proof end;

theorem :: CSSPACE:70
for X being ComplexUnitarySpace
for seq being sequence of X holds () * seq = - seq
proof end;

theorem :: CSSPACE:71
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:72
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds seq1 - seq2 = - (seq2 - seq1)
proof end;

theorem :: CSSPACE:73
for X being ComplexUnitarySpace
for seq being sequence of X holds seq = seq - (0. X)
proof end;

theorem :: CSSPACE:74
for X being ComplexUnitarySpace
for seq being sequence of X holds seq = - (- seq)
proof end;

theorem :: CSSPACE:75
for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof end;

theorem :: CSSPACE:76
for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3)
proof end;

theorem :: CSSPACE:77
for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof end;

theorem :: CSSPACE:78
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;

definition
func cl_scalar -> Function of ,COMPLEX means :: CSSPACE:def 17
for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
it . (x,y) = Sum (() (#) (() *'));
existence
ex b1 being Function of ,COMPLEX st
for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . (x,y) = Sum (() (#) (() *'))
proof end;
uniqueness
for b1, b2 being Function of ,COMPLEX st ( for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . (x,y) = Sum (() (#) (() *')) ) & ( for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b2 . (x,y) = Sum (() (#) (() *')) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines cl_scalar CSSPACE:def 17 :
for b1 being Function of ,COMPLEX holds
( b1 = cl_scalar iff for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . (x,y) = Sum (() (#) (() *')) );

theorem Th74: :: CSSPACE:79
for l being CLSStruct st CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace holds
l is ComplexLinearSpace
proof end;

theorem :: CSSPACE:80
for seq being Complex_Sequence st ( for n being Nat holds seq . n = 0c ) holds
( seq is summable & Sum seq = 0c )
proof end;

registration
coherence by ;
end;

theorem :: CSSPACE:81