:: The {B}anach Algebra of Bounded Linear Operators
:: by Yasunari Shidama
::
:: Received January 26, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: LOPBAN_2:1
for X, Y, Z being RealLinearSpace
for f being LinearOperator of X,Y
for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
proofend;

theorem Th2: :: LOPBAN_2:2
for X, Y, Z being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y
for g being Lipschitzian LinearOperator of Y,Z holds
( g * f is Lipschitzian LinearOperator of X,Z & ( for x being VECTOR of X holds
( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f)) * ||.x.|| &amp; (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) )
proofend;

definition
let X be RealNormSpace;
let f, g be Lipschitzian LinearOperator of X,X;
:: original:*
redefine funcg * f ->  Lipschitzian LinearOperator of X,X;
correctness
coherence
g * f is Lipschitzian LinearOperator of X,X;
by Th2;
end;

definition
let X be RealNormSpace;
let f, g be Element of BoundedLinearOperators (X,X);
funcf + g ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 1
(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g);
correctness
coherence
(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g) is Element of BoundedLinearOperators (X,X);
;
end;

:: deftheorem  defines + LOPBAN_2:def_1_:_
 for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X) holds f + g = (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g);

definition
let X be RealNormSpace;
let f, g be Element of BoundedLinearOperators (X,X);
funcg * f ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 2
(modetrans (g,X,X)) * (modetrans (f,X,X));
correctness
coherence
(modetrans (g,X,X)) * (modetrans (f,X,X)) is Element of BoundedLinearOperators (X,X);
by LOPBAN_1:def_9;
end;

:: deftheorem  defines * LOPBAN_2:def_2_:_
 for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X) holds g * f = (modetrans (g,X,X)) * (modetrans (f,X,X));

definition
let X be RealNormSpace;
let f be Element of BoundedLinearOperators (X,X);
let a be Real;
funca * f ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 3
(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f);
correctness
coherence
(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f) is Element of BoundedLinearOperators (X,X);
;
end;

:: deftheorem  defines * LOPBAN_2:def_3_:_
 for X being RealNormSpace
for f being Element of BoundedLinearOperators (X,X)
for a being Real holds a * f = (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f);

definition
let X be RealNormSpace;
func FuncMult X ->  BinOp of (BoundedLinearOperators (X,X)) means :Def4: :: LOPBAN_2:def 4
 for f, g being Element of BoundedLinearOperators (X,X) holds it . (f,g) = f * g;
existence
 ex b1 being BinOp of (BoundedLinearOperators (X,X)) st
for f, g being Element of BoundedLinearOperators (X,X) holds b1 . (f,g) = f * g
proofend;
uniqueness
 for b1, b2 being BinOp of (BoundedLinearOperators (X,X)) st ( for f, g being Element of BoundedLinearOperators (X,X) holds b1 . (f,g) = f * g ) &amp; ( for f, g being Element of BoundedLinearOperators (X,X) holds b2 . (f,g) = f * g ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines FuncMult LOPBAN_2:def_4_:_
 for X being RealNormSpace
for b2 being BinOp of (BoundedLinearOperators (X,X)) holds
( b2 = FuncMult X iff for f, g being Element of BoundedLinearOperators (X,X) holds b2 . (f,g) = f * g );

theorem Th3: :: LOPBAN_2:3
for X being RealNormSpace holds id the carrier of X is Lipschitzian LinearOperator of X,X
proofend;

definition
let X be RealNormSpace;
func FuncUnit X ->  Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 5
 id the carrier of X;
coherence
 id the carrier of X is Element of BoundedLinearOperators (X,X)
proofend;
end;

:: deftheorem  defines FuncUnit LOPBAN_2:def_5_:_
 for X being RealNormSpace holds FuncUnit X = id the carrier of X;

theorem Th4: :: LOPBAN_2:4
for X being RealNormSpace
for f, g, h being Lipschitzian LinearOperator of X,X holds
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
proofend;

theorem Th5: :: LOPBAN_2:5
for X being RealNormSpace
for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h
proofend;

theorem Th6: :: LOPBAN_2:6
for X being RealNormSpace
for f being Lipschitzian LinearOperator of X,X holds
( f * (id the carrier of X) = f &amp; (id the carrier of X) * f = f )
proofend;

theorem Th7: :: LOPBAN_2:7
for X being RealNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h
proofend;

theorem Th8: :: LOPBAN_2:8
for X being RealNormSpace
for f being Element of BoundedLinearOperators (X,X) holds
( f * (FuncUnit X) = f &amp; (FuncUnit X) * f = f )
proofend;

theorem Th9: :: LOPBAN_2:9
for X being RealNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)
proofend;

