:: CLVECT_1 semantic presentation

definition

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

end;

registration

cluster non empty CLSStruct ;
existence

proof end;

end;

definition

let c₁ be CLSStruct ;
mode VECTOR of a₁ is Element of a₁;

end;

definition

let c₁ be non empty CLSStruct ;
let c₂ be VECTOR of c₁;
let c₃ be Complex;
func c₃ * c₂ -> Element of a₁ equals :: CLVECT_1:def 1
the Mult of a₁ . [a₃,a₂];
coherence ;

end;

:: deftheorem Def1 defines * CLVECT_1:def 1 :

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be BinOp of c₁;
let c₄ be Function of [:COMPLEX ,c₁:],c₁;
cluster CLSStruct(# a₁,a₂,a₃,a₄ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

E1: now

take c₁ = {0};
reconsider c₂ = 0 as Element of c₁ by TARSKI:def 1;
take c₃ = c₂;
deffunc H₁( Element of c₁, Element of c₁) -> Element of c₁ = c₃;
consider c₄ being BinOp of c₁ such that
E2: for b₁, b₂ being Element of c₁ holds c₄ . b₁,b₂ = H₁(b₁,b₂) from BINOP_1:sch 2();
reconsider c₅ = [:COMPLEX ,c₁:] --> c₃ as Function of [:COMPLEX ,c₁:],c₁ by FUNCOP_1:57;
E3: for b₁ being Element of COMPLEX
for b₂ being Element of c₁ holds c₅ . [b₁,b₂] = c₃

proof

let c₆ be Element of COMPLEX ;
let c₇ be Element of c₁;
[c₆,c₇] in [:COMPLEX ,c₁:] ;
hence c₅ . [c₆,c₇] = c₃ by FUNCOP_1:13;

end;

take c₆ = c₄;
take c₇ = c₅;
set c₈ = CLSStruct(# c₁,c₃,c₆,c₇ #);
thus for b₁, b₂ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) holds b₁ + b₂ = b₂ + b₁

proof

let c₉, c₁₀ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
E4: ( c₉ + c₁₀ = c₆ . c₉,c₁₀ & c₁₀ + c₉ = c₆ . c₁₀,c₉ ) ;
reconsider c₁₁ = c₉, c₁₂ = c₁₀ as Element of c₁ ;
( c₉ + c₁₀ = H₁(c₁₁,c₁₂) & c₁₀ + c₉ = H₁(c₁₂,c₁₁) ) by E2, E4;
hence c₉ + c₁₀ = c₁₀ + c₉ ;

end;

thus for b₁, b₂, b₃ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) holds (b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof

let c₉, c₁₀, c₁₁ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
E4: ( (c₉ + c₁₀) + c₁₁ = c₆ . (c₉ + c₁₀),c₁₁ & c₉ + (c₁₀ + c₁₁) = c₆ . c₉,(c₁₀ + c₁₁) ) ;
reconsider c₁₂ = c₉, c₁₃ = c₁₀, c₁₄ = c₁₁ as Element of c₁ ;
( (c₉ + c₁₀) + c₁₁ = H₁(H₁(c₁₂,c₁₃),c₁₄) & c₉ + (c₁₀ + c₁₁) = H₁(c₁₂,H₁(c₁₃,c₁₄)) ) by E2, E4;
hence (c₉ + c₁₀) + c₁₁ = c₉ + (c₁₀ + c₁₁) ;

end;

thus for b₁ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) holds b₁ + (0. CLSStruct(# c₁,c₃,c₆,c₇ #)) = b₁

proof

let c₉ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₀ = c₉ as Element of c₁ ;
c₉ + (0. CLSStruct(# c₁,c₃,c₆,c₇ #)) = c₆ . [c₉,(0. CLSStruct(# c₁,c₃,c₆,c₇ #))]
.= c₆ . c₉,(0. CLSStruct(# c₁,c₃,c₆,c₇ #))
.= H₁(c₁₀,c₃) by E2 ;
hence c₉ + (0. CLSStruct(# c₁,c₃,c₆,c₇ #)) = c₉ by TARSKI:def 1;

end;

thus for b₁ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) ex b₂ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) st b₁ + b₂ = 0. CLSStruct(# c₁,c₃,c₆,c₇ #)

proof

let c₉ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₀ = c₃ as VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) ;
take c₁₀ ;
thus c₉ + c₁₀ = c₆ . [c₉,c₁₀]
.= c₆ . c₉,c₁₀
.= the Zero of CLSStruct(# c₁,c₃,c₆,c₇ #) by E2
.= 0. CLSStruct(# c₁,c₃,c₆,c₇ #) ;

end;

thus for b₁ being Complex
for b₂, b₃ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) holds b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃)

proof

let c₉ be Complex;
let c₁₀, c₁₁ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₂ = c₁₀, c₁₃ = c₁₁ as Element of c₁ ;
(c₉ * c₁₀) + (c₉ * c₁₁) = c₆ . [(c₉ * c₁₀),(c₉ * c₁₁)]
.= c₆ . (c₉ * c₁₀),(c₉ * c₁₁)
.= H₁(c₃,c₃) by E2 ;
hence c₉ * (c₁₀ + c₁₁) = (c₉ * c₁₀) + (c₉ * c₁₁) by E3;

end;

thus for b₁, b₂ being Complex
for b₃ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃)

proof

let c₉, c₁₀ be Complex;
let c₁₁ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
set c₁₂ = c₉ + c₁₀;
reconsider c₁₃ = c₁₁ as Element of c₁ ;
E4: (c₉ + c₁₀) * c₁₁ = c₇ . [(c₉ + c₁₀),c₁₁]
.= c₃ by E3 ;
(c₉ * c₁₁) + (c₁₀ * c₁₁) = c₆ . [(c₉ * c₁₁),(c₁₀ * c₁₁)]
.= c₆ . (c₉ * c₁₁),(c₁₀ * c₁₁)
.= H₁(c₃,c₃) by E2 ;
hence (c₉ + c₁₀) * c₁₁ = (c₉ * c₁₁) + (c₁₀ * c₁₁) by E4;

end;

thus for b₁, b₂ being Complex
for b₃ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)

proof

let c₉, c₁₀ be Complex;
let c₁₁ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
set c₁₂ = c₉ * c₁₀;
reconsider c₁₃ = c₁₁ as Element of c₁ ;
E4: (c₉ * c₁₀) * c₁₁ = c₇ . [(c₉ * c₁₀),c₁₁]
.= c₃ by E3 ;
c₉ * (c₁₀ * c₁₁) = c₇ . [c₉,(c₁₀ * c₁₁)]
.= c₃ by E3 ;
hence (c₉ * c₁₀) * c₁₁ = c₉ * (c₁₀ * c₁₁) by E4;

end;

thus for b₁ being VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #) holds 1r * b₁ = b₁

proof

let c₉ be VECTOR of CLSStruct(# c₁,c₃,c₆,c₇ #);
reconsider c₁₀ = c₉ as Element of c₁ ;
reconsider c₁₁ = 1 as Element of REAL ;
1r * c₉ = c₇ . [1r ,c₉]
.= c₃ by E3 ;
hence 1r * c₉ = c₉ by TARSKI:def 1;

end;

definition

let c₁ be non empty CLSStruct ;
attr a₁ is ComplexLinearSpace-like means :Def2: :: CLVECT_1:def 2
( ( for b₁ being Complex
for b₂, b₃ being VECTOR of a₁ holds b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) ) & ( for b₁, b₂ being Complex
for b₃ being VECTOR of a₁ holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) ) & ( for b₁, b₂ being Complex
for b₃ being VECTOR of a₁ holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being VECTOR of a₁ holds 1r * b₁ = b₁ ) );

end;

:: deftheorem Def2 defines ComplexLinearSpace-like CLVECT_1:def 2 :

registration

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

proof end;

end;

definition

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

end;

theorem Th1: :: CLVECT_1:1

for b₁ being non empty CLSStruct st ( for b₂, b₃ being VECTOR of b₁ holds b₂ + b₃ = b₃ + b₂ ) & ( for b₂, b₃, b₄ being VECTOR of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) ) & ( for b₂ being VECTOR of b₁ holds b₂ + (0. b₁) = b₂ ) & ( for b₂ being VECTOR of b₁ ex b₃ being VECTOR of b₁ st b₂ + b₃ = 0. b₁ ) & ( for b₂ being Complex
for b₃, b₄ being VECTOR of b₁ holds b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) ) & ( for b₂, b₃ being Complex
for b₄ being VECTOR of b₁ holds (b₂ + b₃) * b₄ = (b₂ * b₄) + (b₃ * b₄) ) & ( for b₂, b₃ being Complex
for b₄ being VECTOR of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂ being VECTOR of b₁ holds 1r * b₂ = b₂ ) holds
b₁ is ComplexLinearSpace by Def2, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;

theorem Th2: :: CLVECT_1:2

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex st ( b₃ = 0 or b₂ = 0. b₁ ) holds
b₃ * b₂ = 0. b₁

proof end;

theorem Th3: :: CLVECT_1:3

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex holds
( not b₃ * b₂ = 0. b₁ or b₃ = 0 or b₂ = 0. b₁ )

proof end;

theorem Th4: :: CLVECT_1:4

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ holds - b₂ = (- 1r ) * b₂

proof end;

theorem Th5: :: CLVECT_1:5

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ st b₂ = - b₂ holds
b₂ = 0. b₁

proof end;

theorem Th6: :: CLVECT_1:6

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ st b₂ + b₂ = 0. b₁ holds
b₂ = 0. b₁

proof end;

theorem Th7: :: CLVECT_1:7

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex holds b₃ * (- b₂) = (- b₃) * b₂

proof end;

theorem Th8: :: CLVECT_1:8

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex holds b₃ * (- b₂) = - (b₃ * b₂)

proof end;

theorem Th9: :: CLVECT_1:9

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex holds (- b₃) * (- b₂) = b₃ * b₂

proof end;

theorem Th10: :: CLVECT_1:10

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Complex holds b₄ * (b₂ - b₃) = (b₄ * b₂) - (b₄ * b₃)

proof end;

theorem Th11: :: CLVECT_1:11

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃, b₄ being Complex holds (b₃ - b₄) * b₂ = (b₃ * b₂) - (b₄ * b₂)

proof end;

theorem Th12: :: CLVECT_1:12

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Complex st b₄ <> 0 & b₄ * b₂ = b₄ * b₃ holds
b₂ = b₃

proof end;

theorem Th13: :: CLVECT_1:13

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃, b₄ being Complex st b₂ <> 0. b₁ & b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄

proof end;

Lemma11: for b₁ being non empty LoopStr holds Sum (<*> the carrier of b₁) = 0. b₁

proof end;

Lemma12: for b₁ being non empty LoopStr
for b₂ being FinSequence of the carrier of b₁ st len b₂ = 0 holds
Sum b₂ = 0. b₁

proof end;

theorem Th14: :: CLVECT_1:14

for b₁ being ComplexLinearSpace
for b₂ being Complex
for b₃, b₄ being FinSequence of the carrier of b₁ st len b₃ = len b₄ & ( for b₅ being Nat
for b₆ being VECTOR of b₁ st b₅ in dom b₃ & b₆ = b₄ . b₅ holds
b₃ . b₅ = b₂ * b₆ ) holds
Sum b₃ = b₂ * (Sum b₄)

proof end;

theorem Th15: :: CLVECT_1:15

for b₁ being ComplexLinearSpace
for b₂ being Complex holds b₂ * (Sum (<*> the carrier of b₁)) = 0. b₁

proof end;

theorem Th16: :: CLVECT_1:16

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Complex holds b₄ * (Sum <*b₂,b₃*>) = (b₄ * b₂) + (b₄ * b₃)

proof end;

theorem Th17: :: CLVECT_1:17

for b₁ being ComplexLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Complex holds b₅ * (Sum <*b₂,b₃,b₄*>) = ((b₅ * b₂) + (b₅ * b₃)) + (b₅ * b₄)

proof end;

Lemma13: 1r + 1r = [*2,0*]

proof end;

theorem Th18: :: CLVECT_1:18

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ holds Sum <*b₂,b₂*> = [*2,0*] * b₂

proof end;

theorem Th19: :: CLVECT_1:19

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ holds Sum <*(- b₂),(- b₂)*> = [*(- 2),0*] * b₂

proof end;

theorem Th20: :: CLVECT_1:20

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ holds Sum <*b₂,b₂,b₂*> = [*3,0*] * b₂

proof end;

definition

let c₁ be ComplexLinearSpace;
let c₂ be Subset of c₁;
attr a₂ is lineary-closed means :Def3: :: CLVECT_1:def 3
( ( for b₁, b₂ being VECTOR of a₁ st b₁ in a₂ & b₂ in a₂ holds
b₁ + b₂ in a₂ ) & ( for b₁ being Complex
for b₂ being VECTOR of a₁ st b₂ in a₂ holds
b₁ * b₂ in a₂ ) );

end;

:: deftheorem Def3 defines lineary-closed CLVECT_1:def 3 :

theorem Th21: :: CLVECT_1:21

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st b₂ <> {} & b₂ is lineary-closed holds
0. b₁ in b₂

proof end;

theorem Th22: :: CLVECT_1:22

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st b₂ is lineary-closed holds
for b₃ being VECTOR of b₁ st b₃ in b₂ holds
- b₃ in b₂

proof end;

theorem Th23: :: CLVECT_1:23

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st b₂ is lineary-closed holds
for b₃, b₄ being VECTOR of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ - b₄ in b₂

proof end;

theorem Th24: :: CLVECT_1:24

for b₁ being ComplexLinearSpace holds {(0. b₁)} is lineary-closed

proof end;

theorem Th25: :: CLVECT_1:25

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st the carrier of b₁ = b₂ holds
b₂ is lineary-closed

proof end;

theorem Th26: :: CLVECT_1:26

for b₁ being ComplexLinearSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is lineary-closed & b₃ is lineary-closed & b₄ = { (b₅ + b₆) where B is VECTOR of b₁, B is VECTOR of b₁ : ( b₅ in b₂ & b₆ in b₃ ) } holds
b₄ is lineary-closed

proof end;

theorem Th27: :: CLVECT_1:27

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subset of b₁ st b₂ is lineary-closed & b₃ is lineary-closed holds
b₂ /\ b₃ is lineary-closed

proof end;

definition

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

proof end;

end;

:: deftheorem Def4 defines Subspace CLVECT_1:def 4 :

theorem Th28: :: CLVECT_1:28

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subspace of b₁
for b₄ being set st b₄ in b₂ & b₂ is Subspace of b₃ holds
b₄ in b₃

proof end;

theorem Th29: :: CLVECT_1:29

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁
for b₃ being set st b₃ in b₂ holds
b₃ in b₁

proof end;

theorem Th30: :: CLVECT_1:30

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₂ holds b₃ is VECTOR of b₁

proof end;

theorem Th31: :: CLVECT_1:31

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds 0. b₂ = 0. b₁ by Def4;

theorem Th32: :: CLVECT_1:32

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subspace of b₁ holds 0. b₂ = 0. b₃

proof end;

theorem Th33: :: CLVECT_1:33

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅, b₆ being VECTOR of b₄ st b₅ = b₂ & b₆ = b₃ holds
b₅ + b₆ = b₂ + b₃

proof end;

theorem Th34: :: CLVECT_1:34

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex
for b₄ being Subspace of b₁
for b₅ being VECTOR of b₄ st b₅ = b₂ holds
b₃ * b₅ = b₃ * b₂

proof end;

theorem Th35: :: CLVECT_1:35

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄ being VECTOR of b₃ st b₄ = b₂ holds
- b₂ = - b₄

proof end;

theorem Th36: :: CLVECT_1:36

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅, b₆ being VECTOR of b₄ st b₅ = b₂ & b₆ = b₃ holds
b₅ - b₆ = b₂ - b₃

proof end;

Lemma27: for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁
for b₃ being Subspace of b₁ st the carrier of b₃ = b₂ holds
b₂ is lineary-closed

proof end;

theorem Th37: :: CLVECT_1:37

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds 0. b₁ in b₂

proof end;

theorem Th38: :: CLVECT_1:38

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subspace of b₁ holds 0. b₂ in b₃

proof end;

theorem Th39: :: CLVECT_1:39

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds 0. b₂ in b₁

proof end;

theorem Th40: :: CLVECT_1:40

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ + b₃ in b₄

proof end;

theorem Th41: :: CLVECT_1:41

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex
for b₄ being Subspace of b₁ st b₂ in b₄ holds
b₃ * b₂ in b₄

proof end;

theorem Th42: :: CLVECT_1:42

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ st b₂ in b₃ holds
- b₂ in b₃

proof end;

theorem Th43: :: CLVECT_1:43

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ in b₄ & b₃ in b₄ holds
b₂ - b₃ in b₄

proof end;

theorem Th44: :: CLVECT_1:44

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being BinOp of b₃
for b₆ being Function of [:COMPLEX ,b₃:],b₃ st b₂ = b₃ & b₄ = 0. b₁ & b₅ = the add of b₁ || b₂ & b₆ = the Mult of b₁ | [:COMPLEX ,b₂:] holds
CLSStruct(# b₃,b₄,b₅,b₆ #) is Subspace of b₁

proof end;

theorem Th45: :: CLVECT_1:45

for b₁ being ComplexLinearSpace holds b₁ is Subspace of b₁

proof end;

theorem Th46: :: CLVECT_1:46

for b₁, b₂ being strict ComplexLinearSpace st b₁ is Subspace of b₂ & b₂ is Subspace of b₁ holds
b₁ = b₂

proof end;

theorem Th47: :: CLVECT_1:47

for b₁, b₂, b₃ being ComplexLinearSpace st b₁ is Subspace of b₂ & b₂ is Subspace of b₃ holds
b₁ is Subspace of b₃

proof end;

theorem Th48: :: CLVECT_1:48

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subspace of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is Subspace of b₃

proof end;

theorem Th49: :: CLVECT_1:49

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subspace of b₁ st ( for b₄ being VECTOR of b₁ st b₄ in b₂ holds
b₄ in b₃ ) holds
b₂ is Subspace of b₃

proof end;

registration

let c₁ be ComplexLinearSpace;
cluster strict Subspace of a₁;
existence

proof end;

end;

theorem Th50: :: CLVECT_1:50

for b₁ being ComplexLinearSpace
for b₂, b₃ being strict Subspace of b₁ st the carrier of b₂ = the carrier of b₃ holds
b₂ = b₃

proof end;

theorem Th51: :: CLVECT_1:51

for b₁ being ComplexLinearSpace
for b₂, b₃ being strict Subspace of b₁ st ( for b₄ being VECTOR of b₁ holds
( b₄ in b₂ iff b₄ in b₃ ) ) holds
b₂ = b₃

proof end;

theorem Th52: :: CLVECT_1:52

for b₁ being strict ComplexLinearSpace
for b₂ being strict Subspace of b₁ st the carrier of b₂ = the carrier of b₁ holds
b₂ = b₁

proof end;

theorem Th53: :: CLVECT_1:53

for b₁ being strict ComplexLinearSpace
for b₂ being strict Subspace of b₁ st ( for b₃ being VECTOR of b₁ holds
( b₃ in b₂ iff b₃ in b₁ ) ) holds
b₂ = b₁

proof end;

theorem Th54: :: CLVECT_1:54

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁
for b₃ being Subspace of b₁ st the carrier of b₃ = b₂ holds
b₂ is lineary-closed by Lemma27;

theorem Th55: :: CLVECT_1:55

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st b₂ <> {} & b₂ is lineary-closed holds
ex b₃ being strict Subspace of b₁ st b₂ = the carrier of b₃

proof end;

definition

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

proof end;

end;

:: deftheorem Def5 defines (0). CLVECT_1:def 5 :

definition

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

proof end;

end;

:: deftheorem Def6 defines (Omega). CLVECT_1:def 6 :

theorem Th56: :: CLVECT_1:56

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds (0). b₂ = (0). b₁

proof end;

theorem Th57: :: CLVECT_1:57

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subspace of b₁ holds (0). b₂ = (0). b₃

proof end;

theorem Th58: :: CLVECT_1:58

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds (0). b₂ is Subspace of b₁ by Th47;

theorem Th59: :: CLVECT_1:59

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds (0). b₁ is Subspace of b₂

proof end;

theorem Th60: :: CLVECT_1:60

for b₁ being ComplexLinearSpace
for b₂, b₃ being Subspace of b₁ holds (0). b₂ is Subspace of b₃

proof end;

theorem Th61: :: CLVECT_1:61

for b₁ being strict ComplexLinearSpace holds b₁ is Subspace of (Omega). b₁ ;

definition

let c₁ be ComplexLinearSpace;
let c₂ be VECTOR of c₁;
let c₃ be Subspace of c₁;
func c₂ + c₃ -> Subset of a₁ equals :: CLVECT_1:def 7
{ (a₂ + b₁) where B is VECTOR of a₁ : b₁ in a₃ } ;
coherence

proof end;

end;

:: deftheorem Def7 defines + CLVECT_1:def 7 :

Lemma44: for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds (0. b₁) + b₂ = the carrier of b₂

proof end;

definition

let c₁ be ComplexLinearSpace;
let c₂ be Subspace of c₁;
mode Coset of c₂ -> Subset of a₁ means :Def8: :: CLVECT_1:def 8
ex b₁ being VECTOR of a₁ st a₃ = b₁ + a₂;
existence

proof end;

end;

:: deftheorem Def8 defines Coset CLVECT_1:def 8 :

theorem Th62: :: CLVECT_1:62

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( 0. b₁ in b₂ + b₃ iff b₂ in b₃ )

proof end;

theorem Th63: :: CLVECT_1:63

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds b₂ in b₂ + b₃

proof end;

theorem Th64: :: CLVECT_1:64

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds (0. b₁) + b₂ = the carrier of b₂ by Lemma44;

theorem Th65: :: CLVECT_1:65

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ holds b₂ + ((0). b₁) = {b₂}

proof end;

Lemma49: for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ in b₃ iff b₂ + b₃ = the carrier of b₃ )

proof end;

theorem Th66: :: CLVECT_1:66

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ holds b₂ + ((Omega). b₁) = the carrier of b₁

proof end;

theorem Th67: :: CLVECT_1:67

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( 0. b₁ in b₂ + b₃ iff b₂ + b₃ = the carrier of b₃ )

proof end;

theorem Th68: :: CLVECT_1:68

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ in b₃ iff b₂ + b₃ = the carrier of b₃ ) by Lemma49;

