:: by Noboru Endou

::

:: Received January 26, 2004

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

definition

attr c_{1} is strict ;

struct CLSStruct -> addLoopStr ;

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

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

end;
struct CLSStruct -> addLoopStr ;

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

sel Mult c

definition

let V be non empty CLSStruct ;

let v be VECTOR of V;

let z be Complex;

coherence

the Mult of V . [z,v] is Element of V

end;
let v be VECTOR of V;

let z be Complex;

coherence

the Mult of V . [z,v] is Element of V

proof end;

:: deftheorem defines * CLVECT_1:def 1 :

for V being non empty CLSStruct

for v being VECTOR of V

for z being Complex holds z * v = the Mult of V . [z,v];

for V being non empty CLSStruct

for v being VECTOR of V

for z being Complex holds z * v = the Mult of V . [z,v];

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;

coherence

not CLSStruct(# ZS,O,F,G #) is empty ;

end;
let O be Element of ZS;

let F be BinOp of ZS;

let G be Function of [:COMPLEX,ZS:],ZS;

coherence

not CLSStruct(# ZS,O,F,G #) is empty ;

definition

let IT be non empty CLSStruct ;

end;
attr IT is vector-distributive means :Def2: :: CLVECT_1:def 2

for a being Complex

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w);

for a being Complex

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w);

attr IT is scalar-distributive means :Def3: :: CLVECT_1:def 3

for a, b being Complex

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v);

for a, b being Complex

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v);

attr IT is scalar-associative means :Def4: :: CLVECT_1:def 4

for a, b being Complex

for v being VECTOR of IT holds (a * b) * v = a * (b * v);

for a, b being Complex

for v being VECTOR of IT holds (a * b) * v = a * (b * v);

:: deftheorem Def2 defines vector-distributive CLVECT_1:def 2 :

for IT being non empty CLSStruct holds

( IT is vector-distributive iff for a being Complex

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );

for IT being non empty CLSStruct holds

( IT is vector-distributive iff for a being Complex

for v, w being VECTOR of IT holds a * (v + w) = (a * v) + (a * w) );

:: deftheorem Def3 defines scalar-distributive CLVECT_1:def 3 :

for IT being non empty CLSStruct holds

( IT is scalar-distributive iff for a, b being Complex

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );

for IT being non empty CLSStruct holds

( IT is scalar-distributive iff for a, b being Complex

for v being VECTOR of IT holds (a + b) * v = (a * v) + (b * v) );

:: deftheorem Def4 defines scalar-associative CLVECT_1:def 4 :

for IT being non empty CLSStruct holds

( IT is scalar-associative iff for a, b being Complex

for v being VECTOR of IT holds (a * b) * v = a * (b * v) );

for IT being non empty CLSStruct holds

( IT is scalar-associative iff for a, b being Complex

for v being VECTOR of IT holds (a * b) * v = a * (b * v) );

:: deftheorem Def5 defines scalar-unital CLVECT_1:def 5 :

for IT being non empty CLSStruct holds

( IT is scalar-unital iff for v being VECTOR of IT holds 1r * v = v );

for IT being non empty CLSStruct holds

( IT is scalar-unital iff for v being VECTOR of IT holds 1r * v = v );

definition

