:: Banach Space of Bounded Linear Operators
:: by Yasunari Shidama
::
:: Received December 22, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users


begin

definition
let X be set ;
let Y be non empty set ;
let F be Function of [:REAL,Y:],Y;
let a be real number ;
let f be Function of X,Y;
:: original: [;]
redefine func F [;] (a,f) -> Element of Funcs (X,Y);
coherence
F [;] (a,f) is Element of Funcs (X,Y)
proof end;
end;

theorem Th1: :: LOPBAN_1:1
for X being non empty set
for Y being non empty addLoopStr ex ADD being BinOp of (Funcs (X, the carrier of Y)) st
for f, g being Element of Funcs (X, the carrier of Y) holds ADD . (f,g) = the addF of Y .: (f,g)
proof end;

theorem Th2: :: LOPBAN_1:2
for X being non empty set
for Y being RealLinearSpace ex MULT being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for r being Real
for f being Element of Funcs (X, the carrier of Y)
for s being Element of X holds (MULT . [r,f]) . s = r * (f . s)
proof end;

definition
let X be non empty set ;
let Y be non empty addLoopStr ;
func FuncAdd (X,Y) -> BinOp of (Funcs (X, the carrier of Y)) means :Def1: :: LOPBAN_1:def 1
for f, g being Element of Funcs (X, the carrier of Y) holds it . (f,g) = the addF of Y .: (f,g);
existence
ex b1 being BinOp of (Funcs (X, the carrier of Y)) st
for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g)
by Th1;
uniqueness
for b1, b2 being BinOp of (Funcs (X, the carrier of Y)) st ( for f, g being Element of Funcs (X, the carrier of Y) holds b1 . (f,g) = the addF of Y .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of Y) holds b2 . (f,g) = the addF of Y .: (f,g) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines FuncAdd LOPBAN_1:def 1 :
for X being non empty set
for Y being non empty addLoopStr
for b3 being BinOp of (Funcs (X, the carrier of Y)) holds
( b3 = FuncAdd (X,Y) iff for f, g being Element of Funcs (X, the carrier of Y) holds b3 . (f,g) = the addF of Y .: (f,g) );

definition
let X be non empty set ;
let Y be RealLinearSpace;
func FuncExtMult (X,Y) -> Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) means :Def2: :: LOPBAN_1:def 2
for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (it . [a,f]) . x = a * (f . x);
existence
ex b1 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st
for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x)
by Th2;
uniqueness
for b1, b2 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b1 . [a,f]) . x = a * (f . x) ) & ( for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b2 . [a,f]) . x = a * (f . x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def 2 :
for X being non empty set
for Y being RealLinearSpace
for b3 being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) holds
( b3 = FuncExtMult (X,Y) iff for a being Real
for f being Element of Funcs (X, the carrier of Y)
for x being Element of X holds (b3 . [a,f]) . x = a * (f . x) );

definition
let X be set ;
let Y be non empty ZeroStr ;
func FuncZero (X,Y) -> Element of Funcs (X, the carrier of Y) equals :: LOPBAN_1:def 3
X --> (0. Y);
coherence
X --> (0. Y) is Element of Funcs (X, the carrier of Y)
by FUNCT_2:11;
end;

:: deftheorem defines FuncZero LOPBAN_1:def 3 :
for X being set
for Y being non empty ZeroStr holds FuncZero (X,Y) = X --> (0. Y);

Lm1: for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f
proof end;

theorem Th3: :: LOPBAN_1:3
for X being non empty set
for Y being non empty addLoopStr
for f, g, h being Element of Funcs (X, the carrier of Y) holds
( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )
proof end;

theorem :: LOPBAN_1:4
canceled;

theorem Th5: :: LOPBAN_1:5
for X being non empty set
for Y being RealLinearSpace
for h, f being Element of Funcs (X, the carrier of Y)
for a being Real holds
( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )
proof end;

theorem Th6: :: LOPBAN_1:6
for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)
proof end;

theorem Th7: :: LOPBAN_1:7
for X being non empty set
for Y being RealLinearSpace
for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)
proof end;

