let X be RealNormSpace; :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is Algebra-like & R_Normed_Algebra_of_BoundedLinearOperators X is RealLinearSpace-like )
A1:
for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_Normed_Algebra_of_BoundedLinearOperators X)) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & (a * b) * (x * y) = (a * x) * (b * y) & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1 * x = x )
by Th19;
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;
A2:
R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable
A3:
( ( for a being real number
for v, w being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) & ( for a, b being real number
for v being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds (a + b) * v = (a * v) + (b * v) ) & ( for a, b being real number
for v being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds (a * b) * v = a * (b * v) ) & ( for v being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds 1 * v = v ) )
by Th19;
now let x,
y be
Point of
(R_Normed_Algebra_of_BoundedLinearOperators X);
:: thesis: for a being Real holds
( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| )let a be
Real;
:: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| )reconsider x1 =
x,
y1 =
y as
Point of
(R_NormSpace_of_BoundedLinearOperators X,X) ;
A4:
||.(x + y).|| =
(BoundedLinearOperatorsNorm X,X) . ((Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . x,y)
by NORMSP_1:def 1
.=
||.(x1 + y1).||
by NORMSP_1:def 1
;
||.x1.|| + ||.y1.|| =
((BoundedLinearOperatorsNorm X,X) . x1) + ||.y1.||
by NORMSP_1:def 1
.=
((BoundedLinearOperatorsNorm X,X) . x1) + ((BoundedLinearOperatorsNorm X,X) . y1)
by NORMSP_1:def 1
.=
||.x.|| + (the norm of (R_Normed_Algebra_of_BoundedLinearOperators X) . y)
by NORMSP_1:def 1
.=
||.x.|| + ||.y.||
by NORMSP_1:def 1
;
hence
||.(x + y).|| <= ||.x.|| + ||.y.||
by A4, NORMSP_1:def 2;
:: thesis: ( ( ||.x.|| = 0 implies x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) ) & ( x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| )A5:
||.x1.|| =
(BoundedLinearOperatorsNorm X,X) . x1
by NORMSP_1:def 1
.=
||.x.||
by NORMSP_1:def 1
;
0. (R_NormSpace_of_BoundedLinearOperators X,X) = 0. (R_Normed_Algebra_of_BoundedLinearOperators X)
;
hence
(
||.x.|| = 0 iff
x = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) )
by A5, NORMSP_1:def 2;
:: thesis: ||.(a * x).|| = (abs a) * ||.x.||thus ||.(a * x).|| =
(BoundedLinearOperatorsNorm X,X) . ((Mult_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . a,x)
by NORMSP_1:def 1
.=
||.(a * x1).||
by NORMSP_1:def 1
.=
(abs a) * ||.x.||
by A5, NORMSP_1:def 2
;
:: thesis: verum end;
hence
( R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is Algebra-like & R_Normed_Algebra_of_BoundedLinearOperators X is RealLinearSpace-like )
by A1, A2, A3, FUNCSDOM:def 20, GROUP_1:def 4, NORMSP_1:def 2, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 9, VECTSP_1:def 11, VECTSP_1:def 13; :: thesis: verum