theorem Th69: :: CLVECT_1:69

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex
for b₄ being Subspace of b₁ st b₂ in b₄ holds
(b₃ * b₂) + b₄ = the carrier of b₄

proof end;

theorem Th70: :: CLVECT_1:70

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex
for b₄ being Subspace of b₁ st b₃ <> 0 & (b₃ * b₂) + b₄ = the carrier of b₄ holds
b₂ in b₄

proof end;

theorem Th71: :: CLVECT_1:71

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ in b₃ iff (- b₂) + b₃ = the carrier of b₃ )

proof end;

theorem Th72: :: CLVECT_1:72

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₄ iff b₃ + b₄ = (b₃ + b₂) + b₄ )

proof end;

theorem Th73: :: CLVECT_1:73

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₄ iff b₃ + b₄ = (b₃ - b₂) + b₄ )

proof end;

theorem Th74: :: CLVECT_1:74

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₃ + b₄ iff b₃ + b₄ = b₂ + b₄ )

proof end;

theorem Th75: :: CLVECT_1:75

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( b₂ + b₃ = (- b₂) + b₃ iff b₂ in b₃ )

proof end;

theorem Th76: :: CLVECT_1:76

for b₁ being ComplexLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Subspace of b₁ st b₂ in b₃ + b₅ & b₂ in b₄ + b₅ holds
b₃ + b₅ = b₄ + b₅