theorem Th8: :: LOPBAN_1:8
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f
proof end;

theorem Th9: :: LOPBAN_1:9
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)
proof end;

theorem Th10: :: LOPBAN_1:10
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1,f] = f
proof end;

theorem Th11: :: LOPBAN_1:11
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]
proof end;

theorem Th12: :: LOPBAN_1:12
for X being non empty set
for Y being RealLinearSpace
for f being Element of Funcs (X, the carrier of Y)
for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]
proof end;

Lm2: for X being non empty set
for Y being RealLinearSpace
for f, g being Element of Funcs (X, the carrier of Y)
for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]
proof end;

theorem Th13: :: LOPBAN_1:13
for X being non empty set
for Y being RealLinearSpace holds RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace
proof end;

definition
let X be non empty set ;
let Y be RealLinearSpace;
func RealVectSpace (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 4
RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);
coherence
RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace
by Th13;
end;

:: deftheorem defines RealVectSpace LOPBAN_1:def 4 :
for X being non empty set
for Y being RealLinearSpace holds RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);

registration
let X be non empty set ;
let Y be RealLinearSpace;
cluster RealVectSpace (X,Y) -> strict ;
coherence
RealVectSpace (X,Y) is strict
;
end;

registration
let X be non empty set ;
let Y be RealLinearSpace;
cluster RealVectSpace (X,Y) -> constituted-Functions ;
coherence
RealVectSpace (X,Y) is constituted-Functions
by MONOID_0:89;
end;

definition
let X be non empty set ;
let Y be RealLinearSpace;
let f be VECTOR of (RealVectSpace (X,Y));
let x be Element of X;
:: original: .
redefine func f . x -> VECTOR of Y;
coherence
f . x is VECTOR of Y
proof end;
end;

theorem :: LOPBAN_1:14
for X being non empty set
for Y being RealLinearSpace
for f, g, h being VECTOR of (RealVectSpace (X,Y)) holds
( h = f + g iff for x being Element of X holds h . x = (f . x) + (g . x) ) by Th3;

theorem :: LOPBAN_1:15
for X being non empty set
for Y being RealLinearSpace
for f, h being VECTOR of (RealVectSpace (X,Y))
for a being Real holds
( h = a * f iff for x being Element of X holds h . x = a * (f . x) ) by Th5;

theorem :: LOPBAN_1:16
for X being non empty set
for Y being RealLinearSpace holds 0. (RealVectSpace (X,Y)) = X --> (0. Y) ;

begin

definition
let X, Y be non empty RLSStruct ;
let IT be Function of X,Y;
canceled;
attr IT is homogeneous means :Def6: :: LOPBAN_1:def 6
for x being VECTOR of X
for r being Real holds IT . (r * x) = r * (IT . x);
end;

:: deftheorem LOPBAN_1:def 5 :
canceled;

:: deftheorem Def6 defines homogeneous LOPBAN_1:def 6 :
for X, Y being non empty RLSStruct
for IT being Function of X,Y holds
( IT is homogeneous iff for x being VECTOR of X
for r being Real holds IT . (r * x) = r * (IT . x) );

registration
let X be non empty RLSStruct ;
let Y be RealLinearSpace;
cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous Element of bool [: the carrier of X, the carrier of Y:];
existence
ex b1 being Function of X,Y st
( b1 is additive & b1 is homogeneous )
proof end;
end;

definition
let X, Y be RealLinearSpace;
mode LinearOperator of X,Y is additive homogeneous Function of X,Y;
end;

