:: CLOPBAN1 semantic presentation

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of [:COMPLEX ,c₂:],c₂;
let c₄ be complex number ;
let c₅ be Function of c₁,c₂;
redefine func [;] as c₃ [;] c₄,c₅ -> Element of Funcs a₁,a₂;
coherence

proof end;

end;

theorem Th1: :: CLOPBAN1:1

for b₁ being non empty set
for b₂ being ComplexLinearSpace ex b₃ being Function of [:COMPLEX ,(Funcs b₁,the carrier of b₂):], Funcs b₁,the carrier of b₂ st
for b₄ being Complex
for b₅ being Element of Funcs b₁,the carrier of b₂
for b₆ being Element of b₁ holds (b₃ . [b₄,b₅]) . b₆ = b₄ * (b₅ . b₆)

proof end;

definition

let c₁ be non empty set ;
let c₂ be ComplexLinearSpace;
func FuncExtMult c₁,c₂ -> Function of [:COMPLEX ,(Funcs a₁,the carrier of a₂):], Funcs a₁,the carrier of a₂ means :Def1: :: CLOPBAN1:def 1
for b₁ being Complex
for b₂ being Element of Funcs a₁,the carrier of a₂
for b₃ being Element of a₁ holds (a₃ . [b₁,b₂]) . b₃ = b₁ * (b₂ . b₃);
existence by Th1;
uniqueness

proof end;

end;

:: deftheorem Def1 defines FuncExtMult CLOPBAN1:def 1 :

theorem Th2: :: CLOPBAN1:2

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃ being Element of b₁ holds (FuncZero b₁,b₂) . b₃ = 0. b₂

proof end;

theorem Th3: :: CLOPBAN1:3

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃, b₄ being Element of Funcs b₁,the carrier of b₂
for b₅ being Complex holds
( b₃ = (FuncExtMult b₁,b₂) . [b₅,b₄] iff for b₆ being Element of b₁ holds b₃ . b₆ = b₅ * (b₄ . b₆) )

proof end;

theorem Th4: :: CLOPBAN1:4

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃, b₄ being Element of Funcs b₁,the carrier of b₂ holds (FuncAdd b₁,b₂) . b₃,b₄ = (FuncAdd b₁,b₂) . b₄,b₃

proof end;

theorem Th5: :: CLOPBAN1:5

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃, b₄, b₅ being Element of Funcs b₁,the carrier of b₂ holds (FuncAdd b₁,b₂) . b₃,((FuncAdd b₁,b₂) . b₄,b₅) = (FuncAdd b₁,b₂) . ((FuncAdd b₁,b₂) . b₃,b₄),b₅

proof end;

theorem Th6: :: CLOPBAN1:6

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃ being Element of Funcs b₁,the carrier of b₂ holds (FuncAdd b₁,b₂) . (FuncZero b₁,b₂),b₃ = b₃

proof end;

theorem Th7: :: CLOPBAN1:7

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃ being Element of Funcs b₁,the carrier of b₂ holds (FuncAdd b₁,b₂) . b₃,((FuncExtMult b₁,b₂) . [(- 1r ),b₃]) = FuncZero b₁,b₂

proof end;

theorem Th8: :: CLOPBAN1:8

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃ being Element of Funcs b₁,the carrier of b₂ holds (FuncExtMult b₁,b₂) . [1r ,b₃] = b₃

proof end;

theorem Th9: :: CLOPBAN1:9

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃ being Element of Funcs b₁,the carrier of b₂
for b₄, b₅ being Complex holds (FuncExtMult b₁,b₂) . [b₄,((FuncExtMult b₁,b₂) . [b₅,b₃])] = (FuncExtMult b₁,b₂) . [(b₄ * b₅),b₃]

proof end;

theorem Th10: :: CLOPBAN1:10

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃ being Element of Funcs b₁,the carrier of b₂
for b₄, b₅ being Complex holds (FuncAdd b₁,b₂) . ((FuncExtMult b₁,b₂) . [b₄,b₃]),((FuncExtMult b₁,b₂) . [b₅,b₃]) = (FuncExtMult b₁,b₂) . [(b₄ + b₅),b₃]

