:: LOPBAN_1 semantic presentation

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of [:REAL ,c₂:],c₂;
let c₄ be real 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: :: LOPBAN_1:1

for b₁ being non empty set
for b₂ being non empty LoopStr ex b₃ being BinOp of Funcs b₁,the carrier of b₂ st
for b₄, b₅ being Element of Funcs b₁,the carrier of b₂ holds b₃ . b₄,b₅ = the add of b₂ .: b₄,b₅

proof end;

theorem Th2: :: LOPBAN_1:2

for b₁ being non empty set
for b₂ being RealLinearSpace ex b₃ being Function of [:REAL ,(Funcs b₁,the carrier of b₂):], Funcs b₁,the carrier of b₂ st
for b₄ being Real
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 non empty LoopStr ;
func FuncAdd c₁,c₂ -> BinOp of Funcs a₁,the carrier of a₂ means :Def1: :: LOPBAN_1:def 1
for b₁, b₂ being Element of Funcs a₁,the carrier of a₂ holds a₃ . b₁,b₂ = the add of a₂ .: b₁,b₂;
existence by Th1;
uniqueness

proof end;

end;

:: deftheorem Def1 defines FuncAdd LOPBAN_1:def 1 :

definition

let c₁ be non empty set ;
let c₂ be RealLinearSpace;
func FuncExtMult c₁,c₂ -> Function of [:REAL ,(Funcs a₁,the carrier of a₂):], Funcs a₁,the carrier of a₂ means :Def2: :: LOPBAN_1:def 2
for b₁ being Real
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 Th2;
uniqueness

proof end;

end;

:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def 2 :

definition

let c₁ be set ;
let c₂ be non empty ZeroStr ;
func FuncZero c₁,c₂ -> Element of Funcs a₁,the carrier of a₂ equals :: LOPBAN_1:def 3
a₁ --> (0. a₂);
coherence

proof end;

end;

:: deftheorem Def3 defines FuncZero LOPBAN_1:def 3 :

Lemma5: for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Function of b₁,b₂ holds b₃ in dom b₄

proof end;

theorem Th3: :: LOPBAN_1:3

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

proof end;

theorem Th4: :: LOPBAN_1:4

for b₁ being non empty set
for b₂ being RealLinearSpace
for b₃ being Element of b₁ holds (FuncZero b₁,b₂) . b₃ = 0. b₂ by FUNCOP_1:13;

theorem Th5: :: LOPBAN_1:5

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

proof end;

theorem Th6: :: LOPBAN_1:6

for b₁ being non empty set
for b₂ being RealLinearSpace
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 Th7: :: LOPBAN_1:7

for b₁ being non empty set
for b₂ being RealLinearSpace
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 Th8: :: LOPBAN_1:8

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

proof end;

theorem Th9: :: LOPBAN_1:9

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

proof end;

theorem Th10: :: LOPBAN_1:10

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

proof end;

theorem Th11: :: LOPBAN_1:11

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

proof end;

theorem Th12: :: LOPBAN_1:12

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

proof end;

Lemma16: for b₁ being non empty set
for b₂ being RealLinearSpace
for b₃, b₄ being Element of Funcs b₁,the carrier of b₂
for b₅ being Real 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 Th13: :: LOPBAN_1:13

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be RealLinearSpace;
func RealVectSpace c₁,c₂ -> RealLinearSpace equals :: LOPBAN_1:def 4
RLSStruct(# (Funcs a₁,the carrier of a₂),(FuncZero a₁,a₂),(FuncAdd a₁,a₂),(FuncExtMult a₁,a₂) #);
coherence by Th13;

end;

:: deftheorem Def4 defines RealVectSpace LOPBAN_1:def 4 :

registration

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

end;

registration

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

end;

definition

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

proof end;

end;

theorem Th14: :: LOPBAN_1:14

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

proof end;

theorem Th15: :: LOPBAN_1:15

for b₁ being non empty set
for b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of (RealVectSpace b₁,b₂)
for b₅ being Real holds
( b₄ = b₅ * b₃ iff for b₆ being Element of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) ) by Th5;

theorem Th16: :: LOPBAN_1:16

for b₁ being non empty set
for b₂ being RealLinearSpace holds 0. (RealVectSpace b₁,b₂) = b₁ --> (0. b₂) ;