definition
let X, Y be RealLinearSpace;
func LinearOperators (X,Y) -> Subset of (RealVectSpace ( the carrier of X,Y)) means :Def7: :: LOPBAN_1:def 7
for x being set holds
( x in it iff x is LinearOperator of X,Y );
existence
ex b1 being Subset of (RealVectSpace ( the carrier of X,Y)) st
for x being set holds
( x in b1 iff x is LinearOperator of X,Y )
proof end;
uniqueness
for b1, b2 being Subset of (RealVectSpace ( the carrier of X,Y)) st ( for x being set holds
( x in b1 iff x is LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is LinearOperator of X,Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines LinearOperators LOPBAN_1:def 7 :
for X, Y being RealLinearSpace
for b3 being Subset of (RealVectSpace ( the carrier of X,Y)) holds
( b3 = LinearOperators (X,Y) iff for x being set holds
( x in b3 iff x is LinearOperator of X,Y ) );

registration
let X, Y be RealLinearSpace;
cluster LinearOperators (X,Y) -> non empty functional ;
coherence
( not LinearOperators (X,Y) is empty & LinearOperators (X,Y) is functional )
proof end;
end;

theorem Th17: :: LOPBAN_1:17
for X, Y being RealLinearSpace holds LinearOperators (X,Y) is linearly-closed
proof end;

theorem :: LOPBAN_1:18
for X, Y being RealLinearSpace holds RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Subspace of RealVectSpace ( the carrier of X,Y) by Th17, RSSPACE:13;

registration
let X, Y be RealLinearSpace;
cluster RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Abelian & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is add-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_zeroed & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_complementable & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is vector-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-unital )
by Th17, RSSPACE:13;
end;

definition
let X, Y be RealLinearSpace;
func R_VectorSpace_of_LinearOperators (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 8
RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);
coherence
RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is RealLinearSpace
;
end;

:: deftheorem defines R_VectorSpace_of_LinearOperators LOPBAN_1:def 8 :
for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators (X,Y) = RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);

registration
let X, Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators (X,Y) -> strict ;
coherence
R_VectorSpace_of_LinearOperators (X,Y) is strict
;
end;

registration
let X, Y be RealLinearSpace;
cluster R_VectorSpace_of_LinearOperators (X,Y) -> constituted-Functions ;
coherence
R_VectorSpace_of_LinearOperators (X,Y) is constituted-Functions
by MONOID_0:89;
end;

definition
let X, Y be RealLinearSpace;
let f be Element of (R_VectorSpace_of_LinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y
proof end;
end;

theorem :: LOPBAN_1:19
canceled;

theorem Th20: :: LOPBAN_1:20
for X, Y being RealLinearSpace
for f, g, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th21: :: LOPBAN_1:21
for X, Y being RealLinearSpace
for f, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof end;

theorem Th22: :: LOPBAN_1:22
for X, Y being RealLinearSpace holds 0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)
proof end;

theorem Th23: :: LOPBAN_1:23
for X, Y being RealLinearSpace holds the carrier of X --> (0. Y) is LinearOperator of X,Y
proof end;

begin

theorem Th24: :: LOPBAN_1:24
for X being RealNormSpace
for seq being sequence of X
for g being Point of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
proof end;

definition
let X, Y be RealNormSpace;
let IT be LinearOperator of X,Y;
attr IT is bounded means :Def9: :: LOPBAN_1:def 9
ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) );
end;

:: deftheorem Def9 defines bounded LOPBAN_1:def 9 :
for X, Y being RealNormSpace
for IT being LinearOperator of X,Y holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) ) );

theorem Th25: :: LOPBAN_1:25
for X, Y being RealNormSpace
for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds
f is bounded
proof end;

registration
let X, Y be RealNormSpace;
cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous bounded Element of bool [: the carrier of X, the carrier of Y:];
existence
ex b1 being LinearOperator of X,Y st b1 is bounded
proof end;
end;