proof end;

Lemma12: for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃, b₄ being Element of Funcs b₁,the carrier of b₂
for b₅ being Complex holds (FuncAdd b₁,b₂) . ((FuncExtMult b₁,b₂) . [b₅,b₃]),((FuncExtMult b₁,b₂) . [b₅,b₄]) = (FuncExtMult b₁,b₂) . [b₅,((FuncAdd b₁,b₂) . b₃,b₄)]

proof end;

theorem Th11: :: CLOPBAN1:11

for b₁ being non empty set
for b₂ being ComplexLinearSpace holds CLSStruct(# (Funcs b₁,the carrier of b₂),(FuncZero b₁,b₂),(FuncAdd b₁,b₂),(FuncExtMult b₁,b₂) #) is ComplexLinearSpace

proof end;

definition

let c₁ be non empty set ;
let c₂ be ComplexLinearSpace;
func ComplexVectSpace c₁,c₂ -> ComplexLinearSpace equals :: CLOPBAN1:def 2
CLSStruct(# (Funcs a₁,the carrier of a₂),(FuncZero a₁,a₂),(FuncAdd a₁,a₂),(FuncExtMult a₁,a₂) #);
coherence by Th11;

end;

:: deftheorem Def2 defines ComplexVectSpace CLOPBAN1:def 2 :

registration

let c₁ be non empty set ;
let c₂ be ComplexLinearSpace;
cluster ComplexVectSpace a₁,a₂ -> strict ;
coherence ;

end;

registration

let c₁ be non empty set ;
let c₂ be ComplexLinearSpace;
cluster ComplexVectSpace a₁,a₂ -> strict constituted-Functions ;
coherence by MONOID_0:89;

end;

definition

let c₁ be non empty set ;
let c₂ be ComplexLinearSpace;
let c₃ be VECTOR of (ComplexVectSpace c₁,c₂);
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> VECTOR of a₂;
coherence

proof end;

end;

theorem Th12: :: CLOPBAN1:12

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃, b₄, b₅ being VECTOR of (ComplexVectSpace b₁,b₂) holds
( b₅ = b₃ + b₄ iff for b₆ being Element of b₁ holds b₅ . b₆ = (b₃ . b₆) + (b₄ . b₆) )

proof end;

theorem Th13: :: CLOPBAN1:13

for b₁ being non empty set
for b₂ being ComplexLinearSpace
for b₃, b₄ being VECTOR of (ComplexVectSpace b₁,b₂)
for b₅ being Complex holds
( b₄ = b₅ * b₃ iff for b₆ being Element of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) )

proof end;

theorem Th14: :: CLOPBAN1:14

for b₁ being non empty set
for b₂ being ComplexLinearSpace holds 0. (ComplexVectSpace b₁,b₂) = b₁ --> (0. b₂) by LOPBAN_1:def 3;

definition

let c₁ be non empty CLSStruct ;
let c₂ be non empty LoopStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is additive means :Def3: :: CLOPBAN1:def 3
for b₁, b₂ being VECTOR of a₁ holds a₃ . (b₁ + b₂) = (a₃ . b₁) + (a₃ . b₂);

end;

:: deftheorem Def3 defines additive CLOPBAN1:def 3 :

definition

let c₁, c₂ be non empty CLSStruct ;
let c₃ be Function of c₁,c₂;
attr a₃ is homogeneous means :Def4: :: CLOPBAN1:def 4
for b₁ being VECTOR of a₁
for b₂ being Complex holds a₃ . (b₂ * b₁) = b₂ * (a₃ . b₁);

end;

:: deftheorem Def4 defines homogeneous CLOPBAN1:def 4 :

registration

let c₁ be non empty CLSStruct ;
let c₂ be ComplexLinearSpace;
cluster additive homogeneous M4(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

definition

let c₁, c₂ be ComplexLinearSpace;
mode LinearOperator of a₁,a₂ is additive homogeneous Function of a₁,a₂;

end;

definition

let c₁, c₂ be ComplexLinearSpace;
func LinearOperators c₁,c₂ -> Subset of (ComplexVectSpace the carrier of a₁,a₂) means :Def5: :: CLOPBAN1:def 5
for b₁ being set holds
( b₁ in a₃ iff b₁ is LinearOperator of a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines LinearOperators CLOPBAN1:def 5 :

registration

let c₁, c₂ be ComplexLinearSpace;
cluster LinearOperators a₁,a₂ -> non empty functional ;
coherence

proof end;

end;

theorem Th15: :: CLOPBAN1:15

for b₁, b₂ being ComplexLinearSpace holds LinearOperators b₁,b₂ is lineary-closed

proof end;

theorem Th16: :: CLOPBAN1:16

for b₁, b₂ being ComplexLinearSpace holds CLSStruct(# (LinearOperators b₁,b₂),(Zero_ (LinearOperators b₁,b₂),(ComplexVectSpace the carrier of b₁,b₂)),(Add_ (LinearOperators b₁,b₂),(ComplexVectSpace the carrier of b₁,b₂)),(Mult_ (LinearOperators b₁,b₂),(ComplexVectSpace the carrier of b₁,b₂)) #) is Subspace of ComplexVectSpace the carrier of b₁,b₂

proof end;

registration

let c₁, c₂ be ComplexLinearSpace;
cluster CLSStruct(# (LinearOperators a₁,a₂),(Zero_ (LinearOperators a₁,a₂),(ComplexVectSpace the carrier of a₁,a₂)),(Add_ (LinearOperators a₁,a₂),(ComplexVectSpace the carrier of a₁,a₂)),(Mult_ (LinearOperators a₁,a₂),(ComplexVectSpace the carrier of a₁,a₂)) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence by Th16;

end;

definition

let c₁, c₂ be ComplexLinearSpace;
func C_VectorSpace_of_LinearOperators c₁,c₂ -> ComplexLinearSpace equals :: CLOPBAN1:def 6
CLSStruct(# (LinearOperators a₁,a₂),(Zero_ (LinearOperators a₁,a₂),(ComplexVectSpace the carrier of a₁,a₂)),(Add_ (LinearOperators a₁,a₂),(ComplexVectSpace the carrier of a₁,a₂)),(Mult_ (LinearOperators a₁,a₂),(ComplexVectSpace the carrier of a₁,a₂)) #);
coherence ;

end;

:: deftheorem Def6 defines C_VectorSpace_of_LinearOperators CLOPBAN1:def 6 :

registration

let c₁, c₂ be ComplexLinearSpace;
cluster C_VectorSpace_of_LinearOperators a₁,a₂ -> strict ;
coherence ;

end;

registration

let c₁, c₂ be ComplexLinearSpace;
cluster C_VectorSpace_of_LinearOperators a₁,a₂ -> strict constituted-Functions ;
coherence by MONOID_0:89;

end;

definition

let c₁, c₂ be ComplexLinearSpace;
let c₃ be Element of (C_VectorSpace_of_LinearOperators c₁,c₂);
let c₄ be VECTOR of c₁;
redefine func . as c₃ . c₄ -> VECTOR of a₂;
coherence

proof end;

end;

theorem Th17: :: CLOPBAN1:17

canceled;

theorem Th18: :: CLOPBAN1:18

for b₁, b₂ being ComplexLinearSpace
for b₃, b₄, b₅ being VECTOR of (C_VectorSpace_of_LinearOperators b₁,b₂) holds
( b₅ = b₃ + b₄ iff for b₆ being VECTOR of b₁ holds b₅ . b₆ = (b₃ . b₆) + (b₄ . b₆) )

proof end;

theorem Th19: :: CLOPBAN1:19

for b₁, b₂ being ComplexLinearSpace
for b₃, b₄ being VECTOR of (C_VectorSpace_of_LinearOperators b₁,b₂)
for b₅ being Complex holds
( b₄ = b₅ * b₃ iff for b₆ being VECTOR of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) )

proof end;

theorem Th20: :: CLOPBAN1:20

for b₁, b₂ being ComplexLinearSpace holds 0. (C_VectorSpace_of_LinearOperators b₁,b₂) = the carrier of b₁ --> (0. b₂)

proof end;

theorem Th21: :: CLOPBAN1:21

for b₁, b₂ being ComplexLinearSpace holds the carrier of b₁ --> (0. b₂) is LinearOperator of b₁,b₂

proof end;

theorem Th22: :: CLOPBAN1:22

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

proof end;

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be LinearOperator of c₁,c₂;
attr a₃ is bounded means :Def7: :: CLOPBAN1:def 7
ex b₁ being Real st
( 0 <= b₁ & ( for b₂ being VECTOR of a₁ holds ||.(a₃ . b₂).|| <= b₁ * ||.b₂.|| ) );

end;

:: deftheorem Def7 defines bounded CLOPBAN1:def 7 :

theorem Th23: :: CLOPBAN1:23

for b₁, b₂ being ComplexNormSpace
for b₃ being LinearOperator of b₁,b₂ st ( for b₄ being VECTOR of b₁ holds b₃ . b₄ = 0. b₂ ) holds
b₃ is bounded

proof end;

registration

let c₁, c₂ be ComplexNormSpace;
cluster bounded M4(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

definition

let c₁, c₂ be ComplexNormSpace;
func BoundedLinearOperators c₁,c₂ -> Subset of (C_VectorSpace_of_LinearOperators a₁,a₂) means :Def8: :: CLOPBAN1:def 8
for b₁ being set holds
( b₁ in a₃ iff b₁ is bounded LinearOperator of a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines BoundedLinearOperators CLOPBAN1:def 8 :

registration

let c₁, c₂ be ComplexNormSpace;
cluster BoundedLinearOperators a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th24: :: CLOPBAN1:24

for b₁, b₂ being ComplexNormSpace holds BoundedLinearOperators b₁,b₂ is lineary-closed

proof end;

theorem Th25: :: CLOPBAN1:25

for b₁, b₂ being ComplexNormSpace holds CLSStruct(# (BoundedLinearOperators b₁,b₂),(Zero_ (BoundedLinearOperators b₁,b₂),(C_VectorSpace_of_LinearOperators b₁,b₂)),(Add_ (BoundedLinearOperators b₁,b₂),(C_VectorSpace_of_LinearOperators b₁,b₂)),(Mult_ (BoundedLinearOperators b₁,b₂),(C_VectorSpace_of_LinearOperators b₁,b₂)) #) is Subspace of C_VectorSpace_of_LinearOperators b₁,b₂

proof end;

registration

let c₁, c₂ be ComplexNormSpace;
cluster CLSStruct(# (BoundedLinearOperators a₁,a₂),(Zero_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)),(Add_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)),(Mult_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)) #) -> Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ;
coherence by Th25;

end;

definition

let c₁, c₂ be ComplexNormSpace;
func C_VectorSpace_of_BoundedLinearOperators c₁,c₂ -> ComplexLinearSpace equals :: CLOPBAN1:def 9
CLSStruct(# (BoundedLinearOperators a₁,a₂),(Zero_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)),(Add_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)),(Mult_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)) #);
coherence ;

end;

:: deftheorem Def9 defines C_VectorSpace_of_BoundedLinearOperators CLOPBAN1:def 9 :

registration

let c₁, c₂ be ComplexNormSpace;
cluster C_VectorSpace_of_BoundedLinearOperators a₁,a₂ -> strict ;
coherence ;

end;

registration

let c₁, c₂ be ComplexNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (C_VectorSpace_of_BoundedLinearOperators a₁,a₂);
coherence by Def8;

end;

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be Element of (C_VectorSpace_of_BoundedLinearOperators c₁,c₂);
let c₄ be VECTOR of c₁;
redefine func . as c₃ . c₄ -> VECTOR of a₂;
coherence

proof end;

end;

theorem Th26: :: CLOPBAN1:26

canceled;

theorem Th27: :: CLOPBAN1:27

for b₁, b₂ being ComplexNormSpace
for b₃, b₄, b₅ being VECTOR of (C_VectorSpace_of_BoundedLinearOperators b₁,b₂) holds
( b₅ = b₃ + b₄ iff for b₆ being VECTOR of b₁ holds b₅ . b₆ = (b₃ . b₆) + (b₄ . b₆) )

proof end;

theorem Th28: :: CLOPBAN1:28

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being VECTOR of (C_VectorSpace_of_BoundedLinearOperators b₁,b₂)
for b₅ being Complex holds
( b₄ = b₅ * b₃ iff for b₆ being VECTOR of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) )

proof end;

theorem Th29: :: CLOPBAN1:29

for b₁, b₂ being ComplexNormSpace holds 0. (C_VectorSpace_of_BoundedLinearOperators b₁,b₂) = the carrier of b₁ --> (0. b₂)

proof end;

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be set ;
assume E35: c₃ in BoundedLinearOperators c₁,c₂ ;
func modetrans c₃,c₁,c₂ -> bounded LinearOperator of a₁,a₂ equals :Def10: :: CLOPBAN1:def 10
a₃;
coherence by E35, Def8;

end;

:: deftheorem Def10 defines modetrans CLOPBAN1:def 10 :

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be LinearOperator of c₁,c₂;
func PreNorms c₃ -> non empty Subset of REAL equals :: CLOPBAN1:def 11
{ ||.(a₃ . b₁).|| where B is VECTOR of a₁ : ||.b₁.|| <= 1 } ;
coherence

proof end;

end;

:: deftheorem Def11 defines PreNorms CLOPBAN1:def 11 :

theorem Th30: :: CLOPBAN1:30

for b₁, b₂ being ComplexNormSpace
for b₃ being bounded LinearOperator of b₁,b₂ holds
( not PreNorms b₃ is empty & PreNorms b₃ is bounded_above )

proof end;

theorem Th31: :: CLOPBAN1:31

for b₁, b₂ being ComplexNormSpace
for b₃ being LinearOperator of b₁,b₂ holds
( b₃ is bounded iff PreNorms b₃ is bounded_above )

proof end;

theorem Th32: :: CLOPBAN1:32

for b₁, b₂ being ComplexNormSpace ex b₃ being Function of BoundedLinearOperators b₁,b₂, REAL st
for b₄ being set st b₄ in BoundedLinearOperators b₁,b₂ holds
b₃ . b₄ = sup (PreNorms (modetrans b₄,b₁,b₂))

proof end;

definition

let c₁, c₂ be ComplexNormSpace;
func BoundedLinearOperatorsNorm c₁,c₂ -> Function of BoundedLinearOperators a₁,a₂, REAL means :Def12: :: CLOPBAN1:def 12
for b₁ being set st b₁ in BoundedLinearOperators a₁,a₂ holds
a₃ . b₁ = sup (PreNorms (modetrans b₁,a₁,a₂));
existence by Th32;
uniqueness

proof end;

end;

:: deftheorem Def12 defines BoundedLinearOperatorsNorm CLOPBAN1:def 12 :

theorem Th33: :: CLOPBAN1:33

for b₁, b₂ being ComplexNormSpace
for b₃ being bounded LinearOperator of b₁,b₂ holds modetrans b₃,b₁,b₂ = b₃

proof end;

theorem Th34: :: CLOPBAN1:34

for b₁, b₂ being ComplexNormSpace
for b₃ being bounded LinearOperator of b₁,b₂ holds (BoundedLinearOperatorsNorm b₁,b₂) . b₃ = sup (PreNorms b₃)

proof end;

definition

let c₁, c₂ be ComplexNormSpace;
func C_NormSpace_of_BoundedLinearOperators c₁,c₂ -> non empty CNORMSTR equals :: CLOPBAN1:def 13
CNORMSTR(# (BoundedLinearOperators a₁,a₂),(Zero_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)),(Add_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)),(Mult_ (BoundedLinearOperators a₁,a₂),(C_VectorSpace_of_LinearOperators a₁,a₂)),(BoundedLinearOperatorsNorm a₁,a₂) #);
coherence ;

end;

:: deftheorem Def13 defines C_NormSpace_of_BoundedLinearOperators CLOPBAN1:def 13 :

theorem Th35: :: CLOPBAN1:35

for b₁, b₂ being ComplexNormSpace holds the carrier of b₁ --> (0. b₂) = 0. (C_NormSpace_of_BoundedLinearOperators b₁,b₂)

proof end;

theorem Th36: :: CLOPBAN1:36

for b₁, b₂ being ComplexNormSpace
for b₃ being Point of (C_NormSpace_of_BoundedLinearOperators b₁,b₂)
for b₄ being bounded LinearOperator of b₁,b₂ st b₄ = b₃ holds
for b₅ being VECTOR of b₁ holds ||.(b₄ . b₅).|| <= ||.b₃.|| * ||.b₅.||

proof end;

theorem Th37: :: CLOPBAN1:37

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

proof end;

theorem Th38: :: CLOPBAN1:38

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

proof end;

registration

let c₁, c₂ be ComplexNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (C_NormSpace_of_BoundedLinearOperators a₁,a₂);
coherence by Def8;

end;

definition

let c₁, c₂ be ComplexNormSpace;
let c₃ be Element of (C_NormSpace_of_BoundedLinearOperators c₁,c₂);
let c₄ be VECTOR of c₁;
redefine func . as c₃ . c₄ -> VECTOR of a₂;
coherence

proof end;

end;

theorem Th39: :: CLOPBAN1:39

for b₁, b₂ being ComplexNormSpace
for b₃, b₄, b₅ being Point of (C_NormSpace_of_BoundedLinearOperators b₁,b₂) holds
( b₅ = b₃ + b₄ iff for b₆ being VECTOR of b₁ holds b₅ . b₆ = (b₃ . b₆) + (b₄ . b₆) )

proof end;

theorem Th40: :: CLOPBAN1:40

for b₁, b₂ being ComplexNormSpace
for b₃, b₄ being Point of (C_NormSpace_of_BoundedLinearOperators b₁,b₂)
for b₅ being Complex holds
( b₄ = b₅ * b₃ iff for b₆ being VECTOR of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) )

proof end;

theorem Th41: :: CLOPBAN1:41

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

proof end;

theorem Th42: :: CLOPBAN1:42

for b₁, b₂ being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators b₁,b₂ is ComplexNormSpace-like

proof end;

theorem Th43: :: CLOPBAN1:43

for b₁, b₂ being ComplexNormSpace holds C_NormSpace_of_BoundedLinearOperators b₁,b₂ is ComplexNormSpace

proof end;

registration

let c₁, c₂ be ComplexNormSpace;
cluster C_NormSpace_of_BoundedLinearOperators a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like ;
coherence by Th43;

end;

theorem Th44: :: CLOPBAN1:44

for b₁, b₂ being ComplexNormSpace
for b₃, b₄, b₅ being Point of (C_NormSpace_of_BoundedLinearOperators b₁,b₂) holds
( b₅ = b₃ - b₄ iff for b₆ being VECTOR of b₁ holds b₅ . b₆ = (b₃ . b₆) - (b₄ . b₆) )

proof end;

definition

let c₁ be ComplexNormSpace;
attr a₁ is complete means :Def14: :: CLOPBAN1:def 14
for b₁ being sequence of a₁ st b₁ is CCauchy holds
b₁ is convergent;

end;

:: deftheorem Def14 defines complete CLOPBAN1:def 14 :

registration

cluster complete CNORMSTR ;
existence

proof end;

end;

definition

mode ComplexBanachSpace is complete ComplexNormSpace;

end;

Lemma52: for b₁ being Real
for b₂ being Real_Sequence st b₂ is convergent & ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
b₂ . b₄ <= b₁ holds
lim b₂ <= b₁

proof end;

theorem Th45: :: CLOPBAN1:45

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

proof end;

theorem Th46: :: CLOPBAN1:46

for b₁, b₂ being ComplexNormSpace st b₂ is complete holds
for b₃ being sequence of (C_NormSpace_of_BoundedLinearOperators b₁,b₂) st b₃ is CCauchy holds
b₃ is convergent

proof end;

theorem Th47: :: CLOPBAN1:47

for b₁ being ComplexNormSpace
for b₂ being ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators b₁,b₂ is ComplexBanachSpace

proof end;

registration

let c₁ be ComplexNormSpace;
let c₂ be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedLinearOperators a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like complete ;
coherence by Th47;

end;