proof end;

theorem Th77: :: CLVECT_1:77

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ in b₃ + b₄ & b₂ in (- b₃) + b₄ holds
b₃ in b₄

proof end;

theorem Th78: :: CLVECT_1:78

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex
for b₄ being Subspace of b₁ st b₃ <> 1r & b₃ * b₂ in b₂ + b₄ holds
b₂ in b₄

proof end;

theorem Th79: :: CLVECT_1:79

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Complex
for b₄ being Subspace of b₁ st b₂ in b₄ holds
b₃ * b₂ in b₂ + b₄

proof end;

theorem Th80: :: CLVECT_1:80

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ holds
( - b₂ in b₂ + b₃ iff b₂ in b₃ )

proof end;

theorem Th81: :: CLVECT_1:81

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ + b₃ in b₃ + b₄ iff b₂ in b₄ )

proof end;

theorem Th82: :: CLVECT_1:82

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ - b₃ in b₂ + b₄ iff b₃ in b₄ )

proof end;

theorem Th83: :: CLVECT_1:83

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₃ + b₄ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ = b₃ + b₅ ) )

proof end;

theorem Th84: :: CLVECT_1:84

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( b₂ in b₃ + b₄ iff ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ = b₃ - b₅ ) )

proof end;

theorem Th85: :: CLVECT_1:85

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( ex b₅ being VECTOR of b₁ st
( b₂ in b₅ + b₄ & b₃ in b₅ + b₄ ) iff b₂ - b₃ in b₄ )

