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
LOPBAN_2:def 12 ( R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedLinearOperators X is left_unital & R_Normed_Algebra_of_BoundedLinearOperators X is left-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is complete )proof
let x,
y be
Point of
(R_Normed_Algebra_of_BoundedLinearOperators X);
LOPBAN_2:def 9 ||.(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;
verum
end;
||.(1. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| =
(BoundedLinearOperatorsNorm (X,X)) . (id the carrier of X)
.=
1
by Th18
;
hence
R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like_2
; ( 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
( 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 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 left-distributive
R_Normed_Algebra_of_BoundedLinearOperators X is complete proof
let x,
y,
z be
Element of
(R_Normed_Algebra_of_BoundedLinearOperators X);
VECTSP_1:def 3 (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
;
verum
end;
now for seq being sequence of (R_Normed_Algebra_of_BoundedLinearOperators X) st seq is Cauchy_sequence_by_Norm holds
seq is convergent let seq be
sequence of
(R_Normed_Algebra_of_BoundedLinearOperators X);
( seq is Cauchy_sequence_by_Norm implies seq is convergent )assume A2:
seq is
Cauchy_sequence_by_Norm
;
seq is convergent reconsider seq1 =
seq as
sequence of
(R_NormSpace_of_BoundedLinearOperators (X,X)) ;
now 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)).|| < rlet r be
Real;
( 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
;
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < rthen 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 for n, m being Nat st n >= k & m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < rlet n,
m be
Nat;
( n >= k & m >= k implies ||.((seq1 . n) - (seq1 . m)).|| < r )assume A4:
(
n >= k &
m >= k )
;
||.((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;
verum end; hence
ex
k being
Nat st
for
n,
m being
Nat st
n >= k &
m >= k holds
||.((seq1 . n) - (seq1 . m)).|| < r
;
verum end; then
seq1 is
Cauchy_sequence_by_Norm
by RSSPACE3:8;
then
seq1 is
convergent
by LOPBAN_1:def 15;
then consider g1 being
Point of
(R_NormSpace_of_BoundedLinearOperators (X,X)) such that A5:
for
r being
Real st
0 < r holds
ex
m being
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 for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - g).|| < rlet r be
Real;
( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - g).|| < r )assume
0 < r
;
ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - g).|| < rthen consider m being
Nat such that A6:
for
n being
Nat st
m <= n holds
||.((seq1 . n) - g1).|| < r
by A5;
now for n being Nat st m <= n holds
||.((seq . n) - g).|| < rlet n be
Nat;
( m <= n implies ||.((seq . n) - g).|| < r )assume A7:
m <= n
;
||.((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;
verum end; hence
ex
m being
Nat st
for
n being
Nat st
m <= n holds
||.((seq . n) - g).|| < r
;
verum end; hence
seq is
convergent
by NORMSP_1:def 6;
verum end;
hence
R_Normed_Algebra_of_BoundedLinearOperators X is complete
; verum