:: CLOPBAN2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: CLOPBAN2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th2: :: CLOPBAN2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y, Z being ComplexNormSpace
for f being bounded LinearOperator of X,Y
for g being bounded LinearOperator of Y,Z holds
( g * f is bounded 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 bounded LinearOperator of X,X;
:: original: *
redefine func g * f -> bounded LinearOperator of X,X;
correctness
coherence
g * f is bounded LinearOperator of X,X;
by Th2;
end;

definition
let X be ComplexNormSpace;
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
coherence
(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . f,g is Element of BoundedLinearOperators X,X;
;
end;

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

definition
let X be ComplexNormSpace;
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
coherence
(modetrans g,X,X) * (modetrans f,X,X) is Element of BoundedLinearOperators X,X;
by CLOPBAN1:def 8;
end;

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

definition
let X be ComplexNormSpace;
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
coherence
(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . z,f is Element of BoundedLinearOperators X,X;
;
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;

definition
let X be ComplexNormSpace;
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
ex b1 being BinOp of BoundedLinearOperators X,X st
for f, g being Element of BoundedLinearOperators X,X holds b1 . f,g = f * g
proof end;
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 ) & ( for f, g being Element of BoundedLinearOperators X,X holds b2 . f,g = f * g ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines FuncMult CLOPBAN2:def 4 :
for X being ComplexNormSpace
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: :: CLOPBAN2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace holds id the carrier of X is bounded LinearOperator of X,X
proof end;

definition
let X be ComplexNormSpace;
func FuncUnit X -> Element of BoundedLinearOperators X,X equals :: CLOPBAN2: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 CLOPBAN2:def 5 :
for X being ComplexNormSpace holds FuncUnit X = id the carrier of X;

theorem Th4: :: CLOPBAN2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for f, g, h being bounded 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for f, g, h being bounded LinearOperator of X,X holds f * (g * h) = (f * g) * h
proof end;

theorem Th6: :: CLOPBAN2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for f being bounded 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for f, g, h being Element of BoundedLinearOperators X,X holds f * (g * h) = (f * g) * h
proof end;

theorem Th8: :: CLOPBAN2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for f being Element of BoundedLinearOperators X,X holds
( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
proof end;

theorem Th9: :: CLOPBAN2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for f, g, h being Element of BoundedLinearOperators X,X holds f * (g + h) = (f * g) + (f * h)
proof end;

theorem Th10: :: CLOPBAN2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
for f, g, h being Element of BoundedLinearOperators X,X holds (g + h) * f = (g * f) + (h * f)
proof end;

theorem Th11: :: CLOPBAN2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th12: :: CLOPBAN2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace
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;
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
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;

:: 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)) #);

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

Lm1: now
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 ) )
assume A1: e = FuncUnit X ; :: thesis: ( x * e = x & e * x = x )
reconsider f = x as Element of BoundedLinearOperators X,X ;
thus x * e = the mult of (Ring_of_BoundedLinearOperators X) . x,e
.= (FuncMult X) . f,(FuncUnit X) by A1
.= f * (FuncUnit X) by Def4
.= x by Th8 ; :: thesis: e * x = x
thus e * x = the mult of (Ring_of_BoundedLinearOperators X) . e,x
.= (FuncMult X) . (FuncUnit X),f by A1
.= (FuncUnit X) * f by Def4
.= x by Th8 ; :: thesis: verum
end;

registration
let X be ComplexNormSpace;
cluster Ring_of_BoundedLinearOperators X -> non empty unital strict ;
coherence
Ring_of_BoundedLinearOperators X is unital
proof end;
end;

Lm2: now
let X be ComplexNormSpace; :: thesis: 1. (Ring_of_BoundedLinearOperators X) = FuncUnit X
set F = Ring_of_BoundedLinearOperators X;
reconsider e = FuncUnit X as Element of (Ring_of_BoundedLinearOperators X) ;
for x being Element of (Ring_of_BoundedLinearOperators X) holds
( x * e = x & e * x = x ) by Lm1;
hence 1. (Ring_of_BoundedLinearOperators X) = FuncUnit X by GROUP_1:def 5; :: thesis: verum
end;

theorem Th13: :: CLOPBAN2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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: :: CLOPBAN2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace holds Ring_of_BoundedLinearOperators X is Ring
proof end;

