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

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

proof end;

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.|| & (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) )

proof end;

definition

let X be RealNormSpace;
let f, g be Lipschitzian LinearOperator of X,X;
:: original: *
redefine func g * 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);

func f + 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);

func g * 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;

func a * 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);

proof end;

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 b₁ being BinOp of (BoundedLinearOperators (X,X)) st
for f, g being Element of BoundedLinearOperators (X,X) holds b₁ . (f,g) = f * g

proof end;

uniqueness
for b₁, b₂ being BinOp of (BoundedLinearOperators (X,X)) st ( for f, g being Element of BoundedLinearOperators (X,X) holds b₁ . (f,g) = f * g ) & ( for f, g being Element of BoundedLinearOperators (X,X) holds b₂ . (f,g) = f * g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines FuncMult LOPBAN_2:def 4 :
for X being RealNormSpace
for b₂ being BinOp of (BoundedLinearOperators (X,X)) holds
( b₂ = FuncMult X iff for f, g being Element of BoundedLinearOperators (X,X) holds b₂ . (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

proof end;

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)

proof end;

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) )

proof end;

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

proof end;

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 & (id the carrier of X) * f = f )

proof end;

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

proof end;

theorem Th8: :: LOPBAN_2:8

for X being RealNormSpace
for f being Element of BoundedLinearOperators (X,X) holds
( f * (FuncUnit X) = f & (FuncUnit X) * f = f )

proof end;

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)

proof end;

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)

proof end;

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)

proof end;

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

proof end;

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 & 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 & 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 & 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 & e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; :: thesis: ( x * e = x & 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

proof end;

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 & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )

proof end;

theorem Th14: :: LOPBAN_2:14

for X being RealNormSpace holds Ring_of_BoundedLinearOperators X is Ring

proof end;

registration

let X be RealNormSpace;

cluster Ring_of_BoundedLinearOperators X -> right_complementable Abelian add-associative right_zeroed right_unital well-unital distributive left_unital associative ;

coherence
( Ring_of_BoundedLinearOperators X is Abelian & Ring_of_BoundedLinearOperators X is add-associative & Ring_of_BoundedLinearOperators X is right_zeroed & Ring_of_BoundedLinearOperators X is right_complementable & Ring_of_BoundedLinearOperators X is associative & Ring_of_BoundedLinearOperators X is left_unital & Ring_of_BoundedLinearOperators X is right_unital & Ring_of_BoundedLinearOperators X is distributive & Ring_of_BoundedLinearOperators X is well-unital ) 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 & 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 & 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 & 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 & e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; :: thesis: ( x * e = x & 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

proof end;

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 & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )

proof end;

definition

mode BLAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative right-distributive right_unital associative 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 right-distributive right_unital associative ;

coherence
( R_Algebra_of_BoundedLinearOperators X is Abelian & R_Algebra_of_BoundedLinearOperators X is add-associative & R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )

proof end;

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 by RSSPACE3:9;

end;

registration

cluster l1_Space -> non trivial ;

coherence
not l1_Space is trivial

proof end;

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 V138() discerning reflexive RealNormSpace-like complete for NORMSTR ;

existence
not for b₁ being RealBanachSpace holds b₁ is trivial

proof end;

end;

theorem Th17: :: LOPBAN_2:17

for X being non trivial RealNormSpace ex w being VECTOR of X st ||.w.|| = 1

proof end;

theorem Th18: :: LOPBAN_2:18

for X being non trivial RealNormSpace holds (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1

proof end;

definition

attr c₁ is strict ;
struct Normed_AlgebraStr -> AlgebraStr , NORMSTR ;
aggr Normed_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) -> Normed_AlgebraStr ;

end;

registration

cluster non empty for Normed_AlgebraStr ;

existence
not for b₁ being Normed_AlgebraStr holds b₁ is empty

proof end;

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 & 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 & 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 & 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 & e * x = x ) )
reconsider f = x as Element of BoundedLinearOperators (X,X) ;
assume A1: e = FuncUnit X ; :: thesis: ( x * e = x & 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

proof end;

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 holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x )

proof end;

theorem Th20: :: LOPBAN_2:20

for X being RealNormSpace holds
( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )

proof end;

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 right-distributive right_unital associative strict for Normed_AlgebraStr ;

existence
ex b₁ being non empty Normed_AlgebraStr st
( b₁ is reflexive & b₁ is discerning & b₁ is RealNormSpace-like & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is associative & b₁ is right_unital & b₁ is right-distributive & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ is vector-associative & b₁ is vector-distributive & b₁ is scalar-distributive & b₁ is scalar-associative & b₁ is scalar-unital & b₁ is strict )

proof end;

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 right-distributive right_unital associative 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 right-distributive right_unital associative ;

correctness
coherence
( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital );
by Th20;

end;

definition

let X be non empty Normed_AlgebraStr ;

attr X is Banach_Algebra-like_1 means :: LOPBAN_2:def 9
for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||;

attr X is Banach_Algebra-like_2 means :: LOPBAN_2:def 10
||.(1. X).|| = 1;

attr X 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 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;

attr X is Banach_Algebra-like means :: LOPBAN_2:def 12
( X is Banach_Algebra-like_1 & X is Banach_Algebra-like_2 & X is Banach_Algebra-like_3 & X is left_unital & X is left-distributive & X is complete );

end;

:: deftheorem 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 & X is Banach_Algebra-like_2 & X is Banach_Algebra-like_3 & X is left_unital & X is left-distributive & 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 right-distributive right_unital associative 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 b₁ being Normed_Algebra st b₁ is Banach_Algebra-like holds
( b₁ is Banach_Algebra-like_1 & b₁ is Banach_Algebra-like_2 & b₁ is Banach_Algebra-like_3 & b₁ is left-distributive & b₁ is left_unital & b₁ is complete ) ;

cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like right-distributive left-distributive right_unital left_unital complete associative Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 -> Banach_Algebra-like for Normed_AlgebraStr ;

coherence
for b₁ being Normed_Algebra st b₁ is Banach_Algebra-like_1 & b₁ is Banach_Algebra-like_2 & b₁ is Banach_Algebra-like_3 & b₁ is left-distributive & b₁ is left_unital & b₁ is complete holds
b₁ is Banach_Algebra-like ;

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

proof end;

end;

registration

cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V138() vector-associative discerning reflexive RealNormSpace-like right-distributive right_unital associative Banach_Algebra-like for Normed_AlgebraStr ;

existence
ex b₁ being Normed_Algebra st b₁ is Banach_Algebra-like

proof end;

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 ;