theorem Th10: :: LOPBAN_2:10
for X being RealNormSpace
for f, g, h being Element of BoundedLinearOperators (X,X) holds (g + h) * f = (g * f) + (h * f)
proofend;

theorem Th11: :: LOPBAN_2:11
for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X)
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
proofend;

theorem Th12: :: LOPBAN_2:12
for X being RealNormSpace
for f, g being Element of BoundedLinearOperators (X,X)
for a being Real holds a * (f * g) = (a * f) * g
proofend;

definition
let X be RealNormSpace;
func Ring_of_BoundedLinearOperators X ->  doubleLoopStr  equals :: LOPBAN_2:def 6
 doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
correctness
coherence
doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) is doubleLoopStr ;
;
end;

:: deftheorem  defines Ring_of_BoundedLinearOperators LOPBAN_2:def_6_:_
 for X being RealNormSpace holds Ring_of_BoundedLinearOperators X = doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);

registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  non empty strict ;
coherence
 ( not Ring_of_BoundedLinearOperators X is empty &amp; Ring_of_BoundedLinearOperators X is strict ) ;
end;

Lm1: now__::_thesis:_for_X_being_RealNormSpace
for_x,_e_being_Element_of_(Ring_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_
(_x_*_e_=_x_&amp;_e_*_x_=_x_)
let X be RealNormSpace; ::_thesis: for x, e being Element of (Ring_of_BoundedLinearOperators X) st e = FuncUnit X holds
( x * e = x &amp; e * x = x )
set F = Ring_of_BoundedLinearOperators X;
let x, e be Element of (Ring_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x &amp; e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x &amp; e * x = x )
hence x * e = f * (FuncUnit X) by Def4
.= x by Th8 ;
::_thesis: e * x = x
thus e * x = (FuncUnit X) * f by A1, Def4
.= x by Th8 ; ::_thesis: verum
end;

registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  unital ;
coherence
 Ring_of_BoundedLinearOperators X is unital
proofend;
end;

theorem Th13: :: LOPBAN_2:13
for X being RealNormSpace
for x, y, z being Element of (Ring_of_BoundedLinearOperators X) holds
( x + y = y + x &amp; (x + y) + z = x + (y + z) &amp; x + (0. (Ring_of_BoundedLinearOperators X)) = x &amp; ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) &amp; (x * y) * z = x * (y * z) &amp; x * (1. (Ring_of_BoundedLinearOperators X)) = x &amp; (1. (Ring_of_BoundedLinearOperators X)) * x = x &amp; x * (y + z) = (x * y) + (x * z) &amp; (y + z) * x = (y * x) + (z * x) )
proofend;

theorem Th14: :: LOPBAN_2:14
for X being RealNormSpace holds Ring_of_BoundedLinearOperators X is Ring
proofend;

registration
let X be RealNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed associative right_unital distributive left_unital ;
coherence
 ( Ring_of_BoundedLinearOperators X is Abelian &amp; Ring_of_BoundedLinearOperators X is add-associative &amp; Ring_of_BoundedLinearOperators X is right_zeroed &amp; Ring_of_BoundedLinearOperators X is right_complementable &amp; Ring_of_BoundedLinearOperators X is associative &amp; Ring_of_BoundedLinearOperators X is left_unital &amp; Ring_of_BoundedLinearOperators X is right_unital &amp; Ring_of_BoundedLinearOperators X is distributive ) by Th14;
