:: by Noboru Endou

::

:: Received January 26, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

definition

ex b_{1} being non empty set st

for x being set holds

( x in b_{1} iff x is Complex_Sequence )

for b_{1}, b_{2} being non empty set st ( for x being set holds

( x in b_{1} iff x is Complex_Sequence ) ) & ( for x being set holds

( x in b_{2} iff x is Complex_Sequence ) ) holds

b_{1} = b_{2}
end;

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 for x being set holds

( x in it iff x is Complex_Sequence );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines the_set_of_ComplexSequences CSSPACE:def 1 :

for b_{1} being non empty set holds

( b_{1} = the_set_of_ComplexSequences iff for x being set holds

( x in b_{1} iff x is Complex_Sequence ) );

for b

( b

( x in b

definition

let z be set ;

assume A1: z in the_set_of_ComplexSequences ;

coherence

z is Complex_Sequence by A1, Def1;

end;
assume A1: z in the_set_of_ComplexSequences ;

coherence

z is Complex_Sequence by A1, Def1;

:: deftheorem Def2 defines seq_id CSSPACE:def 2 :

for z being set st z in the_set_of_ComplexSequences holds

seq_id z = z;

for z being set st z in the_set_of_ComplexSequences holds

seq_id z = z;

definition

ex b_{1} being BinOp of the_set_of_ComplexSequences st

for a, b being Element of the_set_of_ComplexSequences holds b_{1} . (a,b) = (seq_id a) + (seq_id b)

for b_{1}, b_{2} being BinOp of the_set_of_ComplexSequences st ( for a, b being Element of the_set_of_ComplexSequences holds b_{1} . (a,b) = (seq_id a) + (seq_id b) ) & ( for a, b being Element of the_set_of_ComplexSequences holds b_{2} . (a,b) = (seq_id a) + (seq_id b) ) holds

b_{1} = b_{2}
end;

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 for a, b being Element of the_set_of_ComplexSequences holds it . (a,b) = (seq_id a) + (seq_id b);

ex b

for a, b being Element of the_set_of_ComplexSequences holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines l_add CSSPACE:def 4 :

for b_{1} being BinOp of the_set_of_ComplexSequences holds

( b_{1} = l_add iff for a, b being Element of the_set_of_ComplexSequences holds b_{1} . (a,b) = (seq_id a) + (seq_id b) );

for b

( b

definition

ex b_{1} being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences st

for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds

b_{1} . (z,x) = (C_id z) (#) (seq_id x)

for b_{1}, b_{2} being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences st ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds

b_{1} . (z,x) = (C_id z) (#) (seq_id x) ) & ( for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds

b_{2} . (z,x) = (C_id z) (#) (seq_id x) ) holds

b_{1} = b_{2}
end;

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 is Complex & x in the_set_of_ComplexSequences holds

it . (z,x) = (C_id z) (#) (seq_id x);

existence for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds

it . (z,x) = (C_id z) (#) (seq_id x);

ex b

for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines l_mult CSSPACE:def 5 :

for b_{1} being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences holds

( b_{1} = l_mult iff for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds

b_{1} . (z,x) = (C_id z) (#) (seq_id x) );

for b

( b

b

definition

ex b_{1} being Element of the_set_of_ComplexSequences st

for n being Element of NAT holds (seq_id b_{1}) . n = 0c

for b_{1}, b_{2} being Element of the_set_of_ComplexSequences st ( for n being Element of NAT holds (seq_id b_{1}) . n = 0c ) & ( for n being Element of NAT holds (seq_id b_{2}) . n = 0c ) holds

b_{1} = b_{2}
end;

func CZeroseq -> Element of the_set_of_ComplexSequences means :Def6: :: CSSPACE:def 6

for n being Element of NAT holds (seq_id it) . n = 0c ;

existence for n being Element of NAT holds (seq_id it) . n = 0c ;

ex b

for n being Element of NAT holds (seq_id b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines CZeroseq CSSPACE:def 6 :

for b_{1} being Element of the_set_of_ComplexSequences holds

( b_{1} = CZeroseq iff for n being Element of NAT holds (seq_id b_{1}) . n = 0c );

for b

( b

theorem :: CSSPACE:2

theorem Th3: :: CSSPACE:3

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)

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

theorem Th4: :: CSSPACE:4

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 Th5: :: CSSPACE:5

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 Th6: :: CSSPACE:6

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 Th7: :: CSSPACE:7

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)

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 Th8: :: CSSPACE:8

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)

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 Th9: :: CSSPACE:9

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)

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 Th10: :: CSSPACE:10

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

proof end;

definition

CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) is non empty strict CLSStruct ;

end;

func Linear_Space_of_ComplexSequences -> non empty strict CLSStruct equals :: CSSPACE:def 7

CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #);

coherence CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #);

CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #) is non empty strict CLSStruct ;

:: deftheorem defines Linear_Space_of_ComplexSequences CSSPACE:def 7 :

Linear_Space_of_ComplexSequences = CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #);

Linear_Space_of_ComplexSequences = CLSStruct(# the_set_of_ComplexSequences,CZeroseq,l_add,l_mult #);

registration

( Linear_Space_of_ComplexSequences is Abelian & Linear_Space_of_ComplexSequences is add-associative & Linear_Space_of_ComplexSequences is right_zeroed & Linear_Space_of_ComplexSequences is right_complementable & Linear_Space_of_ComplexSequences is vector-distributive & Linear_Space_of_ComplexSequences is scalar-distributive & Linear_Space_of_ComplexSequences is scalar-associative & Linear_Space_of_ComplexSequences is scalar-unital )
end;

cluster Linear_Space_of_ComplexSequences -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( Linear_Space_of_ComplexSequences is Abelian & Linear_Space_of_ComplexSequences is add-associative & Linear_Space_of_ComplexSequences is right_zeroed & Linear_Space_of_ComplexSequences is right_complementable & Linear_Space_of_ComplexSequences is vector-distributive & Linear_Space_of_ComplexSequences is scalar-distributive & Linear_Space_of_ComplexSequences is scalar-associative & Linear_Space_of_ComplexSequences is scalar-unital )

proof end;

definition

let X be ComplexLinearSpace;

let X1 be Subset of X;

assume B1: X1 is linearly-closed ;

correctness

coherence

the addF of X || X1 is BinOp of X1;

end;
let X1 be Subset of X;

assume B1: X1 is linearly-closed ;

correctness

coherence

the addF of X || X1 is BinOp of X1;

proof end;

:: deftheorem Def8 defines Add_ CSSPACE:def 8 :

for X being ComplexLinearSpace

for X1 being Subset of X st X1 is linearly-closed holds

Add_ (X1,X) = the addF of X || X1;

for X being ComplexLinearSpace

for X1 being Subset of X st X1 is linearly-closed holds

Add_ (X1,X) = the addF of X || X1;

definition

let X be ComplexLinearSpace;

let X1 be Subset of X;

assume B1: X1 is linearly-closed ;

coherence

the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1;

end;
let X1 be Subset of X;

assume B1: X1 is linearly-closed ;

func Mult_ (X1,X) -> Function of [:COMPLEX,X1:],X1 equals :Def9: :: CSSPACE:def 9

the Mult of X | [:COMPLEX,X1:];

correctness the Mult of X | [:COMPLEX,X1:];

coherence

the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1;

proof end;

:: deftheorem Def9 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:];

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 ;

correctness

coherence

0. X is Element of X1;

end;
let X1 be Subset of X;

assume that

A1: X1 is linearly-closed and

A2: not X1 is empty ;

correctness

coherence

0. X is Element of X1;

proof end;

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

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

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

ex b_{1} being Subset of Linear_Space_of_ComplexSequences st

( not b_{1} is empty & ( for x being set holds

( x in b_{1} iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) )

for b_{1}, b_{2} being Subset of Linear_Space_of_ComplexSequences st not b_{1} is empty & ( for x being set holds

( x in b_{1} iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) & not b_{2} is empty & ( for x being set holds

( x in b_{2} iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) holds

b_{1} = b_{2}
end;

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

ex b

( not b

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :

for b_{1} being Subset of Linear_Space_of_ComplexSequences holds

( b_{1} = the_set_of_l2ComplexSequences iff ( not b_{1} is empty & ( for x being set holds

( x in b_{1} iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) ) );

for b

( b

( x in b

theorem :: CSSPACE:13

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 Th11, Th12;

theorem :: CSSPACE:15

( 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, Def4, Th3;

( 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, Def4, Th3;

begin

definition

attr c_{1} is strict ;

struct CUNITSTR -> CLSStruct ;

aggr CUNITSTR(# carrier, ZeroF, addF, Mult, scalar #) -> CUNITSTR ;

sel scalar c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:],COMPLEX;

end;
struct CUNITSTR -> CLSStruct ;

aggr CUNITSTR(# carrier, ZeroF, addF, Mult, scalar #) -> CUNITSTR ;

sel scalar c

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

coherence

not CUNITSTR(# D,Z,a,m,s #) is empty ;

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

coherence

not CUNITSTR(# D,Z,a,m,s #) is empty ;

deffunc H

definition

let X be non empty CUNITSTR ;

let x, y be Point of X;

correctness

coherence

the scalar of X . (x,y) is Complex;

;

end;
let x, y be Point of X;

correctness

coherence

the scalar of X . (x,y) is Complex;

;

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

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;

Lm1: the carrier of ((0). the ComplexLinearSpace) = {(0. the ComplexLinearSpace)}

by CLVECT_1:def 9;

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

Lm2: for x, y being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [x,y] = 0c

by FUNCOP_1:7;

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

by Lm1, TARSKI:def 1;

then Lm3: nilfunc . [(0. the ComplexLinearSpace),(0. the ComplexLinearSpace)] = 0c

by Lm2;

Lm4: for u being VECTOR of ((0). the ComplexLinearSpace) holds

( 0 <= Re (nilfunc . [u,u]) & Im (nilfunc . [u,u]) = 0 )

by COMPLEX1:4, FUNCOP_1:7;

Lm5: for u, v being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [u,v] = (nilfunc . [v,u]) *'

proof end;

Lm6: for u, v, w being VECTOR of ((0). the ComplexLinearSpace) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])

proof end;

Lm7: for u, v being VECTOR of ((0). the ComplexLinearSpace)

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

proof end;

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

Lm8: now :: thesis: for x, y, z being Point of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)

for a being Complex holds

( ( x .|. x = 0c implies x = H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),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) )

for a being Complex holds

( ( x .|. x = 0c implies x = H

let x, y, z be Point of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: thesis: for a being Complex holds

( ( x .|. x = 0c implies x = H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),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 = H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) ) & ( x = H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),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) )

H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = 0. the ComplexLinearSpace
by CLVECT_1:30;

hence ( x .|. x = 0c iff x = H_{1}( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) )
by Lm1, Lm2, TARSKI:def 1; :: 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 Lm4; :: thesis: ( x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus x .|. y = (y .|. x) *' by Lm5; :: 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)

end;
( ( x .|. x = 0c implies x = H

let a be Complex; :: thesis: ( ( x .|. x = 0c implies x = H

H

hence ( x .|. x = 0c iff x = H

thus ( 0 <= Re (x .|. x) & 0 = Im (x .|. x) ) by Lm4; :: thesis: ( x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )

thus x .|. y = (y .|. x) *' by Lm5; :: 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

thus
(a * x) .|. y = a * (x .|. y)
:: thesis: verum
reconsider u = x, v = y, w = z as VECTOR of ((0). the ComplexLinearSpace) ;

(x + y) .|. z = nilfunc . [(u + v),w] ;

hence (x + y) .|. z = (x .|. z) + (y .|. z) by Lm6; :: thesis: verum

end;
(x + y) .|. z = nilfunc . [(u + v),w] ;

hence (x + y) .|. z = (x .|. z) + (y .|. z) by Lm6; :: thesis: verum

definition

let IT be non empty CUNITSTR ;

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

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

:: deftheorem Def13 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) ) );

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

ex b_{1} being non empty CUNITSTR st

( b_{1} is ComplexUnitarySpace-like & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is scalar-unital & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is strict )
end;

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict ComplexUnitarySpace-like for CUNITSTR ;

existence ex b

( b

proof end;

definition

mode ComplexUnitarySpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ComplexUnitarySpace-like CUNITSTR ;

end;
theorem Th17: :: CSSPACE:17

for X being ComplexUnitarySpace

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

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

proof end;

theorem Th18: :: CSSPACE:18

for a being Complex

for X being ComplexUnitarySpace

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

for X being ComplexUnitarySpace

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

proof end;

theorem Th19: :: CSSPACE:19

for a being Complex

for X being ComplexUnitarySpace

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

for X being ComplexUnitarySpace

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

proof end;

theorem Th20: :: 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))

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

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 Th26: :: CSSPACE:26

for X being ComplexUnitarySpace

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

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

proof end;

theorem Th27: :: CSSPACE:27

for X being ComplexUnitarySpace

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

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)

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, y being Point of X holds (x + y) .|. (x + y) = (((x .|. x) + (x .|. y)) + (y .|. x)) + (y .|. y)

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)

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

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)

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

proof end;

Lm9: 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 Th35: :: CSSPACE:35

for X being ComplexUnitarySpace

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

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;

symmetry

for x, y being Point of X st x .|. y = 0 holds

y .|. x = 0 by Def13, COMPLEX1:28;

end;
let x, y be Point of X;

symmetry

for x, y being Point of X st x .|. y = 0 holds

y .|. x = 0 by Def13, COMPLEX1:28;

:: deftheorem Def14 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 );

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

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

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

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) .|. (x + y) = (x .|. x) + (y .|. y)

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)

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;

correctness

coherence

sqrt |.(x .|. x).| is Real;

;

end;
let x be Point of X;

correctness

coherence

sqrt |.(x .|. x).| is Real;

;

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

for X being ComplexUnitarySpace

for x being Point of X holds ||.x.|| = sqrt |.(x .|. x).|;

for X being ComplexUnitarySpace

for x being Point of X holds ||.x.|| = sqrt |.(x .|. x).|;

theorem Th43: :: CSSPACE:43

for a being Complex

for X being ComplexUnitarySpace

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

for X being ComplexUnitarySpace

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

proof end;

theorem :: CSSPACE:45

theorem :: CSSPACE:49

for X being ComplexUnitarySpace

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

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

proof end;

definition
end;

:: deftheorem defines dist CSSPACE:def 16 :

for X being ComplexUnitarySpace

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

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)

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

theorem :: CSSPACE:51

for X being ComplexUnitarySpace

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

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

proof end;

theorem :: CSSPACE:53

theorem :: CSSPACE:55

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

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

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, z, y being Point of X holds dist ((x - z),(y - z)) = dist (x,y)

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

proof end;

theorem :: CSSPACE:59

for X being ComplexUnitarySpace

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

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

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

theorem :: CSSPACE:60

for X being ComplexUnitarySpace

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

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 seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 + seq2 holds

seq is constant

for seq1, seq2, seq 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 seq1, seq2, seq being sequence of X st seq1 is constant & seq2 is constant & seq = seq1 - seq2 holds

seq is constant

for seq1, seq2, seq 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 seq1, seq being sequence of X st seq1 is constant & seq = a * seq1 holds

seq is constant

for X being ComplexUnitarySpace

for seq1, seq 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)

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

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)

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)

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)

for X being ComplexUnitarySpace

for seq being sequence of X holds (a * b) * seq = a * (b * 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)

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)

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

proof end;

theorem :: CSSPACE:75

for X being ComplexUnitarySpace

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

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)

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

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)

for X being ComplexUnitarySpace

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

proof end;

begin

definition

ex b_{1} 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

b_{1} . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *'))

for b_{1}, b_{2} 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

b_{1} . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ) & ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds

b_{2} . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ) holds

b_{1} = b_{2}
end;

func cl_scalar -> Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX means :: CSSPACE:def 17

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 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) *'));