definition
let X, Y be RealNormSpace;
func BoundedLinearOperators (X,Y) -> Subset of (R_VectorSpace_of_LinearOperators (X,Y)) means :Def10: :: LOPBAN_1:def 10
for x being set holds
( x in it iff x is bounded LinearOperator of X,Y );
existence
ex b1 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st
for x being set holds
( x in b1 iff x is bounded LinearOperator of X,Y )
proof end;
uniqueness
for b1, b2 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st ( for x being set holds
( x in b1 iff x is bounded LinearOperator of X,Y ) ) & ( for x being set holds
( x in b2 iff x is bounded LinearOperator of X,Y ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines BoundedLinearOperators LOPBAN_1:def 10 :
for X, Y being RealNormSpace
for b3 being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) holds
( b3 = BoundedLinearOperators (X,Y) iff for x being set holds
( x in b3 iff x is bounded LinearOperator of X,Y ) );

registration
let X, Y be RealNormSpace;
cluster BoundedLinearOperators (X,Y) -> non empty ;
coherence
not BoundedLinearOperators (X,Y) is empty
proof end;
end;

theorem Th26: :: LOPBAN_1:26
for X, Y being RealNormSpace holds BoundedLinearOperators (X,Y) is linearly-closed
proof end;

theorem :: LOPBAN_1:27
for X, Y being RealNormSpace holds RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Subspace of R_VectorSpace_of_LinearOperators (X,Y) by Th26, RSSPACE:13;

registration
let X, Y be RealNormSpace;
cluster RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital )
by Th26, RSSPACE:13;
end;

definition
let X, Y be RealNormSpace;
func R_VectorSpace_of_BoundedLinearOperators (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 11
RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);
coherence
RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace
;
end;

:: deftheorem defines R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def 11 :
for X, Y being RealNormSpace holds R_VectorSpace_of_BoundedLinearOperators (X,Y) = RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);

registration
let X, Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedLinearOperators (X,Y) -> strict ;
coherence
R_VectorSpace_of_BoundedLinearOperators (X,Y) is strict
;
end;

registration
let X, Y be RealNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (R_VectorSpace_of_BoundedLinearOperators (X,Y));
coherence
for b1 being Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds
( b1 is Function-like & b1 is Relation-like )
;
end;

definition
let X, Y be RealNormSpace;
let f be Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y
proof end;
end;

theorem :: LOPBAN_1:28
canceled;

theorem Th29: :: LOPBAN_1:29
for X, Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th30: :: LOPBAN_1:30
for X, Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof end;

theorem Th31: :: LOPBAN_1:31
for X, Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y)
proof end;

definition
let X, Y be RealNormSpace;
let f be set ;
assume A1: f in BoundedLinearOperators (X,Y) ;
func modetrans (f,X,Y) -> bounded LinearOperator of X,Y equals :Def12: :: LOPBAN_1:def 12
f;
coherence
f is bounded LinearOperator of X,Y
by A1, Def10;
end;

:: deftheorem Def12 defines modetrans LOPBAN_1:def 12 :
for X, Y being RealNormSpace
for f being set st f in BoundedLinearOperators (X,Y) holds
modetrans (f,X,Y) = f;

definition
let X, Y be RealNormSpace;
let u be LinearOperator of X,Y;
func PreNorms u -> non empty Subset of REAL equals :: LOPBAN_1:def 13
{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;
coherence
{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL
proof end;
end;

:: deftheorem defines PreNorms LOPBAN_1:def 13 :
for X, Y being RealNormSpace
for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;

theorem Th32: :: LOPBAN_1:32
for X, Y being RealNormSpace
for g being bounded LinearOperator of X,Y holds PreNorms g is bounded_above
proof end;

theorem :: LOPBAN_1:33
for X, Y being RealNormSpace
for g being LinearOperator of X,Y holds
( g is bounded iff PreNorms g is bounded_above )
proof end;

theorem Th34: :: LOPBAN_1:34
for X, Y being RealNormSpace ex NORM being Function of (BoundedLinearOperators (X,Y)),REAL st
for f being set st f in BoundedLinearOperators (X,Y) holds
NORM . f = upper_bound (PreNorms (modetrans (f,X,Y)))
proof end;

definition
let X, Y be RealNormSpace;
func BoundedLinearOperatorsNorm (X,Y) -> Function of (BoundedLinearOperators (X,Y)),REAL means :Def14: :: LOPBAN_1:def 14
for x being set st x in BoundedLinearOperators (X,Y) holds
it . x = upper_bound (PreNorms (modetrans (x,X,Y)));
existence
ex b1 being Function of (BoundedLinearOperators (X,Y)),REAL st
for x being set st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
by Th34;
uniqueness
for b1, b2 being Function of (BoundedLinearOperators (X,Y)),REAL st ( for x being set st x in BoundedLinearOperators (X,Y) holds
b1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedLinearOperators (X,Y) holds
b2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines BoundedLinearOperatorsNorm LOPBAN_1:def 14 :
for X, Y being RealNormSpace
for b3 being Function of (BoundedLinearOperators (X,Y)),REAL holds
( b3 = BoundedLinearOperatorsNorm (X,Y) iff for x being set st x in BoundedLinearOperators (X,Y) holds
b3 . x = upper_bound (PreNorms (modetrans (x,X,Y))) );

theorem Th35: :: LOPBAN_1:35
for X, Y being RealNormSpace
for f being bounded LinearOperator of X,Y holds modetrans (f,X,Y) = f
proof end;

theorem Th36: :: LOPBAN_1:36
for X, Y being RealNormSpace
for f being bounded LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)
proof end;

definition
let X, Y be RealNormSpace;
func R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty NORMSTR equals :: LOPBAN_1:def 15
NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);
coherence
NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty NORMSTR
;
end;

:: deftheorem defines R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def 15 :
for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) = NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);