end;

definition
let X be RealNormSpace;
func R_Algebra_of_BoundedLinearOperators X ->  AlgebraStr  equals :: LOPBAN_2:def 7
 AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
correctness
coherence
AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) is AlgebraStr ;
;
end;

:: deftheorem  defines R_Algebra_of_BoundedLinearOperators LOPBAN_2:def_7_:_
 for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X = AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);

registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators X ->  non empty strict ;
coherence
 ( not R_Algebra_of_BoundedLinearOperators X is empty &amp; R_Algebra_of_BoundedLinearOperators X is strict ) ;
end;

Lm2: now__::_thesis:_for_X_being_RealNormSpace
for_x,_e_being_Element_of_(R_Algebra_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_
(_x_*_e_=_x_&amp;_e_*_x_=_x_)
let X be RealNormSpace; ::_thesis: for x, e being Element of (R_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds
( x * e = x &amp; e * x = x )
set F = R_Algebra_of_BoundedLinearOperators X;
let x, e be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x &amp; e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x &amp; e * x = x )
hence x * e = f * (FuncUnit X) by Def4
.= x by Th8 ;
::_thesis: e * x = x
thus e * x = (FuncUnit X) * f by A1, Def4
.= x by Th8 ; ::_thesis: verum
end;

registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators X ->  unital ;
coherence
 R_Algebra_of_BoundedLinearOperators X is unital
proofend;
end;

theorem :: LOPBAN_2:15
for X being RealNormSpace
for x, y, z being Element of (R_Algebra_of_BoundedLinearOperators X)
for a, b being Real holds
( x + y = y + x &amp; (x + y) + z = x + (y + z) &amp; x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x &amp; ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) &amp; (x * y) * z = x * (y * z) &amp; x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x &amp; (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x &amp; x * (y + z) = (x * y) + (x * z) &amp; (y + z) * x = (y * x) + (z * x) &amp; a * (x * y) = (a * x) * y &amp; a * (x + y) = (a * x) + (a * y) &amp; (a + b) * x = (a * x) + (b * x) &amp; (a * b) * x = a * (b * x) &amp; (a * b) * (x * y) = (a * x) * (b * y) )
proofend;

definition
mode BLAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative right-distributive right_unital AlgebraStr ;
end;

registration
let X be RealNormSpace;
cluster R_Algebra_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative associative right-distributive right_unital ;
coherence
 ( R_Algebra_of_BoundedLinearOperators X is Abelian &amp; R_Algebra_of_BoundedLinearOperators X is add-associative &amp; R_Algebra_of_BoundedLinearOperators X is right_zeroed &amp; R_Algebra_of_BoundedLinearOperators X is right_complementable &amp; R_Algebra_of_BoundedLinearOperators X is associative &amp; R_Algebra_of_BoundedLinearOperators X is right_unital &amp; R_Algebra_of_BoundedLinearOperators X is right-distributive &amp; R_Algebra_of_BoundedLinearOperators X is vector-distributive &amp; R_Algebra_of_BoundedLinearOperators X is scalar-distributive &amp; R_Algebra_of_BoundedLinearOperators X is scalar-associative &amp; R_Algebra_of_BoundedLinearOperators X is vector-associative &amp; R_Algebra_of_BoundedLinearOperators X is strict )
proofend;
end;

theorem :: LOPBAN_2:16
for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X is BLAlgebra ;

registration
cluster l1_Space  ->  complete ;
coherence
 l1_Space is complete
proofend;
end;

registration
cluster l1_Space  ->  non trivial ;
coherence
 not l1_Space is trivial
proofend;
end;

registration
cluster non empty non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like complete for NORMSTR ;
existence
 not for b1 being RealBanachSpace holds b1 is trivial
proofend;
end;

theorem Th17: :: LOPBAN_2:17
for X being non trivial RealNormSpace ex w being VECTOR of X st ||.w.|| = 1
proofend;

theorem Th18: :: LOPBAN_2:18
for X being non trivial RealNormSpace holds (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1
proofend;

definition
attrc1 is strict ;
struct Normed_AlgebraStr  ->  AlgebraStr , NORMSTR ;
aggrNormed_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) ->  Normed_AlgebraStr ;
end;

registration
cluster non empty for Normed_AlgebraStr ;
existence
 not for b1 being Normed_AlgebraStr holds b1 is empty
proofend;
end;

definition
let X be RealNormSpace;
func R_Normed_Algebra_of_BoundedLinearOperators X ->  Normed_AlgebraStr  equals :: LOPBAN_2:def 8
 Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);