CLSStruct(# {0},op0,op2,(pr2 (COMPLEX,{0})) #) is strict CLSStruct ;

end;

func Trivial-CLSStruct -> strict CLSStruct equals :: CLVECT_1:def 6

CLSStruct(# {0},op0,op2,(pr2 (COMPLEX,{0})) #);

coherence CLSStruct(# {0},op0,op2,(pr2 (COMPLEX,{0})) #);

CLSStruct(# {0},op0,op2,(pr2 (COMPLEX,{0})) #) is strict CLSStruct ;

:: deftheorem defines Trivial-CLSStruct CLVECT_1:def 6 :

Trivial-CLSStruct = CLSStruct(# {0},op0,op2,(pr2 (COMPLEX,{0})) #);

Trivial-CLSStruct = CLSStruct(# {0},op0,op2,(pr2 (COMPLEX,{0})) #);

registration
end;

registration

ex b_{1} being non empty CLSStruct st

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

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

existence ex b

( b

proof end;

definition

mode ComplexLinearSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct ;

end;
theorem Th1: :: CLVECT_1:1

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex st ( z = 0 or v = 0. V ) holds

z * v = 0. V

for v being VECTOR of V

for z being Complex st ( z = 0 or v = 0. V ) holds

z * v = 0. V

proof end;

theorem Th2: :: CLVECT_1:2

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex holds

( not z * v = 0. V or z = 0 or v = 0. V )

for v being VECTOR of V

for z being Complex holds

( not z * v = 0. V or z = 0 or v = 0. V )

proof end;

theorem Th6: :: CLVECT_1:6

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex holds z * (- v) = (- z) * v

for v being VECTOR of V

for z being Complex holds z * (- v) = (- z) * v

proof end;

theorem Th7: :: CLVECT_1:7

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex holds z * (- v) = - (z * v)

for v being VECTOR of V

for z being Complex holds z * (- v) = - (z * v)

proof end;

theorem :: CLVECT_1:8

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex holds (- z) * (- v) = z * v

for v being VECTOR of V

for z being Complex holds (- z) * (- v) = z * v

proof end;

theorem Th9: :: CLVECT_1:9

for V being ComplexLinearSpace

for u, v being VECTOR of V

for z being Complex holds z * (v - u) = (z * v) - (z * u)

for u, v being VECTOR of V

for z being Complex holds z * (v - u) = (z * v) - (z * u)

proof end;

theorem Th10: :: CLVECT_1:10

for V being ComplexLinearSpace

for v being VECTOR of V

for z1, z2 being Complex holds (z1 - z2) * v = (z1 * v) - (z2 * v)

for v being VECTOR of V

for z1, z2 being Complex holds (z1 - z2) * v = (z1 * v) - (z2 * v)

proof end;

theorem :: CLVECT_1:11

for V being ComplexLinearSpace

for u, v being VECTOR of V

for z being Complex st z <> 0 & z * v = z * u holds

v = u

for u, v being VECTOR of V

for z being Complex st z <> 0 & z * v = z * u holds

v = u

proof end;

theorem :: CLVECT_1:12

for V being ComplexLinearSpace

for v being VECTOR of V

for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds

z1 = z2

for v being VECTOR of V

for z1, z2 being Complex st v <> 0. V & z1 * v = z2 * v holds

z1 = z2

proof end;

Lm1: for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V

proof end;

Lm2: for V being non empty addLoopStr

for F being FinSequence of the carrier of V st len F = 0 holds

Sum F = 0. V

proof end;

theorem :: CLVECT_1:13

for V being ComplexLinearSpace

for z being Complex

for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat

for v being VECTOR of V st k in dom F & v = G . k holds

F . k = z * v ) holds

Sum F = z * (Sum G)

for z being Complex

for F, G being FinSequence of the carrier of V st len F = len G & ( for k being Nat

for v being VECTOR of V st k in dom F & v = G . k holds

F . k = z * v ) holds

Sum F = z * (Sum G)

proof end;

theorem :: CLVECT_1:14

theorem :: CLVECT_1:15

for V being ComplexLinearSpace

for u, v being VECTOR of V

for z being Complex holds z * (Sum <*v,u*>) = (z * v) + (z * u)

for u, v being VECTOR of V

for z being Complex holds z * (Sum <*v,u*>) = (z * v) + (z * u)

proof end;

theorem :: CLVECT_1:16

for V being ComplexLinearSpace

for u, v1, v2 being VECTOR of V

for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)

for u, v1, v2 being VECTOR of V

for z being Complex holds z * (Sum <*u,v1,v2*>) = ((z * u) + (z * v1)) + (z * v2)

proof end;

theorem :: CLVECT_1:18

for V being ComplexLinearSpace

for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- (1r + 1r)) * v

for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- (1r + 1r)) * v

proof end;

:: deftheorem defines linearly-closed CLVECT_1:def 7 :

for V being ComplexLinearSpace

for V1 being Subset of V holds

( V1 is linearly-closed iff ( ( 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 ) ) );

for V being ComplexLinearSpace

for V1 being Subset of V holds

( V1 is linearly-closed iff ( ( 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 ) ) );

theorem Th20: :: CLVECT_1:20

for V being ComplexLinearSpace

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

0. V in V1

proof end;

theorem Th21: :: CLVECT_1:21

for V being ComplexLinearSpace

for V1 being Subset of V st V1 is linearly-closed holds

for v being VECTOR of V st v in V1 holds

- v in V1

for V1 being Subset of V st V1 is linearly-closed holds

for v being VECTOR of V st v in V1 holds

- v in V1

proof end;

theorem :: CLVECT_1:22

for V being ComplexLinearSpace

for V1 being Subset of V st V1 is linearly-closed holds

for v, u being VECTOR of V st v in V1 & u in V1 holds

v - u in V1

for V1 being Subset of V st V1 is linearly-closed holds

for v, u being VECTOR of V st v in V1 & u in V1 holds

v - u in V1

proof end;

theorem :: CLVECT_1:24

for V being ComplexLinearSpace

for V1 being Subset of V st the carrier of V = V1 holds

V1 is linearly-closed ;

for V1 being Subset of V st the carrier of V = V1 holds

V1 is linearly-closed ;

theorem :: CLVECT_1:25

for V being ComplexLinearSpace

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is VECTOR of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

for V1, V2, V3 being Subset of V st V1 is linearly-closed & V2 is linearly-closed & V3 = { (v + u) where u, v is VECTOR of V : ( v in V1 & u in V2 ) } holds

V3 is linearly-closed

proof end;

theorem :: CLVECT_1:26

for V being ComplexLinearSpace

for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds

V1 /\ V2 is linearly-closed

for V1, V2 being Subset of V st V1 is linearly-closed & V2 is linearly-closed holds

V1 /\ V2 is linearly-closed

proof end;

definition

let V be ComplexLinearSpace;

ex b_{1} being ComplexLinearSpace st

( the carrier of b_{1} c= the carrier of V & 0. b_{1} = 0. V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the Mult of b_{1} = the Mult of V | [:COMPLEX, the carrier of b_{1}:] )

end;
mode Subspace of V -> ComplexLinearSpace means :Def8: :: CLVECT_1:def 8

( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX, the carrier of it:] );

existence ( the carrier of it c= the carrier of V & 0. it = 0. V & the addF of it = the addF of V || the carrier of it & the Mult of it = the Mult of V | [:COMPLEX, the carrier of it:] );

ex b

( the carrier of b

proof end;

:: deftheorem Def8 defines Subspace CLVECT_1:def 8 :

for V, b_{2} being ComplexLinearSpace holds

( b_{2} is Subspace of V iff ( the carrier of b_{2} c= the carrier of V & 0. b_{2} = 0. V & the addF of b_{2} = the addF of V || the carrier of b_{2} & the Mult of b_{2} = the Mult of V | [:COMPLEX, the carrier of b_{2}:] ) );

for V, b

( b

theorem :: CLVECT_1:27

for V being ComplexLinearSpace

for W1, W2 being Subspace of V

for x being set st x in W1 & W1 is Subspace of W2 holds

x in W2

for W1, W2 being Subspace of V

for x being set st x in W1 & W1 is Subspace of W2 holds

x in W2

proof end;

theorem Th29: :: CLVECT_1:29

for V being ComplexLinearSpace

for W being Subspace of V

for w being VECTOR of W holds w is VECTOR of V

for W being Subspace of V

for w being VECTOR of W holds w is VECTOR of V

proof end;

theorem :: CLVECT_1:30

theorem Th32: :: CLVECT_1:32

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V

for w1, w2 being VECTOR of W st w1 = v & w2 = u holds

w1 + w2 = v + u

for u, v being VECTOR of V

for W being Subspace of V

for w1, w2 being VECTOR of W st w1 = v & w2 = u holds

w1 + w2 = v + u

proof end;

theorem Th33: :: CLVECT_1:33

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex

for W being Subspace of V

for w being VECTOR of W st w = v holds

z * w = z * v

for v being VECTOR of V

for z being Complex

for W being Subspace of V

for w being VECTOR of W st w = v holds

z * w = z * v

proof end;

theorem Th34: :: CLVECT_1:34

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V

for w being VECTOR of W st w = v holds

- v = - w

for v being VECTOR of V

for W being Subspace of V

for w being VECTOR of W st w = v holds

- v = - w

proof end;

theorem Th35: :: CLVECT_1:35

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V

for w1, w2 being VECTOR of W st w1 = v & w2 = u holds

w1 - w2 = v - u

for u, v being VECTOR of V

for W being Subspace of V

for w1, w2 being VECTOR of W st w1 = v & w2 = u holds

w1 - w2 = v - u

proof end;

Lm3: for V being ComplexLinearSpace

for V1 being Subset of V

for W being Subspace of V st the carrier of W = V1 holds

V1 is linearly-closed

proof end;

theorem :: CLVECT_1:38

theorem Th39: :: CLVECT_1:39

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V st u in W & v in W holds

u + v in W

for u, v being VECTOR of V

for W being Subspace of V st u in W & v in W holds

u + v in W

proof end;

theorem Th40: :: CLVECT_1:40

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex

for W being Subspace of V st v in W holds

z * v in W

for v being VECTOR of V

for z being Complex

for W being Subspace of V st v in W holds

z * v in W

proof end;

theorem Th41: :: CLVECT_1:41

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V st v in W holds

- v in W

for v being VECTOR of V

for W being Subspace of V st v in W holds

- v in W

proof end;

theorem Th42: :: CLVECT_1:42

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V st u in W & v in W holds

u - v in W

for u, v being VECTOR of V

for W being Subspace of V st u in W & v in W holds

u - v in W

proof end;

Lm4: now :: thesis: for V being ComplexLinearSpace

for V1 being Subset of V

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

for V1 being Subset of V

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let V be ComplexLinearSpace; :: thesis: for V1 being Subset of V

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let V1 be Subset of V; :: thesis: for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let D be non empty set ; :: thesis: for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let d1 be Element of D; :: thesis: for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let A be BinOp of D; :: thesis: for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let M be Function of [:COMPLEX,D:],D; :: thesis: for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let z be Complex; :: thesis: for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let w be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis: for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let v be Element of V; :: thesis: ( V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v implies z * w = z * v )

assume that

A1: V1 = D and

A2: M = the Mult of V | [:COMPLEX,V1:] and

A3: w = v ; :: thesis: z * w = z * v

z in COMPLEX by XCMPLX_0:def 2;

then [z,w] in [:COMPLEX,V1:] by A1, ZFMISC_1:def 2;

hence z * w = z * v by A3, A2, FUNCT_1:49; :: thesis: verum

end;
for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let V1 be Subset of V; :: thesis: for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let D be non empty set ; :: thesis: for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let d1 be Element of D; :: thesis: for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let A be BinOp of D; :: thesis: for M being Function of [:COMPLEX,D:],D

for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let M be Function of [:COMPLEX,D:],D; :: thesis: for z being Complex

for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let z be Complex; :: thesis: for w being VECTOR of CLSStruct(# D,d1,A,M #)

for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let w be VECTOR of CLSStruct(# D,d1,A,M #); :: thesis: for v being Element of V st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v

let v be Element of V; :: thesis: ( V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v implies z * w = z * v )

assume that

A1: V1 = D and

A2: M = the Mult of V | [:COMPLEX,V1:] and

A3: w = v ; :: thesis: z * w = z * v

z in COMPLEX by XCMPLX_0:def 2;

then [z,w] in [:COMPLEX,V1:] by A1, ZFMISC_1:def 2;

hence z * w = z * v by A3, A2, FUNCT_1:49; :: thesis: verum

theorem Th43: :: CLVECT_1:43

for V being ComplexLinearSpace

for V1 being Subset of V

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds

CLSStruct(# D,d1,A,M #) is Subspace of V

for V1 being Subset of V

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds

CLSStruct(# D,d1,A,M #) is Subspace of V

proof end;

theorem Th46: :: CLVECT_1:46

for V, X, Y being ComplexLinearSpace st V is Subspace of X & X is Subspace of Y holds

V is Subspace of Y

V is Subspace of Y

proof end;

theorem Th47: :: CLVECT_1:47

for V being ComplexLinearSpace

for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds

W1 is Subspace of W2

for W1, W2 being Subspace of V st the carrier of W1 c= the carrier of W2 holds

W1 is Subspace of W2

proof end;

theorem :: CLVECT_1:48

for V being ComplexLinearSpace

for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds

v in W2 ) holds

W1 is Subspace of W2

for W1, W2 being Subspace of V st ( for v being VECTOR of V st v in W1 holds

v in W2 ) holds

W1 is Subspace of W2

proof end;

registration

let V be ComplexLinearSpace;

ex b_{1} being Subspace of V st b_{1} is strict

end;
cluster non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital for Subspace of V;

existence ex b

proof end;

theorem Th49: :: CLVECT_1:49

for V being ComplexLinearSpace

for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds

W1 = W2

for W1, W2 being strict Subspace of V st the carrier of W1 = the carrier of W2 holds

W1 = W2

proof end;

theorem Th50: :: CLVECT_1:50

for V being ComplexLinearSpace

for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds

( v in W1 iff v in W2 ) ) holds

W1 = W2

for W1, W2 being strict Subspace of V st ( for v being VECTOR of V holds

( v in W1 iff v in W2 ) ) holds

W1 = W2

proof end;

theorem :: CLVECT_1:51

for V being strict ComplexLinearSpace

for W being strict Subspace of V st the carrier of W = the carrier of V holds

W = V

for W being strict Subspace of V st the carrier of W = the carrier of V holds

W = V

proof end;

theorem :: CLVECT_1:52

for V being strict ComplexLinearSpace

for W being strict Subspace of V st ( for v being VECTOR of V holds

( v in W iff v in V ) ) holds

W = V

for W being strict Subspace of V st ( for v being VECTOR of V holds

( v in W iff v in V ) ) holds

W = V

proof end;

theorem :: CLVECT_1:53

for V being ComplexLinearSpace

for V1 being Subset of V

for W being Subspace of V st the carrier of W = V1 holds

V1 is linearly-closed by Lm3;

for V1 being Subset of V

for W being Subspace of V st the carrier of W = V1 holds

V1 is linearly-closed by Lm3;

theorem Th54: :: CLVECT_1:54

for V being ComplexLinearSpace

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Subspace of V st V1 = the carrier of W

for V1 being Subset of V st V1 <> {} & V1 is linearly-closed holds

ex W being strict Subspace of V st V1 = the carrier of W

proof end;

:: Definition of zero subspace and improper subspace of complex linear space.

definition

let V be ComplexLinearSpace;

correctness

existence

ex b_{1} being strict Subspace of V st the carrier of b_{1} = {(0. V)};

uniqueness

for b_{1}, b_{2} being strict Subspace of V st the carrier of b_{1} = {(0. V)} & the carrier of b_{2} = {(0. V)} holds

b_{1} = b_{2};

by Th23, Th49, Th54;

end;
correctness

existence

ex b

uniqueness

for b

b

by Th23, Th49, Th54;

:: deftheorem Def9 defines (0). CLVECT_1:def 9 :

for V being ComplexLinearSpace

for b_{2} being strict Subspace of V holds

( b_{2} = (0). V iff the carrier of b_{2} = {(0. V)} );

for V being ComplexLinearSpace

for b

( b

definition

let V be ComplexLinearSpace;

CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V

end;
func (Omega). V -> strict Subspace of V equals :: CLVECT_1:def 10

CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

coherence CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is strict Subspace of V

proof end;

:: deftheorem defines (Omega). CLVECT_1:def 10 :

for V being ComplexLinearSpace holds (Omega). V = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

for V being ComplexLinearSpace holds (Omega). V = CLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #);

:: Definitional theorems of zero subspace and improper subspace.

theorem :: CLVECT_1:57

:: Introduction of the cosets of subspace.

definition

let V be ComplexLinearSpace;

let v be VECTOR of V;

let W be Subspace of V;

coherence

{ (v + u) where u is VECTOR of V : u in W } is Subset of V

end;
let v be VECTOR of V;

let W be Subspace of V;

coherence

{ (v + u) where u is VECTOR of V : u in W } is Subset of V

proof end;

:: deftheorem defines + CLVECT_1:def 11 :

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V holds v + W = { (v + u) where u is VECTOR of V : u in W } ;

Lm5: for V being ComplexLinearSpace

for W being Subspace of V holds (0. V) + W = the carrier of W

proof end;

definition

let V be ComplexLinearSpace;

let W be Subspace of V;

ex b_{1} being Subset of V ex v being VECTOR of V st b_{1} = v + W

end;
let W be Subspace of V;

mode Coset of W -> Subset of V means :Def12: :: CLVECT_1:def 12

ex v being VECTOR of V st it = v + W;

existence ex v being VECTOR of V st it = v + W;

ex b

proof end;

:: deftheorem Def12 defines Coset CLVECT_1:def 12 :

for V being ComplexLinearSpace

for W being Subspace of V

for b_{3} being Subset of V holds

( b_{3} is Coset of W iff ex v being VECTOR of V st b_{3} = v + W );

for V being ComplexLinearSpace

for W being Subspace of V

for b

( b

:: Definitional theorems of the cosets.

theorem Th61: :: CLVECT_1:61

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V holds

( 0. V in v + W iff v in W )

for v being VECTOR of V

for W being Subspace of V holds

( 0. V in v + W iff v in W )

proof end;

theorem :: CLVECT_1:63

Lm6: for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V holds

( v in W iff v + W = the carrier of W )

proof end;

theorem Th65: :: CLVECT_1:65

for V being ComplexLinearSpace

for v being VECTOR of V holds v + ((Omega). V) = the carrier of V by STRUCT_0:def 5, Lm6;

for v being VECTOR of V holds v + ((Omega). V) = the carrier of V by STRUCT_0:def 5, Lm6;

theorem :: CLVECT_1:67

theorem Th68: :: CLVECT_1:68

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex

for W being Subspace of V st v in W holds

(z * v) + W = the carrier of W

for v being VECTOR of V

for z being Complex

for W being Subspace of V st v in W holds

(z * v) + W = the carrier of W

proof end;

theorem Th69: :: CLVECT_1:69

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex

for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds

v in W

for v being VECTOR of V

for z being Complex

for W being Subspace of V st z <> 0 & (z * v) + W = the carrier of W holds

v in W

proof end;

theorem Th70: :: CLVECT_1:70

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V holds

( v in W iff (- v) + W = the carrier of W )

for v being VECTOR of V

for W being Subspace of V holds

( v in W iff (- v) + W = the carrier of W )

proof end;

theorem Th71: :: CLVECT_1:71

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( u in W iff v + W = (v + u) + W )

for u, v being VECTOR of V

for W being Subspace of V holds

( u in W iff v + W = (v + u) + W )

proof end;

theorem :: CLVECT_1:72

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( u in W iff v + W = (v - u) + W )

for u, v being VECTOR of V

for W being Subspace of V holds

( u in W iff v + W = (v - u) + W )

proof end;

theorem Th73: :: CLVECT_1:73

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( v in u + W iff u + W = v + W )

for u, v being VECTOR of V

for W being Subspace of V holds

( v in u + W iff u + W = v + W )

proof end;

theorem Th74: :: CLVECT_1:74

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V holds

( v + W = (- v) + W iff v in W )

for v being VECTOR of V

for W being Subspace of V holds

( v + W = (- v) + W iff v in W )

proof end;

theorem Th75: :: CLVECT_1:75

for V being ComplexLinearSpace

for u, v1, v2 being VECTOR of V

for W being Subspace of V st u in v1 + W & u in v2 + W holds

v1 + W = v2 + W

for u, v1, v2 being VECTOR of V

for W being Subspace of V st u in v1 + W & u in v2 + W holds

v1 + W = v2 + W

proof end;

theorem :: CLVECT_1:76

theorem Th77: :: CLVECT_1:77

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex

for W being Subspace of V st z <> 1r & z * v in v + W holds

v in W

for v being VECTOR of V

for z being Complex

for W being Subspace of V st z <> 1r & z * v in v + W holds

v in W

proof end;

theorem Th78: :: CLVECT_1:78

for V being ComplexLinearSpace

for v being VECTOR of V

for z being Complex

for W being Subspace of V st v in W holds

z * v in v + W

for v being VECTOR of V

for z being Complex

for W being Subspace of V st v in W holds

z * v in v + W

proof end;

theorem :: CLVECT_1:79

for V being ComplexLinearSpace

for v being VECTOR of V

for W being Subspace of V holds

( - v in v + W iff v in W )

for v being VECTOR of V

for W being Subspace of V holds

( - v in v + W iff v in W )

proof end;

theorem Th80: :: CLVECT_1:80

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( u + v in v + W iff u in W )

for u, v being VECTOR of V

for W being Subspace of V holds

( u + v in v + W iff u in W )

proof end;

theorem :: CLVECT_1:81

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( v - u in v + W iff u in W )

for u, v being VECTOR of V

for W being Subspace of V holds

( v - u in v + W iff u in W )

proof end;

theorem Th82: :: CLVECT_1:82

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( u in v + W iff ex v1 being VECTOR of V st

( v1 in W & u = v + v1 ) )

for u, v being VECTOR of V

for W being Subspace of V holds

( u in v + W iff ex v1 being VECTOR of V st

( v1 in W & u = v + v1 ) )

proof end;

theorem :: CLVECT_1:83

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V holds

( u in v + W iff ex v1 being VECTOR of V st

( v1 in W & u = v - v1 ) )

for u, v being VECTOR of V

for W being Subspace of V holds

( u in v + W iff ex v1 being VECTOR of V st

( v1 in W & u = v - v1 ) )

proof end;

theorem Th84: :: CLVECT_1:84

for V being ComplexLinearSpace

for v1, v2 being VECTOR of V

for W being Subspace of V holds

( ex v being VECTOR of V st

( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )

for v1, v2 being VECTOR of V

for W being Subspace of V holds

( ex v being VECTOR of V st

( v1 in v + W & v2 in v + W ) iff v1 - v2 in W )

proof end;

theorem Th85: :: CLVECT_1:85

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V st v + W = u + W holds

ex v1 being VECTOR of V st

( v1 in W & v + v1 = u )

for u, v being VECTOR of V

for W being Subspace of V st v + W = u + W holds

ex v1 being VECTOR of V st

( v1 in W & v + v1 = u )

proof end;

theorem Th86: :: CLVECT_1:86

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V st v + W = u + W holds

ex v1 being VECTOR of V st

( v1 in W & v - v1 = u )

for u, v being VECTOR of V

for W being Subspace of V st v + W = u + W holds

ex v1 being VECTOR of V st

( v1 in W & v - v1 = u )

proof end;

theorem Th87: :: CLVECT_1:87

for V being ComplexLinearSpace

for v being VECTOR of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

for v being VECTOR of V

for W1, W2 being strict Subspace of V holds

( v + W1 = v + W2 iff W1 = W2 )

proof end;

theorem Th88: :: CLVECT_1:88

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds

W1 = W2

for u, v being VECTOR of V

for W1, W2 being strict Subspace of V st v + W1 = u + W2 holds

W1 = W2

proof end;

:: Theorems concerning cosets of subspace

:: regarded as subsets of the carrier.

:: regarded as subsets of the carrier.

theorem :: CLVECT_1:89

for V being ComplexLinearSpace

for W being Subspace of V

for C being Coset of W holds

( C is linearly-closed iff C = the carrier of W )

for W being Subspace of V

for C being Coset of W holds

( C is linearly-closed iff C = the carrier of W )

proof end;

theorem :: CLVECT_1:90

for V being ComplexLinearSpace

for W1, W2 being strict Subspace of V

for C1 being Coset of W1

for C2 being Coset of W2 st C1 = C2 holds

W1 = W2

for W1, W2 being strict Subspace of V

for C1 being Coset of W1

for C2 being Coset of W2 st C1 = C2 holds

W1 = W2

proof end;

theorem :: CLVECT_1:92

for V being ComplexLinearSpace

for V1 being Subset of V st V1 is Coset of (0). V holds

ex v being VECTOR of V st V1 = {v}

for V1 being Subset of V st V1 is Coset of (0). V holds

ex v being VECTOR of V st V1 = {v}

proof end;

theorem :: CLVECT_1:95

for V being ComplexLinearSpace

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

for V1 being Subset of V st V1 is Coset of (Omega). V holds

V1 = the carrier of V

proof end;

theorem :: CLVECT_1:96

for V being ComplexLinearSpace

for W being Subspace of V

for C being Coset of W holds

( 0. V in C iff C = the carrier of W )

for W being Subspace of V

for C being Coset of W holds

( 0. V in C iff C = the carrier of W )

proof end;

theorem Th97: :: CLVECT_1:97

for V being ComplexLinearSpace

for u being VECTOR of V

for W being Subspace of V

for C being Coset of W holds

( u in C iff C = u + W )

for u being VECTOR of V

for W being Subspace of V

for C being Coset of W holds

( u in C iff C = u + W )

proof end;

theorem :: CLVECT_1:98

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V

for C being Coset of W st u in C & v in C holds

ex v1 being VECTOR of V st

( v1 in W & u + v1 = v )

for u, v being VECTOR of V

for W being Subspace of V

for C being Coset of W st u in C & v in C holds

ex v1 being VECTOR of V st

( v1 in W & u + v1 = v )

proof end;

theorem :: CLVECT_1:99

for V being ComplexLinearSpace

for u, v being VECTOR of V

for W being Subspace of V

for C being Coset of W st u in C & v in C holds

ex v1 being VECTOR of V st

( v1 in W & u - v1 = v )

for u, v being VECTOR of V

for W being Subspace of V

for C being Coset of W st u in C & v in C holds

ex v1 being VECTOR of V st

( v1 in W & u - v1 = v )

proof end;

theorem :: CLVECT_1:100

for V being ComplexLinearSpace

for v1, v2 being VECTOR of V

for W being Subspace of V holds

( ex C being Coset of W st

( v1 in C & v2 in C ) iff v1 - v2 in W )

for v1, v2 being VECTOR of V

for W being Subspace of V holds

( ex C being Coset of W st

( v1 in C & v2 in C ) iff v1 - v2 in W )

proof end;

theorem :: CLVECT_1:101

for V being ComplexLinearSpace

for u being VECTOR of V

for W being Subspace of V

for B, C being Coset of W st u in B & u in C holds

B = C

for u being VECTOR of V

for W being Subspace of V

for B, C being Coset of W st u in B & u in C holds

B = C

proof end;

definition

attr c_{1} is strict ;

struct CNORMSTR -> CLSStruct , N-ZeroStr ;

aggr CNORMSTR(# carrier, ZeroF, addF, Mult, normF #) -> CNORMSTR ;

end;
struct CNORMSTR -> CLSStruct , N-ZeroStr ;

aggr CNORMSTR(# carrier, ZeroF, addF, Mult, normF #) -> CNORMSTR ;

deffunc H

set V = the ComplexLinearSpace;

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

by Def9;

reconsider niltonil = the carrier of ((0). the ComplexLinearSpace) --> (In (0,REAL)) as Function of the carrier of ((0). the ComplexLinearSpace),REAL ;

0. the ComplexLinearSpace is VECTOR of ((0). the ComplexLinearSpace)

by Lm7, TARSKI:def 1;

then Lm8: niltonil . (0. the ComplexLinearSpace) = 0

by FUNCOP_1:7;

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

for z being Complex holds niltonil . (z * u) = |.z.| * (niltonil . u)

proof end;

Lm10: for u, v being VECTOR of ((0). the ComplexLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)

proof end;

reconsider X = CNORMSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),niltonil #) as non empty CNORMSTR ;

Lm11: now :: thesis: for x, y being Point of X

for z being Complex holds

( ( ||.x.|| = 0 implies x = H_{1}(X) ) & ( x = H_{1}(X) implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

for z being Complex holds

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

let x, y be Point of X; :: thesis: for z being Complex holds

( ( ||.x.|| = 0 implies x = H_{1}(X) ) & ( x = H_{1}(X) implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

let z be Complex; :: thesis: ( ( ||.x.|| = 0 implies x = H_{1}(X) ) & ( x = H_{1}(X) implies ||.x.|| = 0 ) & ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

reconsider u = x, w = y as VECTOR of ((0). the ComplexLinearSpace) ;

H_{1}(X) = 0. the ComplexLinearSpace
by Def8;

hence ( ||.x.|| = 0 iff x = H_{1}(X) )
by Lm7, FUNCOP_1:7, TARSKI:def 1; :: thesis: ( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

z * x = z * u ;

hence ||.(z * x).|| = |.z.| * ||.x.|| by Lm9; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||

x + y = u + w ;

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm10; :: thesis: verum

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

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

reconsider u = x, w = y as VECTOR of ((0). the ComplexLinearSpace) ;

H

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

z * x = z * u ;

hence ||.(z * x).|| = |.z.| * ||.x.|| by Lm9; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||

x + y = u + w ;

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm10; :: thesis: verum

:: deftheorem Def13 defines ComplexNormSpace-like CLVECT_1:def 13 :

for IT being non empty CNORMSTR holds

( IT is ComplexNormSpace-like iff for x, y being Point of IT

for z being Complex holds

( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

for IT being non empty CNORMSTR holds

( IT is ComplexNormSpace-like iff for x, y being Point of IT

for z being Complex holds

( ||.(z * x).|| = |.z.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

registration

ex b_{1} being non empty CNORMSTR st

( b_{1} is reflexive & b_{1} is discerning & b_{1} is ComplexNormSpace-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 discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital strict ComplexNormSpace-like for CNORMSTR ;

existence ex b

( b

proof end;

definition

mode ComplexNormSpace is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR ;

end;
theorem :: CLVECT_1:106

for z1, z2 being Complex

for CNS being ComplexNormSpace

for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)

for CNS being ComplexNormSpace

for x, y being Point of CNS holds ||.((z1 * x) + (z2 * y)).|| <= (|.z1.| * ||.x.||) + (|.z2.| * ||.y.||)

proof end;

theorem Th110: :: CLVECT_1:110

for CNS being ComplexNormSpace

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

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

proof end;

theorem Th111: :: CLVECT_1:111

for CNS being ComplexNormSpace

for x, y, w being Point of CNS holds ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||

for x, y, w being Point of CNS holds ||.(x - w).|| <= ||.(x - y).|| + ||.(y - w).||

proof end;

theorem :: CLVECT_1:112

definition

let CNS be ComplexLinearSpace;

let S be sequence of CNS;

let z be Complex;

ex b_{1} being sequence of CNS st

for n being Nat holds b_{1} . n = z * (S . n)

for b_{1}, b_{2} being sequence of CNS st ( for n being Nat holds b_{1} . n = z * (S . n) ) & ( for n being Nat holds b_{2} . n = z * (S . n) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = z * (S . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines * CLVECT_1:def 14 :

for CNS being ComplexLinearSpace

for S being sequence of CNS

for z being Complex

for b_{4} being sequence of CNS holds

( b_{4} = z * S iff for n being Nat holds b_{4} . n = z * (S . n) );

for CNS being ComplexLinearSpace

for S being sequence of CNS

for z being Complex

for b

( b

:: deftheorem defines convergent CLVECT_1:def 15 :

for CNS being ComplexNormSpace

for S being sequence of CNS holds

( S is convergent iff 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 );

for CNS being ComplexNormSpace

for S being sequence of CNS holds

( S is convergent iff 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 );

theorem Th113: :: CLVECT_1:113

for CNS being ComplexNormSpace

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

S1 + S2 is convergent

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

S1 + S2 is convergent

proof end;

theorem Th114: :: CLVECT_1:114

for CNS being ComplexNormSpace

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

S1 - S2 is convergent

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

S1 - S2 is convergent

proof end;

theorem Th115: :: CLVECT_1:115

for CNS being ComplexNormSpace

for x being Point of CNS

for S being sequence of CNS st S is convergent holds

S - x is convergent

for x being Point of CNS

for S being sequence of CNS st S is convergent holds

S - x is convergent

proof end;

theorem Th116: :: CLVECT_1:116

for z being Complex

for CNS being ComplexNormSpace

for S being sequence of CNS st S is convergent holds

z * S is convergent

for CNS being ComplexNormSpace

for S being sequence of CNS st S is convergent holds

z * S is convergent

proof end;

theorem Th117: :: CLVECT_1:117

for CNS being ComplexNormSpace

for S being sequence of CNS st S is convergent holds

||.S.|| is convergent

for S being sequence of CNS st S is convergent holds

||.S.|| is convergent

proof end;

definition

let CNS be ComplexNormSpace;

let S be sequence of CNS;

assume A1: S is convergent ;

ex b_{1} 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) - b_{1}).|| < r
by A1;

uniqueness

for b_{1}, b_{2} 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) - b_{1}).|| < r ) & ( for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b_{2}).|| < r ) holds

b_{1} = b_{2}

end;
let S be sequence of CNS;

assume A1: S is convergent ;

func lim S -> Point of CNS means :Def16: :: CLVECT_1:def 16

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

ex b

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

uniqueness

for b

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

b

proof end;

:: deftheorem Def16 defines lim CLVECT_1:def 16 :

for CNS being ComplexNormSpace

for S being sequence of CNS st S is convergent holds

for b_{3} being Point of CNS holds

( b_{3} = lim S iff for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b_{3}).|| < r );

for CNS being ComplexNormSpace

for S being sequence of CNS st S is convergent holds

for b

( b

ex m being Nat st

for n being Nat st m <= n holds

||.((S . n) - b

theorem :: CLVECT_1:118

for CNS being ComplexNormSpace

for g being Point of CNS

for S being sequence of CNS st S is convergent & lim S = g holds

( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )

for g being Point of CNS

for S being sequence of CNS st S is convergent & lim S = g holds

( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )

proof end;

theorem :: CLVECT_1:119

for CNS being ComplexNormSpace

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

lim (S1 + S2) = (lim S1) + (lim S2)

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

lim (S1 + S2) = (lim S1) + (lim S2)

proof end;

theorem :: CLVECT_1:120

for CNS being ComplexNormSpace

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

lim (S1 - S2) = (lim S1) - (lim S2)

for S1, S2 being sequence of CNS st S1 is convergent & S2 is convergent holds

lim (S1 - S2) = (lim S1) - (lim S2)

proof end;

theorem :: CLVECT_1:121

for CNS being ComplexNormSpace

for x being Point of CNS

for S being sequence of CNS st S is convergent holds

lim (S - x) = (lim S) - x

for x being Point of CNS

for S being sequence of CNS st S is convergent holds

lim (S - x) = (lim S) - x

proof end;

theorem :: CLVECT_1:122

for z being Complex

for CNS being ComplexNormSpace

for S being sequence of CNS st S is convergent holds

lim (z * S) = z * (lim S)

for CNS being ComplexNormSpace

for S being sequence of CNS st S is convergent holds

lim (z * S) = z * (lim S)

proof end;

theorem :: CLVECT_1:123

for z being Complex

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for V being ComplexLinearSpace

for V1 being Subset of V

for v being VECTOR of V

for w being VECTOR of CLSStruct(# D,d1,A,M #) st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v by Lm4;

for D being non empty set

for d1 being Element of D

for A being BinOp of D

for M being Function of [:COMPLEX,D:],D

for V being ComplexLinearSpace

for V1 being Subset of V

for v being VECTOR of V

for w being VECTOR of CLSStruct(# D,d1,A,M #) st V1 = D & M = the Mult of V | [:COMPLEX,V1:] & w = v holds

z * w = z * v by Lm4;