:: CLOPBAN2 semantic presentation

begin

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
proof
let X, Y, Z be ComplexLinearSpace; ::_thesis: for f being LinearOperator of X,Y
for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
let f be LinearOperator of X,Y; ::_thesis: for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z
let g be LinearOperator of Y,Z; ::_thesis: g * f is LinearOperator of X,Z
A1: now__::_thesis:_for_v_being_VECTOR_of_X
for_z_being_Complex_holds_(g_*_f)_._(z_*_v)_=_z_*_((g_*_f)_._v)
let v be VECTOR of X; ::_thesis: for z being Complex holds (g * f) . (z * v) = z * ((g * f) . v)
let z be Complex; ::_thesis: (g * f) . (z * v) = z * ((g * f) . v)
thus (g * f) . (z * v) = g . (f . (z * v)) by FUNCT_2:15
.= g . (z * (f . v)) by CLOPBAN1:def_3
.= z * (g . (f . v)) by CLOPBAN1:def_3
.= z * ((g * f) . v) by FUNCT_2:15 ; ::_thesis: verum
end;
now__::_thesis:_for_v,_w_being_VECTOR_of_X_holds_(g_*_f)_._(v_+_w)_=_((g_*_f)_._v)_+_((g_*_f)_._w)
let v, w be VECTOR of X; ::_thesis: (g * f) . (v + w) = ((g * f) . v) + ((g * f) . w)
thus (g * f) . (v + w) = g . (f . (v + w)) by FUNCT_2:15
.= g . ((f . v) + (f . w)) by VECTSP_1:def_20
.= (g . (f . v)) + (g . (f . w)) by VECTSP_1:def_20
.= ((g * f) . v) + (g . (f . w)) by FUNCT_2:15
.= ((g * f) . v) + ((g * f) . w) by FUNCT_2:15 ; ::_thesis: verum
end;
hence  g * f is LinearOperator of X,Z by A1, CLOPBAN1:def_3, VECTSP_1:def_20; ::_thesis: verum
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) ) ) )
proof
let X, Y, Z be ComplexNormSpace; ::_thesis: 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) ) ) )
let f be Lipschitzian LinearOperator of X,Y; ::_thesis: 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) ) ) )
let g be Lipschitzian LinearOperator of Y,Z; ::_thesis: ( 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) ) ) )
reconsider ff = f as Point of (C_NormSpace_of_BoundedLinearOperators (X,Y)) by CLOPBAN1:def_7;
reconsider gg = g as Point of (C_NormSpace_of_BoundedLinearOperators (Y,Z)) by CLOPBAN1:def_7;
A1: now__::_thesis:_for_v_being_VECTOR_of_X_holds_||.((g_*_f)_._v).||_<=_(||.gg.||_*_||.ff.||)_*_||.v.||
let v be VECTOR of X; ::_thesis: ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.||
 0 <= ||.gg.|| by CLVECT_1:105;
then A2: ||.gg.|| * ||.(f . v).|| <= ||.gg.|| * (||.ff.|| * ||.v.||) by CLOPBAN1:31, XREAL_1:64;
 ( ||.((g * f) . v).|| = ||.(g . (f . v)).|| & ||.(g . (f . v)).|| <= ||.gg.|| * ||.(f . v).|| ) by CLOPBAN1:31, FUNCT_2:15;
hence  ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.|| by A2, XXREAL_0:2; ::_thesis: verum
end;
set K = ||.gg.|| * ||.ff.||;
A3: ( 0 <= ||.gg.|| & 0 <= ||.ff.|| ) by CLVECT_1:105;
then reconsider gf = g * f as Lipschitzian LinearOperator of X,Z by A1, Th1, CLOPBAN1:def_6;
A4: now__::_thesis:_for_t_being_VECTOR_of_X_st_||.t.||_<=_1_holds_
||.((g_*_f)_._t).||_<=_||.gg.||_*_||.ff.||
let t be VECTOR of X; ::_thesis: ( ||.t.|| <= 1 implies ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.|| )
assume  ||.t.|| <= 1 ; ::_thesis: ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.||
then A5: (||.gg.|| * ||.ff.||) * ||.t.|| <= (||.gg.|| * ||.ff.||) * 1 by A3, XREAL_1:64;
 ||.((g * f) . t).|| <= (||.gg.|| * ||.ff.||) * ||.t.|| by A1;
hence  ||.((g * f) . t).|| <= ||.gg.|| * ||.ff.|| by A5, XXREAL_0:2; ::_thesis: verum
end;
A6: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_gf_holds_
r_<=_||.gg.||_*_||.ff.||
let r be Real; ::_thesis: ( r in PreNorms gf implies r <= ||.gg.|| * ||.ff.|| )
assume  r in PreNorms gf ; ::_thesis: r <= ||.gg.|| * ||.ff.||
then  ex t being VECTOR of X st
( r = ||.(gf . t).|| & ||.t.|| <= 1 ) ;
hence  r <= ||.gg.|| * ||.ff.|| by A4; ::_thesis: verum
end;
 ( ( for s being real number st s in PreNorms gf holds
s <= ||.gg.|| * ||.ff.|| ) implies upper_bound (PreNorms gf) <= ||.gg.|| * ||.ff.|| ) by SEQ_4:45;
hence  ( 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) ) ) ) by A1, A6, CLOPBAN1:29; ::_thesis: verum
end;

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

definition
let X be ComplexNormSpace;
let f, g be Element of BoundedLinearOperators (X,X);
funcf + 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);
funcg * 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_7;
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;
funcz * 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);
proof
reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2;
 (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f) is Element of BoundedLinearOperators (X,X) ;