correctness
coherence
Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #) is Normed_AlgebraStr ;
;
end;

:: deftheorem  defines R_Normed_Algebra_of_BoundedLinearOperators LOPBAN_2:def_8_:_
 for X being RealNormSpace holds R_Normed_Algebra_of_BoundedLinearOperators X = Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);

registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  non empty strict ;
coherence
 ( not R_Normed_Algebra_of_BoundedLinearOperators X is empty &amp; R_Normed_Algebra_of_BoundedLinearOperators X is strict ) ;
end;

Lm3: now__::_thesis:_for_X_being_RealNormSpace
for_x,_e_being_Element_of_(R_Normed_Algebra_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_
(_x_*_e_=_x_&amp;_e_*_x_=_x_)
let X be RealNormSpace; ::_thesis: for x, e being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds
( x * e = x &amp; e * x = x )
set F = R_Normed_Algebra_of_BoundedLinearOperators X;
let x, e be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x &amp; e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x &amp; e * x = x )
hence x * e = f * (FuncUnit X) by Def4
.= x by Th8 ;
::_thesis: e * x = x
thus e * x = (FuncUnit X) * f by A1, Def4
.= x by Th8 ; ::_thesis: verum
end;

registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  unital ;
coherence
 R_Normed_Algebra_of_BoundedLinearOperators X is unital
proofend;
end;

theorem Th19: :: LOPBAN_2:19
for X being RealNormSpace
for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being real number holds
( x + y = y + x &amp; (x + y) + z = x + (y + z) &amp; x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x &amp; ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) &amp; (x * y) * z = x * (y * z) &amp; x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x &amp; (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x &amp; x * (y + z) = (x * y) + (x * z) &amp; (y + z) * x = (y * x) + (z * x) &amp; a * (x * y) = (a * x) * y &amp; (a * b) * (x * y) = (a * x) * (b * y) &amp; a * (x + y) = (a * x) + (a * y) &amp; (a + b) * x = (a * x) + (b * x) &amp; (a * b) * x = a * (b * x) &amp; 1 * x = x )
proofend;

theorem Th20: :: LOPBAN_2:20
for X being RealNormSpace holds
( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is discerning &amp; R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like &amp; R_Normed_Algebra_of_BoundedLinearOperators X is Abelian &amp; R_Normed_Algebra_of_BoundedLinearOperators X is add-associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable &amp; R_Normed_Algebra_of_BoundedLinearOperators X is associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right_unital &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )
proofend;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital strict for Normed_AlgebraStr ;
existence
 ex b1 being non empty Normed_AlgebraStr st
( b1 is reflexive &amp; b1 is discerning &amp; b1 is RealNormSpace-like &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is associative &amp; b1 is right_unital &amp; b1 is right-distributive &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is vector-associative &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital &amp; b1 is strict )
proofend;
end;

definition
mode Normed_Algebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Normed_AlgebraStr ;
end;

