let X be RealNormSpace; :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & 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 vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )

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. (R_NormSpace_of_BoundedLinearOperators (X,X))).|| = (BoundedLinearOperatorsNorm (X,X)) . (0. (R_NormSpace_of_BoundedLinearOperators (X,X)))

.= ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| ;

thus ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| = 0 by A1; :: according to NORMSP_0:def 6 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & 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 vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )

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 ) ) & ( for a being Real

for v, w being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) ) by Th19;

hence ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & 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 vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) by A5, A2, NORMSP_1:def 1; :: thesis: verum

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. (R_NormSpace_of_BoundedLinearOperators (X,X))).|| = (BoundedLinearOperatorsNorm (X,X)) . (0. (R_NormSpace_of_BoundedLinearOperators (X,X)))

.= ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| ;

thus ||.(0. (R_Normed_Algebra_of_BoundedLinearOperators X)).|| = 0 by A1; :: according to NORMSP_0:def 6 :: thesis: ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & 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 vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )

A2: now :: thesis: for x, y being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)

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).|| = |.a.| * ||.x.|| )

A5:
R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable
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).|| = |.a.| * ||.x.|| )

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).|| = |.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).|| = |.a.| * ||.x.|| )

reconsider x1 = x, y1 = y as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;

A3: ||.x1.|| + ||.y1.|| = ((BoundedLinearOperatorsNorm (X,X)) . x1) + ||.y1.||

.= ((BoundedLinearOperatorsNorm (X,X)) . x1) + ((BoundedLinearOperatorsNorm (X,X)) . y1)

.= ||.x.|| + ( the normF of (R_Normed_Algebra_of_BoundedLinearOperators X) . y)

.= ||.x.|| + ||.y.|| ;

||.(x + y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (x,y))

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

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A3, NORMSP_1:def 1; :: 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).|| = |.a.| * ||.x.|| )

A4: ||.x1.|| = (BoundedLinearOperatorsNorm (X,X)) . x1

.= ||.x.|| ;

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 A4, NORMSP_0:def 5; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||

thus ||.(a * x).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,x))

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

.= |.a.| * ||.x.|| by A4, NORMSP_1:def 1 ; :: thesis: verum

end;( ||.(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).|| = |.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).|| = |.a.| * ||.x.|| )

reconsider x1 = x, y1 = y as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;

A3: ||.x1.|| + ||.y1.|| = ((BoundedLinearOperatorsNorm (X,X)) . x1) + ||.y1.||

.= ((BoundedLinearOperatorsNorm (X,X)) . x1) + ((BoundedLinearOperatorsNorm (X,X)) . y1)

.= ||.x.|| + ( the normF of (R_Normed_Algebra_of_BoundedLinearOperators X) . y)

.= ||.x.|| + ||.y.|| ;

||.(x + y).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (x,y))

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

hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A3, NORMSP_1:def 1; :: 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).|| = |.a.| * ||.x.|| )

A4: ||.x1.|| = (BoundedLinearOperatorsNorm (X,X)) . x1

.= ||.x.|| ;

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 A4, NORMSP_0:def 5; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||

thus ||.(a * x).|| = (BoundedLinearOperatorsNorm (X,X)) . ((Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,x))

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

.= |.a.| * ||.x.|| by A4, NORMSP_1:def 1 ; :: thesis: verum

proof

( ( for x, y, z being Element of (R_Normed_Algebra_of_BoundedLinearOperators X)
let x be Element of (R_Normed_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable

thus ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) by Th19; :: according to ALGSTR_0:def 11 :: thesis: verum

end;thus ex t being Element of (R_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Normed_Algebra_of_BoundedLinearOperators X) by Th19; :: according to ALGSTR_0:def 11 :: thesis: verum

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 ) ) & ( for a being Real

for v, w being VECTOR of (R_Normed_Algebra_of_BoundedLinearOperators X) holds a * (v + w) = (a * v) + (a * w) ) ) by Th19;

hence ( R_Normed_Algebra_of_BoundedLinearOperators X is discerning & 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 vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital ) by A5, A2, NORMSP_1:def 1; :: thesis: verum