hence  (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f) is Element of BoundedLinearOperators (X,X) ; ::_thesis: verum
end;
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
deffunc H1( Element of BoundedLinearOperators (X,X), Element of BoundedLinearOperators (X,X)) ->  Element of BoundedLinearOperators (X,X) = $1 * $2;
consider F being BinOp of (BoundedLinearOperators (X,X)) such that
A1: for x, y being Element of BoundedLinearOperators (X,X) holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  F ; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X) holds F . (f,g) = f * g
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: F . (f,g) = f * g
thus  F . (f,g) = f * g by A1; ::_thesis: verum
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
let it1, it2 be BinOp of (BoundedLinearOperators (X,X)); ::_thesis: ( ( for f, g being Element of BoundedLinearOperators (X,X) holds it1 . (f,g) = f * g ) & ( for f, g being Element of BoundedLinearOperators (X,X) holds it2 . (f,g) = f * g ) implies it1 = it2 )
assume that
A2: for f, g being Element of BoundedLinearOperators (X,X) holds it1 . (f,g) = f * g and
A3: for f, g being Element of BoundedLinearOperators (X,X) holds it2 . (f,g) = f * g ; ::_thesis: it1 = it2
now__::_thesis:_for_f,_g_being_Element_of_BoundedLinearOperators_(X,X)_holds_it1_._(f,g)_=_it2_._(f,g)
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: it1 . (f,g) = it2 . (f,g)
thus it1 . (f,g) = f * g by A2
.= it2 . (f,g) by A3 ; ::_thesis: verum
end;
hence  it1 = it2 by BINOP_1:2; ::_thesis: verum
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
for X being ComplexNormSpace holds id the carrier of X is Lipschitzian LinearOperator of X,X
proof
let X be ComplexNormSpace; ::_thesis: id the carrier of X is Lipschitzian LinearOperator of X,X
A1: now__::_thesis:_for_v,_w_being_VECTOR_of_X_holds_(id_the_carrier_of_X)_._(v_+_w)_=_((id_the_carrier_of_X)_._v)_+_((id_the_carrier_of_X)_._w)
let v, w be VECTOR of X; ::_thesis: (id the carrier of X) . (v + w) = ((id the carrier of X) . v) + ((id the carrier of X) . w)
thus (id the carrier of X) . (v + w) = v + w by FUNCT_1:18
.= ((id the carrier of X) . v) + w by FUNCT_1:18
.= ((id the carrier of X) . v) + ((id the carrier of X) . w) by FUNCT_1:18 ; ::_thesis: verum
end;
A2: now__::_thesis:_for_v_being_VECTOR_of_X
for_z_being_Complex_holds_(id_the_carrier_of_X)_._(z_*_v)_=_z_*_((id_the_carrier_of_X)_._v)
let v be VECTOR of X; ::_thesis: for z being Complex holds (id the carrier of X) . (z * v) = z * ((id the carrier of X) . v)
let z be Complex; ::_thesis: (id the carrier of X) . (z * v) = z * ((id the carrier of X) . v)
thus (id the carrier of X) . (z * v) = z * v by FUNCT_1:18
.= z * ((id the carrier of X) . v) by FUNCT_1:18 ; ::_thesis: verum
end;
 for v being VECTOR of X holds ||.((id the carrier of X) . v).|| <= 1 * ||.v.|| by FUNCT_1:18;
hence  id the carrier of X is Lipschitzian LinearOperator of X,X by A1, A2, CLOPBAN1:def_3, CLOPBAN1:def_6, VECTSP_1:def_20; ::_thesis: verum
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
 id the carrier of X is Lipschitzian LinearOperator of X,X by Th3;
hence  id the carrier of X is Element of BoundedLinearOperators (X,X) by CLOPBAN1:def_7; ::_thesis: verum
end;
end;

:: deftheorem  defines FuncUnit CLOPBAN2:def_5_:_
 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) )
proof
let X be ComplexNormSpace; ::_thesis: 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) )
let f, g, h be Lipschitzian LinearOperator of X,X; ::_thesis: ( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )
now__::_thesis:_(_(_for_x_being_VECTOR_of_X_holds_h_._x_=_f_._(g_._x)_)_implies_h_=_f_*_g_)
assume A1: for x being VECTOR of X holds h . x = f . (g . x) ; ::_thesis: h = f * g
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(f_*_g)_._x_=_h_._x
let x be VECTOR of X; ::_thesis: (f * g) . x = h . x
thus (f * g) . x = f . (g . x) by FUNCT_2:15
.= h . x by A1 ; ::_thesis: verum
end;
hence  h = f * g by FUNCT_2:63; ::_thesis: verum
end;
hence  ( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) ) by FUNCT_2:15; ::_thesis: verum
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
proof
let X be ComplexNormSpace; ::_thesis: for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h
let f, g, h be Lipschitzian LinearOperator of X,X; ::_thesis: f * (g * h) = (f * g) * h
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(f_*_(g_*_h))_._x_=_((f_*_g)_*_h)_._x
let x be VECTOR of X; ::_thesis: (f * (g * h)) . x = ((f * g) * h) . x
thus (f * (g * h)) . x = f . ((g * h) . x) by Th4
.= f . (g . (h . x)) by Th4
.= (f * g) . (h . x) by FUNCT_2:15
.= ((f * g) * h) . x by Th4 ; ::_thesis: verum
end;
hence  f * (g * h) = (f * g) * h by FUNCT_2:63; ::_thesis: verum
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 )
proof
let X be ComplexNormSpace; ::_thesis: for f being Lipschitzian LinearOperator of X,X holds
( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
reconsider ii = id the carrier of X as Lipschitzian LinearOperator of X,X by Th3;
let f be Lipschitzian LinearOperator of X,X; ::_thesis: ( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
A1: now__::_thesis:_for_x_being_VECTOR_of_X_holds_((id_the_carrier_of_X)_*_f)_._x_=_f_._x
let x be VECTOR of X; ::_thesis: ((id the carrier of X) * f) . x = f . x
thus ((id the carrier of X) * f) . x = (ii * f) . x
.= ii . (f . x) by Th4
.= f . x by FUNCT_1:18 ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_VECTOR_of_X_holds_(f_*_(id_the_carrier_of_X))_._x_=_f_._x
let x be VECTOR of X; ::_thesis: (f * (id the carrier of X)) . x = f . x
thus (f * (id the carrier of X)) . x = (f * ii) . x
.= f . (ii . x) by Th4
.= f . x by FUNCT_1:18 ; ::_thesis: verum
end;
hence  ( f * (id the carrier of X) = f & (id the carrier of X) * f = f ) by A1, FUNCT_2:63; ::_thesis: verum
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
proof
let X be ComplexNormSpace; ::_thesis: for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h
let f, g, h be Element of BoundedLinearOperators (X,X); ::_thesis: f * (g * h) = (f * g) * h
 modetrans ((g * h),X,X) = (modetrans (g,X,X)) * (modetrans (h,X,X)) by CLOPBAN1:def_9;
then  (modetrans (f,X,X)) * (modetrans ((g * h),X,X)) = ((modetrans (f,X,X)) * (modetrans (g,X,X))) * (modetrans (h,X,X)) by Th5;
hence  f * (g * h) = (f * g) * h by CLOPBAN1:def_9; ::_thesis: verum
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 )
proof
let X be ComplexNormSpace; ::_thesis: for f being Element of BoundedLinearOperators (X,X) holds
( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
let f be Element of BoundedLinearOperators (X,X); ::_thesis: ( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
 id the carrier of X is Lipschitzian LinearOperator of X,X by Th3;
then  id the carrier of X is Element of BoundedLinearOperators (X,X) by CLOPBAN1:def_7;
then A1: modetrans ((id the carrier of X),X,X) = id the carrier of X by CLOPBAN1:def_9;
hence f * (FuncUnit X) = modetrans (f,X,X) by Th6
.= f by CLOPBAN1:def_9 ;
::_thesis: (FuncUnit X) * f = f
thus (FuncUnit X) * f = modetrans (f,X,X) by A1, Th6
.= f by CLOPBAN1:def_9 ; ::_thesis: verum
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)
proof
let X be ComplexNormSpace; ::_thesis: for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)
let f, g, h be Element of BoundedLinearOperators (X,X); ::_thesis: f * (g + h) = (f * g) + (f * h)
set BLOP = C_NormSpace_of_BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set mf = modetrans (f,X,X);
set mg = modetrans (g,X,X);
set mh = modetrans (h,X,X);
set mgh = modetrans ((g + h),X,X);
 (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (f,X,X)) * (modetrans (g,X,X))),((modetrans (f,X,X)) * (modetrans (h,X,X)))) = (modetrans (f,X,X)) * (modetrans ((g + h),X,X))