registration
let X be RealNormSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital ;
correctness
coherence
( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is discerning &amp; R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like &amp; R_Normed_Algebra_of_BoundedLinearOperators X is Abelian &amp; R_Normed_Algebra_of_BoundedLinearOperators X is add-associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable &amp; R_Normed_Algebra_of_BoundedLinearOperators X is associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right_unital &amp; R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative &amp; R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital );
by Th20;
end;

definition
let X be non empty Normed_AlgebraStr ;
attrX is Banach_Algebra-like_1  means :: LOPBAN_2:def 9
 for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||;
attrX is Banach_Algebra-like_2  means :Def10: :: LOPBAN_2:def 10
||.(1. X).|| = 1;
attrX is Banach_Algebra-like_3  means :: LOPBAN_2:def 11
 for a being Real
for x, y being Element of X holds a * (x * y) = x * (a * y);
end;

:: deftheorem  defines Banach_Algebra-like_1 LOPBAN_2:def_9_:_
 for X being non empty Normed_AlgebraStr holds
( X is Banach_Algebra-like_1 iff for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.|| );

:: deftheorem Def10 defines Banach_Algebra-like_2 LOPBAN_2:def_10_:_
 for X being non empty Normed_AlgebraStr holds
( X is Banach_Algebra-like_2 iff ||.(1. X).|| = 1 );

:: deftheorem  defines Banach_Algebra-like_3 LOPBAN_2:def_11_:_
 for X being non empty Normed_AlgebraStr holds
( X is Banach_Algebra-like_3 iff for a being Real
for x, y being Element of X holds a * (x * y) = x * (a * y) );

definition
let X be Normed_Algebra;
attrX is Banach_Algebra-like  means :Def12: :: LOPBAN_2:def 12
( X is Banach_Algebra-like_1 &amp; X is Banach_Algebra-like_2 &amp; X is Banach_Algebra-like_3 &amp; X is left_unital &amp; X is left-distributive &amp; X is complete );
end;

:: deftheorem Def12 defines Banach_Algebra-like LOPBAN_2:def_12_:_
 for X being Normed_Algebra holds
( X is Banach_Algebra-like iff ( X is Banach_Algebra-like_1 &amp; X is Banach_Algebra-like_2 &amp; X is Banach_Algebra-like_3 &amp; X is left_unital &amp; X is left-distributive &amp; X is complete ) );

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Banach_Algebra-like  ->  left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 for Normed_AlgebraStr ;
coherence
 for b1 being Normed_Algebra st b1 is Banach_Algebra-like holds
( b1 is Banach_Algebra-like_1 &amp; b1 is Banach_Algebra-like_2 &amp; b1 is Banach_Algebra-like_3 &amp; b1 is left-distributive &amp; b1 is left_unital &amp; b1 is complete ) by Def12;
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive left-distributive right_unital left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3  ->  Banach_Algebra-like for Normed_AlgebraStr ;
coherence
 for b1 being Normed_Algebra st b1 is Banach_Algebra-like_1 &amp; b1 is Banach_Algebra-like_2 &amp; b1 is Banach_Algebra-like_3 &amp; b1 is left-distributive &amp; b1 is left_unital &amp; b1 is complete holds
b1 is Banach_Algebra-like by Def12;
end;

registration
let X be non trivial RealBanachSpace;
cluster R_Normed_Algebra_of_BoundedLinearOperators X ->  Banach_Algebra-like ;
coherence
 R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like
proofend;
end;

registration
cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Banach_Algebra-like for Normed_AlgebraStr ;
existence
 ex b1 being Normed_Algebra st b1 is Banach_Algebra-like
proofend;
end;

definition
mode Banach_Algebra is Banach_Algebra-like Normed_Algebra;
end;

theorem :: LOPBAN_2:21
for X being RealNormSpace holds 1. (Ring_of_BoundedLinearOperators X) = FuncUnit X ;

theorem :: LOPBAN_2:22
for X being RealNormSpace holds 1. (R_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;

theorem :: LOPBAN_2:23
for X being RealNormSpace holds 1. (R_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;