:: by Noboru Endou

::

:: Received March 18, 2004

:: Copyright (c) 2004-2016 Association of Mizar Users

theorem Th1: :: CLOPBAN2:1

for X, Y, Z being ComplexLinearSpace

for f being LinearOperator of X,Y

for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z

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: :: CLOPBAN2:2

for X, Y, Z being ComplexNormSpace

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

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 ComplexNormSpace;

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

definition

let X be ComplexNormSpace;

let f, g be Element of BoundedLinearOperators (X,X);

coherence

(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (f,g) is Element of BoundedLinearOperators (X,X);

;

end;
let f, g be Element of BoundedLinearOperators (X,X);

func f + g -> Element of BoundedLinearOperators (X,X) equals :: CLOPBAN2:def 1

(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (f,g);

correctness (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (f,g);

coherence

(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (f,g) is Element of BoundedLinearOperators (X,X);

;

:: deftheorem defines + CLOPBAN2:def 1 :

for X being ComplexNormSpace

for f, g being Element of BoundedLinearOperators (X,X) holds f + g = (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (f,g);

for X being ComplexNormSpace

for f, g being Element of BoundedLinearOperators (X,X) holds f + g = (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (f,g);

definition

let X be ComplexNormSpace;

let f, g be Element of BoundedLinearOperators (X,X);

coherence

(modetrans (g,X,X)) * (modetrans (f,X,X)) is Element of BoundedLinearOperators (X,X);

by CLOPBAN1:def 7;

end;
let f, g be Element of BoundedLinearOperators (X,X);

func g * f -> Element of BoundedLinearOperators (X,X) equals :: CLOPBAN2:def 2

(modetrans (g,X,X)) * (modetrans (f,X,X));

correctness (modetrans (g,X,X)) * (modetrans (f,X,X));

coherence

(modetrans (g,X,X)) * (modetrans (f,X,X)) is Element of BoundedLinearOperators (X,X);

by CLOPBAN1:def 7;

:: deftheorem defines * CLOPBAN2:def 2 :

for X being ComplexNormSpace

for f, g being Element of BoundedLinearOperators (X,X) holds g * f = (modetrans (g,X,X)) * (modetrans (f,X,X));

for X being ComplexNormSpace

for f, g being Element of BoundedLinearOperators (X,X) holds g * f = (modetrans (g,X,X)) * (modetrans (f,X,X));

definition

let X be ComplexNormSpace;

let f be Element of BoundedLinearOperators (X,X);

let z be Complex;

coherence

(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f) is Element of BoundedLinearOperators (X,X);

end;
let f be Element of BoundedLinearOperators (X,X);

let z be Complex;

func z * f -> Element of BoundedLinearOperators (X,X) equals :: CLOPBAN2:def 3

(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f);

correctness (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f);

coherence

(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f) is Element of BoundedLinearOperators (X,X);

proof end;

:: deftheorem defines * CLOPBAN2:def 3 :

for X being ComplexNormSpace

for f being Element of BoundedLinearOperators (X,X)

for z being Complex holds z * f = (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f);

for X being ComplexNormSpace

for f being Element of BoundedLinearOperators (X,X)

for z being Complex holds z * f = (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f);

definition

let X be ComplexNormSpace;

ex b_{1} being BinOp of (BoundedLinearOperators (X,X)) st

for f, g being Element of BoundedLinearOperators (X,X) holds b_{1} . (f,g) = f * g

for b_{1}, b_{2} being BinOp of (BoundedLinearOperators (X,X)) st ( for f, g being Element of BoundedLinearOperators (X,X) holds b_{1} . (f,g) = f * g ) & ( for f, g being Element of BoundedLinearOperators (X,X) holds b_{2} . (f,g) = f * g ) holds

b_{1} = b_{2}

end;
func FuncMult X -> BinOp of (BoundedLinearOperators (X,X)) means :Def4: :: CLOPBAN2:def 4

for f, g being Element of BoundedLinearOperators (X,X) holds it . (f,g) = f * g;

existence for f, g being Element of BoundedLinearOperators (X,X) holds it . (f,g) = f * g;

ex b

for f, g being Element of BoundedLinearOperators (X,X) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines FuncMult CLOPBAN2:def 4 :

for X being ComplexNormSpace

for b_{2} being BinOp of (BoundedLinearOperators (X,X)) holds

( b_{2} = FuncMult X iff for f, g being Element of BoundedLinearOperators (X,X) holds b_{2} . (f,g) = f * g );

for X being ComplexNormSpace

for b

( b

definition

let X be ComplexNormSpace;

id the carrier of X is Element of BoundedLinearOperators (X,X)

end;
func FuncUnit X -> Element of BoundedLinearOperators (X,X) equals :: CLOPBAN2:def 5

id the carrier of X;

coherence id the carrier of X;

id the carrier of X is Element of BoundedLinearOperators (X,X)

proof end;

:: deftheorem defines FuncUnit CLOPBAN2:def 5 :

for X being ComplexNormSpace holds FuncUnit X = id the carrier of X;

for X being ComplexNormSpace holds FuncUnit X = id the carrier of X;

theorem Th4: :: CLOPBAN2:4

for X being ComplexNormSpace

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

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: :: CLOPBAN2:5

for X being ComplexNormSpace

for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h

for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h

proof end;

theorem Th6: :: CLOPBAN2:6

for X being ComplexNormSpace

for f being Lipschitzian LinearOperator of X,X holds

( f * (id the carrier of X) = f & (id the carrier of X) * f = f )

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: :: CLOPBAN2:7

for X being ComplexNormSpace

for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h

for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h

proof end;

theorem Th8: :: CLOPBAN2:8

for X being ComplexNormSpace

for f being Element of BoundedLinearOperators (X,X) holds

( f * (FuncUnit X) = f & (FuncUnit X) * f = f )

for f being Element of BoundedLinearOperators (X,X) holds

( f * (FuncUnit X) = f & (FuncUnit X) * f = f )

proof end;

theorem Th9: :: CLOPBAN2:9

for X being ComplexNormSpace

for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)

for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)

proof end;

theorem Th10: :: CLOPBAN2:10

for X being ComplexNormSpace

for f, g, h being Element of BoundedLinearOperators (X,X) holds (g + h) * f = (g * f) + (h * f)

for f, g, h being Element of BoundedLinearOperators (X,X) holds (g + h) * f = (g * f) + (h * f)

proof end;

theorem Th11: :: CLOPBAN2:11

for X being ComplexNormSpace

for f, g being Element of BoundedLinearOperators (X,X)

for a, b being Complex holds (a * b) * (f * g) = (a * f) * (b * g)

for f, g being Element of BoundedLinearOperators (X,X)

for a, b being Complex holds (a * b) * (f * g) = (a * f) * (b * g)

proof end;

theorem Th12: :: CLOPBAN2:12

for X being ComplexNormSpace

for f, g being Element of BoundedLinearOperators (X,X)

for a being Complex holds a * (f * g) = (a * f) * g

for f, g being Element of BoundedLinearOperators (X,X)

for a being Complex holds a * (f * g) = (a * f) * g

proof end;

definition

let X be ComplexNormSpace;

coherence

doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) is doubleLoopStr ;

;

end;
func Ring_of_BoundedLinearOperators X -> doubleLoopStr equals :: CLOPBAN2:def 6

doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

correctness doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

coherence

doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) is doubleLoopStr ;

;

:: deftheorem defines Ring_of_BoundedLinearOperators CLOPBAN2:def 6 :

for X being ComplexNormSpace holds Ring_of_BoundedLinearOperators X = doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

for X being ComplexNormSpace holds Ring_of_BoundedLinearOperators X = doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

registration

let X be ComplexNormSpace;

coherence

( not Ring_of_BoundedLinearOperators X is empty & Ring_of_BoundedLinearOperators X is strict ) ;

end;
coherence

( not Ring_of_BoundedLinearOperators X is empty & Ring_of_BoundedLinearOperators X is strict ) ;

Lm1: now :: thesis: for X being ComplexNormSpace

for x, e being Element of (Ring_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

for x, e being Element of (Ring_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

let X be ComplexNormSpace; :: 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;
( 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

registration
end;

theorem Th13: :: CLOPBAN2:13

for X being ComplexNormSpace

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 & x is right_complementable & (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) )

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 & x is right_complementable & (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;

registration

let X be ComplexNormSpace;

( 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 well-unital & Ring_of_BoundedLinearOperators X is distributive ) by Th14;

end;
cluster Ring_of_BoundedLinearOperators X -> right_complementable Abelian add-associative right_zeroed well-unital distributive 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 well-unital & Ring_of_BoundedLinearOperators X is distributive ) by Th14;

definition

let X be ComplexNormSpace;

coherence

ComplexAlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) is ComplexAlgebraStr ;

;

end;
func C_Algebra_of_BoundedLinearOperators X -> ComplexAlgebraStr equals :: CLOPBAN2:def 7

ComplexAlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

correctness ComplexAlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

coherence

ComplexAlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) is ComplexAlgebraStr ;

;

:: deftheorem defines C_Algebra_of_BoundedLinearOperators CLOPBAN2:def 7 :

for X being ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators X = ComplexAlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

for X being ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators X = ComplexAlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);

registration

let X be ComplexNormSpace;

coherence

( not C_Algebra_of_BoundedLinearOperators X is empty & C_Algebra_of_BoundedLinearOperators X is strict ) ;

end;
coherence

( not C_Algebra_of_BoundedLinearOperators X is empty & C_Algebra_of_BoundedLinearOperators X is strict ) ;

Lm2: now :: thesis: for X being ComplexNormSpace

for x, e being Element of (C_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

for x, e being Element of (C_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

let X be ComplexNormSpace; :: thesis: for x, e being Element of (C_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

set F = C_Algebra_of_BoundedLinearOperators X;

let x, e be Element of (C_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;
( x * e = x & e * x = x )

set F = C_Algebra_of_BoundedLinearOperators X;

let x, e be Element of (C_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

registration
end;

theorem :: CLOPBAN2:15

for X being ComplexNormSpace

for x, y, z being Element of (C_Algebra_of_BoundedLinearOperators X)

for a, b being Complex holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) )

for x, y, z being Element of (C_Algebra_of_BoundedLinearOperators X)

for a, b being Complex holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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 ComplexBLAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital vector-associative associative ComplexAlgebraStr ;

end;
registration

let X be ComplexNormSpace;

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

end;
cluster C_Algebra_of_BoundedLinearOperators X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative right-distributive right_unital vector-associative associative ;

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

proof end;

theorem :: CLOPBAN2:16

registration
end;

registration
end;

registration

not for b_{1} being ComplexBanachSpace holds b_{1} is trivial
end;

cluster non empty non trivial right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like complete for CNORMSTR ;

existence not for b

proof end;

theorem Th18: :: CLOPBAN2:18

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

proof end;

definition

attr c_{1} is strict ;

struct Normed_Complex_AlgebraStr -> ComplexAlgebraStr , CNORMSTR ;

aggr Normed_Complex_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) -> Normed_Complex_AlgebraStr ;

end;
struct Normed_Complex_AlgebraStr -> ComplexAlgebraStr , CNORMSTR ;

aggr Normed_Complex_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) -> Normed_Complex_AlgebraStr ;

registration
end;

definition

let X be ComplexNormSpace;

coherence

Normed_Complex_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #) is Normed_Complex_AlgebraStr ;

;

end;
func C_Normed_Algebra_of_BoundedLinearOperators X -> Normed_Complex_AlgebraStr equals :: CLOPBAN2:def 8

Normed_Complex_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);

correctness Normed_Complex_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);

coherence

Normed_Complex_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #) is Normed_Complex_AlgebraStr ;

;

:: deftheorem defines C_Normed_Algebra_of_BoundedLinearOperators CLOPBAN2:def 8 :

for X being ComplexNormSpace holds C_Normed_Algebra_of_BoundedLinearOperators X = Normed_Complex_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);

