:: CLVECT_1 semantic presentation

definition

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

end;

registration

cluster non empty CLSStruct ;
existence

proof end;

end;

definition

let V be CLSStruct ;
mode VECTOR of V is Element of V;

end;

definition

let V be non empty CLSStruct ;
let v be VECTOR of V;
let z be Complex;
func z * v -> Element of V equals :: CLVECT_1:def 1
the Mult of V . [z,v];
coherence ;

end;

registration

let ZS be non empty set ;
let O be Element of ZS;
let F be BinOp of ZS;
let G be Function of [:COMPLEX ,ZS:],ZS;
cluster CLSStruct(# ZS,O,F,G #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

Lm1: now

take ZS = {0}; :: thesis:
reconsider O = 0 as Element of ZS by TARSKI:def 1;
take O = O; :: thesis:
deffunc H₁( Element of ZS, Element of ZS) -> Element of ZS = O;
consider F being BinOp of ZS such that
A1: for x, y being Element of ZS holds F . x,y = H₁(x,y) from BINOP_1:sch 2( V );
reconsider G = [:COMPLEX ,ZS:] --> O as Function of [:COMPLEX ,ZS:],ZS by FUNCOP_1:57;
A2: for a being Element of COMPLEX
for x being Element of ZS holds G . [a,x] = O

proof

let a be Element of COMPLEX ; :: thesis:
let x be Element of ZS; :: thesis:
[a,x] in [:COMPLEX ,ZS:] ;
hence G . [a,x] = O by FUNCOP_1:13; :: thesis:

end;

take F = F; :: thesis:
take G = G; :: thesis:
set W = CLSStruct(# ZS,O,F,G #);
thus for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + y = y + x :: thesis:

proof

let x, y be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
A3: ( x + y = F . x,y & y + x = F . y,x ) ;
reconsider X = x, Y = y as Element of ZS ;
( x + y = H₁(X,Y) & y + x = H₁(Y,X) ) by A1, A3;
hence x + y = y + x ; :: thesis:

end;

thus for x, y, z being VECTOR of CLSStruct(# ZS,O,F,G #) holds (x + y) + z = x + (y + z) :: thesis:

proof

let x, y, z be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
A4: ( (x + y) + z = F . (x + y),z & x + (y + z) = F . x,(y + z) ) ;
reconsider X = x, Y = y, Z = z as Element of ZS ;
( (x + y) + z = H₁(H₁(X,Y),Z) & x + (y + z) = H₁(X,H₁(Y,Z)) ) by A1, A4;
hence (x + y) + z = x + (y + z) ; :: thesis:

end;

thus for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds x + (0. CLSStruct(# ZS,O,F,G #)) = x :: thesis:

proof

let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
reconsider X = x as Element of ZS ;
x + (0. CLSStruct(# ZS,O,F,G #)) = F . [x,(0. CLSStruct(# ZS,O,F,G #))]
.= F . x,(0. CLSStruct(# ZS,O,F,G #))
.= H₁(X,O) by A1 ;
hence x + (0. CLSStruct(# ZS,O,F,G #)) = x by TARSKI:def 1; :: thesis:

end;

thus for x being VECTOR of CLSStruct(# ZS,O,F,G #) ex y being VECTOR of CLSStruct(# ZS,O,F,G #) st x + y = 0. CLSStruct(# ZS,O,F,G #) :: thesis:

proof

let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
reconsider y = O as VECTOR of CLSStruct(# ZS,O,F,G #) ;
take y ; :: thesis:
thus x + y = F . [x,y]
.= F . x,y
.= the Zero of CLSStruct(# ZS,O,F,G #) by A1
.= 0. CLSStruct(# ZS,O,F,G #) ; :: thesis:

end;

thus for z being Complex
for x, y being VECTOR of CLSStruct(# ZS,O,F,G #) holds z * (x + y) = (z * x) + (z * y) :: thesis:

proof

let z be Complex; :: thesis:
let x, y be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
reconsider X = x, Y = y as Element of ZS ;
(z * x) + (z * y) = F . [(z * x),(z * y)]
.= F . (z * x),(z * y)
.= H₁(O,O) by A1 ;
hence z * (x + y) = (z * x) + (z * y) by A2; :: thesis:

end;

thus for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 + z2) * x = (z1 * x) + (z2 * x) :: thesis:

proof

let z1, z2 be Complex; :: thesis:
let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
set c = z1 + z2;
reconsider X = x as Element of ZS ;
A5: (z1 + z2) * x = G . [(z1 + z2),x]
.= O by A2 ;
(z1 * x) + (z2 * x) = F . [(z1 * x),(z2 * x)]
.= F . (z1 * x),(z2 * x)
.= H₁(O,O) by A1 ;
hence (z1 + z2) * x = (z1 * x) + (z2 * x) by A5; :: thesis:

end;

thus for z1, z2 being Complex
for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds (z1 * z2) * x = z1 * (z2 * x) :: thesis:

proof

let z1, z2 be Complex; :: thesis:
let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
set c = z1 * z2;
reconsider X = x as Element of ZS ;
A6: (z1 * z2) * x = G . [(z1 * z2),x]
.= O by A2 ;
z1 * (z2 * x) = G . [z1,(z2 * x)]
.= O by A2 ;
hence (z1 * z2) * x = z1 * (z2 * x) by A6; :: thesis:

end;

thus for x being VECTOR of CLSStruct(# ZS,O,F,G #) holds 1r * x = x :: thesis:

proof

let x be VECTOR of CLSStruct(# ZS,O,F,G #); :: thesis:
reconsider X = x as Element of ZS ;
reconsider A' = 1 as Element of REAL ;
1r * x = G . [1r ,x]
.= O by A2 ;
hence 1r * x = x by TARSKI:def 1; :: thesis:

end;

definition

let IT be non empty CLSStruct ;
attr IT is ComplexLinearSpace-like means :Def2: :: CLVECT_1:def 2
( ( for z being Complex
for v, w being VECTOR of IT holds z * (v + w) = (z * v) + (z * w) ) & ( for z1, z2 being Complex
for v being VECTOR of IT holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex
for v being VECTOR of IT holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of IT holds 1r * v = v ) );

end;

registration

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

proof end;

end;

definition

let V be ComplexLinearSpace;
let V1 be Subset of V;
attr V1 is lineary-closed means :Def3: :: CLVECT_1:def 3
( ( for v, u being VECTOR of V st v in V1 & u in V1 holds
v + u in V1 ) & ( for z being Complex
for v being VECTOR of V st v in V1 holds
z * v in V1 ) );

end;

definition

let V be ComplexLinearSpace;
mode Subspace of V -> ComplexLinearSpace means :Def4: :: CLVECT_1:def 4
( the carrier of it c= the carrier of V & the Zero of it = the Zero of V & the add of it = the add of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX ,the carrier of it:] );
existence

proof end;

end;

registration

let V be ComplexLinearSpace;
cluster strict Subspace of V;
existence

proof end;

end;

definition

let V be ComplexLinearSpace;
func (0). V -> strict Subspace of V means :Def5: :: CLVECT_1:def 5
the carrier of it = {(0. V)};
correctness

proof end;

end;

definition

let V be ComplexLinearSpace;
func (Omega). V -> strict Subspace of V equals :: CLVECT_1:def 6
CLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #);
coherence

proof end;

end;

definition

let V be ComplexLinearSpace;
let v be VECTOR of V;
let W be Subspace of V;
func v + W -> Subset of V equals :: CLVECT_1:def 7
{ (v + u) where u is VECTOR of V : u in W } ;
coherence

proof end;

end;

definition

let V be ComplexLinearSpace;
let W be Subspace of V;
mode Coset of W -> Subset of V means :Def8: :: CLVECT_1:def 8
ex v being VECTOR of V st it = v + W;
existence

proof end;

end;

definition

attr c₁ is strict;
struct CNORMSTR -> CLSStruct ;
aggr CNORMSTR(# carrier, Zero, add, Mult, norm #) -> CNORMSTR ;
sel norm c₁ -> Function of the carrier of c₁, REAL ;

end;

registration

cluster non empty CNORMSTR ;
existence

proof end;

end;

definition

let X be non empty CNORMSTR ;
let x be Point of X;
func ||.x.|| -> Real equals :: CLVECT_1:def 9
the norm of X . x;
coherence ;

end;

Lm12: now

let x, y be Point of X; :: thesis:
let z be Complex; :: thesis:
reconsider u = x, w = y as VECTOR of ((0). V) ;
thus ( ||.x.|| = 0 iff x = H₁(X) ) :: thesis:

proof

H₁(X) = the Zero of X
.= 0. ((0). V)
.= 0. V by Th31 ;
hence ( ||.x.|| = 0 iff x = H₁(X) ) by Lm8, Lm9, TARSKI:def 1; :: thesis:

end;

z * x = the Mult of X . [z,u]
.= z * u ;
hence ||.(z * x).|| = |.z.| * ||.x.|| by Lm10; :: thesis:
x + y = the add of X . [x,y]
.= u + w ;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm11; :: thesis:

end;

definition

let IT be non empty CNORMSTR ;
attr IT is ComplexNormSpace-like means :Def10: :: CLVECT_1:def 10
for x, y being Point of IT
for z being Complex holds
( ( ||.x.|| = 0 implies x = 0. IT ) & ( x = 0. IT implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| );

end;

definition

let CNS be ComplexLinearSpace;
let S1, S2 be sequence of CNS;
func S1 + S2 -> sequence of CNS means :Def11: :: CLVECT_1:def 11
for n being Nat holds it . n = (S1 . n) + (S2 . n);
existence

proof end;

uniqueness

proof end;

end;

definition

let CNS be ComplexLinearSpace;
let S1, S2 be sequence of CNS;
func S1 - S2 -> sequence of CNS means :Def12: :: CLVECT_1:def 12
for n being Nat holds it . n = (S1 . n) - (S2 . n);
existence

proof end;

uniqueness

proof end;

end;

definition

let CNS be ComplexLinearSpace;
let S be sequence of CNS;
let x be Element of CNS;
func S - x -> sequence of CNS means :Def13: :: CLVECT_1:def 13
for n being Nat holds it . n = (S . n) - x;
existence

proof end;

uniqueness

proof end;

end;

definition

let CNS be ComplexLinearSpace;
let S be sequence of CNS;
let z be Complex;
func z * S -> sequence of CNS means :Def14: :: CLVECT_1:def 14
for n being Nat holds it . n = z * (S . n);
existence

proof end;

uniqueness

proof end;

end;

definition

let CNS be ComplexNormSpace;
let S be sequence of CNS;
attr S is convergent means :Def15: :: CLVECT_1:def 15
ex g being Point of CNS st
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r;

end;

definition

let CNS be ComplexNormSpace;
let S be sequence of CNS;
func ||.S.|| -> Real_Sequence means :Def16: :: CLVECT_1:def 16
for n being Nat holds it . n = ||.(S . n).||;
existence

proof end;

uniqueness

proof end;

end;

definition

let CNS be ComplexNormSpace;
let S be sequence of CNS;
assume A1: S is convergent ;
func lim S -> Point of CNS means :Def17: :: CLVECT_1:def 17
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - it).|| < r;
existence by A1, Def15;
uniqueness

proof end;

end;