ex b

for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines cl_scalar CSSPACE:def 17 :

for b_{1} being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX holds

( b_{1} = cl_scalar iff for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds

b_{1} . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) );

for b

( b

b

registration

not CUNITSTR(# 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)),cl_scalar #) is empty by Def11;

end;

cluster CUNITSTR(# 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)),cl_scalar #) -> non empty ;

coherence not CUNITSTR(# 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)),cl_scalar #) is empty by Def11;

definition

coherence

CUNITSTR(# 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)),cl_scalar #) is non empty CUNITSTR ;

;

end;

func Complex_l2_Space -> non empty CUNITSTR equals :: CSSPACE:def 18

CUNITSTR(# 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)),cl_scalar #);

correctness CUNITSTR(# 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)),cl_scalar #);

coherence

CUNITSTR(# 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)),cl_scalar #) is non empty CUNITSTR ;

;

:: deftheorem defines Complex_l2_Space CSSPACE:def 18 :

Complex_l2_Space = CUNITSTR(# 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)),cl_scalar #);

Complex_l2_Space = CUNITSTR(# 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)),cl_scalar #);

theorem Th79: :: 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

l is ComplexLinearSpace

proof end;

theorem :: CSSPACE:80

for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds

( seq is summable & Sum seq = 0c )

( seq is summable & Sum seq = 0c )

proof end;

registration

( Complex_l2_Space is Abelian & Complex_l2_Space is add-associative & Complex_l2_Space is right_zeroed & Complex_l2_Space is right_complementable & Complex_l2_Space is vector-distributive & Complex_l2_Space is scalar-distributive & Complex_l2_Space is scalar-associative & Complex_l2_Space is scalar-unital ) by Th14, Th79;

end;

cluster Complex_l2_Space -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( Complex_l2_Space is Abelian & Complex_l2_Space is add-associative & Complex_l2_Space is right_zeroed & Complex_l2_Space is right_complementable & Complex_l2_Space is vector-distributive & Complex_l2_Space is scalar-distributive & Complex_l2_Space is scalar-associative & Complex_l2_Space is scalar-unital ) by Th14, Th79;