for X being ComplexNormSpace holds C_Normed_Algebra_of_BoundedLinearOperators X = Normed_Complex_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #);

registration

let X be ComplexNormSpace;

coherence

( not C_Normed_Algebra_of_BoundedLinearOperators X is empty & C_Normed_Algebra_of_BoundedLinearOperators X is strict ) ;

end;
coherence

( not C_Normed_Algebra_of_BoundedLinearOperators X is empty & C_Normed_Algebra_of_BoundedLinearOperators X is strict ) ;

Lm3: now :: thesis: for X being ComplexNormSpace

for x, e being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

for x, e being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

let X be ComplexNormSpace; :: thesis: for x, e being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds

( x * e = x & e * x = x )

set F = C_Normed_Algebra_of_BoundedLinearOperators X;

let x, e be Element of (C_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;
( x * e = x & e * x = x )

set F = C_Normed_Algebra_of_BoundedLinearOperators X;

let x, e be Element of (C_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

registration

let X be ComplexNormSpace;

coherence

C_Normed_Algebra_of_BoundedLinearOperators X is unital

end;
coherence

C_Normed_Algebra_of_BoundedLinearOperators X is unital

proof end;

theorem Th19: :: CLOPBAN2:19

for X being ComplexNormSpace

for x, y, z being Element of (C_Normed_Algebra_of_BoundedLinearOperators X)

for a, b being Complex holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )

for x, y, z being Element of (C_Normed_Algebra_of_BoundedLinearOperators X)

for a, b being Complex holds

( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )

proof end;

theorem Th20: :: CLOPBAN2:20

for X being ComplexNormSpace holds

( C_Normed_Algebra_of_BoundedLinearOperators X is reflexive & C_Normed_Algebra_of_BoundedLinearOperators X is discerning & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )

( C_Normed_Algebra_of_BoundedLinearOperators X is reflexive & C_Normed_Algebra_of_BoundedLinearOperators X is discerning & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )

proof end;

registration

ex b_{1} being non empty Normed_Complex_AlgebraStr st

( b_{1} is reflexive & b_{1} is discerning & b_{1} is ComplexNormSpace-like & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is associative & b_{1} is right_unital & b_{1} is right-distributive & b_{1} is vector-distributive & b_{1} is scalar-distributive & b_{1} is scalar-associative & b_{1} is vector-associative & b_{1} is scalar-unital & b_{1} is strict )
end;

cluster non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like right-distributive right_unital vector-associative associative strict for Normed_Complex_AlgebraStr ;

existence ex b

( b

proof end;

definition

mode Normed_Complex_Algebra is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like right-distributive right_unital vector-associative associative Normed_Complex_AlgebraStr ;

end;
registration

let X be ComplexNormSpace;

coherence

( C_Normed_Algebra_of_BoundedLinearOperators X is reflexive & C_Normed_Algebra_of_BoundedLinearOperators X is discerning & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital );

by Th20;

end;
cluster C_Normed_Algebra_of_BoundedLinearOperators X -> right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like right-distributive right_unital vector-associative associative ;

correctness coherence

( C_Normed_Algebra_of_BoundedLinearOperators X is reflexive & C_Normed_Algebra_of_BoundedLinearOperators X is discerning & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital );

by Th20;

definition

let X be non empty Normed_Complex_AlgebraStr ;

end;
attr X is Banach_Algebra-like_1 means :: CLOPBAN2:def 9

for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||;

for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||;

attr X is Banach_Algebra-like_3 means :: CLOPBAN2:def 11

for a being Complex

for x, y being Element of X holds a * (x * y) = x * (a * y);

for a being Complex

for x, y being Element of X holds a * (x * y) = x * (a * y);

:: deftheorem defines Banach_Algebra-like_1 CLOPBAN2:def 9 :

for X being non empty Normed_Complex_AlgebraStr holds

( X is Banach_Algebra-like_1 iff for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.|| );

for X being non empty Normed_Complex_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 CLOPBAN2:def 10 :

for X being non empty Normed_Complex_AlgebraStr holds

( X is Banach_Algebra-like_2 iff ||.(1. X).|| = 1 );

for X being non empty Normed_Complex_AlgebraStr holds

( X is Banach_Algebra-like_2 iff ||.(1. X).|| = 1 );

:: deftheorem defines Banach_Algebra-like_3 CLOPBAN2:def 11 :

for X being non empty Normed_Complex_AlgebraStr holds

( X is Banach_Algebra-like_3 iff for a being Complex

for x, y being Element of X holds a * (x * y) = x * (a * y) );

for X being non empty Normed_Complex_AlgebraStr holds

( X is Banach_Algebra-like_3 iff for a being Complex

for x, y being Element of X holds a * (x * y) = x * (a * y) );

definition

let X be Normed_Complex_Algebra;

end;
attr X is Banach_Algebra-like means :: CLOPBAN2: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 );

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

:: deftheorem defines Banach_Algebra-like CLOPBAN2:def 12 :

for X being Normed_Complex_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 ) );

for X being Normed_Complex_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

for b_{1} being Normed_Complex_Algebra st b_{1} is Banach_Algebra-like holds

( b_{1} is Banach_Algebra-like_1 & b_{1} is Banach_Algebra-like_2 & b_{1} is Banach_Algebra-like_3 & b_{1} is left-distributive & b_{1} is left_unital & b_{1} is complete )
;

for b_{1} being Normed_Complex_Algebra st b_{1} is Banach_Algebra-like_1 & b_{1} is Banach_Algebra-like_2 & b_{1} is Banach_Algebra-like_3 & b_{1} is left-distributive & b_{1} is left_unital & b_{1} is complete holds

b_{1} is Banach_Algebra-like
;

end;

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

coherence for b

( b

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

coherence for b

b

registration

let X be non trivial ComplexBanachSpace;

coherence

C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like

end;
coherence

C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like

proof end;

registration

ex b_{1} being Normed_Complex_Algebra st b_{1} is Banach_Algebra-like
end;

cluster non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like right-distributive right_unital vector-associative associative Banach_Algebra-like for Normed_Complex_AlgebraStr ;

existence ex b

proof end;

theorem :: CLOPBAN2:21

theorem :: CLOPBAN2:22

theorem :: CLOPBAN2:23