theorem Th37: :: LOPBAN_1:37
for X, Y being RealNormSpace holds the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y))
proof end;

theorem Th38: :: LOPBAN_1:38
for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g being bounded LinearOperator of X,Y st g = f holds
for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||
proof end;

theorem Th39: :: LOPBAN_1:39
for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||
proof end;

theorem Th40: :: LOPBAN_1:40
for X, Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
0 = ||.f.||
proof end;

registration
let X, Y be RealNormSpace;
cluster -> Relation-like Function-like Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y));
coherence
for b1 being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( b1 is Function-like & b1 is Relation-like )
;
end;

definition
let X, Y be RealNormSpace;
let f be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y));
let v be VECTOR of X;
:: original: .
redefine func f . v -> VECTOR of Y;
coherence
f . v is VECTOR of Y
proof end;
end;

theorem Th41: :: LOPBAN_1:41
for X, Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th42: :: LOPBAN_1:42
for X, Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof end;

theorem Th43: :: LOPBAN_1:43
for X, Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
proof end;

theorem Th44: :: LOPBAN_1:44
for X, Y being RealNormSpace holds
( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like )
proof end;

theorem Th45: :: LOPBAN_1:45
for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace
proof end;

registration
let X, Y be RealNormSpace;
cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators (X,Y) is vector-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-unital & R_NormSpace_of_BoundedLinearOperators (X,Y) is Abelian & R_NormSpace_of_BoundedLinearOperators (X,Y) is add-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_zeroed & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_complementable )
by Th45;
end;

theorem Th46: :: LOPBAN_1:46
for X, Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds
( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
proof end;

begin

definition
let X be RealNormSpace;
attr X is complete means :Def16: :: LOPBAN_1:def 16
for seq being sequence of X st seq is CCauchy holds
seq is convergent ;
end;

:: deftheorem Def16 defines complete LOPBAN_1:def 16 :
for X being RealNormSpace holds
( X is complete iff for seq being sequence of X st seq is CCauchy holds
seq is convergent );

registration
cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V97() discerning reflexive RealNormSpace-like complete NORMSTR ;
existence
ex b1 being RealNormSpace st b1 is complete
proof end;
end;

definition
mode RealBanachSpace is complete RealNormSpace;
end;

Lm3: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
proof end;

theorem Th47: :: LOPBAN_1:47
for X being RealNormSpace
for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )
proof end;

theorem Th48: :: LOPBAN_1:48
for X, Y being RealNormSpace st Y is complete holds
for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is CCauchy holds
seq is convergent
proof end;

theorem Th49: :: LOPBAN_1:49
for X being RealNormSpace
for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace
proof end;

registration
let X be RealNormSpace;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty complete ;
coherence
R_NormSpace_of_BoundedLinearOperators (X,Y) is complete
by Th49;
end;