set NRM = BoundedLinearOperatorsNorm (X,X);

set UNIT = FuncUnit X;

set MULT = FuncMult X;

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

set BS = R_NormSpace_of_BoundedLinearOperators (X,X);

set BLOP = BoundedLinearOperators (X,X);

set RBLOP = R_Normed_Algebra_of_BoundedLinearOperators X;

thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_1 :: according to LOPBAN_2:def 12 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )

.= 1 by Th18 ;

hence R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 ; :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )

thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )

set UNIT = FuncUnit X;

set MULT = FuncMult X;

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

set BS = R_NormSpace_of_BoundedLinearOperators (X,X);

set BLOP = BoundedLinearOperators (X,X);

set RBLOP = R_Normed_Algebra_of_BoundedLinearOperators X;

thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_1 :: according to LOPBAN_2:def 12 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )

proof

||.(1. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| =
(BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X)
let x, y be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to LOPBAN_2:def 9 :: thesis: ||.(x * y).|| <= ||.x.|| * ||.y.||

reconsider x1 = x, y1 = y as Element of BoundedLinearOperators (X,X) ;

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

.= ((BoundedLinearOperatorsNorm (X,X)) . x1) * ((BoundedLinearOperatorsNorm (X,X)) . y1) by LOPBAN_1:def 11

.= ||.x.|| * ((BoundedLinearOperatorsNorm (X,X)) . y)

.= ||.x.|| * ||.y.|| ;

||.(x * y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((FuncMult X) . (x,y))

.= (BoundedLinearOperatorsNorm (X,X)) . (x1 * y1) by Def4

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

hence ||.(x * y).|| <= ||.x.|| * ||.y.|| by A1, Th2; :: thesis: verum

end;reconsider x1 = x, y1 = y as Element of BoundedLinearOperators (X,X) ;

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

.= ((BoundedLinearOperatorsNorm (X,X)) . x1) * ((BoundedLinearOperatorsNorm (X,X)) . y1) by LOPBAN_1:def 11

.= ||.x.|| * ((BoundedLinearOperatorsNorm (X,X)) . y)

.= ||.x.|| * ||.y.|| ;

||.(x * y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((FuncMult X) . (x,y))

.= (BoundedLinearOperatorsNorm (X,X)) . (x1 * y1) by Def4

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

hence ||.(x * y).|| <= ||.x.|| * ||.y.|| by A1, Th2; :: thesis: verum

.= 1 by Th18 ;

hence R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 ; :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )

thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )

proof

thus
R_Normed_Algebra_of_BoundedLinearOperators X is left_unital
:: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )
let a be Real; :: according to LOPBAN_2:def 11 :: thesis: for x, y being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (x * y) = x * (a * y)

let x, y be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: a * (x * y) = x * (a * y)

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

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

.= x * (a * y) by Th19 ; :: thesis: verum

end;let x, y be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: a * (x * y) = x * (a * y)

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

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

.= x * (a * y) by Th19 ; :: thesis: verum

proof

thus
R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive
:: thesis: R_Normed_Algebra_of_BoundedLinearOperators X is complete
let x be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def 8 :: thesis: (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x

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

(FuncUnit X) * xx = xx by Th8;

hence (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x by Def4; :: thesis: verum

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

(FuncUnit X) * xx = xx by Th8;

hence (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x by Def4; :: thesis: verum

proof

let x, y, z be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def 3 :: thesis: (y + z) * x = (y * x) + (z * x)

reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;

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

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

.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4

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

end;reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;

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

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

.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((yy * xx),((FuncMult X) . (zz,xx))) by Def4

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

now :: thesis: for seq being sequence of (R_Normed_Algebra_of_BoundedLinearOperators X) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

hence
R_Normed_Algebra_of_BoundedLinearOperators X is complete
; :: thesis: verumseq is convergent

let seq be sequence of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )

assume A2: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

reconsider seq1 = seq as sequence of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;

then seq1 is convergent by LOPBAN_1:def 15;

then consider g1 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) such that

A5: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((seq1 . n) - g1).|| < r by NORMSP_1:def 6;

reconsider g = g1 as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;

end;assume A2: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

reconsider seq1 = seq as sequence of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;

now :: thesis: for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

then
seq1 is Cauchy_sequence_by_Norm
by RSSPACE3:8;ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

then consider k being Nat such that

A3: for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r by A2, RSSPACE3:8;

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r ; :: thesis: verum

end;for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

then consider k being Nat such that

A3: for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r by A2, RSSPACE3:8;

now :: thesis: for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

hence
ex k being Nat st ||.((seq1 . n) - (seq1 . m)).|| < r

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seq1 . n) - (seq1 . m)).|| < r )

assume A4: ( n >= k & m >= k ) ; :: thesis: ||.((seq1 . n) - (seq1 . m)).|| < r

||.((seq1 . n) - (seq1 . m)).|| = (BoundedLinearOperatorsNorm (X,X)) . ((seq1 . n) + (- (seq1 . m)))

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * (seq1 . m)))) by RLVECT_1:16

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * (seq . m))))

.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- (seq . m))) by RLVECT_1:16

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

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

end;assume A4: ( n >= k & m >= k ) ; :: thesis: ||.((seq1 . n) - (seq1 . m)).|| < r

||.((seq1 . n) - (seq1 . m)).|| = (BoundedLinearOperatorsNorm (X,X)) . ((seq1 . n) + (- (seq1 . m)))

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * (seq1 . m)))) by RLVECT_1:16

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * (seq . m))))

.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- (seq . m))) by RLVECT_1:16

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

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

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r ; :: thesis: verum

then seq1 is convergent by LOPBAN_1:def 15;

then consider g1 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) such that

A5: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((seq1 . n) - g1).|| < r by NORMSP_1:def 6;

reconsider g = g1 as Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ;

now :: thesis: for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - g).|| < r

hence
seq is convergent
by NORMSP_1:def 6; :: thesis: verumex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - g).|| < r

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - g).|| < r )

assume 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - g).|| < r

then consider m being Nat such that

A6: for n being Nat st m <= n holds

||.((seq1 . n) - g1).|| < r by A5;

for n being Nat st m <= n holds

||.((seq . n) - g).|| < r ; :: thesis: verum

end;for n being Nat st m <= n holds

||.((seq . n) - g).|| < r )

assume 0 < r ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - g).|| < r

then consider m being Nat such that

A6: for n being Nat st m <= n holds

||.((seq1 . n) - g1).|| < r by A5;

now :: thesis: for n being Nat st m <= n holds

||.((seq . n) - g).|| < r

hence
ex m being Nat st ||.((seq . n) - g).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - g).|| < r )

assume A7: m <= n ; :: thesis: ||.((seq . n) - g).|| < r

||.((seq1 . n) - g1).|| = (BoundedLinearOperatorsNorm (X,X)) . ((seq1 . n) + (- g1))

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * g1))) by RLVECT_1:16

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * g)))

.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- g)) by RLVECT_1:16

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

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

end;assume A7: m <= n ; :: thesis: ||.((seq . n) - g).|| < r

||.((seq1 . n) - g1).|| = (BoundedLinearOperatorsNorm (X,X)) . ((seq1 . n) + (- g1))

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq1 . n),((- 1) * g1))) by RLVECT_1:16

.= (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((seq . n),((- 1) * g)))

.= (BoundedLinearOperatorsNorm (X,X)) . ((seq . n) + (- g)) by RLVECT_1:16

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

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

for n being Nat st m <= n holds

||.((seq . n) - g).|| < r ; :: thesis: verum