:: LOPBAN_2 semantic presentation begin theorem Th1: :: LOPBAN_2:1 for X, Y, Z being RealLinearSpace for f being LinearOperator of X,Y for g being LinearOperator of Y,Z holds g * f is LinearOperator of X,Z proof let X, Y, Z be RealLinearSpace; ::_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_a_being_Real_holds_(g_*_f)_._(a_*_v)_=_a_*_((g_*_f)_._v) let v be VECTOR of X; ::_thesis: for a being Real holds (g * f) . (a * v) = a * ((g * f) . v) let a be Real; ::_thesis: (g * f) . (a * v) = a * ((g * f) . v) thus (g * f) . (a * v) = g . (f . (a * v)) by FUNCT_2:15 .= g . (a * (f . v)) by LOPBAN_1:def_5 .= a * (g . (f . v)) by LOPBAN_1:def_5 .= a * ((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, VECTSP_1:def_20, LOPBAN_1:def_5; ::_thesis: verum end; theorem Th2: :: LOPBAN_2:2 for X, Y, Z being RealNormSpace for f being Lipschitzian LinearOperator of X,Y for g being Lipschitzian LinearOperator of Y,Z holds ( g * f is Lipschitzian LinearOperator of X,Z & ( for x being VECTOR of X holds ( ||.((g * f) . x).|| <= (((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f)) * ||.x.|| & (BoundedLinearOperatorsNorm (X,Z)) . (g * f) <= ((BoundedLinearOperatorsNorm (Y,Z)) . g) * ((BoundedLinearOperatorsNorm (X,Y)) . f) ) ) ) proof let X, Y, Z be RealNormSpace; ::_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 (R_NormSpace_of_BoundedLinearOperators (X,Y)) by LOPBAN_1:def_9; reconsider gg = g as Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) by LOPBAN_1:def_9; 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 NORMSP_1:4; then A2: ||.gg.|| * ||.(f . v).|| <= ||.gg.|| * (||.ff.|| * ||.v.||) by LOPBAN_1:32, XREAL_1:64; ( ||.((g * f) . v).|| = ||.(g . (f . v)).|| & ||.(g . (f . v)).|| <= ||.gg.|| * ||.(f . v).|| ) by FUNCT_2:15, LOPBAN_1:32; hence ||.((g * f) . v).|| <= (||.gg.|| * ||.ff.||) * ||.v.|| by A2, XXREAL_0:2; ::_thesis: verum end; A3: ( 0 <= ||.gg.|| & 0 <= ||.ff.|| ) by NORMSP_1:4; then reconsider gf = g * f as Lipschitzian LinearOperator of X,Z by A1, Th1, LOPBAN_1:def_8; set K = ||.gg.|| * ||.ff.||; 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, LOPBAN_1:30; ::_thesis: verum end; definition let X be RealNormSpace; let f, g be Lipschitzian LinearOperator of X,X; :: original: * redefine funcg * f -> Lipschitzian LinearOperator of X,X; correctness coherence g * f is Lipschitzian LinearOperator of X,X; by Th2; end; definition let X be RealNormSpace; let f, g be Element of BoundedLinearOperators (X,X); funcf + g -> Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 1 (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g); correctness coherence (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g) is Element of BoundedLinearOperators (X,X); ; end; :: deftheorem defines + LOPBAN_2:def_1_:_ for X being RealNormSpace for f, g being Element of BoundedLinearOperators (X,X) holds f + g = (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (f,g); definition let X be RealNormSpace; let f, g be Element of BoundedLinearOperators (X,X); funcg * f -> Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 2 (modetrans (g,X,X)) * (modetrans (f,X,X)); correctness coherence (modetrans (g,X,X)) * (modetrans (f,X,X)) is Element of BoundedLinearOperators (X,X); by LOPBAN_1:def_9; end; :: deftheorem defines * LOPBAN_2:def_2_:_ for X being RealNormSpace for f, g being Element of BoundedLinearOperators (X,X) holds g * f = (modetrans (g,X,X)) * (modetrans (f,X,X)); definition let X be RealNormSpace; let f be Element of BoundedLinearOperators (X,X); let a be Real; funca * f -> Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 3 (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f); correctness coherence (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f) is Element of BoundedLinearOperators (X,X); ; end; :: deftheorem defines * LOPBAN_2:def_3_:_ for X being RealNormSpace for f being Element of BoundedLinearOperators (X,X) for a being Real holds a * f = (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f); definition let X be RealNormSpace; func FuncMult X -> BinOp of (BoundedLinearOperators (X,X)) means :Def4: :: LOPBAN_2:def 4 for f, g being Element of BoundedLinearOperators (X,X) holds it . (f,g) = f * g; existence ex b1 being BinOp of (BoundedLinearOperators (X,X)) st for f, g being Element of BoundedLinearOperators (X,X) holds b1 . (f,g) = f * g 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 LOPBAN_2:def_4_:_ for X being RealNormSpace for b2 being BinOp of (BoundedLinearOperators (X,X)) holds ( b2 = FuncMult X iff for f, g being Element of BoundedLinearOperators (X,X) holds b2 . (f,g) = f * g ); theorem Th3: :: LOPBAN_2:3 for X being RealNormSpace holds id the carrier of X is Lipschitzian LinearOperator of X,X proof let X be RealNormSpace; ::_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_a_being_Real_holds_(id_the_carrier_of_X)_._(a_*_v)_=_a_*_((id_the_carrier_of_X)_._v) let v be VECTOR of X; ::_thesis: for a being Real holds (id the carrier of X) . (a * v) = a * ((id the carrier of X) . v) let a be Real; ::_thesis: (id the carrier of X) . (a * v) = a * ((id the carrier of X) . v) thus (id the carrier of X) . (a * v) = a * v by FUNCT_1:18 .= a * ((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, VECTSP_1:def_20, LOPBAN_1:def_5, LOPBAN_1:def_8; ::_thesis: verum end; definition let X be RealNormSpace; func FuncUnit X -> Element of BoundedLinearOperators (X,X) equals :: LOPBAN_2:def 5 id the carrier of X; coherence id the carrier of X is Element of BoundedLinearOperators (X,X) proof 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 LOPBAN_1:def_9; ::_thesis: verum end; end; :: deftheorem defines FuncUnit LOPBAN_2:def_5_:_ for X being RealNormSpace holds FuncUnit X = id the carrier of X; theorem Th4: :: LOPBAN_2:4 for X being RealNormSpace for f, g, h being Lipschitzian LinearOperator of X,X holds ( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) ) proof let X be RealNormSpace; ::_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: :: LOPBAN_2:5 for X being RealNormSpace for f, g, h being Lipschitzian LinearOperator of X,X holds f * (g * h) = (f * g) * h proof let X be RealNormSpace; ::_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: :: LOPBAN_2:6 for X being RealNormSpace for f being Lipschitzian LinearOperator of X,X holds ( f * (id the carrier of X) = f & (id the carrier of X) * f = f ) proof let X be RealNormSpace; ::_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: :: LOPBAN_2:7 for X being RealNormSpace for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g * h) = (f * g) * h proof let X be RealNormSpace; ::_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 LOPBAN_1:def_11; 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 LOPBAN_1:def_11; ::_thesis: verum end; theorem Th8: :: LOPBAN_2:8 for X being RealNormSpace for f being Element of BoundedLinearOperators (X,X) holds ( f * (FuncUnit X) = f & (FuncUnit X) * f = f ) proof let X be RealNormSpace; ::_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 LOPBAN_1:def_9; then A1: modetrans ((id the carrier of X),X,X) = id the carrier of X by LOPBAN_1:def_11; hence f * (FuncUnit X) = modetrans (f,X,X) by Th6 .= f by LOPBAN_1:def_11 ; ::_thesis: (FuncUnit X) * f = f thus (FuncUnit X) * f = modetrans (f,X,X) by A1, Th6 .= f by LOPBAN_1:def_11 ; ::_thesis: verum end; theorem Th9: :: LOPBAN_2:9 for X being RealNormSpace for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h) proof let X be RealNormSpace; ::_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 = R_NormSpace_of_BoundedLinearOperators (X,X); set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_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)),(R_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 (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider k = (modetrans (f,X,X)) * (modetrans ((g + h),X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider hh = h as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ; reconsider gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ; A1: ( gg = modetrans (g,X,X) & hh = modetrans (h,X,X) ) by LOPBAN_1:def_11; 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 LOPBAN_1:def_11; then A2: (modetrans ((g + h),X,X)) . x = ((modetrans (g,X,X)) . x) + ((modetrans (h,X,X)) . x) by A1, LOPBAN_1:35; 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 LOPBAN_1:35; hence (Add_ ((BoundedLinearOperators (X,X)),(R_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: :: LOPBAN_2:10 for X being RealNormSpace for f, g, h being Element of BoundedLinearOperators (X,X) holds (g + h) * f = (g * f) + (h * f) proof let X be RealNormSpace; ::_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 = R_NormSpace_of_BoundedLinearOperators (X,X); set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_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)),(R_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 (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider gf = (modetrans (g,X,X)) * (modetrans (f,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider k = (modetrans ((g + h),X,X)) * (modetrans (f,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider hh = h as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ; reconsider gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ; A1: ( gg = modetrans (g,X,X) & hh = modetrans (h,X,X) ) by LOPBAN_1:def_11; 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 LOPBAN_1:def_11; 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, LOPBAN_1:35; 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 LOPBAN_1:35; hence (Add_ ((BoundedLinearOperators (X,X)),(R_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: :: LOPBAN_2:11 for X being RealNormSpace for f, g being Element of BoundedLinearOperators (X,X) for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g) proof let X be RealNormSpace; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X) for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g) let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g) let a, b be Real; ::_thesis: (a * b) * (f * g) = (a * f) * (b * g) set BLOP = R_NormSpace_of_BoundedLinearOperators (X,X); set EXMULT = Mult_ ((BoundedLinearOperators (X,X)),(R_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)),(R_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 (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def_9; reconsider ff = f, gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) ; A1: gg = modetrans (g,X,X) by LOPBAN_1:def_11; A2: ff = modetrans (f,X,X) by LOPBAN_1:def_11; 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 LOPBAN_1:def_11; 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, LOPBAN_1:36; ( b * g = b * gg & modetrans ((b * g),X,X) = b * g ) by LOPBAN_1:def_11; then A4: (modetrans ((b * g),X,X)) . x = b * ((modetrans (g,X,X)) . x) by A1, LOPBAN_1:36; 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, LOPBAN_1:def_5 .= (a * b) * ((modetrans (f,X,X)) . ((modetrans (g,X,X)) . x)) by RLVECT_1:def_7 .= (a * b) * (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) by Th4 ; ::_thesis: verum end; then k = (a * b) * fg by LOPBAN_1:36; hence (Mult_ ((BoundedLinearOperators (X,X)),(R_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: :: LOPBAN_2:12 for X being RealNormSpace for f, g being Element of BoundedLinearOperators (X,X) for a being Real holds a * (f * g) = (a * f) * g proof let X be RealNormSpace; ::_thesis: for f, g being Element of BoundedLinearOperators (X,X) for a being Real holds a * (f * g) = (a * f) * g let f, g be Element of BoundedLinearOperators (X,X); ::_thesis: for a being Real holds a * (f * g) = (a * f) * g let a be Real; ::_thesis: a * (f * g) = (a * f) * g set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); reconsider gg = g as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ; A1: 1 * g = 1 * gg .= g by RLVECT_1:def_8 ; a * (f * g) = (a * 1) * (f * g) .= (a * f) * (1 * g) by Th11 ; hence a * (f * g) = (a * f) * g by A1; ::_thesis: verum end; definition let X be RealNormSpace; func Ring_of_BoundedLinearOperators X -> doubleLoopStr equals :: LOPBAN_2:def 6 doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); correctness coherence doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) is doubleLoopStr ; ; end; :: deftheorem defines Ring_of_BoundedLinearOperators LOPBAN_2:def_6_:_ for X being RealNormSpace holds Ring_of_BoundedLinearOperators X = doubleLoopStr(# (BoundedLinearOperators (X,X)),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncMult X),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); registration let X be RealNormSpace; cluster Ring_of_BoundedLinearOperators X -> non empty strict ; coherence ( not Ring_of_BoundedLinearOperators X is empty & Ring_of_BoundedLinearOperators X is strict ) ; end; Lm1: now__::_thesis:_for_X_being_RealNormSpace for_x,_e_being_Element_of_(Ring_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let X be RealNormSpace; ::_thesis: for x, e being Element of (Ring_of_BoundedLinearOperators X) st e = FuncUnit X holds ( x * e = x & e * x = x ) set F = Ring_of_BoundedLinearOperators X; let x, e be Element of (Ring_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x & e * x = x ) ) reconsider f = x as Element of BoundedLinearOperators (X,X) ; assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x & e * x = x ) hence x * e = f * (FuncUnit X) by Def4 .= x by Th8 ; ::_thesis: e * x = x thus e * x = (FuncUnit X) * f by A1, Def4 .= x by Th8 ; ::_thesis: verum end; registration let X be RealNormSpace; cluster Ring_of_BoundedLinearOperators X -> unital ; coherence Ring_of_BoundedLinearOperators X is unital proof 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: :: LOPBAN_2:13 for X being RealNormSpace for x, y, z being Element of (Ring_of_BoundedLinearOperators X) holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) proof let X be RealNormSpace; ::_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 & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) 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 & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) set RBLOP = Ring_of_BoundedLinearOperators X; set BLOP = BoundedLinearOperators (X,X); set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))); set MULT = FuncMult X; set UNIT = FuncUnit X; set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_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 & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) 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 & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) thus x + (0. (Ring_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #)) .= x by RLVECT_1:def_4 ; ::_thesis: ( ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) thus ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) ::_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 RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_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)),(R_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)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4 .= (y * x) + (z * x) by Def4 ; ::_thesis: verum end; theorem Th14: :: LOPBAN_2:14 for X being RealNormSpace holds Ring_of_BoundedLinearOperators X is Ring proof let X be RealNormSpace; ::_thesis: Ring_of_BoundedLinearOperators X is Ring set R = Ring_of_BoundedLinearOperators X; A1: Ring_of_BoundedLinearOperators X is right_complementable proof let x be Element of (Ring_of_BoundedLinearOperators X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable thus ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) by Th13; :: according to ALGSTR_0:def_11 ::_thesis: verum end; for x, y, z being Element of (Ring_of_BoundedLinearOperators X) holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (Ring_of_BoundedLinearOperators X)) = x & ex t being Element of (Ring_of_BoundedLinearOperators X) st x + t = 0. (Ring_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (Ring_of_BoundedLinearOperators X)) = x & (1. (Ring_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by Th13; hence Ring_of_BoundedLinearOperators X is Ring by A1, 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 RealNormSpace; cluster Ring_of_BoundedLinearOperators X -> right_complementable Abelian add-associative right_zeroed associative right_unital distributive left_unital ; coherence ( Ring_of_BoundedLinearOperators X is Abelian & Ring_of_BoundedLinearOperators X is add-associative & Ring_of_BoundedLinearOperators X is right_zeroed & Ring_of_BoundedLinearOperators X is right_complementable & Ring_of_BoundedLinearOperators X is associative & Ring_of_BoundedLinearOperators X is left_unital & Ring_of_BoundedLinearOperators X is right_unital & Ring_of_BoundedLinearOperators X is distributive ) by Th14; end; definition let X be RealNormSpace; func R_Algebra_of_BoundedLinearOperators X -> AlgebraStr equals :: LOPBAN_2:def 7 AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); correctness coherence AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) is AlgebraStr ; ; end; :: deftheorem defines R_Algebra_of_BoundedLinearOperators LOPBAN_2:def_7_:_ for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X = AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); registration let X be RealNormSpace; cluster R_Algebra_of_BoundedLinearOperators X -> non empty strict ; coherence ( not R_Algebra_of_BoundedLinearOperators X is empty & R_Algebra_of_BoundedLinearOperators X is strict ) ; end; Lm2: now__::_thesis:_for_X_being_RealNormSpace for_x,_e_being_Element_of_(R_Algebra_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let X be RealNormSpace; ::_thesis: for x, e being Element of (R_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds ( x * e = x & e * x = x ) set F = R_Algebra_of_BoundedLinearOperators X; let x, e be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x & e * x = x ) ) reconsider f = x as Element of BoundedLinearOperators (X,X) ; assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x & e * x = x ) hence x * e = f * (FuncUnit X) by Def4 .= x by Th8 ; ::_thesis: e * x = x thus e * x = (FuncUnit X) * f by A1, Def4 .= x by Th8 ; ::_thesis: verum end; registration let X be RealNormSpace; cluster R_Algebra_of_BoundedLinearOperators X -> unital ; coherence R_Algebra_of_BoundedLinearOperators X is unital proof reconsider e = FuncUnit X as Element of (R_Algebra_of_BoundedLinearOperators X) ; take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds ( b1 * e = b1 & e * b1 = b1 ) thus for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds ( b1 * e = b1 & e * b1 = b1 ) by Lm2; ::_thesis: verum end; end; theorem :: LOPBAN_2:15 for X being RealNormSpace for x, y, z being Element of (R_Algebra_of_BoundedLinearOperators X) for a, b being Real holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) proof let X be RealNormSpace; ::_thesis: for x, y, z being Element of (R_Algebra_of_BoundedLinearOperators X) for a, b being Real holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: for a, b being Real holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) let a, b be Real; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) set RBLOP = R_Algebra_of_BoundedLinearOperators X; set BLOP = BoundedLinearOperators (X,X); set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))); set MULT = FuncMult X; set UNIT = FuncUnit X; set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_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. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) thus (x + y) + z = (f + g) + h .= f + (g + h) by RLVECT_1:def_3 .= x + (y + z) ; ::_thesis: ( x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) thus x + (0. (R_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #)) .= x by RLVECT_1:def_4 ; ::_thesis: ( ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) thus ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) ::_thesis: ( (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) proof consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11; reconsider t = s as Element of (R_Algebra_of_BoundedLinearOperators X) ; take t ; ::_thesis: x + t = 0. (R_Algebra_of_BoundedLinearOperators X) thus x + t = 0. (R_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. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4 .= x by Th8 ; ::_thesis: ( (1. (R_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) ) thus (1. (R_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)),(R_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)),(R_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 RLVECT_1:def_5 .= (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 RLVECT_1:def_6 .= (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 RLVECT_1:def_7 .= 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 BLAlgebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative vector-associative associative right-distributive right_unital AlgebraStr ; end; registration let X be RealNormSpace; cluster R_Algebra_of_BoundedLinearOperators X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative associative right-distributive right_unital ; coherence ( R_Algebra_of_BoundedLinearOperators X is Abelian & R_Algebra_of_BoundedLinearOperators X is add-associative & R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof set A = R_Algebra_of_BoundedLinearOperators X; set BLOP = BoundedLinearOperators (X,X); set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); set MULT = FuncMult X; set UNIT = FuncUnit X; set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))); thus R_Algebra_of_BoundedLinearOperators X is Abelian ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is add-associative & R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_2 ::_thesis: x + y = y + x reconsider f = x, g = y as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ; thus x + y = f + g .= y + x by RLVECT_1:2 ; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is add-associative ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let x, y, z be Element of (R_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 RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_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 R_Algebra_of_BoundedLinearOperators X is right_zeroed ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def_4 ::_thesis: x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ; thus x + (0. (R_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #)) .= x by RLVECT_1:def_4 ; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is right_complementable ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ; consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11; reconsider t = s as Element of (R_Algebra_of_BoundedLinearOperators X) ; take t ; :: according to ALGSTR_0:def_11 ::_thesis: x + t = 0. (R_Algebra_of_BoundedLinearOperators X) thus x + t = 0. (R_Algebra_of_BoundedLinearOperators X) by A1; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is associative ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let x, y, z be Element of (R_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 R_Algebra_of_BoundedLinearOperators X is right_unital ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_4 ::_thesis: x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x reconsider xx = x as Element of BoundedLinearOperators (X,X) ; thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4 .= x by Th8 ; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is right-distributive ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let x, y, z be Element of (R_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)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4 .= (x * y) + (x * z) by Def4 ; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is vector-distributive ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let a be real number ; :: according to RLVECT_1:def_5 ::_thesis: for b1, b2 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds a * (b1 + b2) = (a * b1) + (a * b2) let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: a * (x + y) = (a * x) + (a * y) reconsider f = x, g = y as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ; thus a * (x + y) = a * (f + g) .= (a * f) + (a * g) by RLVECT_1:def_5 .= (a * x) + (a * y) ; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is scalar-distributive ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let a, b be real number ; :: according to RLVECT_1:def_6 ::_thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds (a + b) * b1 = (a * b1) + (b * b1) let x be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: (a + b) * x = (a * x) + (b * x) reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ; thus (a + b) * x = (a + b) * f .= (a * f) + (b * f) by RLVECT_1:def_6 .= (a * x) + (b * x) ; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is scalar-associative ::_thesis: ( R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict ) proof let a, b be real number ; :: according to RLVECT_1:def_7 ::_thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds (a * b) * b1 = a * (b * b1) let x be Element of (R_Algebra_of_BoundedLinearOperators X); ::_thesis: (a * b) * x = a * (b * x) reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ; thus (a * b) * x = (a * b) * f .= a * (b * f) by RLVECT_1:def_7 .= a * (b * x) ; ::_thesis: verum end; thus R_Algebra_of_BoundedLinearOperators X is vector-associative ::_thesis: R_Algebra_of_BoundedLinearOperators X is strict proof let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to FUNCSDOM:def_9 ::_thesis: for b1 being Element of REAL holds b1 * (x * y) = (b1 * x) * y let a be Real; ::_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; thus R_Algebra_of_BoundedLinearOperators X is strict ; ::_thesis: verum end; end; theorem :: LOPBAN_2:16 for X being RealNormSpace holds R_Algebra_of_BoundedLinearOperators X is BLAlgebra ; registration cluster l1_Space -> complete ; coherence l1_Space is complete proof thus for vseq being sequence of l1_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent by RSSPACE3:9; :: according to LOPBAN_1:def_15 ::_thesis: verum end; end; registration cluster l1_Space -> non trivial ; coherence not l1_Space is trivial proof set a = 1 / 2; reconsider x = (1 / 2) GeoSeq as Real_Sequence ; A1: abs (1 / 2) = 1 / 2 by ABSVALUE:def_1; defpred S1[ Element of NAT ] means 0 <= x . c1; A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) A3: x . (n + 1) = (x . n) * (1 / 2) by PREPOWER:3; assume S1[n] ; ::_thesis: S1[n + 1] hence S1[n + 1] by A3; ::_thesis: verum end; A4: S1[ 0 ] by PREPOWER:3; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); then x is absolutely_summable by A1, SERIES_1:24, SERIES_1:36; then seq_id x is absolutely_summable by RSSPACE:1; then reconsider v = x as VECTOR of l1_Space by RSSPACE3:6; (seq_id v) . 0 = x . 0 by RSSPACE:1 .= 1 by PREPOWER:3 ; then v <> Zeroseq by RSSPACE:def_6; hence not l1_Space is trivial by RSSPACE3:6, STRUCT_0:def_18; ::_thesis: verum end; end; registration cluster non empty non trivial left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() discerning reflexive RealNormSpace-like complete for NORMSTR ; existence not for b1 being RealBanachSpace holds b1 is trivial proof take l1_Space ; ::_thesis: not l1_Space is trivial thus not l1_Space is trivial ; ::_thesis: verum end; end; theorem Th17: :: LOPBAN_2:17 for X being non trivial RealNormSpace ex w being VECTOR of X st ||.w.|| = 1 proof let X be non trivial RealNormSpace; ::_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; set a = ||.v.||; reconsider w = (||.v.|| ") * v as VECTOR of X ; take w ; ::_thesis: ||.w.|| = 1 A2: ||.v.|| <> 0 by A1, NORMSP_0:def_5; then A3: 0 < ||.v.|| by NORMSP_1:4; A4: abs (||.v.|| ") = abs (1 * (||.v.|| ")) .= abs (1 / ||.v.||) by XCMPLX_0:def_9 .= 1 / (abs ||.v.||) by ABSVALUE:7 .= 1 * ((abs ||.v.||) ") by XCMPLX_0:def_9 .= ||.v.|| " by A3, ABSVALUE:def_1 ; thus ||.w.|| = (abs (||.v.|| ")) * ||.v.|| by NORMSP_1:def_1 .= 1 by A2, A4, XCMPLX_0:def_7 ; ::_thesis: verum end; theorem Th18: :: LOPBAN_2:18 for X being non trivial RealNormSpace holds (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) = 1 proof let X be non trivial RealNormSpace; ::_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 LOPBAN_1:27; 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 LOPBAN_1:30; ::_thesis: verum end; definition attrc1 is strict ; struct Normed_AlgebraStr -> AlgebraStr , NORMSTR ; aggrNormed_AlgebraStr(# carrier, multF, addF, Mult, OneF, ZeroF, normF #) -> Normed_AlgebraStr ; end; registration cluster non empty for Normed_AlgebraStr ; existence not for b1 being Normed_AlgebraStr holds b1 is empty 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 [:REAL, 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_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, 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_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, 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_AlgebraStr(# the non empty set , the BinOp of the non empty set , the BinOp of the non empty set , the Function of [:REAL, 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 RealNormSpace; func R_Normed_Algebra_of_BoundedLinearOperators X -> Normed_AlgebraStr equals :: LOPBAN_2:def 8 Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #); correctness coherence Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #) is Normed_AlgebraStr ; ; end; :: deftheorem defines R_Normed_Algebra_of_BoundedLinearOperators LOPBAN_2:def_8_:_ for X being RealNormSpace holds R_Normed_Algebra_of_BoundedLinearOperators X = Normed_AlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(BoundedLinearOperatorsNorm (X,X)) #); registration let X be RealNormSpace; cluster R_Normed_Algebra_of_BoundedLinearOperators X -> non empty strict ; coherence ( not R_Normed_Algebra_of_BoundedLinearOperators X is empty & R_Normed_Algebra_of_BoundedLinearOperators X is strict ) ; end; Lm3: now__::_thesis:_for_X_being_RealNormSpace for_x,_e_being_Element_of_(R_Normed_Algebra_of_BoundedLinearOperators_X)_st_e_=_FuncUnit_X_holds_ (_x_*_e_=_x_&_e_*_x_=_x_) let X be RealNormSpace; ::_thesis: for x, e being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st e = FuncUnit X holds ( x * e = x & e * x = x ) set F = R_Normed_Algebra_of_BoundedLinearOperators X; let x, e be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: ( e = FuncUnit X implies ( x * e = x & e * x = x ) ) reconsider f = x as Element of BoundedLinearOperators (X,X) ; assume A1: e = FuncUnit X ; ::_thesis: ( x * e = x & e * x = x ) hence x * e = f * (FuncUnit X) by Def4 .= x by Th8 ; ::_thesis: e * x = x thus e * x = (FuncUnit X) * f by A1, Def4 .= x by Th8 ; ::_thesis: verum end; registration let X be RealNormSpace; cluster R_Normed_Algebra_of_BoundedLinearOperators X -> unital ; coherence R_Normed_Algebra_of_BoundedLinearOperators X is unital proof reconsider e = FuncUnit X as Element of (R_Normed_Algebra_of_BoundedLinearOperators X) ; take e ; :: according to GROUP_1:def_1 ::_thesis: for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedLinearOperators X) holds ( b1 * e = b1 & e * b1 = b1 ) thus for b1 being Element of the carrier of (R_Normed_Algebra_of_BoundedLinearOperators X) holds ( b1 * e = b1 & e * b1 = b1 ) by Lm3; ::_thesis: verum end; end; theorem Th19: :: LOPBAN_2:19 for X being RealNormSpace for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) for a, b being real number holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) proof let X be RealNormSpace; ::_thesis: for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) for a, b being real number holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) let x, y, z be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: for a, b being real number holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) let a, b be real number ; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) reconsider a1 = a, b1 = b as Real by XREAL_0:def_1; set RBLOP = R_Normed_Algebra_of_BoundedLinearOperators X; set BLOP = BoundedLinearOperators (X,X); set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))); set MULT = FuncMult X; set UNIT = FuncUnit X; set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #); reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_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. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) thus (x + y) + z = (f + g) + h .= f + (g + h) by RLVECT_1:def_3 .= x + (y + z) ; ::_thesis: ( x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) thus x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #)) .= x by RLVECT_1:def_4 ; ::_thesis: ( ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) thus ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ::_thesis: ( (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) proof consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def_11; reconsider t = s as Element of (R_Normed_Algebra_of_BoundedLinearOperators X) ; take t ; ::_thesis: x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) thus x + t = 0. (R_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. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) thus x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4 .= x by Th8 ; ::_thesis: ( (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) thus (1. (R_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) & 1 * x = x ) thus x * (y + z) = xx * (yy + zz) by Def4 .= (xx * yy) + (xx * zz) by Th9 .= (Add_ ((BoundedLinearOperators (X,X)),(R_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) & 1 * x = x ) thus (y + z) * x = (yy + zz) * xx by Def4 .= (yy * xx) + (zz * xx) by Th10 .= (Add_ ((BoundedLinearOperators (X,X)),(R_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) & 1 * x = x ) thus a * (x * y) = a1 * (xx * yy) by Def4 .= (a1 * 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) & 1 * x = x ) thus (a * b) * (x * y) = (a1 * b1) * (xx * yy) by Def4 .= (a1 * xx) * (b1 * 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) & 1 * x = x ) thus a * (x + y) = a * (f + g) .= (a * f) + (a * g) by RLVECT_1:def_5 .= (a * x) + (a * y) ; ::_thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) thus (a + b) * x = (a + b) * f .= (a * f) + (b * f) by RLVECT_1:def_6 .= (a * x) + (b * x) ; ::_thesis: ( (a * b) * x = a * (b * x) & 1 * x = x ) thus (a * b) * x = (a * b) * f .= a * (b * f) by RLVECT_1:def_7 .= a * (b * x) ; ::_thesis: 1 * x = x thus 1 * x = 1 * f .= x by RLVECT_1:def_8 ; ::_thesis: verum end; theorem Th20: :: LOPBAN_2:20 for X being RealNormSpace holds ( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) proof let X be RealNormSpace; ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) set RBLOP = R_Normed_Algebra_of_BoundedLinearOperators X; set BS = R_NormSpace_of_BoundedLinearOperators (X,X); set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))); set EXMULT = Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X))); set NRM = BoundedLinearOperatorsNorm (X,X); A1: ||.(0. (R_NormSpace_of_BoundedLinearOperators (X,X))).|| = (BoundedLinearOperatorsNorm (X,X)) . (0. (R_NormSpace_of_BoundedLinearOperators (X,X))) .= ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| ; thus ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| = 0 by A1; :: according to NORMSP_0:def_6 ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) A2: now__::_thesis:_for_x,_y_being_Point_of_(R_Normed_Algebra_of_BoundedLinearOperators_X) for_a_being_Real_holds_ (_||.(x_+_y).||_<=_||.x.||_+_||.y.||_&_(_||.x.||_=_0_implies_x_=_0._(R_Normed_Algebra_of_BoundedLinearOperators_X)_)_&_(_x_=_0._(R_Normed_Algebra_of_BoundedLinearOperators_X)_implies_||.x.||_=_0_)_&_||.(a_*_x).||_=_(abs_a)_*_||.x.||_) let x, y be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: for a being Real holds ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| ) let a be Real; ::_thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| ) reconsider x1 = x, y1 = y as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ; A3: ||.x1.|| + ||.y1.|| = ((BoundedLinearOperatorsNorm (X,X)) . x1) + ||.y1.|| .= ((BoundedLinearOperatorsNorm (X,X)) . x1) + ((BoundedLinearOperatorsNorm (X,X)) . y1) .= ||.x.|| + ( the normF of (R_Normed_Algebra_of_BoundedLinearOperators X) . y) .= ||.x.|| + ||.y.|| ; ||.(x + y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (x,y)) .= ||.(x1 + y1).|| ; hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A3, NORMSP_1:def_1; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| ) A4: ||.x1.|| = (BoundedLinearOperatorsNorm (X,X)) . x1 .= ||.x.|| ; 0. (R_NormSpace_of_BoundedLinearOperators (X,X)) = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ; hence ( ||.x.|| = 0 iff x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) by A4, NORMSP_0:def_5; ::_thesis: ||.(a * x).|| = (abs a) * ||.x.|| thus ||.(a * x).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,x)) .= ||.(a * x1).|| .= (abs a) * ||.x.|| by A4, NORMSP_1:def_1 ; ::_thesis: verum end; A5: R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable proof let x be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def_16 ::_thesis: x is right_complementable thus ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) by Th19; :: according to ALGSTR_0:def_11 ::_thesis: verum end; A6: ( ( for a, b being real number for v being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds (a + b) * v = (a * v) + (b * v) ) & ( for a, b being real number for v being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds (a * b) * v = a * (b * v) ) ) by Th19; ( ( for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) for a, b being Real holds ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x ) ) & ( for a being real number for v, w being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) ) by Th19; hence ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) by A5, A6, A2, FUNCSDOM:def_9, GROUP_1:def_3, NORMSP_0:def_5, NORMSP_1:def_1, RLVECT_1:def_2, RLVECT_1:def_3, RLVECT_1:def_4, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8, VECTSP_1:def_2, VECTSP_1:def_4; ::_thesis: verum end; registration cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital strict for Normed_AlgebraStr ; existence ex b1 being non empty Normed_AlgebraStr st ( b1 is reflexive & b1 is discerning & b1 is RealNormSpace-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 vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital & b1 is strict ) proof set X = the RealNormSpace; take R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace ; ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is reflexive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is discerning & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is Abelian & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is add-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is strict ) thus ( R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is reflexive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is discerning & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is Abelian & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is add-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right_unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is scalar-unital & R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace is strict ) by Th20; ::_thesis: verum end; end; definition mode Normed_Algebra is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Normed_AlgebraStr ; end; registration let X be RealNormSpace; cluster R_Normed_Algebra_of_BoundedLinearOperators X -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital ; correctness coherence ( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ); by Th20; end; definition let X be non empty Normed_AlgebraStr ; attrX is Banach_Algebra-like_1 means :: LOPBAN_2:def 9 for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.||; attrX is Banach_Algebra-like_2 means :Def10: :: LOPBAN_2:def 10 ||.(1. X).|| = 1; attrX is Banach_Algebra-like_3 means :: LOPBAN_2:def 11 for a being Real for x, y being Element of X holds a * (x * y) = x * (a * y); end; :: deftheorem defines Banach_Algebra-like_1 LOPBAN_2:def_9_:_ for X being non empty Normed_AlgebraStr holds ( X is Banach_Algebra-like_1 iff for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.|| ); :: deftheorem Def10 defines Banach_Algebra-like_2 LOPBAN_2:def_10_:_ for X being non empty Normed_AlgebraStr holds ( X is Banach_Algebra-like_2 iff ||.(1. X).|| = 1 ); :: deftheorem defines Banach_Algebra-like_3 LOPBAN_2:def_11_:_ for X being non empty Normed_AlgebraStr holds ( X is Banach_Algebra-like_3 iff for a being Real for x, y being Element of X holds a * (x * y) = x * (a * y) ); definition let X be Normed_Algebra; attrX is Banach_Algebra-like means :Def12: :: LOPBAN_2:def 12 ( X is Banach_Algebra-like_1 & 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 LOPBAN_2:def_12_:_ for X being Normed_Algebra holds ( X is Banach_Algebra-like iff ( X is Banach_Algebra-like_1 & X is Banach_Algebra-like_2 & X is Banach_Algebra-like_3 & X is left_unital & X is left-distributive & X is complete ) ); registration cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Banach_Algebra-like -> left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 for Normed_AlgebraStr ; coherence for b1 being Normed_Algebra st b1 is Banach_Algebra-like holds ( b1 is Banach_Algebra-like_1 & 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 vector-distributive scalar-distributive scalar-associative scalar-unital vector-associative discerning reflexive RealNormSpace-like associative right-distributive left-distributive right_unital left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 -> Banach_Algebra-like for Normed_AlgebraStr ; coherence for b1 being Normed_Algebra st b1 is Banach_Algebra-like_1 & 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 RealBanachSpace; cluster R_Normed_Algebra_of_BoundedLinearOperators X -> Banach_Algebra-like ; coherence R_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)),(R_VectorSpace_of_LinearOperators (X,X))); set BS = R_NormSpace_of_BoundedLinearOperators (X,X); set BLOP = BoundedLinearOperators (X,X); set RBLOP = R_Normed_Algebra_of_BoundedLinearOperators X; thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_1 :: according to LOPBAN_2:def_12 ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete ) proof let x, y be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to LOPBAN_2: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 LOPBAN_1:def_11 .= ((BoundedLinearOperatorsNorm (X,X)) . x1) * ((BoundedLinearOperatorsNorm (X,X)) . y1) by LOPBAN_1:def_11 .= ||.x.|| * ((BoundedLinearOperatorsNorm (X,X)) . y) .= ||.x.|| * ||.y.|| ; ||.(x * y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((FuncMult X) . (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. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| = (BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X) .= 1 by Th18 ; hence R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 by Def10; ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete ) thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete ) proof let a be Real; :: according to LOPBAN_2:def_11 ::_thesis: for x, y being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (x * y) = x * (a * y) let x, y be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); ::_thesis: a * (x * y) = x * (a * y) thus a * (x * y) = (1 * a) * (x * y) .= (1 * x) * (a * y) by Th19 .= x * (a * y) by Th19 ; ::_thesis: verum end; thus R_Normed_Algebra_of_BoundedLinearOperators X is left_unital ::_thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete ) proof let x be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def_8 ::_thesis: (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x reconsider xx = x as Element of BoundedLinearOperators (X,X) ; (FuncUnit X) * xx = xx by Th8; hence (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x by Def4; ::_thesis: verum end; thus R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive ::_thesis: R_Normed_Algebra_of_BoundedLinearOperators X is complete proof let x, y, z be Element of (R_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)),(R_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_(R_Normed_Algebra_of_BoundedLinearOperators_X)_st_seq_is_Cauchy_sequence_by_Norm_holds_ seq_is_convergent let seq be sequence of (R_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 (R_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, RSSPACE3: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)) . ((seq1 . n) + (- (seq1 . m))) .= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * (seq1 . m)))) by RLVECT_1:16 .= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * (seq . m)))) .= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- (seq . m))) by RLVECT_1:16 .= ||.((seq . n) - (seq . m)).|| ; 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 RSSPACE3:8; then seq1 is convergent by LOPBAN_1:def_15; then consider g1 being Point of (R_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 NORMSP_1:def_6; reconsider g = g1 as Point of (R_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)) . ((seq1 . n) + (- g1)) .= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * g1))) by RLVECT_1:16 .= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * g))) .= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- g)) by RLVECT_1:16 .= ||.((seq . n) - g).|| ; 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 NORMSP_1:def_6; ::_thesis: verum end; hence R_Normed_Algebra_of_BoundedLinearOperators X is complete by LOPBAN_1:def_15; ::_thesis: verum end; end; registration cluster non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V134() vector-associative discerning reflexive RealNormSpace-like associative right-distributive right_unital Banach_Algebra-like for Normed_AlgebraStr ; existence ex b1 being Normed_Algebra st b1 is Banach_Algebra-like proof set X = the non trivial RealBanachSpace; take R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace ; ::_thesis: R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace is Banach_Algebra-like thus R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace is Banach_Algebra-like ; ::_thesis: verum end; end; definition mode Banach_Algebra is Banach_Algebra-like Normed_Algebra; end; theorem :: LOPBAN_2:21 for X being RealNormSpace holds 1. (Ring_of_BoundedLinearOperators X) = FuncUnit X ; theorem :: LOPBAN_2:22 for X being RealNormSpace holds 1. (R_Algebra_of_BoundedLinearOperators X) = FuncUnit X ; theorem :: LOPBAN_2:23 for X being RealNormSpace holds 1. (R_Normed_Algebra_of_BoundedLinearOperators X) = FuncUnit X ;