proof
reconsider fh = (modetrans (f,X,X)) * (modetrans (h,X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider k = (modetrans (f,X,X)) * (modetrans ((g + h),X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider hh = h as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider gg = g as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: ( gg = modetrans (g,X,X) & hh = modetrans (h,X,X) ) by CLOPBAN1:def_9;
 for x being VECTOR of X holds ((modetrans (f,X,X)) * (modetrans ((g + h),X,X))) . x = (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + (((modetrans (f,X,X)) * (modetrans (h,X,X))) . x)
proof
let x be VECTOR of X; ::_thesis: ((modetrans (f,X,X)) * (modetrans ((g + h),X,X))) . x = (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + (((modetrans (f,X,X)) * (modetrans (h,X,X))) . x)
 ( g + h = gg + hh & modetrans ((g + h),X,X) = g + h ) by CLOPBAN1:def_9;
then A2: (modetrans ((g + h),X,X)) . x = ((modetrans (g,X,X)) . x) + ((modetrans (h,X,X)) . x) by A1, CLOPBAN1:34;
thus ((modetrans (f,X,X)) * (modetrans ((g + h),X,X))) . x = (modetrans (f,X,X)) . ((modetrans ((g + h),X,X)) . x) by Th4
.= ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x)) + ((modetrans (f,X,X)) . ((modetrans (h,X,X)) . x)) by A2, VECTSP_1:def_20
.= (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + ((modetrans (f,X,X)) . ((modetrans (h,X,X)) . x)) by Th4
.= (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + (((modetrans (f,X,X)) * (modetrans (h,X,X))) . x) by Th4 ; ::_thesis: verum
end;
then  k = fg + fh by CLOPBAN1:34;
hence  (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (f,X,X)) * (modetrans (g,X,X))),((modetrans (f,X,X)) * (modetrans (h,X,X)))) = (modetrans (f,X,X)) * (modetrans ((g + h),X,X)) ; ::_thesis: verum
end;
hence  f * (g + h) = (f * g) + (f * h) ; ::_thesis: verum
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)
proof
let X be ComplexNormSpace; ::_thesis: for f, g, h being Element of BoundedLinearOperators (X,X) holds (g + h) * f = (g * f) + (h * f)
let f, g, h be Element of BoundedLinearOperators (X,X); ::_thesis: (g + h) * f = (g * f) + (h * f)
set BLOP = C_NormSpace_of_BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set mf = modetrans (f,X,X);
set mg = modetrans (g,X,X);
set mh = modetrans (h,X,X);
set mgh = modetrans ((g + h),X,X);
 (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (g,X,X)) * (modetrans (f,X,X))),((modetrans (h,X,X)) * (modetrans (f,X,X)))) = (modetrans ((g + h),X,X)) * (modetrans (f,X,X))
proof
reconsider hf = (modetrans (h,X,X)) * (modetrans (f,X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider gf = (modetrans (g,X,X)) * (modetrans (f,X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider k = (modetrans ((g + h),X,X)) * (modetrans (f,X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider hh = h as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider gg = g as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: ( gg = modetrans (g,X,X) & hh = modetrans (h,X,X) ) by CLOPBAN1:def_9;
 for x being VECTOR of X holds ((modetrans ((g + h),X,X)) * (modetrans (f,X,X))) . x = (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + (((modetrans (h,X,X)) * (modetrans (f,X,X))) . x)
proof
let x be VECTOR of X; ::_thesis: ((modetrans ((g + h),X,X)) * (modetrans (f,X,X))) . x = (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + (((modetrans (h,X,X)) * (modetrans (f,X,X))) . x)
 ( g + h = gg + hh & modetrans ((g + h),X,X) = g + h ) by CLOPBAN1:def_9;
then A2: (modetrans ((g + h),X,X)) . ((modetrans (f,X,X)) . x) = ((modetrans (g,X,X)) . ((modetrans (f,X,X)) . x)) + ((modetrans (h,X,X)) . ((modetrans (f,X,X)) . x)) by A1, CLOPBAN1:34;
thus ((modetrans ((g + h),X,X)) * (modetrans (f,X,X))) . x = (modetrans ((g + h),X,X)) . ((modetrans (f,X,X)) . x) by Th4
.= (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + ((modetrans (h,X,X)) . ((modetrans (f,X,X)) . x)) by A2, Th4
.= (((modetrans (g,X,X)) * (modetrans (f,X,X))) . x) + (((modetrans (h,X,X)) * (modetrans (f,X,X))) . x) by Th4 ; ::_thesis: verum
end;
then  k = gf + hf by CLOPBAN1:34;
hence  (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (((modetrans (g,X,X)) * (modetrans (f,X,X))),((modetrans (h,X,X)) * (modetrans (f,X,X)))) = (modetrans ((g + h),X,X)) * (modetrans (f,X,X)) ; ::_thesis: verum
end;
hence  (g + h) * f = (g * f) + (h * f) ; ::_thesis: verum
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)
proof
let X be ComplexNormSpace; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X)
for a, b being Complex holds (a * b) * (f * g) = (a * f) * (b * g)
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: for a, b being Complex holds (a * b) * (f * g) = (a * f) * (b * g)
let a, b be Complex; ::_thesis: (a * b) * (f * g) = (a * f) * (b * g)
set BLOP = C_NormSpace_of_BoundedLinearOperators (X,X);
set EXMULT = Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set mf = modetrans (f,X,X);
set mg = modetrans (g,X,X);
set maf = modetrans ((a * f),X,X);
set mbg = modetrans ((b * g),X,X);
 (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((a * b),((modetrans (f,X,X)) * (modetrans (g,X,X)))) = (modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))
proof
reconsider k = (modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) by CLOPBAN1:def_7;
reconsider ff = f, gg = g as VECTOR of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: gg = modetrans (g,X,X) by CLOPBAN1:def_9;
A2: ff = modetrans (f,X,X) by CLOPBAN1:def_9;
 for x being VECTOR of X holds ((modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))) . x = (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x)
proof
let x be VECTOR of X; ::_thesis: ((modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))) . x = (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x)
set y = b * ((modetrans (g,X,X)) . x);
 ( a * f = a * ff & modetrans ((a * f),X,X) = a * f ) by CLOPBAN1:def_9;
then A3: (modetrans ((a * f),X,X)) . (b * ((modetrans (g,X,X)) . x)) = a * ((modetrans (f,X,X)) . (b * ((modetrans (g,X,X)) . x))) by A2, CLOPBAN1:35;
 ( b * g = b * gg & modetrans ((b * g),X,X) = b * g ) by CLOPBAN1:def_9;
then A4: (modetrans ((b * g),X,X)) . x = b * ((modetrans (g,X,X)) . x) by A1, CLOPBAN1:35;
thus ((modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X))) . x = (modetrans ((a * f),X,X)) . ((modetrans ((b * g),X,X)) . x) by Th4
.= a * (b * ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x))) by A3, A4, CLOPBAN1:def_3
.= (a * b) * ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x)) by CLVECT_1:def_4
.= (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) by Th4 ; ::_thesis: verum
end;
then  k = (a * b) * fg by CLOPBAN1:35;
hence  (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((a * b),((modetrans (f,X,X)) * (modetrans (g,X,X)))) = (modetrans ((a * f),X,X)) * (modetrans ((b * g),X,X)) ; ::_thesis: verum
end;
hence  (a * b) * (f * g) = (a * f) * (b * g) ; ::_thesis: verum
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
proof
let X be ComplexNormSpace; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X)
for a being Complex holds a * (f * g) = (a * f) * g
let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: for a being Complex holds a * (f * g) = (a * f) * g
let a be Complex; ::_thesis: a * (f * g) = (a * f) * g
set RRL = CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider gg = g as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
A1: 1r * g = 1r * gg
.= g by CLVECT_1:def_5 ;
a * (f * g) = (a * 1r) * (f * g) by COMPLEX1:def_4
.= (a * f) * (1r * g) by Th11 ;
hence  a * (f * g) = (a * f) * g by A1; ::_thesis: verum
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 ) ;
end;

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

registration
let X be ComplexNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  unital ;
coherence
 Ring_of_BoundedLinearOperators X is unital
proof
reconsider e = FuncUnit X as Element of (Ring_of_BoundedLinearOperators X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (Ring_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (Ring_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm1; ::_thesis: verum
end;
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) )
proof
let X be ComplexNormSpace; ::_thesis: 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) )
let x, y, z be Element of (Ring_of_BoundedLinearOperators X); ::_thesis: ( 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) )
set RBLOP = Ring_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set RRL = CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider f = x, g = y, h = z as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: ( (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) )
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: ( 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) )
thus x + (0. (Ring_of_BoundedLinearOperators X)) = f + (0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: ( 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) )
thus  ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) :: according to ALGSTR_0:def_11 ::_thesis: ( (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
consider s being Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (Ring_of_BoundedLinearOperators X) ;
take  t ; ::_thesis: x + t = 0. (Ring_of_BoundedLinearOperators X)
thus  x + t = 0. (Ring_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: ( 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) )
thus x * (1. (Ring_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: ( (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus (1. (Ring_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; ::_thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: (y + z) * x = (y * x) + (z * x)
thus (y + z) * x = (yy + zz) * xx by Def4
.= (yy * xx) + (zz * xx) by Th10
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4
.= (y * x) + (z * x) by Def4 ; ::_thesis: verum
end;

theorem Th14: :: CLOPBAN2:14
for X being ComplexNormSpace holds Ring_of_BoundedLinearOperators X is Ring
proof
let X be ComplexNormSpace; ::_thesis: Ring_of_BoundedLinearOperators X is Ring
 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) ) by Th13;
hence  Ring_of_BoundedLinearOperators X is Ring by ALGSTR_0:def_16, GROUP_1:def_3, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, VECTSP_1:def_6, VECTSP_1:def_7; ::_thesis: verum
end;

registration
let X be ComplexNormSpace;
cluster Ring_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed associative well-unital distributive ;
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;
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 ) ;
end;

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

registration
let X be ComplexNormSpace;
cluster C_Algebra_of_BoundedLinearOperators X ->  unital ;
coherence
 C_Algebra_of_BoundedLinearOperators X is unital
proof
reconsider e = FuncUnit X as Element of (C_Algebra_of_BoundedLinearOperators X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (C_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (C_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm2; ::_thesis: verum
end;
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) )
proof
let X be ComplexNormSpace; ::_thesis: 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) )
let x, y, z be Element of (C_Algebra_of_BoundedLinearOperators X); ::_thesis: 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) )
let a, b be Complex; ::_thesis: ( 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) )
set RBLOP = C_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set RRL = CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider f = x, g = y, h = z as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: ( (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) )
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: ( 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) )
thus x + (0. (C_Algebra_of_BoundedLinearOperators X)) = f + (0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: ( 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) )
thus  ex t being Element of (C_Algebra_of_BoundedLinearOperators X) st x + t = 0. (C_Algebra_of_BoundedLinearOperators X) :: according to ALGSTR_0:def_11 ::_thesis: ( (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
consider s being Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (C_Algebra_of_BoundedLinearOperators X) ;
take  t ; ::_thesis: x + t = 0. (C_Algebra_of_BoundedLinearOperators X)
thus  x + t = 0. (C_Algebra_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: ( 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) )
thus x * (1. (C_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: ( (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) )
thus (1. (C_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; ::_thesis: ( 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) )
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: ( (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) )
thus (y + z) * x = (yy + zz) * xx by Def4
.= (yy * xx) + (zz * xx) by Th10
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4
.= (y * x) + (z * x) by Def4 ; ::_thesis: ( 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) )
thus a * (x * y) = a * (xx * yy) by Def4
.= (a * xx) * yy by Th12
.= (a * x) * y by Def4 ; ::_thesis: ( 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) )
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by CLVECT_1:def_2
.= (a * x) + (a * y) ; ::_thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by CLVECT_1:def_3
.= (a * x) + (b * x) ; ::_thesis: ( (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (a * b) * x = (a * b) * f
.= a * (b * f) by CLVECT_1:def_4
.= a * (b * x) ; ::_thesis: (a * b) * (x * y) = (a * x) * (b * y)
thus (a * b) * (x * y) = (a * b) * (xx * yy) by Def4
.= (a * xx) * (b * yy) by Th11
.= (a * x) * (b * y) by Def4 ; ::_thesis: verum
end;

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

registration
let X be ComplexNormSpace;
cluster C_Algebra_of_BoundedLinearOperators X ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative associative right-distributive right_unital vector-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
set A = C_Algebra_of_BoundedLinearOperators X;
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set RRL = CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);
thus  C_Algebra_of_BoundedLinearOperators X is Abelian ::_thesis: ( 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
let x, y be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x
reconsider f = x, g = y as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is add-associative ::_thesis: ( 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
let x, y, z be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_3 ::_thesis: (x + y) + z = x + (y + z)
reconsider f = x, g = y, h = z as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is right_zeroed ::_thesis: ( 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
let x be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (C_Algebra_of_BoundedLinearOperators X)) = x
reconsider f = x as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + (0. (C_Algebra_of_BoundedLinearOperators X)) = f + (0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is right_complementable ::_thesis: ( 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
let x be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
reconsider f = x as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
consider s being Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (C_Algebra_of_BoundedLinearOperators X) ;
take  t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (C_Algebra_of_BoundedLinearOperators X)
thus  x + t = 0. (C_Algebra_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is associative ::_thesis: ( 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
let x, y, z be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is right_unital ::_thesis: ( 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
let x be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_4 ::_thesis: x * (1. (C_Algebra_of_BoundedLinearOperators X)) = x
reconsider xx = x as Element of BoundedLinearOperators (X,X) ;
thus x * (1. (C_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is right-distributive ::_thesis: ( 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
let x, y, z be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_2 ::_thesis: x * (y + z) = (x * y) + (x * z)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is vector-distributive ::_thesis: ( 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
let a be Complex; :: according to CLVECT_1:def_2 ::_thesis: for b1, b2 being Element of the carrier of (C_Algebra_of_BoundedLinearOperators X) holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of (C_Algebra_of_BoundedLinearOperators X); ::_thesis: a * (x + y) = (a * x) + (a * y)
reconsider f = x, g = y as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by CLVECT_1:def_2
.= (a * x) + (a * y) ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is scalar-distributive ::_thesis: ( C_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Algebra_of_BoundedLinearOperators X is vector-associative )
proof
let a, b be Complex; :: according to CLVECT_1:def_3 ::_thesis: for b1 being Element of the carrier of (C_Algebra_of_BoundedLinearOperators X) holds (a + b) * b1 = (a * b1) + (b * b1)
let x be Element of (C_Algebra_of_BoundedLinearOperators X); ::_thesis: (a + b) * x = (a * x) + (b * x)
reconsider f = x as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by CLVECT_1:def_3
.= (a * x) + (b * x) ; ::_thesis: verum
end;
thus  C_Algebra_of_BoundedLinearOperators X is scalar-associative ::_thesis: C_Algebra_of_BoundedLinearOperators X is vector-associative
proof
let a, b be Complex; :: according to CLVECT_1:def_4 ::_thesis: for b1 being Element of the carrier of (C_Algebra_of_BoundedLinearOperators X) holds (a * b) * b1 = a * (b * b1)
let x be Element of (C_Algebra_of_BoundedLinearOperators X); ::_thesis: (a * b) * x = a * (b * x)
reconsider f = x as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (a * b) * x = (a * b) * f
.= a * (b * f) by CLVECT_1:def_4
.= a * (b * x) ; ::_thesis: verum
end;
let x, y be Element of (C_Algebra_of_BoundedLinearOperators X); :: according to CFUNCDOM:def_9 ::_thesis: for b1 being Element of COMPLEX holds b1 * (x * y) = (b1 * x) * y
let a be Element of COMPLEX ; ::_thesis: a * (x * y) = (a * x) * y
reconsider xx = x, yy = y as Element of BoundedLinearOperators (X,X) ;
thus a * (x * y) = a * (xx * yy) by Def4
.= (a * xx) * yy by Th12
.= (a * x) * y by Def4 ; ::_thesis: verum
end;
end;

theorem :: CLOPBAN2:16
for X being ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators X is ComplexBLAlgebra ;

registration
cluster Complex_l1_Space  ->  complete ;
coherence
 Complex_l1_Space is complete
proof
thus  for vseq being sequence of Complex_l1_Space st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent by CSSPACE3:9; :: according to CLOPBAN1:def_13 ::_thesis: verum
end;
end;

registration
cluster Complex_l1_Space  ->  non trivial ;
coherence
 not Complex_l1_Space is trivial
proof
reconsider a = (1 / 2) + (0 * <i>) as Element of COMPLEX ;
reconsider x = a GeoSeq as Complex_Sequence ;
A1: for m being Element of NAT holds |.x.| . (m + 1) = (|.x.| . m) * |.a.|
proof
let m be Element of NAT ; ::_thesis: |.x.| . (m + 1) = (|.x.| . m) * |.a.|
|.x.| . (m + 1) = |.(x . (m + 1)).| by VALUED_1:18
.= |.((x . m) * a).| by COMSEQ_3:def_1
.= |.(x . m).| * |.a.| by COMPLEX1:65 ;
hence  |.x.| . (m + 1) = (|.x.| . m) * |.a.| by VALUED_1:18; ::_thesis: verum
end;
|.x.| . 0 = |.(x . 0).| by VALUED_1:18
.= 1 by COMPLEX1:48, COMSEQ_3:def_1 ;
then  ( |.a.| = 1 / 2 & |.x.| = |.a.| GeoSeq ) by A1, ABSVALUE:def_1, PREPOWER:3;
then  |.x.| is summable by SERIES_1:24;
then  x is absolutely_summable by COMSEQ_3:def_9;
then  seq_id x is absolutely_summable by CSSPACE:1;
then reconsider v = x as VECTOR of Complex_l1_Space by CSSPACE3:6;
(seq_id v) . 0 = x . 0 by CSSPACE:1
.= 1 by COMPLEX1:def_4, COMSEQ_3:def_1 ;
then  v <> CZeroseq by CSSPACE:def_6;
hence  not Complex_l1_Space is trivial by CSSPACE3:6, STRUCT_0:def_18; ::_thesis: verum
end;
end;

registration
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 b1 being ComplexBanachSpace holds b1 is trivial
proof
take  Complex_l1_Space ; ::_thesis: not Complex_l1_Space is trivial
thus  not Complex_l1_Space is trivial ; ::_thesis: verum
end;
end;

theorem Th17: :: CLOPBAN2:17
for X being non trivial ComplexNormSpace ex w being VECTOR of X st ||.w.|| = 1
proof
let X be non trivial ComplexNormSpace; ::_thesis: ex w being VECTOR of X st ||.w.|| = 1
consider v being VECTOR of X such that
A1: v <> 0. X by STRUCT_0:def_18;
reconsider a = ||.v.|| + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def_2;
take w = (a ") * v; ::_thesis: ||.w.|| = 1
A2: ||.v.|| <> 0 by A1, NORMSP_0:def_5;
then A3: 0 < ||.v.|| by CLVECT_1:105;
A4: |.(a ").| = |.(1r * (a ")).| by COMPLEX1:def_4
.= |.(1r / a).| by XCMPLX_0:def_9
.= 1 / |.a.| by COMPLEX1:48, COMPLEX1:67
.= 1 * (|.a.| ") by XCMPLX_0:def_9
.= ||.v.|| " by A3, ABSVALUE:def_1 ;
thus ||.w.|| = |.(a ").| * ||.v.|| by CLVECT_1:def_13
.= 1 by A2, A4, XCMPLX_0:def_7 ; ::_thesis: verum
end;

theorem Th18: :: CLOPBAN2:18
for X being non trivial ComplexNormSpace holds (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1
proof
let X be non trivial ComplexNormSpace; ::_thesis: (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1
consider v being VECTOR of X such that
A1: ||.v.|| = 1 by Th17;
reconsider ii = id the carrier of X as Lipschitzian LinearOperator of X,X by Th3;
A2: now__::_thesis:_for_r_being_Real_st_r_in_PreNorms_ii_holds_
r_<=_1
let r be Real; ::_thesis: ( r in PreNorms ii implies r <= 1 )
assume  r in PreNorms ii ; ::_thesis: r <= 1
then  ex t being VECTOR of X st
( r = ||.(ii . t).|| & ||.t.|| <= 1 ) ;
hence  r <= 1 by FUNCT_1:18; ::_thesis: verum
end;
 ii . v = v by FUNCT_1:18;
then A3: 1 in  {  ||.(ii . t).|| where t is VECTOR of X : ||.t.|| <= 1  }  by A1;
 ( not PreNorms ii is empty & PreNorms ii is bounded_above ) by CLOPBAN1:26;
then A4: 1 <= upper_bound (PreNorms ii) by A3, SEQ_4:def_1;
 ( ( for s being real number st s in PreNorms ii holds
s <= 1 ) implies upper_bound (PreNorms ii) <= 1 ) by SEQ_4:45;
then  upper_bound (PreNorms ii) = 1 by A2, A4, XXREAL_0:1;
hence  (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1 by CLOPBAN1:29; ::_thesis: verum
end;

definition
attrc1 is strict ;
struct Normed_Complex_AlgebraStr  ->  ComplexAlgebraStr , CNORMSTR ;
aggrNormed_Complex_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) ->  Normed_Complex_AlgebraStr ;
end;

registration
cluster non empty for Normed_Complex_AlgebraStr ;
existence
 not for b1 being Normed_Complex_AlgebraStr holds b1 is empty
proof
set A = the non empty set ;
set m = the BinOp of the non empty set ;
set a = the BinOp of the non empty set ;
set M = the Function of [:COMPLEX, the non empty set :], the non empty set ;
set U = the Element of the non empty set ;
set Z = the Element of the non empty set ;
set n = the Function of the non empty set ,REAL;
take  Normed_Complex_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set , the Function of the non empty set ,REAL #) ; ::_thesis: not Normed_Complex_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set , the Function of the non empty set ,REAL #) is empty
thus  not the carrier of Normed_Complex_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:COMPLEX, the non empty set :], the non empty set , the Element of the non empty set , the Element of the non empty set , the Function of the non empty set ,REAL #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
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 ) ;
end;

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

registration
let X be ComplexNormSpace;
cluster C_Normed_Algebra_of_BoundedLinearOperators X ->  unital ;
coherence
 C_Normed_Algebra_of_BoundedLinearOperators X is unital
proof
reconsider e = FuncUnit X as Element of (C_Normed_Algebra_of_BoundedLinearOperators X) ;
take  e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (C_Normed_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 )
thus  for b1 being Element of the carrier of (C_Normed_Algebra_of_BoundedLinearOperators X) holds
( b1 * e = b1 & e * b1 = b1 ) by Lm3; ::_thesis: verum
end;
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 )
proof
let X be ComplexNormSpace; ::_thesis: 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 )
let x, y, z be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: 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 )
let a, b be Complex; ::_thesis: ( 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 )
set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set RRL = CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider f = x, g = y, h = z as Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; ::_thesis: ( (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 )
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def_3
.= x + (y + z) ; ::_thesis: ( 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 )
thus x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = f + (0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #))
.= x by RLVECT_1:def_4 ; ::_thesis: ( 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 )
thus  ex t being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) :: according to ALGSTR_0:def_11 ::_thesis: ( (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
consider s being Element of CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. CLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11;
reconsider t = s as Element of (C_Normed_Algebra_of_BoundedLinearOperators X) ;
take  t ; ::_thesis: x + t = 0. (C_Normed_Algebra_of_BoundedLinearOperators X)
thus  x + t = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) by A1; ::_thesis: verum
end;
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; ::_thesis: ( 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 )
thus x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; ::_thesis: ( (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 )
thus (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; ::_thesis: ( 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 )
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; ::_thesis: ( (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 )
thus (y + z) * x = (yy + zz) * xx by Def4
.= (yy * xx) + (zz * xx) by Th10
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4
.= (y * x) + (z * x) by Def4 ; ::_thesis: ( 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 )
thus a * (x * y) = a * (xx * yy) by Def4
.= (a * xx) * yy by Th12
.= (a * x) * y by Def4 ; ::_thesis: ( (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 )
thus (a * b) * (x * y) = (a * b) * (xx * yy) by Def4
.= (a * xx) * (b * yy) by Th11
.= (a * x) * (b * y) by Def4 ; ::_thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1r * x = x )
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by CLVECT_1:def_2
.= (a * x) + (a * y) ; ::_thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1r * x = x )
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by CLVECT_1:def_3
.= (a * x) + (b * x) ; ::_thesis: ( (a * b) * x = a * (b * x) & 1r * x = x )
thus (a * b) * x = (a * b) * f
.= a * (b * f) by CLVECT_1:def_4
.= a * (b * x) ; ::_thesis: 1r * x = x
thus 1r * x = 1r * f
.= x by CLVECT_1:def_5 ; ::_thesis: verum
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 )
proof
let X be ComplexNormSpace; ::_thesis: ( 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 )
set C = C_Normed_Algebra_of_BoundedLinearOperators X;
set BS = C_NormSpace_of_BoundedLinearOperators (X,X);
thus  C_Normed_Algebra_of_BoundedLinearOperators X is reflexive ::_thesis: ( 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
thus ||.(0. (C_Normed_Algebra_of_BoundedLinearOperators X)).|| = ||.(0. (C_NormSpace_of_BoundedLinearOperators (X,X))).||
.= 0 ; :: according to NORMSP_0:def_6 ::_thesis: verum
end;
thus  C_Normed_Algebra_of_BoundedLinearOperators X is discerning ::_thesis: ( 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
let x be Point of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to NORMSP_0:def_5 ::_thesis: ( not ||.x.|| = 0 or x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) )
reconsider y = x as Point of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
assume  ||.x.|| = 0 ; ::_thesis: x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X)
then  ||.y.|| = 0 ;
then  y = 0. (C_NormSpace_of_BoundedLinearOperators (X,X)) by NORMSP_0:def_5;
hence  x = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) ; ::_thesis: verum
end;
thus  C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like ::_thesis: ( 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
let x, y be Point of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to CLVECT_1:def_13 ::_thesis: for b1 being set holds
( ||.(b1 * x).|| = |.b1.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Complex; ::_thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider x1 = x, y1 = y as Point of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
A1: ||.x1.|| = ||.x.|| ;
thus ||.(a * x).|| = ||.(a * x1).||
.= |.a.| * ||.x.|| by A1, CLVECT_1:def_13 ; ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
 ( ||.(x + y).|| = ||.(x1 + y1).|| & ||.x1.|| + ||.y1.|| = ||.x.|| + ||.y.|| ) ;
hence  ||.(x + y).|| <= ||.x.|| + ||.y.|| by CLVECT_1:def_13; ::_thesis: verum
end;
set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
A2: C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable
proof
let x be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable
thus  x is right_complementable by Th19; ::_thesis: verum
end;
A3: ( ( for a, b being Complex
for v being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds (a + b) * v = (a * v) + (b * v) ) & ( for a, b being Complex
for v being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds (a * b) * v = a * (b * v) ) ) by Th19;
 ( ( for x, y, z being Element of (C_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being Element of 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 a being Complex
for v, w being VECTOR of (C_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) ) by Th19;
hence  ( 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 ) by A2, A3, CFUNCDOM:def_9, CLVECT_1:def_2, CLVECT_1:def_3, CLVECT_1:def_4, CLVECT_1:def_5, GROUP_1:def_3, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, VECTSP_1:def_2, VECTSP_1:def_4; ::_thesis: verum
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like associative right-distributive right_unital vector-associative strict for Normed_Complex_AlgebraStr ;
existence
 ex b1 being non empty Normed_Complex_AlgebraStr st
( b1 is reflexive & b1 is discerning & b1 is ComplexNormSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is associative & b1 is right_unital & b1 is right-distributive & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is vector-associative & b1 is scalar-unital & b1 is strict )
proof
set X = the ComplexNormSpace;
take  C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace ; ::_thesis: ( C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is reflexive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is discerning & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is Abelian & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is add-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_unital & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-unital & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is strict )
thus  ( C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is reflexive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is discerning & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is Abelian & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is add-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_unital & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-unital & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is strict ) by Th20; ::_thesis: verum
end;
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 associative right-distributive right_unital vector-associative Normed_Complex_AlgebraStr ;
end;

registration
let X be ComplexNormSpace;
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 associative right-distributive right_unital vector-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;
end;

definition
let X be non empty Normed_Complex_AlgebraStr ;
attrX is Banach_Algebra-like_1  means :: CLOPBAN2:def 9
 for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||;
attrX is Banach_Algebra-like_2  means :Def10: :: CLOPBAN2:def 10
||.(1. X).|| = 1;
attrX 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 Def10 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;
attrX 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 non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like associative right-distributive right_unital vector-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 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 non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like associative right-distributive left-distributive right_unital left_unital complete vector-associative Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3  ->  Banach_Algebra-like for 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 ->  Banach_Algebra-like ;
coherence
 C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like
proof
set NRM = BoundedLinearOperatorsNorm (X,X);
set UNIT = FuncUnit X;
set MULT = FuncMult X;
set ADD = Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)));
set BS = C_NormSpace_of_BoundedLinearOperators (X,X);
set BLOP = BoundedLinearOperators (X,X);
set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
thus  C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_1 :: according to CLOPBAN2:def_12 ::_thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 & C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
proof
let x, y be Point of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to CLOPBAN2:def_9 ::_thesis: ||.(x * y).|| <= ||.x.|| * ||.y.||
reconsider x1 = x, y1 = y as Element of BoundedLinearOperators (X,X) ;
A1: ((BoundedLinearOperatorsNorm (X,X)) . (modetrans (x1,X,X))) * ((BoundedLinearOperatorsNorm (X,X)) . (modetrans (y1,X,X))) = ((BoundedLinearOperatorsNorm (X,X)) . x1) * ((BoundedLinearOperatorsNorm (X,X)) . (modetrans (y1,X,X))) by CLOPBAN1:def_9
.= ||.x.|| * ||.y.|| by CLOPBAN1:def_9 ;
||.(x * y).|| = (BoundedLinearOperatorsNorm (X,X)) . (x1 * y1) by Def4
.= (BoundedLinearOperatorsNorm (X,X)) . ((modetrans (x1,X,X)) * (modetrans (y1,X,X))) ;
hence  ||.(x * y).|| <= ||.x.|| * ||.y.|| by A1, Th2; ::_thesis: verum
end;
 ||.(1. (C_Normed_Algebra_of_BoundedLinearOperators X)).|| = 1 by Th18;
hence  C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 by Def10; ::_thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
thus  C_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 ::_thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is left_unital & C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
proof
let a be Complex; :: according to CLOPBAN2:def_11 ::_thesis: for x, y being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) holds a * (x * y) = x * (a * y)
let x, y be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: a * (x * y) = x * (a * y)
thus a * (x * y) = (1r * a) * (x * y) by COMPLEX1:def_4
.= (1r * x) * (a * y) by Th19
.= x * (a * y) by Th19 ; ::_thesis: verum
end;
thus  C_Normed_Algebra_of_BoundedLinearOperators X is left_unital ::_thesis: ( C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is complete )
proof
let x be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_8 ::_thesis: (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) * x = x
reconsider xx = x as Element of BoundedLinearOperators (X,X) ;
thus (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; ::_thesis: verum
end;
thus  C_Normed_Algebra_of_BoundedLinearOperators X is left-distributive ::_thesis: C_Normed_Algebra_of_BoundedLinearOperators X is complete
proof
let x, y, z be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_3 ::_thesis: (y + z) * x = (y * x) + (z * x)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (y + z) * x = (yy + zz) * xx by Def4
.= (yy * xx) + (zz * xx) by Th10
.= (Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4
.= (y * x) + (z * x) by Def4 ; ::_thesis: verum
end;
now__::_thesis:_for_seq_being_sequence_of_(C_Normed_Algebra_of_BoundedLinearOperators_X)_st_seq_is_Cauchy_sequence_by_Norm_holds_
seq_is_convergent
let seq be sequence of (C_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume A2: seq is Cauchy_sequence_by_Norm ; ::_thesis: seq is convergent
reconsider seq1 = seq as sequence of (C_NormSpace_of_BoundedLinearOperators (X,X)) ;
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seq1_._n)_-_(seq1_._m)).||_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r
then consider k being Element of NAT  such that
A3: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A2, CSSPACE3:8;
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
||.((seq1_._n)_-_(seq1_._m)).||_<_r
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((seq1 . n) - (seq1 . m)).|| < r )
assume A4: ( n >= k & m >= k ) ; ::_thesis: ||.((seq1 . n) - (seq1 . m)).|| < r
||.((seq1 . n) - (seq1 . m)).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1r) * (seq1 . m)))) by CLVECT_1:3
.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + ((- 1r) * (seq . m)))
.= ||.((seq . n) - (seq . m)).|| by CLVECT_1:3 ;
hence  ||.((seq1 . n) - (seq1 . m)).|| < r by A3, A4; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r ; ::_thesis: verum
end;
then  seq1 is Cauchy_sequence_by_Norm by CSSPACE3:8;
then  seq1 is convergent by CLOPBAN1:def_13;
then consider g1 being Point of (C_NormSpace_of_BoundedLinearOperators (X,X)) such that
A5: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq1 . n) - g1).|| < r by CLVECT_1:def_15;
reconsider g = g1 as Point of (C_Normed_Algebra_of_BoundedLinearOperators X) ;
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((seq_._n)_-_g).||_<_r
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - g).|| < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - g).|| < r
then consider m being Element of NAT  such that
A6: for n being Element of NAT st m <= n holds
||.((seq1 . n) - g1).|| < r by A5;
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.((seq_._n)_-_g).||_<_r
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((seq . n) - g).|| < r )
assume A7: m <= n ; ::_thesis: ||.((seq . n) - g).|| < r
||.((seq1 . n) - g1).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1r) * g1))) by CLVECT_1:3
.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + ((- 1r) * g))
.= ||.((seq . n) - g).|| by CLVECT_1:3 ;
hence  ||.((seq . n) - g).|| < r by A6, A7; ::_thesis: verum
end;
hence  ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((seq . n) - g).|| < r ; ::_thesis: verum
end;
hence  seq is convergent by CLVECT_1:def_15; ::_thesis: verum
end;
hence  C_Normed_Algebra_of_BoundedLinearOperators X is complete by CLOPBAN1:def_13; ::_thesis: verum
end;
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like associative right-distributive right_unital vector-associative Banach_Algebra-like for Normed_Complex_AlgebraStr ;
existence
 ex b1 being Normed_Complex_Algebra st b1 is Banach_Algebra-like
proof
take  C_Normed_Algebra_of_BoundedLinearOperators the non trivial ComplexBanachSpace ; ::_thesis: C_Normed_Algebra_of_BoundedLinearOperators the non trivial ComplexBanachSpace is Banach_Algebra-like
thus  C_Normed_Algebra_of_BoundedLinearOperators the non trivial ComplexBanachSpace is Banach_Algebra-like ; ::_thesis: verum
end;
end;

definition
mode Complex_Banach_Algebra is Banach_Algebra-like Normed_Complex_Algebra;
end;

theorem :: CLOPBAN2:21
for X being ComplexNormSpace holds 1. (Ring_of_BoundedLinearOperators X) = FuncUnit X ;

theorem :: CLOPBAN2:22
for X being ComplexNormSpace holds 1. (C_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;

theorem :: CLOPBAN2:23
for X being ComplexNormSpace holds 1. (C_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;