proof end;

theorem Th86: :: CLVECT_1:86

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ + b₄ = b₃ + b₄ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ + b₅ = b₃ )

proof end;

theorem Th87: :: CLVECT_1:87

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ st b₂ + b₄ = b₃ + b₄ holds
ex b₅ being VECTOR of b₁ st
( b₅ in b₄ & b₂ - b₅ = b₃ )

proof end;

theorem Th88: :: CLVECT_1:88

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃, b₄ being strict Subspace of b₁ holds
( b₂ + b₃ = b₂ + b₄ iff b₃ = b₄ )

proof end;

theorem Th89: :: CLVECT_1:89

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄, b₅ being strict Subspace of b₁ st b₂ + b₄ = b₃ + b₅ holds
b₄ = b₅

proof end;

theorem Th90: :: CLVECT_1:90

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂ holds
( b₃ is lineary-closed iff b₃ = the carrier of b₂ )

proof end;

theorem Th91: :: CLVECT_1:91

for b₁ being ComplexLinearSpace
for b₂, b₃ being strict Subspace of b₁
for b₄ being Coset of b₂
for b₅ being Coset of b₃ st b₄ = b₅ holds
b₂ = b₃

proof end;

theorem Th92: :: CLVECT_1:92

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁ holds {b₂} is Coset of (0). b₁