registration
let X be ComplexNormSpace;
cluster Ring_of_BoundedLinearOperators X -> non empty Abelian add-associative right_zeroed right_complementable unital associative strict right_unital distributive left_unital ;
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 ) by Th14;
end;

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

:: 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)) #);

registration
let X be ComplexNormSpace;
cluster C_Algebra_of_BoundedLinearOperators X -> non empty strict ;
coherence
( not C_Algebra_of_BoundedLinearOperators X is empty & C_Algebra_of_BoundedLinearOperators X is strict )
proof end;
end;

Lm3: now
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 ) )
assume A1: e = FuncUnit X ; :: thesis: ( x * e = x & e * x = x )
reconsider f = x as Element of BoundedLinearOperators X,X ;
thus x * e = the mult of (C_Algebra_of_BoundedLinearOperators X) . x,e
.= (FuncMult X) . f,(FuncUnit X) by A1
.= f * (FuncUnit X) by Def4
.= x by Th8 ; :: thesis: e * x = x
thus e * x = the mult of (C_Algebra_of_BoundedLinearOperators X) . e,x
.= (FuncMult X) . (FuncUnit X),f by A1
.= (FuncUnit X) * f by Def4
.= x by Th8 ; :: thesis: verum
end;

registration
let X be ComplexNormSpace;
cluster C_Algebra_of_BoundedLinearOperators X -> non empty unital strict ;
coherence
C_Algebra_of_BoundedLinearOperators X is unital
proof end;
end;

Lm4: now
let X be ComplexNormSpace; :: thesis: 1. (C_Algebra_of_BoundedLinearOperators X) = FuncUnit X
set F = C_Algebra_of_BoundedLinearOperators X;
reconsider e = FuncUnit X as Element of (C_Algebra_of_BoundedLinearOperators X) ;
for x being Element of (C_Algebra_of_BoundedLinearOperators X) holds
( x * e = x & e * x = x ) by Lm3;
hence 1. (C_Algebra_of_BoundedLinearOperators X) = FuncUnit X by GROUP_1:def 5; :: thesis: verum
end;

theorem Th15: :: CLOPBAN2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ex t being Element of (C_Algebra_of_BoundedLinearOperators X) st x + t = 0. (C_Algebra_of_BoundedLinearOperators X) & (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 Abelian add-associative right_zeroed right_complementable associative ComplexAlgebra-like ComplexAlgebraStr ;
end;

theorem :: CLOPBAN2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators X is ComplexBLAlgebra
proof end;

registration
cluster Complex_l1_Space -> complete ;
coherence
Complex_l1_Space is complete
proof end;
end;

registration
cluster Complex_l1_Space -> complete non trivial ;
coherence
not Complex_l1_Space is trivial
proof end;
end;

registration
cluster non trivial CNORMSTR ;
existence
not for b1 being ComplexBanachSpace holds b1 is trivial
proof end;
end;

theorem Th17: :: CLOPBAN2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non trivial ComplexNormSpace ex w being VECTOR of X st ||.w.|| = 1
proof end;

theorem Th18: :: CLOPBAN2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non trivial ComplexNormSpace holds (BoundedLinearOperatorsNorm X,X) . (id the carrier of X) = 1
proof end;

definition
attr c1 is strict;
struct Normed_Complex_AlgebraStr -> ComplexAlgebraStr , CNORMSTR ;
aggr Normed_Complex_AlgebraStr(# carrier, mult, add, Mult, unity, Zero, norm #) -> Normed_Complex_AlgebraStr ;
end;

registration
cluster non empty Normed_Complex_AlgebraStr ;
existence
not for b1 being Normed_Complex_AlgebraStr holds b1 is empty
proof end;
end;

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

:: 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) #);

registration
let X be ComplexNormSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators X -> non empty strict ;
coherence
( not C_Normed_Algebra_of_BoundedLinearOperators X is empty & C_Normed_Algebra_of_BoundedLinearOperators X is strict )
proof end;
end;

Lm5: now
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 ) )
assume A1: e = FuncUnit X ; :: thesis: ( x * e = x & e * x = x )
reconsider f = x as Element of BoundedLinearOperators X,X ;
thus x * e = the mult of (C_Normed_Algebra_of_BoundedLinearOperators X) . x,e
.= (FuncMult X) . f,(FuncUnit X) by A1
.= f * (FuncUnit X) by Def4
.= x by Th8 ; :: thesis: e * x = x
thus e * x = the mult of (C_Normed_Algebra_of_BoundedLinearOperators X) . e,x
.= (FuncMult X) . (FuncUnit X),f by A1
.= (FuncUnit X) * f by Def4
.= x by Th8 ; :: thesis: verum
end;

