clopban2.miz



    begin

    theorem :: CLOPBAN2:1

    

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

    proof

      let X,Y,Z be ComplexLinearSpace;

      let f be LinearOperator of X, Y;

      let g be LinearOperator of Y, Z;

       A1:

      now

        let v be VECTOR of X, z be Complex;

        

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

        .= (g . (z * (f . v))) by CLOPBAN1:def 3

        .= (z * (g . (f . v))) by CLOPBAN1:def 3

        .= (z * ((g * f) . v)) by FUNCT_2: 15;

      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, CLOPBAN1:def 3, VECTSP_1:def 20;

    end;

    theorem :: CLOPBAN2:2

    

     Th2: for X,Y,Z be ComplexNormSpace 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 ComplexNormSpace;

      let f be Lipschitzian LinearOperator of X, Y;

      let g be Lipschitzian LinearOperator of Y, Z;

      reconsider ff = f as Point of ( C_NormSpace_of_BoundedLinearOperators (X,Y)) by CLOPBAN1:def 7;

      reconsider gg = g as Point of ( C_NormSpace_of_BoundedLinearOperators (Y,Z)) by CLOPBAN1:def 7;

       A1:

      now

        let v be VECTOR of X;

         0 <= ||.gg.|| by CLVECT_1: 105;

        then

         A2: ( ||.gg.|| * ||.(f . v).||) <= ( ||.gg.|| * ( ||.ff.|| * ||.v.||)) by CLOPBAN1: 31, XREAL_1: 64;

         ||.((g * f) . v).|| = ||.(g . (f . v)).|| & ||.(g . (f . v)).|| <= ( ||.gg.|| * ||.(f . v).||) by CLOPBAN1: 31, FUNCT_2: 15;

        hence ||.((g * f) . v).|| <= (( ||.gg.|| * ||.ff.||) * ||.v.||) by A2, XXREAL_0: 2;

      end;

      set K = ( ||.gg.|| * ||.ff.||);

      

       A3: 0 <= ||.gg.|| & 0 <= ||.ff.|| by CLVECT_1: 105;

      then

      reconsider gf = (g * f) as Lipschitzian LinearOperator of X, Z by A1, Th1, CLOPBAN1:def 6;

       A4:

      now

        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, CLOPBAN1: 29;

    end;

    definition

      let X be ComplexNormSpace;

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

      :: original: *

      redefine

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

      correctness by Th2;

    end

    definition

      let X be ComplexNormSpace;

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

      :: CLOPBAN2:def1

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

      correctness ;

    end

    definition

      let X be ComplexNormSpace;

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

      :: CLOPBAN2:def2

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

      correctness by CLOPBAN1:def 7;

    end

    definition

      let X be ComplexNormSpace;

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

      let z be Complex;

      :: CLOPBAN2:def3

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

      correctness

      proof

        reconsider z as Element of COMPLEX by XCMPLX_0:def 2;

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

        hence thesis;

      end;

    end

    definition

      let X be ComplexNormSpace;

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

      end;

    end

    theorem :: CLOPBAN2:3

    

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

    proof

      let X be ComplexNormSpace;

      

       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, z be Complex holds (( id the carrier of X) . (z * v)) = (z * (( 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, CLOPBAN1:def 3, CLOPBAN1:def 6, VECTSP_1:def 20;

    end;

    definition

      let X be ComplexNormSpace;

      :: CLOPBAN2: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 CLOPBAN1:def 7;

      end;

    end

    theorem :: CLOPBAN2:4

    

     Th4: for X be ComplexNormSpace 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 ComplexNormSpace;

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

    

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

    proof

      let X be ComplexNormSpace;

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

    

     Th6: for X be ComplexNormSpace 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 ComplexNormSpace;

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

    

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

    proof

      let X be ComplexNormSpace;

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

      ( modetrans ((g * h),X,X)) = (( modetrans (g,X,X)) * ( modetrans (h,X,X))) by CLOPBAN1:def 9;

      then (( modetrans (f,X,X)) * ( modetrans ((g * h),X,X))) = ((( modetrans (f,X,X)) * ( modetrans (g,X,X))) * ( modetrans (h,X,X))) by Th5;

      hence thesis by CLOPBAN1:def 9;

    end;

    theorem :: CLOPBAN2:8

    

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

    proof

      let X be ComplexNormSpace;

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

      then

       A1: ( modetrans (( id the carrier of X),X,X)) = ( id the carrier of X) by CLOPBAN1:def 9;

      

      hence (f * ( FuncUnit X)) = ( modetrans (f,X,X)) by Th6

      .= f by CLOPBAN1:def 9;

      

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

      .= f by CLOPBAN1:def 9;

    end;

    theorem :: CLOPBAN2:9

    

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

    proof

      let X be ComplexNormSpace;

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

      set BLOP = ( C_NormSpace_of_BoundedLinearOperators (X,X));

      set ADD = ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X))));

      set mf = ( modetrans (f,X,X));

      set mg = ( modetrans (g,X,X));

      set mh = ( modetrans (h,X,X));

      set mgh = ( modetrans ((g + h),X,X));

      (ADD . ((mf * mg),(mf * mh))) = (mf * mgh)

      proof

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

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

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

        reconsider hh = h as VECTOR of BLOP;

        reconsider gg = g as VECTOR of BLOP;

        

         A1: gg = mg & hh = mh by CLOPBAN1:def 9;

        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 CLOPBAN1:def 9;

          then

           A2: (mgh . x) = ((mg . x) + (mh . x)) by A1, CLOPBAN1: 34;

          

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

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: CLOPBAN2:10

    

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

    proof

      let X be ComplexNormSpace;

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

      set BLOP = ( C_NormSpace_of_BoundedLinearOperators (X,X));

      set ADD = ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X))));

      set mf = ( modetrans (f,X,X));

      set mg = ( modetrans (g,X,X));

      set mh = ( modetrans (h,X,X));

      set mgh = ( modetrans ((g + h),X,X));

      (ADD . ((mg * mf),(mh * mf))) = (mgh * mf)

      proof

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

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

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

        reconsider hh = h as VECTOR of BLOP;

        reconsider gg = g as VECTOR of BLOP;

        

         A1: gg = mg & hh = mh by CLOPBAN1:def 9;

        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 CLOPBAN1:def 9;

          then

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

          

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

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: CLOPBAN2:11

    

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

    proof

      let X be ComplexNormSpace;

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

      let a,b be Complex;

      set BLOP = ( C_NormSpace_of_BoundedLinearOperators (X,X));

      set EXMULT = ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X))));

      set mf = ( modetrans (f,X,X));

      set mg = ( modetrans (g,X,X));

      set maf = ( modetrans ((a * f),X,X));

      set mbg = ( modetrans ((b * g),X,X));

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

      proof

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

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

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

        

         A1: gg = mg by CLOPBAN1:def 9;

        

         A2: ff = mf by CLOPBAN1:def 9;

        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 CLOPBAN1:def 9;

          then

           A3: (maf . y) = (a * (mf . y)) by A2, CLOPBAN1: 35;

          (b * g) = (b * gg) & ( modetrans ((b * g),X,X)) = (b * g) by CLOPBAN1:def 9;

          then

           A4: (mbg . x) = (b * (mg . x)) by A1, CLOPBAN1: 35;

          

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

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

          .= ((a * b) * (mf . (mg . x))) by CLVECT_1:def 4

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

        end;

        then k = ((a * b) * fg) by CLOPBAN1: 35;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: CLOPBAN2:12

    

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

    proof

      let X be ComplexNormSpace;

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

      let a be Complex;

      set RRL = CLSStruct (# ( BoundedLinearOperators (X,X)), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))) #);

      reconsider gg = g as Element of RRL;

      

       A1: ( 1r * g) = ( 1r * gg)

      .= g by CLVECT_1:def 5;

      (a * (f * g)) = ((a * 1r ) * (f * g)) by COMPLEX1:def 4

      .= ((a * f) * ( 1r * g)) by Th11;

      hence thesis by A1;

    end;

    definition

      let X be ComplexNormSpace;

      :: CLOPBAN2:def6

      func Ring_of_BoundedLinearOperators (X) -> doubleLoopStr equals doubleLoopStr (# ( BoundedLinearOperators (X,X)), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( FuncMult X), ( FuncUnit X), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))) #);

      correctness ;

    end

    registration

      let X be ComplexNormSpace;

      cluster ( Ring_of_BoundedLinearOperators X) -> non empty strict;

      coherence ;

    end

     Lm1:

    now

      let X be ComplexNormSpace;

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

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

    

     Th13: for X be ComplexNormSpace 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 & x is right_complementable & ((x * y) * z) = (x * (y * z)) & (x * ( 1. ( Ring_of_BoundedLinearOperators X))) = x & (( 1. ( Ring_of_BoundedLinearOperators X)) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x))

    proof

      let X be ComplexNormSpace;

      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)),( C_VectorSpace_of_LinearOperators (X,X))));

      set MULT = ( FuncMult X);

      set UNIT = ( FuncUnit X);

      set RRL = CLSStruct (# ( BoundedLinearOperators (X,X)), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))) #);

      reconsider f = x, g = y, h = z as Element of 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 by RLVECT_1:def 4;

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

    

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

    proof

      let X be ComplexNormSpace;

      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 & x is right_complementable & ((x * y) * z) = (x * (y * z)) & (x * ( 1. ( Ring_of_BoundedLinearOperators X))) = x & (( 1. ( Ring_of_BoundedLinearOperators X)) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x)) by Th13;

      hence thesis by ALGSTR_0:def 16, GROUP_1:def 3, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, VECTSP_1:def 6, VECTSP_1:def 7;

    end;

    registration

      let X be ComplexNormSpace;

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

      coherence by Th14;

    end

    definition

      let X be ComplexNormSpace;

      :: CLOPBAN2:def7

      func C_Algebra_of_BoundedLinearOperators (X) -> ComplexAlgebraStr equals ComplexAlgebraStr (# ( BoundedLinearOperators (X,X)), ( FuncMult X), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( FuncUnit X), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))) #);

      correctness ;

    end

    registration

      let X be ComplexNormSpace;

      cluster ( C_Algebra_of_BoundedLinearOperators X) -> non empty strict;

      coherence ;

    end

     Lm2:

    now

      let X be ComplexNormSpace;

      set F = ( C_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 ComplexNormSpace;

      cluster ( C_Algebra_of_BoundedLinearOperators X) -> unital;

      coherence

      proof

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

        take e;

        thus thesis by Lm2;

      end;

    end

    theorem :: CLOPBAN2:15

    for X be ComplexNormSpace holds for x,y,z be Element of ( C_Algebra_of_BoundedLinearOperators X) holds for a,b be Complex holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( C_Algebra_of_BoundedLinearOperators X))) = x & x is right_complementable & ((x * y) * z) = (x * (y * z)) & (x * ( 1. ( C_Algebra_of_BoundedLinearOperators X))) = x & (( 1. ( C_Algebra_of_BoundedLinearOperators X)) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x)) & (a * (x * y)) = ((a * x) * y) & (a * (x + y)) = ((a * x) + (a * y)) & ((a + b) * x) = ((a * x) + (b * x)) & ((a * b) * x) = (a * (b * x)) & ((a * b) * (x * y)) = ((a * x) * (b * y))

    proof

      let X be ComplexNormSpace;

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

      let a,b be Complex;

      set RBLOP = ( C_Algebra_of_BoundedLinearOperators X);

      set BLOP = ( BoundedLinearOperators (X,X));

      set ADD = ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X))));

      set MULT = ( FuncMult X);

      set UNIT = ( FuncUnit X);

      set RRL = CLSStruct (# ( BoundedLinearOperators (X,X)), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))) #);

      reconsider f = x, g = y, h = z as Element of 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 by RLVECT_1:def 4;

      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 CLVECT_1:def 2

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

      

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

      .= ((a * f) + (b * f)) by CLVECT_1:def 3

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

      

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

      .= (a * (b * f)) by CLVECT_1:def 4

      .= (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 ComplexBLAlgebra is Abelian add-associative right_zeroed right_complementable associative right_unital right-distributive vector-distributive scalar-distributive scalar-associative vector-associative non empty ComplexAlgebraStr;

    end

    registration

      let X be ComplexNormSpace;

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

      coherence

      proof

        set A = ( C_Algebra_of_BoundedLinearOperators X);

        set MULT = ( FuncMult X);

        set UNIT = ( FuncUnit X);

        set BLOP = ( BoundedLinearOperators (X,X));

        set ADD = ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X))));

        set RRL = CLSStruct (# ( BoundedLinearOperators (X,X)), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))) #);

        thus 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 by RLVECT_1:def 4;

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

          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 CLVECT_1:def 2

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

        end;

        thus A is scalar-distributive

        proof

          let a,b be Complex;

          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 CLVECT_1:def 3

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

        end;

        thus A is scalar-associative

        proof

          let a,b be Complex;

          let x be Element of A;

          reconsider f = x as Element of RRL;

          

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

          .= (a * (b * f)) by CLVECT_1:def 4

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

        end;

        let x,y be Element of A;

        let a be Complex;

        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;

    end

    theorem :: CLOPBAN2:16

    for X be ComplexNormSpace holds ( C_Algebra_of_BoundedLinearOperators X) is ComplexBLAlgebra;

    registration

      cluster Complex_l1_Space -> complete;

      coherence by CSSPACE3: 9;

    end

    registration

      cluster Complex_l1_Space -> non trivial;

      coherence

      proof

        reconsider a = ((1 / 2) + ( 0 * <i> )) as Element of COMPLEX by XCMPLX_0:def 2;

        reconsider x = (a GeoSeq ) as Complex_Sequence;

        

         A1: for m be Nat holds ( |.x.| . (m + 1)) = (( |.x.| . m) * |.a.|)

        proof

          let m be Nat;

          ( |.x.| . (m + 1)) = |.(x . (m + 1)).| by VALUED_1: 18

          .= |.((x . m) * a).| by COMSEQ_3:def 1

          .= ( |.(x . m).| * |.a.|) by COMPLEX1: 65;

          hence thesis by VALUED_1: 18;

        end;

        ( |.x.| . 0 ) = |.(x . 0 ).| by VALUED_1: 18

        .= 1 by COMPLEX1: 48, COMSEQ_3:def 1;

        then |.a.| = (1 / 2) & |.x.| = ( |.a.| GeoSeq ) by A1, ABSVALUE:def 1, PREPOWER: 3;

        then |.x.| is summable by SERIES_1: 24;

        then x is absolutely_summable by COMSEQ_3:def 9;

        then ( seq_id x) is absolutely_summable by CSSPACE: 1;

        then

        reconsider v = x as VECTOR of Complex_l1_Space by CSSPACE3: 6;

        (( seq_id v) . 0 ) = (x . 0 ) by CSSPACE: 1

        .= 1 by COMPLEX1:def 4, COMSEQ_3:def 1;

        then v <> CZeroseq by CSSPACE: 4;

        hence thesis by CSSPACE3: 6;

      end;

    end

    registration

      cluster non trivial for ComplexBanachSpace;

      existence

      proof

        take Complex_l1_Space ;

        thus thesis;

      end;

    end

    theorem :: CLOPBAN2:17

    

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

    proof

      let X be non trivial ComplexNormSpace;

      consider v be VECTOR of X such that

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

      reconsider a = ( ||.v.|| + ( 0 * <i> )) as Element of COMPLEX by XCMPLX_0:def 2;

      take w = ((a " ) * v);

      

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

      then

       A3: 0 < ||.v.|| by CLVECT_1: 105;

      

       A4: |.(a " ).| = |.( 1r * (a " )).| by COMPLEX1:def 4

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

      .= (1 / |.a.|) by COMPLEX1: 48, COMPLEX1: 67

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

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

      

      thus ||.w.|| = ( |.(a " ).| * ||.v.||) by CLVECT_1:def 13

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

    end;

    theorem :: CLOPBAN2:18

    

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

    proof

      let X be non trivial ComplexNormSpace;

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

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

    end;

    definition

      struct ( ComplexAlgebraStr, CNORMSTR) Normed_Complex_AlgebraStr (# the carrier -> set,

the multF, addF -> BinOp of the carrier,

the Mult -> Function of [: COMPLEX , 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_Complex_AlgebraStr;

      existence

      proof

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

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

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

      end;

    end

    definition

      let X be ComplexNormSpace;

      :: CLOPBAN2:def8

      func C_Normed_Algebra_of_BoundedLinearOperators (X) -> Normed_Complex_AlgebraStr equals Normed_Complex_AlgebraStr (# ( BoundedLinearOperators (X,X)), ( FuncMult X), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( FuncUnit X), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( BoundedLinearOperatorsNorm (X,X)) #);

      correctness ;

    end

    registration

      let X be ComplexNormSpace;

      cluster ( C_Normed_Algebra_of_BoundedLinearOperators X) -> non empty strict;

      coherence ;

    end

     Lm3:

    now

      let X be ComplexNormSpace;

      set F = ( C_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 ComplexNormSpace;

      cluster ( C_Normed_Algebra_of_BoundedLinearOperators X) -> unital;

      coherence

      proof

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

        take e;

        thus thesis by Lm3;

      end;

    end

    theorem :: CLOPBAN2:19

    

     Th19: for X be ComplexNormSpace holds for x,y,z be Element of ( C_Normed_Algebra_of_BoundedLinearOperators X) holds for a,b be Complex holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. ( C_Normed_Algebra_of_BoundedLinearOperators X))) = x & x is right_complementable & ((x * y) * z) = (x * (y * z)) & (x * ( 1. ( C_Normed_Algebra_of_BoundedLinearOperators X))) = x & (( 1. ( C_Normed_Algebra_of_BoundedLinearOperators X)) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x)) & (a * (x * y)) = ((a * x) * y) & ((a * b) * (x * y)) = ((a * x) * (b * y)) & (a * (x + y)) = ((a * x) + (a * y)) & ((a + b) * x) = ((a * x) + (b * x)) & ((a * b) * x) = (a * (b * x)) & ( 1r * x) = x

    proof

      let X be ComplexNormSpace;

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

      let a,b be Complex;

      set RBLOP = ( C_Normed_Algebra_of_BoundedLinearOperators X);

      set BLOP = ( BoundedLinearOperators (X,X));

      set ADD = ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X))));

      set MULT = ( FuncMult X);

      set UNIT = ( FuncUnit X);

      set RRL = CLSStruct (# ( BoundedLinearOperators (X,X)), ( Zero_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Add_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))), ( Mult_ (( BoundedLinearOperators (X,X)),( C_VectorSpace_of_LinearOperators (X,X)))) #);

      reconsider f = x, g = y, h = z as Element of 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 by RLVECT_1:def 4;

      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 * b) * (x * y)) = ((a * b) * (xx * yy)) by Def4

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

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

      

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

      .= ((a * f) + (a * g)) by CLVECT_1:def 2

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

      

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

      .= ((a * f) + (b * f)) by CLVECT_1:def 3

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

      

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

      .= (a * (b * f)) by CLVECT_1:def 4

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

      

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

      .= x by CLVECT_1:def 5;

    end;

    theorem :: CLOPBAN2:20

    

     Th20: for X be ComplexNormSpace holds ( C_Normed_Algebra_of_BoundedLinearOperators X) is reflexive discerning ComplexNormSpace-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 ComplexNormSpace;

      set C = ( C_Normed_Algebra_of_BoundedLinearOperators X);

      set BS = ( C_NormSpace_of_BoundedLinearOperators (X,X));

      thus C is reflexive

      proof

        

        thus ||.( 0. C).|| = ||.( 0. BS).||

        .= 0 ;

      end;

      thus C is discerning

      proof

        let x be Point of C;

        reconsider y = x as Point of BS;

        assume ||.x.|| = 0 ;

        then ||.y.|| = 0 ;

        then y = ( 0. BS) by NORMSP_0:def 5;

        hence x = ( 0. C);

      end;

      thus C is ComplexNormSpace-like

      proof

        let x,y be Point of C;

        let a be Complex;

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

        

         A1: ||.x1.|| = ||.x.||;

        

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

        .= ( |.a.| * ||.x.||) by A1, CLVECT_1:def 13;

         ||.(x + y).|| = ||.(x1 + y1).|| & ( ||.x1.|| + ||.y1.||) = ( ||.x.|| + ||.y.||);

        hence thesis by CLVECT_1:def 13;

      end;

      set RBLOP = C;

      (for x,y,z be Element of C holds for a,b be Complex holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. C)) = x & x is right_complementable & ((x * y) * z) = (x * (y * z)) & (x * ( 1. C)) = x & (( 1. C) * x) = x & (x * (y + z)) = ((x * y) + (x * z)) & ((y + z) * x) = ((y * x) + (z * x)) & (a * (x * y)) = ((a * x) * y) & ((a * b) * (x * y)) = ((a * x) * (b * y)) & (a * (x + y)) = ((a * x) + (a * y)) & ((a + b) * x) = ((a * x) + (b * x)) & ((a * b) * x) = (a * (b * x)) & ( 1r * x) = x) & for a be Complex, v,w be VECTOR of RBLOP holds (a * (v + w)) = ((a * v) + (a * w)) by Th19;

      hence thesis;

    end;

    registration

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

      existence

      proof

        set X = the ComplexNormSpace;

        take ( C_Normed_Algebra_of_BoundedLinearOperators X);

        thus thesis by Th20;

      end;

    end

    definition

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

    end

    registration

      let X be ComplexNormSpace;

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

      correctness by Th20;

    end

    definition

      let X be non empty Normed_Complex_AlgebraStr;

      :: CLOPBAN2:def9

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

      :: CLOPBAN2:def10

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

      :: CLOPBAN2:def11

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

    end

    definition

      let X be Normed_Complex_Algebra;

      :: CLOPBAN2: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_Complex_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_Complex_Algebra;

      coherence ;

    end

    registration

      let X be non trivial ComplexBanachSpace;

      cluster ( C_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)),( C_VectorSpace_of_LinearOperators (X,X))));

        set BS = ( C_NormSpace_of_BoundedLinearOperators (X,X));

        set BLOP = ( BoundedLinearOperators (X,X));

        set RBLOP = ( C_Normed_Algebra_of_BoundedLinearOperators X);

        thus 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 CLOPBAN1:def 9

          .= ( ||.x.|| * ||.y.||) by CLOPBAN1:def 9;

           ||.(x * y).|| = (NRM . (x1 * y1)) by Def4

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

          hence thesis by A1, Th2;

        end;

         ||.( 1. RBLOP).|| = 1 by Th18;

        hence RBLOP is Banach_Algebra-like_2;

        thus RBLOP is Banach_Algebra-like_3

        proof

          let a be Complex;

          let x,y be Element of RBLOP;

          

          thus (a * (x * y)) = (( 1r * a) * (x * y)) by COMPLEX1:def 4

          .= (( 1r * 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;

          

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

          .= x by Th8;

        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, CSSPACE3: 8;

            now

              let n,m be Nat such that

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

               ||.((seq1 . n) - (seq1 . m)).|| = (NRM . (ADD . ((seq1 . n),(( - 1r ) * (seq1 . m))))) by CLVECT_1: 3

              .= (NRM . ((seq . n) + (( - 1r ) * (seq . m))))

              .= ||.((seq . n) - (seq . m)).|| by CLVECT_1: 3;

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

          then seq1 is convergent by CLOPBAN1:def 13;

          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;

          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 . (ADD . ((seq1 . n),(( - 1r ) * g1)))) by CLVECT_1: 3

              .= (NRM . ((seq . n) + (( - 1r ) * g)))

              .= ||.((seq . n) - g).|| by CLVECT_1: 3;

              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;

        end;

        hence thesis;

      end;

    end

    registration

      cluster Banach_Algebra-like for Normed_Complex_Algebra;

      existence

      proof

        take ( C_Normed_Algebra_of_BoundedLinearOperators the non trivial ComplexBanachSpace);

        thus thesis;

      end;

    end

    definition

      mode Complex_Banach_Algebra is Banach_Algebra-like Normed_Complex_Algebra;

    end

    theorem :: CLOPBAN2:21

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

    theorem :: CLOPBAN2:22

    for X be ComplexNormSpace holds ( 1. ( C_Algebra_of_BoundedLinearOperators X)) = ( FuncUnit X);

    theorem :: CLOPBAN2:23

    for X be ComplexNormSpace holds ( 1. ( C_Normed_Algebra_of_BoundedLinearOperators X)) = ( FuncUnit X);