proof end;

theorem Th93: :: CLVECT_1:93

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st b₂ is Coset of (0). b₁ holds
ex b₃ being VECTOR of b₁ st b₂ = {b₃}

proof end;

theorem Th94: :: CLVECT_1:94

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁ holds the carrier of b₂ is Coset of b₂

proof end;

theorem Th95: :: CLVECT_1:95

for b₁ being ComplexLinearSpace holds the carrier of b₁ is Coset of (Omega). b₁

proof end;

theorem Th96: :: CLVECT_1:96

for b₁ being ComplexLinearSpace
for b₂ being Subset of b₁ st b₂ is Coset of (Omega). b₁ holds
b₂ = the carrier of b₁

proof end;

theorem Th97: :: CLVECT_1:97

for b₁ being ComplexLinearSpace
for b₂ being Subspace of b₁
for b₃ being Coset of b₂ holds
( 0. b₁ in b₃ iff b₃ = the carrier of b₂ )

proof end;

theorem Th98: :: CLVECT_1:98

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄ being Coset of b₃ holds
( b₂ in b₄ iff b₄ = b₂ + b₃ )

proof end;

theorem Th99: :: CLVECT_1:99

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅ being Coset of b₄ st b₂ in b₅ & b₃ in b₅ holds
ex b₆ being VECTOR of b₁ st
( b₆ in b₄ & b₂ + b₆ = b₃ )