registration
let X be ComplexNormSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators X -> non empty unital strict ;
coherence
C_Normed_Algebra_of_BoundedLinearOperators X is unital
proof end;
end;

Lm6: now
let X be ComplexNormSpace; :: thesis: 1. (C_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X
set F = C_Normed_Algebra_of_BoundedLinearOperators X;
reconsider e = FuncUnit X as Element of (C_Normed_Algebra_of_BoundedLinearOperators X) ;
for x being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) holds
( x * e = x & e * x = x ) by Lm5;
hence 1. (C_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X by GROUP_1:def 5; :: thesis: verum
end;

theorem Th19: :: CLOPBAN2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & ex t being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) & (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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace holds
( 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 ComplexAlgebra-like & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexLinearSpace-like )
proof end;

registration
cluster non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like associative ComplexAlgebra-like strict Normed_Complex_AlgebraStr ;
existence
ex b1 being non empty Normed_Complex_AlgebraStr st
( b1 is ComplexNormSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is ComplexAlgebra-like & b1 is ComplexLinearSpace-like & b1 is strict )
proof end;
end;

definition
mode Normed_Complex_Algebra is non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like associative ComplexAlgebra-like Normed_Complex_AlgebraStr ;
end;

registration
let X be ComplexNormSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators X -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like unital associative ComplexAlgebra-like strict ;
correctness
coherence
( 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 ComplexAlgebra-like & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexLinearSpace-like );
by Th20;
end;

definition
let X be non empty Normed_Complex_AlgebraStr ;
attr X is Banach_Algebra-like_1 means :: CLOPBAN2:def 9
for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||;
attr X is Banach_Algebra-like_2 means :: CLOPBAN2:def 10
||.(1. X).|| = 1;
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);
end;

:: 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.|| );

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

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

definition
let X be Normed_Complex_Algebra;
attr X is Banach_Algebra-like means :Def12: :: 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 );
end;

:: deftheorem Def12 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 ) );

registration
cluster Banach_Algebra-like -> complete left-distributive left_unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Complex_AlgebraStr ;
coherence
for b1 being Normed_Complex_Algebra st b1 is Banach_Algebra-like holds
( b1 is Banach_Algebra-like_1 & b1 is Banach_Algebra-like_2 & b1 is Banach_Algebra-like_3 & b1 is left-distributive & b1 is left_unital & b1 is complete ) by Def12;
cluster complete left-distributive left_unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 -> Banach_Algebra-like Normed_Complex_AlgebraStr ;
coherence
for b1 being Normed_Complex_Algebra st b1 is Banach_Algebra-like_1 & b1 is Banach_Algebra-like_2 & b1 is Banach_Algebra-like_3 & b1 is left-distributive & b1 is left_unital & b1 is complete holds
b1 is Banach_Algebra-like by Def12;
end;

registration
let X be non trivial ComplexBanachSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators X -> non empty Abelian add-associative right_zeroed right_complementable ComplexLinearSpace-like ComplexNormSpace-like complete unital associative left-distributive left_unital ComplexAlgebra-like strict Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like ;
coherence
C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like
proof end;
end;

registration
cluster complete left-distributive left_unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Normed_Complex_AlgebraStr ;
existence
ex b1 being Normed_Complex_Algebra st b1 is Banach_Algebra-like
proof end;
end;

definition
mode Complex_Banach_Algebra is Banach_Algebra-like Normed_Complex_Algebra;
end;

theorem :: CLOPBAN2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace holds 1. (Ring_of_BoundedLinearOperators X) = FuncUnit X by Lm2;

theorem :: CLOPBAN2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace holds 1. (C_Algebra_of_BoundedLinearOperators X) = FuncUnit X by Lm4;

theorem :: CLOPBAN2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexNormSpace holds 1. (C_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X by Lm6;