definition

let c₁ be non empty RLSStruct ;
let c₂ be non empty LoopStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is additive means :Def5: :: LOPBAN_1:def 5
for b₁, b₂ being VECTOR of a₁ holds a₃ . (b₁ + b₂) = (a₃ . b₁) + (a₃ . b₂);

end;

:: deftheorem Def5 defines additive LOPBAN_1:def 5 :

definition

let c₁, c₂ be non empty RLSStruct ;
let c₃ be Function of c₁,c₂;
attr a₃ is homogeneous means :Def6: :: LOPBAN_1:def 6
for b₁ being VECTOR of a₁
for b₂ being Real holds a₃ . (b₂ * b₁) = b₂ * (a₃ . b₁);

end;

:: deftheorem Def6 defines homogeneous LOPBAN_1:def 6 :

registration

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

proof end;

end;

definition

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

end;

definition

let c₁, c₂ be RealLinearSpace;
func LinearOperators c₁,c₂ -> Subset of (RealVectSpace the carrier of a₁,a₂) means :Def7: :: LOPBAN_1:def 7
for b₁ being set holds
( b₁ in a₃ iff b₁ is LinearOperator of a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines LinearOperators LOPBAN_1:def 7 :

registration

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

proof end;

end;

theorem Th17: :: LOPBAN_1:17

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

proof end;

theorem Th18: :: LOPBAN_1:18

for b₁, b₂ being RealLinearSpace holds RLSStruct(# (LinearOperators b₁,b₂),(Zero_ (LinearOperators b₁,b₂),(RealVectSpace the carrier of b₁,b₂)),(Add_ (LinearOperators b₁,b₂),(RealVectSpace the carrier of b₁,b₂)),(Mult_ (LinearOperators b₁,b₂),(RealVectSpace the carrier of b₁,b₂)) #) is Subspace of RealVectSpace the carrier of b₁,b₂

proof end;

registration

let c₁, c₂ be RealLinearSpace;
cluster RLSStruct(# (LinearOperators a₁,a₂),(Zero_ (LinearOperators a₁,a₂),(RealVectSpace the carrier of a₁,a₂)),(Add_ (LinearOperators a₁,a₂),(RealVectSpace the carrier of a₁,a₂)),(Mult_ (LinearOperators a₁,a₂),(RealVectSpace the carrier of a₁,a₂)) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence by Th18;

end;

definition

let c₁, c₂ be RealLinearSpace;
func R_VectorSpace_of_LinearOperators c₁,c₂ -> RealLinearSpace equals :: LOPBAN_1:def 8
RLSStruct(# (LinearOperators a₁,a₂),(Zero_ (LinearOperators a₁,a₂),(RealVectSpace the carrier of a₁,a₂)),(Add_ (LinearOperators a₁,a₂),(RealVectSpace the carrier of a₁,a₂)),(Mult_ (LinearOperators a₁,a₂),(RealVectSpace the carrier of a₁,a₂)) #);
coherence ;

end;

:: deftheorem Def8 defines R_VectorSpace_of_LinearOperators LOPBAN_1:def 8 :

registration

let c₁, c₂ be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators a₁,a₂ -> strict ;
coherence ;

end;

registration

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

end;

definition

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

proof end;

end;

theorem Th19: :: LOPBAN_1:19

canceled;

theorem Th20: :: LOPBAN_1:20

for b₁, b₂ being RealLinearSpace
for b₃, b₄, b₅ being VECTOR of (R_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 Th21: :: LOPBAN_1:21

for b₁, b₂ being RealLinearSpace
for b₃, b₄ being VECTOR of (R_VectorSpace_of_LinearOperators b₁,b₂)
for b₅ being Real holds
( b₄ = b₅ * b₃ iff for b₆ being VECTOR of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) )

proof end;

theorem Th22: :: LOPBAN_1:22

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

proof end;

theorem Th23: :: LOPBAN_1:23

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

proof end;

theorem Th24: :: LOPBAN_1:24

for b₁ being RealNormSpace
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 RealNormSpace;
let c₃ be LinearOperator of c₁,c₂;
attr a₃ is bounded means :Def9: :: LOPBAN_1:def 9
ex b₁ being Real st
( 0 <= b₁ & ( for b₂ being VECTOR of a₁ holds ||.(a₃ . b₂).|| <= b₁ * ||.b₂.|| ) );

end;

:: deftheorem Def9 defines bounded LOPBAN_1:def 9 :

theorem Th25: :: LOPBAN_1:25

for b₁, b₂ being RealNormSpace
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 RealNormSpace;
cluster bounded M4(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

definition

let c₁, c₂ be RealNormSpace;
func BoundedLinearOperators c₁,c₂ -> Subset of (R_VectorSpace_of_LinearOperators a₁,a₂) means :Def10: :: LOPBAN_1:def 10
for b₁ being set holds
( b₁ in a₃ iff b₁ is bounded LinearOperator of a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines BoundedLinearOperators LOPBAN_1:def 10 :

registration

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

proof end;

end;

theorem Th26: :: LOPBAN_1:26

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

proof end;

theorem Th27: :: LOPBAN_1:27

for b₁, b₂ being RealNormSpace holds RLSStruct(# (BoundedLinearOperators b₁,b₂),(Zero_ (BoundedLinearOperators b₁,b₂),(R_VectorSpace_of_LinearOperators b₁,b₂)),(Add_ (BoundedLinearOperators b₁,b₂),(R_VectorSpace_of_LinearOperators b₁,b₂)),(Mult_ (BoundedLinearOperators b₁,b₂),(R_VectorSpace_of_LinearOperators b₁,b₂)) #) is Subspace of R_VectorSpace_of_LinearOperators b₁,b₂

proof end;

registration

let c₁, c₂ be RealNormSpace;
cluster RLSStruct(# (BoundedLinearOperators a₁,a₂),(Zero_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)),(Add_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)),(Mult_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence by Th27;

end;

definition

let c₁, c₂ be RealNormSpace;
func R_VectorSpace_of_BoundedLinearOperators c₁,c₂ -> RealLinearSpace equals :: LOPBAN_1:def 11
RLSStruct(# (BoundedLinearOperators a₁,a₂),(Zero_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)),(Add_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)),(Mult_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)) #);
coherence ;

end;

:: deftheorem Def11 defines R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def 11 :

registration

let c₁, c₂ be RealNormSpace;
cluster R_VectorSpace_of_BoundedLinearOperators a₁,a₂ -> strict ;
coherence ;

end;

registration

let c₁, c₂ be RealNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (R_VectorSpace_of_BoundedLinearOperators a₁,a₂);
coherence by Def10;

end;

definition

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

proof end;

end;

theorem Th28: :: LOPBAN_1:28

canceled;

theorem Th29: :: LOPBAN_1:29

for b₁, b₂ being RealNormSpace
for b₃, b₄, b₅ being VECTOR of (R_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 Th30: :: LOPBAN_1:30

for b₁, b₂ being RealNormSpace
for b₃, b₄ being VECTOR of (R_VectorSpace_of_BoundedLinearOperators b₁,b₂)
for b₅ being Real holds
( b₄ = b₅ * b₃ iff for b₆ being VECTOR of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) )

proof end;

theorem Th31: :: LOPBAN_1:31

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

proof end;

definition

let c₁, c₂ be RealNormSpace;
let c₃ be set ;
assume E38: c₃ in BoundedLinearOperators c₁,c₂ ;
func modetrans c₃,c₁,c₂ -> bounded LinearOperator of a₁,a₂ equals :Def12: :: LOPBAN_1:def 12
a₃;
coherence by E38, Def10;

end;

:: deftheorem Def12 defines modetrans LOPBAN_1:def 12 :

definition

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

proof end;

end;

:: deftheorem Def13 defines PreNorms LOPBAN_1:def 13 :

theorem Th32: :: LOPBAN_1:32

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

proof end;

theorem Th33: :: LOPBAN_1:33

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

proof end;

theorem Th34: :: LOPBAN_1:34

for b₁, b₂ being RealNormSpace 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 RealNormSpace;
func BoundedLinearOperatorsNorm c₁,c₂ -> Function of BoundedLinearOperators a₁,a₂, REAL means :Def14: :: LOPBAN_1:def 14
for b₁ being set st b₁ in BoundedLinearOperators a₁,a₂ holds
a₃ . b₁ = sup (PreNorms (modetrans b₁,a₁,a₂));
existence by Th34;
uniqueness

proof end;

end;

:: deftheorem Def14 defines BoundedLinearOperatorsNorm LOPBAN_1:def 14 :

theorem Th35: :: LOPBAN_1:35

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

proof end;

theorem Th36: :: LOPBAN_1:36

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

proof end;

definition

let c₁, c₂ be RealNormSpace;
func R_NormSpace_of_BoundedLinearOperators c₁,c₂ -> non empty NORMSTR equals :: LOPBAN_1:def 15
NORMSTR(# (BoundedLinearOperators a₁,a₂),(Zero_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)),(Add_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)),(Mult_ (BoundedLinearOperators a₁,a₂),(R_VectorSpace_of_LinearOperators a₁,a₂)),(BoundedLinearOperatorsNorm a₁,a₂) #);
coherence ;

end;

:: deftheorem Def15 defines R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def 15 :

theorem Th37: :: LOPBAN_1:37

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

proof end;

theorem Th38: :: LOPBAN_1:38

for b₁, b₂ being RealNormSpace
for b₃ being Point of (R_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 Th39: :: LOPBAN_1:39

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

proof end;

theorem Th40: :: LOPBAN_1:40

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

proof end;

registration

let c₁, c₂ be RealNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators a₁,a₂);
coherence by Def10;

end;

definition

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

proof end;

end;

theorem Th41: :: LOPBAN_1:41

for b₁, b₂ being RealNormSpace
for b₃, b₄, b₅ being Point of (R_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 Th42: :: LOPBAN_1:42

for b₁, b₂ being RealNormSpace
for b₃, b₄ being Point of (R_NormSpace_of_BoundedLinearOperators b₁,b₂)
for b₅ being Real holds
( b₄ = b₅ * b₃ iff for b₆ being VECTOR of b₁ holds b₄ . b₆ = b₅ * (b₃ . b₆) )

proof end;

theorem Th43: :: LOPBAN_1:43

for b₁, b₂ being RealNormSpace
for b₃, b₄ being Point of (R_NormSpace_of_BoundedLinearOperators b₁,b₂)
for b₅ being Real holds
( ( ||.b₃.|| = 0 implies b₃ = 0. (R_NormSpace_of_BoundedLinearOperators b₁,b₂) ) & ( b₃ = 0. (R_NormSpace_of_BoundedLinearOperators b₁,b₂) implies ||.b₃.|| = 0 ) & ||.(b₅ * b₃).|| = (abs b₅) * ||.b₃.|| & ||.(b₃ + b₄).|| <= ||.b₃.|| + ||.b₄.|| )

proof end;

theorem Th44: :: LOPBAN_1:44

for b₁, b₂ being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators b₁,b₂ is RealNormSpace-like

proof end;

theorem Th45: :: LOPBAN_1:45

for b₁, b₂ being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators b₁,b₂ is RealNormSpace

proof end;

registration

let c₁, c₂ be RealNormSpace;
cluster R_NormSpace_of_BoundedLinearOperators a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealNormSpace-like ;
coherence by Th45;

end;

theorem Th46: :: LOPBAN_1:46

for b₁, b₂ being RealNormSpace
for b₃, b₄, b₅ being Point of (R_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 RealNormSpace;
attr a₁ is complete means :Def16: :: LOPBAN_1:def 16
for b₁ being sequence of a₁ st b₁ is CCauchy holds
b₁ is convergent;

end;

:: deftheorem Def16 defines complete LOPBAN_1:def 16 :

registration

cluster complete NORMSTR ;
existence

proof end;

end;

definition

mode RealBanachSpace is complete RealNormSpace;

end;

Lemma55: 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 Th47: :: LOPBAN_1:47

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

proof end;

theorem Th48: :: LOPBAN_1:48

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

proof end;

theorem Th49: :: LOPBAN_1:49

for b₁ being RealNormSpace
for b₂ being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators b₁,b₂ is RealBanachSpace

proof end;

registration

let c₁ be RealNormSpace;
let c₂ be RealBanachSpace;
cluster R_NormSpace_of_BoundedLinearOperators a₁,a₂ -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealNormSpace-like complete ;
coherence by Th49;

end;