proof end;

theorem Th100: :: CLVECT_1:100

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁
for b₅ being Coset of b₄ st b₂ in b₅ & b₃ in b₅ holds
ex b₆ being VECTOR of b₁ st
( b₆ in b₄ & b₂ - b₆ = b₃ )

proof end;

theorem Th101: :: CLVECT_1:101

for b₁ being ComplexLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Subspace of b₁ holds
( ex b₅ being Coset of b₄ st
( b₂ in b₅ & b₃ in b₅ ) iff b₂ - b₃ in b₄ )

proof end;

theorem Th102: :: CLVECT_1:102

for b₁ being ComplexLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄, b₅ being Coset of b₃ st b₂ in b₄ & b₂ in b₅ holds
b₄ = b₅

proof end;

definition

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

end;

registration

cluster non empty CNORMSTR ;
existence

proof end;

end;

deffunc H₁( CNORMSTR ) -> Element of the carrier of a₁ = 0. a₁;

definition

let c₁ be non empty CNORMSTR ;
let c₂ be Point of c₁;
func ||.c₂.|| -> Real equals :: CLVECT_1:def 9
the norm of a₁ . a₂;
coherence ;

end;

:: deftheorem Def9 defines ||. CLVECT_1:def 9 :

consider c₁ being ComplexLinearSpace;

