lopban_2.miz



    begin

    theorem :: LOPBAN_2:1

    

     Th1: for X,Y,Z be RealLinearSpace holds for f be LinearOperator of X, Y holds for g be LinearOperator of Y, Z holds (g * f) is LinearOperator of X, Z

    proof

      let X,Y,Z be RealLinearSpace;

      let f be LinearOperator of X, Y;

      let g be LinearOperator of Y, Z;

       A1:

      now

        let v be VECTOR of X, a be Real;

        

        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;

      end;

      now

        let v,w be VECTOR of X;

        

        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;

      end;

      hence thesis by A1, LOPBAN_1:def 5, VECTSP_1:def 20;

    end;

    theorem :: LOPBAN_2:2

    

     Th2: for X,Y,Z be RealNormSpace holds for f be Lipschitzian LinearOperator of X, Y holds for g be Lipschitzian LinearOperator of Y, Z holds (g * f) is Lipschitzian LinearOperator of X, Z & for x be 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;

      let f be Lipschitzian LinearOperator of X, Y;

      let g be Lipschitzian LinearOperator of Y, Z;

      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

        let v be VECTOR of X;

         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;

      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

        let t be VECTOR of X;

        assume ||.t.|| <= 1;

        then

         A5: (K * ||.t.||) <= (K * 1) by A3, XREAL_1: 64;

         ||.((g * f) . t).|| <= (K * ||.t.||) by A1;

        hence ||.((g * f) . t).|| <= K by A5, XXREAL_0: 2;

      end;

       A6:

      now

        let r be Real;

        assume r in ( PreNorms gf);

        then ex t be VECTOR of X st r = ||.(gf . t).|| & ||.t.|| <= 1;

        hence r <= K by A4;

      end;

      (for s be Real st s in ( PreNorms gf) holds s <= K) implies ( upper_bound ( PreNorms gf)) <= K by SEQ_4: 45;

      hence thesis by A1, A6, LOPBAN_1: 30;

    end;

    definition

      let X be RealNormSpace;

      let f,g be Lipschitzian LinearOperator of X, X;

      :: original: *

      redefine

      func g * f -> Lipschitzian LinearOperator of X, X ;

      correctness by Th2;

    end

    definition

      let X be RealNormSpace;

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

      :: LOPBAN_2:def1

      func f + g -> Element of ( BoundedLinearOperators (X,X)) equals (( Add_ (( BoundedLinearOperators (X,X)),( R_VectorSpace_of_LinearOperators (X,X)))) . (f,g));

      correctness ;

    end

    definition

      let X be RealNormSpace;

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

      :: LOPBAN_2:def2

      func g * f -> Element of ( BoundedLinearOperators (X,X)) equals (( modetrans (g,X,X)) * ( modetrans (f,X,X)));

      correctness by LOPBAN_1:def 9;

    end

    definition

      let X be RealNormSpace;

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

      let a be Real;

      :: LOPBAN_2:def3

      func a * f -> Element of ( BoundedLinearOperators (X,X)) equals (( Mult_ (( BoundedLinearOperators (X,X)),( R_VectorSpace_of_LinearOperators (X,X)))) . (a,f));

      correctness

      proof

        reconsider a as Element of REAL by XREAL_0:def 1;

        (( Mult_ (( BoundedLinearOperators (X,X)),( R_VectorSpace_of_LinearOperators (X,X)))) . (a,f)) is Element of ( BoundedLinearOperators (X,X));

        hence thesis;

      end;

    end

    definition

      let X be RealNormSpace;

      :: LOPBAN_2:def4

      func FuncMult (X) -> BinOp of ( BoundedLinearOperators (X,X)) means

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

      existence

      proof

        deffunc F( Element of ( BoundedLinearOperators (X,X)), Element of ( BoundedLinearOperators (X,X))) = ($1 * $2);

        consider F be BinOp of ( BoundedLinearOperators (X,X)) such that

         A1: for x,y be Element of ( BoundedLinearOperators (X,X)) holds (F . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take F;

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

        thus thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be BinOp of ( BoundedLinearOperators (X,X)) such that

         A2: for f,g be Element of ( BoundedLinearOperators (X,X)) holds (it1 . (f,g)) = (f * g) and

         A3: for f,g be Element of ( BoundedLinearOperators (X,X)) holds (it2 . (f,g)) = (f * g);

        now

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

          

          thus (it1 . (f,g)) = (f * g) by A2

          .= (it2 . (f,g)) by A3;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: LOPBAN_2:3

    

     Th3: for X be RealNormSpace holds ( id the carrier of X) is Lipschitzian LinearOperator of X, X

    proof

      let X be RealNormSpace;

      

       A1: for v,w be VECTOR of X holds (( id the carrier of X) . (v + w)) = ((( id the carrier of X) . v) + (( id the carrier of X) . w));

      

       A2: for v be VECTOR of X, a be Real holds (( id the carrier of X) . (a * v)) = (a * (( id the carrier of X) . v));

      for v be VECTOR of X holds ||.(( id the carrier of X) . v).|| <= (1 * ||.v.||);

      hence thesis by A1, A2, LOPBAN_1:def 5, LOPBAN_1:def 8, VECTSP_1:def 20;

    end;

    definition

      let X be RealNormSpace;

      :: LOPBAN_2:def5

      func FuncUnit (X) -> Element of ( BoundedLinearOperators (X,X)) equals ( id the carrier of X);

      coherence

      proof

        ( id the carrier of X) is Lipschitzian LinearOperator of X, X by Th3;

        hence thesis by LOPBAN_1:def 9;

      end;

    end

    theorem :: LOPBAN_2:4

    

     Th4: for X be RealNormSpace holds for f,g,h be Lipschitzian LinearOperator of X, X holds h = (f * g) iff for x be VECTOR of X holds (h . x) = (f . (g . x))

    proof

      let X be RealNormSpace;

      let f,g,h be Lipschitzian LinearOperator of X, X;

      now

        assume

         A1: for x be VECTOR of X holds (h . x) = (f . (g . x));

        now

          let x be VECTOR of X;

          

          thus ((f * g) . x) = (f . (g . x)) by FUNCT_2: 15

          .= (h . x) by A1;

        end;

        hence h = (f * g) by FUNCT_2: 63;

      end;

      hence thesis by FUNCT_2: 15;

    end;

    theorem :: LOPBAN_2:5

    

     Th5: for X be RealNormSpace holds for f,g,h be Lipschitzian LinearOperator of X, X holds (f * (g * h)) = ((f * g) * h)

    proof

      let X be RealNormSpace;

      let f,g,h be Lipschitzian LinearOperator of X, X;

      now

        let x be VECTOR of 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;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: LOPBAN_2:6

    

     Th6: for X be RealNormSpace holds for f be 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;

      reconsider ii = ( id the carrier of X) as Lipschitzian LinearOperator of X, X by Th3;

      let f be Lipschitzian LinearOperator of X, X;

       A1:

      now

        let x be VECTOR of X;

        

        thus ((( id the carrier of X) * f) . x) = ((ii * f) . x)

        .= (ii . (f . x)) by Th4

        .= (f . x);

      end;

      now

        let x be VECTOR of X;

        

        thus ((f * ( id the carrier of X)) . x) = ((f * ii) . x)

        .= (f . (ii . x)) by Th4

        .= (f . x);

      end;

      hence thesis by A1, FUNCT_2: 63;

    end;

    theorem :: LOPBAN_2:7

    

     Th7: for X be RealNormSpace holds for f,g,h be Element of ( BoundedLinearOperators (X,X)) holds (f * (g * h)) = ((f * g) * h)

    proof

      let X be RealNormSpace;

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

      ( 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 thesis by LOPBAN_1:def 11;

    end;

    theorem :: LOPBAN_2:8

    

     Th8: for X be RealNormSpace holds for f be Element of ( BoundedLinearOperators (X,X)) holds (f * ( FuncUnit X)) = f & (( FuncUnit X) * f) = f

    proof

      let X be RealNormSpace;

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

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

      

      thus (( FuncUnit X) * f) = ( modetrans (f,X,X)) by A1, Th6

      .= f by LOPBAN_1:def 11;

    end;

    theorem :: LOPBAN_2:9

    

     Th9: for X be RealNormSpace holds for f,g,h be Element of ( BoundedLinearOperators (X,X)) holds (f * (g + h)) = ((f * g) + (f * h))

    proof

      let X be RealNormSpace;

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

      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 . ((mf * mg),(mf * mh))) = (mf * mgh)

      proof

        reconsider fh = (mf * mh) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider fg = (mf * mg) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider k = (mf * mgh) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider hh = h as VECTOR of BLOP;

        reconsider gg = g as VECTOR of BLOP;

        

         A1: gg = mg & hh = mh by LOPBAN_1:def 11;

        for x be VECTOR of X holds ((mf * mgh) . x) = (((mf * mg) . x) + ((mf * mh) . x))

        proof

          let x be VECTOR of X;

          (g + h) = (gg + hh) & ( modetrans ((g + h),X,X)) = (g + h) by LOPBAN_1:def 11;

          then

           A2: (mgh . x) = ((mg . x) + (mh . x)) by A1, LOPBAN_1: 35;

          

          thus ((mf * mgh) . x) = (mf . (mgh . x)) by Th4

          .= ((mf . (mg . x)) + (mf . (mh . x))) by A2, VECTSP_1:def 20

          .= (((mf * mg) . x) + (mf . (mh . x))) by Th4

          .= (((mf * mg) . x) + ((mf * mh) . x)) by Th4;

        end;

        then k = (fg + fh) by LOPBAN_1: 35;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_2:10

    

     Th10: for X be RealNormSpace holds for f,g,h be Element of ( BoundedLinearOperators (X,X)) holds ((g + h) * f) = ((g * f) + (h * f))

    proof

      let X be RealNormSpace;

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

      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 . ((mg * mf),(mh * mf))) = (mgh * mf)

      proof

        reconsider hf = (mh * mf) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider gf = (mg * mf) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider k = (mgh * mf) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider hh = h as VECTOR of BLOP;

        reconsider gg = g as VECTOR of BLOP;

        

         A1: gg = mg & hh = mh by LOPBAN_1:def 11;

        for x be VECTOR of X holds ((mgh * mf) . x) = (((mg * mf) . x) + ((mh * mf) . x))

        proof

          let x be VECTOR of X;

          (g + h) = (gg + hh) & ( modetrans ((g + h),X,X)) = (g + h) by LOPBAN_1:def 11;

          then

           A2: (mgh . (mf . x)) = ((mg . (mf . x)) + (mh . (mf . x))) by A1, LOPBAN_1: 35;

          

          thus ((mgh * mf) . x) = (mgh . (mf . x)) by Th4

          .= (((mg * mf) . x) + (mh . (mf . x))) by A2, Th4

          .= (((mg * mf) . x) + ((mh * mf) . x)) by Th4;

        end;

        then k = (gf + hf) by LOPBAN_1: 35;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_2:11

    

     Th11: for X be RealNormSpace holds for f,g be Element of ( BoundedLinearOperators (X,X)) holds for a,b be Real holds ((a * b) * (f * g)) = ((a * f) * (b * g))

    proof

      let X be RealNormSpace;

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

      let a,b be Real;

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

      (EXMULT . ((a * b),(mf * mg))) = (maf * mbg)

      proof

        reconsider k = (maf * mbg) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider fg = (mf * mg) as VECTOR of BLOP by LOPBAN_1:def 9;

        reconsider ff = f, gg = g as VECTOR of BLOP;

        

         A1: gg = mg by LOPBAN_1:def 11;

        

         A2: ff = mf by LOPBAN_1:def 11;

        for x be VECTOR of X holds ((maf * mbg) . x) = ((a * b) * ((mf * mg) . x))

        proof

          let x be VECTOR of X;

          set y = (b * (mg . x));

          (a * f) = (a * ff) & ( modetrans ((a * f),X,X)) = (a * f) by LOPBAN_1:def 11;

          then

           A3: (maf . y) = (a * (mf . y)) by A2, LOPBAN_1: 36;

          (b * g) = (b * gg) & ( modetrans ((b * g),X,X)) = (b * g) by LOPBAN_1:def 11;

          then

           A4: (mbg . x) = (b * (mg . x)) by A1, LOPBAN_1: 36;

          

          thus ((maf * mbg) . x) = (maf . (mbg . x)) by Th4

          .= (a * (b * (mf . (mg . x)))) by A3, A4, LOPBAN_1:def 5

          .= ((a * b) * (mf . (mg . x))) by RLVECT_1:def 7

          .= ((a * b) * ((mf * mg) . x)) by Th4;

        end;

        then k = ((a * b) * fg) by LOPBAN_1: 36;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: LOPBAN_2:12

    

     Th12: for X be RealNormSpace holds for f,g be Element of ( BoundedLinearOperators (X,X)) holds for a be Real holds (a * (f * g)) = ((a * f) * g)

    proof

      let X be RealNormSpace;

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

      let a be Real;

      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 jj = 1 as Real;

      reconsider gg = g as Element of RRL;

      

       A1: (jj * g) = (jj * gg)

      .= g by RLVECT_1:def 8;

      (a * (f * g)) = ((a * jj) * (f * g))

      .= ((a * f) * (jj * g)) by Th11;

      hence thesis by A1;

    end;

    definition

      let X be RealNormSpace;

      :: LOPBAN_2:def6

      func Ring_of_BoundedLinearOperators (X) -> doubleLoopStr equals 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 ;

    end

    registration

      let X be RealNormSpace;

      cluster ( Ring_of_BoundedLinearOperators X) -> non empty strict;

      coherence ;

    end

     Lm1:

    now

      let X be RealNormSpace;

      set F = ( Ring_of_BoundedLinearOperators X);

      let x,e be Element of F;

      reconsider f = x as Element of ( BoundedLinearOperators (X,X));

      assume

       A1: e = ( FuncUnit X);

      

      hence (x * e) = (f * ( FuncUnit X)) by Def4

      .= x by Th8;

      

      thus (e * x) = (( FuncUnit X) * f) by A1, Def4

      .= x by Th8;

    end;

    registration

      let X be RealNormSpace;

      cluster ( Ring_of_BoundedLinearOperators X) -> unital;

      coherence

      proof

        reconsider e = ( FuncUnit X) as Element of ( Ring_of_BoundedLinearOperators X);

        take e;

        thus thesis by Lm1;

      end;

    end

    theorem :: LOPBAN_2:13

    

     Th13: for X be RealNormSpace holds for x,y,z be 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 be 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;

      let x,y,z be Element of ( Ring_of_BoundedLinearOperators 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 RRL;

      

      thus (x + y) = (f + g)

      .= (y + x) by RLVECT_1: 2;

      

      thus ((x + y) + z) = ((f + g) + h)

      .= (f + (g + h)) by RLVECT_1:def 3

      .= (x + (y + z));

      

      thus (x + ( 0. RBLOP)) = (f + ( 0. RRL))

      .= x;

      thus ex t be Element of RBLOP st (x + t) = ( 0. RBLOP)

      proof

        consider s be Element of RRL such that

         A1: (f + s) = ( 0. RRL) by ALGSTR_0:def 11;

        reconsider t = s as Element of RBLOP;

        take t;

        thus thesis by A1;

      end;

      reconsider xx = x, yy = y, zz = z as Element of BLOP;

      

      thus ((x * y) * z) = (MULT . ((xx * yy),zz)) by Def4

      .= ((xx * yy) * zz) by Def4

      .= (xx * (yy * zz)) by Th7

      .= (MULT . (xx,(yy * zz))) by Def4

      .= (x * (y * z)) by Def4;

      

      thus (x * ( 1. RBLOP)) = (xx * UNIT) by Def4

      .= x by Th8;

      

      thus (( 1. RBLOP) * x) = (UNIT * xx) by Def4

      .= x by Th8;

      

      thus (x * (y + z)) = (xx * (yy + zz)) by Def4

      .= ((xx * yy) + (xx * zz)) by Th9

      .= (ADD . ((xx * yy),(MULT . (xx,zz)))) by Def4

      .= ((x * y) + (x * z)) by Def4;

      

      thus ((y + z) * x) = ((yy + zz) * xx) by Def4

      .= ((yy * xx) + (zz * xx)) by Th10

      .= (ADD . ((yy * xx),(MULT . (zz,xx)))) by Def4

      .= ((y * x) + (z * x)) by Def4;

    end;

    theorem :: LOPBAN_2:14

    

     Th14: for X be RealNormSpace holds ( Ring_of_BoundedLinearOperators X) is Ring

    proof

      let X be RealNormSpace;

      set R = ( Ring_of_BoundedLinearOperators X);

      

       A1: R is right_complementable

      proof

        let x be Element of R;

        thus ex t be Element of R st (x + t) = ( 0. R) by Th13;

      end;

      for x,y,z be Element of R holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( Ring_of_BoundedLinearOperators X))) = x & (ex t be 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 thesis 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;

    end;

    registration

      let X be RealNormSpace;

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

      coherence by Th14;

    end

    definition

      let X be RealNormSpace;

      :: LOPBAN_2:def7

      func R_Algebra_of_BoundedLinearOperators (X) -> AlgebraStr equals 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 ;

    end

    registration

      let X be RealNormSpace;

      cluster ( R_Algebra_of_BoundedLinearOperators X) -> non empty strict;

      coherence ;

    end

     Lm2:

    now

      let X be RealNormSpace;

      set F = ( R_Algebra_of_BoundedLinearOperators X);

      let x,e be Element of F;

      reconsider f = x as Element of ( BoundedLinearOperators (X,X));

      assume

       A1: e = ( FuncUnit X);

      

      hence (x * e) = (f * ( FuncUnit X)) by Def4

      .= x by Th8;

      

      thus (e * x) = (( FuncUnit X) * f) by A1, Def4

      .= x by Th8;

    end;

    registration

      let X be RealNormSpace;

      cluster ( R_Algebra_of_BoundedLinearOperators X) -> unital;

      coherence

      proof

        reconsider e = ( FuncUnit X) as Element of ( R_Algebra_of_BoundedLinearOperators X);

        take e;

        thus thesis by Lm2;

      end;

    end

    theorem :: LOPBAN_2:15

    for X be RealNormSpace holds for x,y,z be Element of ( R_Algebra_of_BoundedLinearOperators X) holds for a,b be Real holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( R_Algebra_of_BoundedLinearOperators X))) = x & (ex t be 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;

      let x,y,z be Element of ( R_Algebra_of_BoundedLinearOperators X);

      let a,b be Real;

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

      

      thus (x + y) = (f + g)

      .= (y + x) by RLVECT_1: 2;

      

      thus ((x + y) + z) = ((f + g) + h)

      .= (f + (g + h)) by RLVECT_1:def 3

      .= (x + (y + z));

      

      thus (x + ( 0. RBLOP)) = (f + ( 0. RRL))

      .= x;

      thus ex t be Element of RBLOP st (x + t) = ( 0. RBLOP)

      proof

        consider s be Element of RRL such that

         A1: (f + s) = ( 0. RRL) by ALGSTR_0:def 11;

        reconsider t = s as Element of RBLOP;

        take t;

        thus thesis by A1;

      end;

      reconsider xx = x, yy = y, zz = z as Element of BLOP;

      

      thus ((x * y) * z) = (MULT . ((xx * yy),zz)) by Def4

      .= ((xx * yy) * zz) by Def4

      .= (xx * (yy * zz)) by Th7

      .= (MULT . (xx,(yy * zz))) by Def4

      .= (x * (y * z)) by Def4;

      

      thus (x * ( 1. RBLOP)) = (xx * UNIT) by Def4

      .= x by Th8;

      

      thus (( 1. RBLOP) * x) = (UNIT * xx) by Def4

      .= x by Th8;

      

      thus (x * (y + z)) = (xx * (yy + zz)) by Def4

      .= ((xx * yy) + (xx * zz)) by Th9

      .= (ADD . ((xx * yy),(MULT . (xx,zz)))) by Def4

      .= ((x * y) + (x * z)) by Def4;

      

      thus ((y + z) * x) = ((yy + zz) * xx) by Def4

      .= ((yy * xx) + (zz * xx)) by Th10

      .= (ADD . ((yy * xx),(MULT . (zz,xx)))) by Def4

      .= ((y * x) + (z * x)) by Def4;

      

      thus (a * (x * y)) = (a * (xx * yy)) by Def4

      .= ((a * xx) * yy) by Th12

      .= ((a * x) * y) by Def4;

      

      thus (a * (x + y)) = (a * (f + g))

      .= ((a * f) + (a * g)) by RLVECT_1:def 5

      .= ((a * x) + (a * y));

      

      thus ((a + b) * x) = ((a + b) * f)

      .= ((a * f) + (b * f)) by RLVECT_1:def 6

      .= ((a * x) + (b * x));

      

      thus ((a * b) * x) = ((a * b) * f)

      .= (a * (b * f)) by RLVECT_1:def 7

      .= (a * (b * x));

      

      thus ((a * b) * (x * y)) = ((a * b) * (xx * yy)) by Def4

      .= ((a * xx) * (b * yy)) by Th11

      .= ((a * x) * (b * y)) by Def4;

    end;

    definition

      mode BLAlgebra is Abelian add-associative right_zeroed right_complementable associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative non empty AlgebraStr;

    end

    registration

      let X be RealNormSpace;

      cluster ( R_Algebra_of_BoundedLinearOperators X) -> Abelian add-associative right_zeroed right_complementable associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative strict;

      coherence

      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 A is Abelian

        proof

          let x,y be Element of A;

          reconsider f = x, g = y as Element of RRL;

          

          thus (x + y) = (f + g)

          .= (y + x) by RLVECT_1: 2;

        end;

        thus A is add-associative

        proof

          let x,y,z be Element of A;

          reconsider f = x, g = y, h = z as Element of RRL;

          

          thus ((x + y) + z) = ((f + g) + h)

          .= (f + (g + h)) by RLVECT_1:def 3

          .= (x + (y + z));

        end;

        thus A is right_zeroed

        proof

          let x be Element of A;

          reconsider f = x as Element of RRL;

          

          thus (x + ( 0. A)) = (f + ( 0. RRL))

          .= x;

        end;

        thus A is right_complementable

        proof

          let x be Element of A;

          reconsider f = x as Element of RRL;

          consider s be Element of RRL such that

           A1: (f + s) = ( 0. RRL) by ALGSTR_0:def 11;

          reconsider t = s as Element of A;

          take t;

          thus thesis by A1;

        end;

        thus A is associative

        proof

          let x,y,z be Element of A;

          reconsider xx = x, yy = y, zz = z as Element of BLOP;

          

          thus ((x * y) * z) = (MULT . ((xx * yy),zz)) by Def4

          .= ((xx * yy) * zz) by Def4

          .= (xx * (yy * zz)) by Th7

          .= (MULT . (xx,(yy * zz))) by Def4

          .= (x * (y * z)) by Def4;

        end;

        thus A is right_unital

        proof

          let x be Element of A;

          reconsider xx = x as Element of BLOP;

          

          thus (x * ( 1. A)) = (xx * UNIT) by Def4

          .= x by Th8;

        end;

        thus A is right-distributive

        proof

          let x,y,z be Element of A;

          reconsider xx = x, yy = y, zz = z as Element of BLOP;

          

          thus (x * (y + z)) = (xx * (yy + zz)) by Def4

          .= ((xx * yy) + (xx * zz)) by Th9

          .= (ADD . ((xx * yy),(MULT . (xx,zz)))) by Def4

          .= ((x * y) + (x * z)) by Def4;

        end;

        thus A is vector-distributive

        proof

          let a be Real;

          let x,y be Element of A;

          reconsider f = x, g = y as Element of RRL;

          

          thus (a * (x + y)) = (a * (f + g))

          .= ((a * f) + (a * g)) by RLVECT_1:def 5

          .= ((a * x) + (a * y));

        end;

        thus A is scalar-distributive

        proof

          let a,b be Real;

          let x be Element of A;

          reconsider f = x as Element of RRL;

          

          thus ((a + b) * x) = ((a + b) * f)

          .= ((a * f) + (b * f)) by RLVECT_1:def 6

          .= ((a * x) + (b * x));

        end;

        thus A is scalar-associative

        proof

          let a,b be Real;

          let x be Element of A;

          reconsider f = x as Element of RRL;

          

          thus ((a * b) * x) = ((a * b) * f)

          .= (a * (b * f)) by RLVECT_1:def 7

          .= (a * (b * x));

        end;

        thus A is vector-associative

        proof

          let x,y be Element of A;

          let a be Real;

          reconsider xx = x, yy = y as Element of BLOP;

          

          thus (a * (x * y)) = (a * (xx * yy)) by Def4

          .= ((a * xx) * yy) by Th12

          .= ((a * x) * y) by Def4;

        end;

        thus thesis;

      end;

    end

    theorem :: LOPBAN_2:16

    for X be RealNormSpace holds ( R_Algebra_of_BoundedLinearOperators X) is BLAlgebra;

    registration

      cluster l1_Space -> complete;

      coherence by RSSPACE3: 9;

    end

    registration

      cluster l1_Space -> non trivial;

      coherence

      proof

        set a = (1 / 2);

        reconsider x = (a GeoSeq ) as Real_Sequence;

        

         A1: |.a.| = (1 / 2) by ABSVALUE:def 1;

        defpred P[ Nat] means 0 <= (x . $1);

        

         A2: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          (x . (n + 1)) = ((x . n) * a) by PREPOWER: 3;

          hence thesis;

        end;

        

         A4: P[ 0 ] by PREPOWER: 3;

        for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

        then x is absolutely_summable by A1, SERIES_1: 24, SERIES_1: 36;

        then ( seq_id x) is absolutely_summable;

        then

        reconsider v = x as VECTOR of l1_Space by RSSPACE3: 6;

        (( seq_id v) . 0 ) = 1 by PREPOWER: 3;

        then v <> ( seq_id Zeroseq ) by RSSPACE: 4;

        hence thesis by RSSPACE3: 6;

      end;

    end

    registration

      cluster non trivial for RealBanachSpace;

      existence

      proof

        take l1_Space ;

        thus thesis;

      end;

    end

    theorem :: LOPBAN_2:17

    

     Th17: for X be non trivial RealNormSpace holds ex w be VECTOR of X st ||.w.|| = 1

    proof

      let X be non trivial RealNormSpace;

      consider v be VECTOR of X such that

       A1: v <> ( 0. X) by STRUCT_0:def 18;

      set a = ||.v.||;

      reconsider w = ((a " ) * v) as VECTOR of X;

      take w;

      

       A2: ||.v.|| <> 0 by A1, NORMSP_0:def 5;

      then

       A3: 0 < ||.v.|| by NORMSP_1: 4;

      

       A4: |.(a " ).| = |.(1 * (a " )).|

      .= |.(1 / a).| by XCMPLX_0:def 9

      .= (1 / |.a.|) by ABSVALUE: 7

      .= (1 * ( |.a.| " )) by XCMPLX_0:def 9

      .= (a " ) by A3, ABSVALUE:def 1;

      

      thus ||.w.|| = ( |.(a " ).| * ||.v.||) by NORMSP_1:def 1

      .= 1 by A2, A4, XCMPLX_0:def 7;

    end;

    theorem :: LOPBAN_2:18

    

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

    proof

      let X be non trivial RealNormSpace;

      consider v be 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

        let r be Real;

        assume r in ( PreNorms ii);

        then ex t be VECTOR of X st r = ||.(ii . t).|| & ||.t.|| <= 1;

        hence r <= 1;

      end;

      (ii . v) = v;

      then

       A3: 1 in { ||.(ii . t).|| where t be VECTOR of X : ||.t.|| <= 1 } by A1;

      ( PreNorms ii) is non empty bounded_above by LOPBAN_1: 27;

      then

       A4: 1 <= ( upper_bound ( PreNorms ii)) by A3, SEQ_4:def 1;

      (for s be Real 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 thesis by LOPBAN_1: 30;

    end;

    definition

      struct ( AlgebraStr, NORMSTR) Normed_AlgebraStr (# the carrier -> set,

the multF, addF -> BinOp of the carrier,

the Mult -> Function of [: REAL , the carrier:], the carrier,

the OneF, ZeroF -> Element of the carrier,

the normF -> Function of the carrier, REAL #)

       attr strict strict;

    end

    registration

      cluster non empty for Normed_AlgebraStr;

      existence

      proof

        set A = the non empty set, m = the BinOp of A, a = the BinOp of A, M = the Function of [: REAL , A:], A, U = the Element of A, Z = the Element of A, n = the Function of A, REAL ;

        take Normed_AlgebraStr (# A, m, a, M, U, Z, n #);

        thus the carrier of Normed_AlgebraStr (# A, m, a, M, U, Z, n #) is non empty;

      end;

    end

    definition

      let X be RealNormSpace;

      :: LOPBAN_2:def8

      func R_Normed_Algebra_of_BoundedLinearOperators (X) -> Normed_AlgebraStr equals 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 ;

    end

    registration

      let X be RealNormSpace;

      cluster ( R_Normed_Algebra_of_BoundedLinearOperators X) -> non empty strict;

      coherence ;

    end

     Lm3:

    now

      let X be RealNormSpace;

      set F = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      let x,e be Element of F;

      reconsider f = x as Element of ( BoundedLinearOperators (X,X));

      assume

       A1: e = ( FuncUnit X);

      

      hence (x * e) = (f * ( FuncUnit X)) by Def4

      .= x by Th8;

      

      thus (e * x) = (( FuncUnit X) * f) by A1, Def4

      .= x by Th8;

    end;

    registration

      let X be RealNormSpace;

      cluster ( R_Normed_Algebra_of_BoundedLinearOperators X) -> unital;

      coherence

      proof

        reconsider e = ( FuncUnit X) as Element of ( R_Normed_Algebra_of_BoundedLinearOperators X);

        take e;

        thus thesis by Lm3;

      end;

    end

    theorem :: LOPBAN_2:19

    

     Th19: for X be RealNormSpace holds for x,y,z be Element of ( R_Normed_Algebra_of_BoundedLinearOperators X) holds for a,b be Real holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( R_Normed_Algebra_of_BoundedLinearOperators X))) = x & (ex t be 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;

      let x,y,z be Element of ( R_Normed_Algebra_of_BoundedLinearOperators X);

      let a,b be Real;

      reconsider a1 = a, b1 = b as Real;

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

      

      thus (x + y) = (f + g)

      .= (y + x) by RLVECT_1: 2;

      

      thus ((x + y) + z) = ((f + g) + h)

      .= (f + (g + h)) by RLVECT_1:def 3

      .= (x + (y + z));

      

      thus (x + ( 0. RBLOP)) = (f + ( 0. RRL))

      .= x;

      thus ex t be Element of RBLOP st (x + t) = ( 0. RBLOP)

      proof

        consider s be Element of RRL such that

         A1: (f + s) = ( 0. RRL) by ALGSTR_0:def 11;

        reconsider t = s as Element of RBLOP;

        take t;

        thus thesis by A1;

      end;

      reconsider xx = x, yy = y, zz = z as Element of BLOP;

      

      thus ((x * y) * z) = (MULT . ((xx * yy),zz)) by Def4

      .= ((xx * yy) * zz) by Def4

      .= (xx * (yy * zz)) by Th7

      .= (MULT . (xx,(yy * zz))) by Def4

      .= (x * (y * z)) by Def4;

      

      thus (x * ( 1. RBLOP)) = (xx * UNIT) by Def4

      .= x by Th8;

      

      thus (( 1. RBLOP) * x) = (UNIT * xx) by Def4

      .= x by Th8;

      

      thus (x * (y + z)) = (xx * (yy + zz)) by Def4

      .= ((xx * yy) + (xx * zz)) by Th9

      .= (ADD . ((xx * yy),(MULT . (xx,zz)))) by Def4

      .= ((x * y) + (x * z)) by Def4;

      

      thus ((y + z) * x) = ((yy + zz) * xx) by Def4

      .= ((yy * xx) + (zz * xx)) by Th10

      .= (ADD . ((yy * xx),(MULT . (zz,xx)))) by Def4

      .= ((y * x) + (z * x)) by Def4;

      

      thus (a * (x * y)) = (a1 * (xx * yy)) by Def4

      .= ((a1 * xx) * yy) by Th12

      .= ((a * x) * y) by Def4;

      

      thus ((a * b) * (x * y)) = ((a1 * b1) * (xx * yy)) by Def4

      .= ((a1 * xx) * (b1 * yy)) by Th11

      .= ((a * x) * (b * y)) by Def4;

      

      thus (a * (x + y)) = (a * (f + g))

      .= ((a * f) + (a * g)) by RLVECT_1:def 5

      .= ((a * x) + (a * y));

      

      thus ((a + b) * x) = ((a + b) * f)

      .= ((a * f) + (b * f)) by RLVECT_1:def 6

      .= ((a * x) + (b * x));

      

      thus ((a * b) * x) = ((a * b) * f)

      .= (a * (b * f)) by RLVECT_1:def 7

      .= (a * (b * x));

      

      thus (1 * x) = (1 * f)

      .= x by RLVECT_1:def 8;

    end;

    theorem :: LOPBAN_2:20

    

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

    proof

      let X be RealNormSpace;

      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. BS).|| = (NRM . ( 0. BS))

      .= ||.( 0. RBLOP).||;

      thus ||.( 0. RBLOP).|| = 0 by A1;

       A2:

      now

        let x,y be Point of RBLOP;

        let a be Real;

        reconsider x1 = x, y1 = y as Point of BS;

        

         A3: ( ||.x1.|| + ||.y1.||) = ((NRM . x1) + ||.y1.||)

        .= ((NRM . x1) + (NRM . y1))

        .= ( ||.x.|| + (the normF of RBLOP . y))

        .= ( ||.x.|| + ||.y.||);

         ||.(x + y).|| = (NRM . (ADD . (x,y)))

        .= ||.(x1 + y1).||;

        hence ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by A3, NORMSP_1:def 1;

        

         A4: ||.x1.|| = (NRM . x1)

        .= ||.x.||;

        ( 0. BS) = ( 0. RBLOP);

        hence ||.x.|| = 0 iff x = ( 0. RBLOP) by A4, NORMSP_0:def 5;

        

        thus ||.(a * x).|| = (NRM . (EXMULT . (a,x)))

        .= ||.(a * x1).||

        .= ( |.a.| * ||.x.||) by A4, NORMSP_1:def 1;

      end;

      

       A5: RBLOP is right_complementable

      proof

        let x be Element of RBLOP;

        thus ex t be Element of RBLOP st (x + t) = ( 0. RBLOP) by Th19;

      end;

      (for x,y,z be Element of ( R_Normed_Algebra_of_BoundedLinearOperators X) holds for a,b be Real holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( R_Normed_Algebra_of_BoundedLinearOperators X))) = x & (ex t be 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 be Real holds for v,w be VECTOR of RBLOP holds (a * (v + w)) = ((a * v) + (a * w)) by Th19;

      hence thesis by A5, A2, NORMSP_1:def 1;

    end;

    registration

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

      existence

      proof

        set X = the RealNormSpace;

        take ( R_Normed_Algebra_of_BoundedLinearOperators X);

        thus thesis by Th20;

      end;

    end

    definition

      mode Normed_Algebra is reflexive discerning RealNormSpace-like Abelian add-associative right_zeroed right_complementable associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative scalar-unital non empty Normed_AlgebraStr;

    end

    registration

      let X be RealNormSpace;

      cluster ( R_Normed_Algebra_of_BoundedLinearOperators X) -> reflexive discerning RealNormSpace-like Abelian add-associative right_zeroed right_complementable associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative scalar-unital;

      correctness by Th20;

    end

    definition

      let X be non empty Normed_AlgebraStr;

      :: LOPBAN_2:def9

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

      :: LOPBAN_2:def10

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

      :: LOPBAN_2:def11

      attr X is Banach_Algebra-like_3 means for a be Real holds for x,y be Element of X holds (a * (x * y)) = (x * (a * y));

    end

    definition

      let X be Normed_Algebra;

      :: LOPBAN_2:def12

      attr X is Banach_Algebra-like means X is Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 left_unital left-distributive complete;

    end

    registration

      cluster Banach_Algebra-like -> Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 left-distributive left_unital complete for Normed_Algebra;

      coherence ;

      cluster Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 left-distributive left_unital complete -> Banach_Algebra-like for Normed_Algebra;

      coherence ;

    end

    registration

      let X be non trivial RealBanachSpace;

      cluster ( R_Normed_Algebra_of_BoundedLinearOperators X) -> Banach_Algebra-like;

      coherence

      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 RBLOP is Banach_Algebra-like_1

        proof

          let x,y be Point of RBLOP;

          reconsider x1 = x, y1 = y as Element of BLOP;

          

           A1: ((NRM . ( modetrans (x1,X,X))) * (NRM . ( modetrans (y1,X,X)))) = ((NRM . x1) * (NRM . ( modetrans (y1,X,X)))) by LOPBAN_1:def 11

          .= ((NRM . x1) * (NRM . y1)) by LOPBAN_1:def 11

          .= ( ||.x.|| * (NRM . y))

          .= ( ||.x.|| * ||.y.||);

           ||.(x * y).|| = (NRM . (MULT . (x,y)))

          .= (NRM . (x1 * y1)) by Def4

          .= (NRM . (( modetrans (x1,X,X)) * ( modetrans (y1,X,X))));

          hence thesis by A1, Th2;

        end;

         ||.( 1. RBLOP).|| = (NRM . ( id the carrier of X))

        .= 1 by Th18;

        hence RBLOP is Banach_Algebra-like_2;

        thus RBLOP is Banach_Algebra-like_3

        proof

          let a be Real;

          let x,y be Element of RBLOP;

          

          thus (a * (x * y)) = ((1 * a) * (x * y))

          .= ((1 * x) * (a * y)) by Th19

          .= (x * (a * y)) by Th19;

        end;

        thus RBLOP is left_unital

        proof

          let x be Element of RBLOP;

          reconsider xx = x as Element of BLOP;

          (UNIT * xx) = xx by Th8;

          hence thesis by Def4;

        end;

        thus RBLOP is left-distributive

        proof

          let x,y,z be Element of RBLOP;

          reconsider xx = x, yy = y, zz = z as Element of BLOP;

          

          thus ((y + z) * x) = ((yy + zz) * xx) by Def4

          .= ((yy * xx) + (zz * xx)) by Th10

          .= (ADD . ((yy * xx),(MULT . (zz,xx)))) by Def4

          .= ((y * x) + (z * x)) by Def4;

        end;

        now

          let seq be sequence of RBLOP such that

           A2: seq is Cauchy_sequence_by_Norm;

          reconsider seq1 = seq as sequence of BS;

          now

            let r be Real;

            assume r > 0 ;

            then

            consider k be Nat such that

             A3: for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by A2, RSSPACE3: 8;

            now

              let n,m be Nat such that

               A4: n >= k & m >= k;

               ||.((seq1 . n) - (seq1 . m)).|| = (NRM . ((seq1 . n) + ( - (seq1 . m))))

              .= (NRM . (ADD . ((seq1 . n),(( - 1) * (seq1 . m))))) by RLVECT_1: 16

              .= (NRM . (ADD . ((seq . n),(( - 1) * (seq . m)))))

              .= (NRM . ((seq . n) + ( - (seq . m)))) by RLVECT_1: 16

              .= ||.((seq . n) - (seq . m)).||;

              hence ||.((seq1 . n) - (seq1 . m)).|| < r by A3, A4;

            end;

            hence ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((seq1 . n) - (seq1 . m)).|| < r;

          end;

          then seq1 is Cauchy_sequence_by_Norm by RSSPACE3: 8;

          then seq1 is convergent by LOPBAN_1:def 15;

          then

          consider g1 be Point of BS such that

           A5: for r be Real st 0 < r holds ex m be Nat st for n be Nat st m <= n holds ||.((seq1 . n) - g1).|| < r by NORMSP_1:def 6;

          reconsider g = g1 as Point of RBLOP;

          now

            let r be Real;

            assume 0 < r;

            then

            consider m be Nat such that

             A6: for n be Nat st m <= n holds ||.((seq1 . n) - g1).|| < r by A5;

            now

              let n be Nat such that

               A7: m <= n;

               ||.((seq1 . n) - g1).|| = (NRM . ((seq1 . n) + ( - g1)))

              .= (NRM . (ADD . ((seq1 . n),(( - 1) * g1)))) by RLVECT_1: 16

              .= (NRM . (ADD . ((seq . n),(( - 1) * g))))

              .= (NRM . ((seq . n) + ( - g))) by RLVECT_1: 16

              .= ||.((seq . n) - g).||;

              hence ||.((seq . n) - g).|| < r by A6, A7;

            end;

            hence ex m be Nat st for n be Nat st m <= n holds ||.((seq . n) - g).|| < r;

          end;

          hence seq is convergent by NORMSP_1:def 6;

        end;

        hence thesis;

      end;

    end

    registration

      cluster Banach_Algebra-like for Normed_Algebra;

      existence

      proof

        set X = the non trivial RealBanachSpace;

        take ( R_Normed_Algebra_of_BoundedLinearOperators X);

        thus thesis;

      end;

    end

    definition

      mode Banach_Algebra is Banach_Algebra-like Normed_Algebra;

    end

    theorem :: LOPBAN_2:21

    for X be RealNormSpace holds ( 1. ( Ring_of_BoundedLinearOperators X)) = ( FuncUnit X);

    theorem :: LOPBAN_2:22

    for X be RealNormSpace holds ( 1. ( R_Algebra_of_BoundedLinearOperators X)) = ( FuncUnit X);

    theorem :: LOPBAN_2:23

    for X be RealNormSpace holds ( 1. ( R_Normed_Algebra_of_BoundedLinearOperators X)) = ( FuncUnit X);