Lemma69: the carrier of ((0). c₁) = {(0. c₁)}
by Def5;

reconsider c₂ = the carrier of ((0). c₁) --> 0 as Function of the carrier of ((0). c₁), REAL by FUNCOP_1:57;

0. c₁ is VECTOR of ((0). c₁)
by Lemma69, TARSKI:def 1;

then Lemma70: c₂ . (0. c₁) = 0
by FUNCOP_1:13;

Lemma71: for b₁ being VECTOR of ((0). c₁)
for b₂ being Complex holds c₂ . (b₂ * b₁) = |.b₂.| * (c₂ . b₁)

proof end;

Lemma72: for b₁, b₂ being VECTOR of ((0). c₁) holds c₂ . (b₁ + b₂) <= (c₂ . b₁) + (c₂ . b₂)

proof end;

reconsider c₃ = CNORMSTR(# the carrier of ((0). c₁),the Zero of ((0). c₁),the add of ((0). c₁),the Mult of ((0). c₁),c₂ #) as non empty CNORMSTR by STRUCT_0:def 1;

E73: now

let c₄, c₅ be Point of c₃;
let c₆ be Complex;
reconsider c₇ = c₄, c₈ = c₅ as VECTOR of ((0). c₁) ;
thus ( ||.c₄.|| = 0 iff c₄ = H₁(c₃) )

proof

H₁(c₃) = the Zero of c₃
.= 0. ((0). c₁)
.= 0. c₁ by Th31 ;
hence ( ||.c₄.|| = 0 iff c₄ = H₁(c₃) ) by Lemma69, Lemma70, TARSKI:def 1;

end;

c₆ * c₄ = the Mult of c₃ . [c₆,c₇]
.= c₆ * c₇ ;
hence ||.(c₆ * c₄).|| = |.c₆.| * ||.c₄.|| by Lemma71;
c₄ + c₅ = the add of c₃ . [c₄,c₅]
.= c₇ + c₈ ;
hence ||.(c₄ + c₅).|| <= ||.c₄.|| + ||.c₅.|| by Lemma72;

end;

definition

let c₄ be non empty CNORMSTR ;
attr a₁ is ComplexNormSpace-like means :Def10: :: CLVECT_1:def 10
for b₁, b₂ being Point of a₁
for b₃ being Complex holds
( ( ||.b₁.|| = 0 implies b₁ = 0. a₁ ) & ( b₁ = 0. a₁ implies ||.b₁.|| = 0 ) & ||.(b₃ * b₁).|| = |.b₃.| * ||.b₁.|| & ||.(b₁ + b₂).|| <= ||.b₁.|| + ||.b₂.|| );

end;

:: deftheorem Def10 defines ComplexNormSpace-like CLVECT_1:def 10 :

registration

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

proof end;

end;

definition

mode ComplexNormSpace is non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like CNORMSTR ;

end;

theorem Th103: :: CLVECT_1:103

for b₁ being ComplexNormSpace holds ||.(0. b₁).|| = 0 by Def10;

theorem Th104: :: CLVECT_1:104

for b₁ being ComplexNormSpace
for b₂ being Point of b₁ holds ||.(- b₂).|| = ||.b₂.||

proof end;

theorem Th105: :: CLVECT_1:105

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ - b₃).|| <= ||.b₂.|| + ||.b₃.||

proof end;

theorem Th106: :: CLVECT_1:106

for b₁ being ComplexNormSpace
for b₂ being Point of b₁ holds 0 <= ||.b₂.||

proof end;

theorem Th107: :: CLVECT_1:107

for b₁, b₂ being Complex
for b₃ being ComplexNormSpace
for b₄, b₅ being Point of b₃ holds ||.((b₁ * b₄) + (b₂ * b₅)).|| <= (|.b₁.| * ||.b₄.||) + (|.b₂.| * ||.b₅.||)

proof end;

theorem Th108: :: CLVECT_1:108

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ holds
( ||.(b₂ - b₃).|| = 0 iff b₂ = b₃ )

proof end;

theorem Th109: :: CLVECT_1:109

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ holds ||.(b₂ - b₃).|| = ||.(b₃ - b₂).||

proof end;

theorem Th110: :: CLVECT_1:110

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ holds ||.b₂.|| - ||.b₃.|| <= ||.(b₂ - b₃).||

proof end;

theorem Th111: :: CLVECT_1:111

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ holds abs (||.b₂.|| - ||.b₃.||) <= ||.(b₂ - b₃).||

proof end;

theorem Th112: :: CLVECT_1:112

for b₁ being ComplexNormSpace
for b₂, b₃, b₄ being Point of b₁ holds ||.(b₂ - b₃).|| <= ||.(b₂ - b₄).|| + ||.(b₄ - b₃).||

proof end;

theorem Th113: :: CLVECT_1:113

for b₁ being ComplexNormSpace
for b₂, b₃ being Point of b₁ st b₂ <> b₃ holds
||.(b₂ - b₃).|| <> 0 by Th108;

definition

let c₄ be ComplexLinearSpace;
let c₅, c₆ be sequence of c₄;
func c₂ + c₃ -> sequence of a₁ means :Def11: :: CLVECT_1:def 11
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) + (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines + CLVECT_1:def 11 :

definition

let c₄ be ComplexLinearSpace;
let c₅, c₆ be sequence of c₄;
func c₂ - c₃ -> sequence of a₁ means :Def12: :: CLVECT_1:def 12
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) - (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines - CLVECT_1:def 12 :

definition

let c₄ be ComplexLinearSpace;
let c₅ be sequence of c₄;
let c₆ be Element of c₄;
func c₂ - c₃ -> sequence of a₁ means :Def13: :: CLVECT_1:def 13
for b₁ being Nat holds a₄ . b₁ = (a₂ . b₁) - a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines - CLVECT_1:def 13 :

definition

let c₄ be ComplexLinearSpace;
let c₅ be sequence of c₄;
let c₆ be Complex;
func c₃ * c₂ -> sequence of a₁ means :Def14: :: CLVECT_1:def 14
for b₁ being Nat holds a₄ . b₁ = a₃ * (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines * CLVECT_1:def 14 :

definition

let c₄ be ComplexNormSpace;
let c₅ be sequence of c₄;
attr a₂ is convergent means :Def15: :: CLVECT_1:def 15
ex b₁ being Point of a₁ st
for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
||.((a₂ . b₄) - b₁).|| < b₂;

end;

:: deftheorem Def15 defines convergent CLVECT_1:def 15 :

theorem Th114: :: CLVECT_1:114

canceled;

theorem Th115: :: CLVECT_1:115

for b₁ being ComplexNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ + b₃ is convergent

proof end;

theorem Th116: :: CLVECT_1:116

for b₁ being ComplexNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
b₂ - b₃ is convergent

proof end;

theorem Th117: :: CLVECT_1:117

for b₁ being ComplexNormSpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
b₃ - b₂ is convergent

proof end;

theorem Th118: :: CLVECT_1:118

for b₁ being Complex
for b₂ being ComplexNormSpace
for b₃ being sequence of b₂ st b₃ is convergent holds
b₁ * b₃ is convergent

proof end;

definition

let c₄ be ComplexNormSpace;
let c₅ be sequence of c₄;
func ||.c₂.|| -> Real_Sequence means :Def16: :: CLVECT_1:def 16
for b₁ being Nat holds a₃ . b₁ = ||.(a₂ . b₁).||;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines ||. CLVECT_1:def 16 :

theorem Th119: :: CLVECT_1:119

for b₁ being ComplexNormSpace
for b₂ being sequence of b₁ st b₂ is convergent holds
||.b₂.|| is convergent

proof end;

definition

let c₄ be ComplexNormSpace;
let c₅ be sequence of c₄;
assume E94: c₅ is convergent ;
func lim c₂ -> Point of a₁ means :Def17: :: CLVECT_1:def 17
for b₁ being Real st 0 < b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
||.((a₂ . b₃) - a₃).|| < b₁;
existence by E94, Def15;
uniqueness

proof end;

end;

:: deftheorem Def17 defines lim CLVECT_1:def 17 :

theorem Th120: :: CLVECT_1:120

for b₁ being ComplexNormSpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent & lim b₃ = b₂ holds
( ||.(b₃ - b₂).|| is convergent & lim ||.(b₃ - b₂).|| = 0 )

proof end;

theorem Th121: :: CLVECT_1:121

for b₁ being ComplexNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ + b₃) = (lim b₂) + (lim b₃)

proof end;

theorem Th122: :: CLVECT_1:122

for b₁ being ComplexNormSpace
for b₂, b₃ being sequence of b₁ st b₂ is convergent & b₃ is convergent holds
lim (b₂ - b₃) = (lim b₂) - (lim b₃)

proof end;

theorem Th123: :: CLVECT_1:123

for b₁ being ComplexNormSpace
for b₂ being Point of b₁
for b₃ being sequence of b₁ st b₃ is convergent holds
lim (b₃ - b₂) = (lim b₃) - b₂

proof end;

theorem Th124: :: CLVECT_1:124

for b₁ being Complex
for b₂ being ComplexNormSpace
for b₃ being sequence of b₂ st b₃ is convergent holds
lim (b₁ * b₃) = b₁ * (lim b₃)

proof end;