set A = R_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
thus R_Algebra_of_BoundedLinearOperators X is Abelian :: thesis: ( R_Algebra_of_BoundedLinearOperators X is add-associative & R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider f = x, g = y as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:2 ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is add-associative :: thesis: ( R_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider f = x, g = y, h = z as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def 3
.= x + (y + z) ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is right_zeroed :: thesis: ( R_Algebra_of_BoundedLinearOperators X is right_complementable & R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to RLVECT_1:def 4 :: thesis: x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus x + (0. (R_Algebra_of_BoundedLinearOperators X)) = f + (0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #))
.= x ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is right_complementable :: thesis: ( R_Algebra_of_BoundedLinearOperators X is associative & R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
consider s being Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) such that
A1: f + s = 0. RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) by ALGSTR_0:def 11;
reconsider t = s as Element of (R_Algebra_of_BoundedLinearOperators X) ;
take t ; :: according to ALGSTR_0:def 11 :: thesis: x + t = 0. (R_Algebra_of_BoundedLinearOperators X)
thus x + t = 0. (R_Algebra_of_BoundedLinearOperators X) by A1; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is associative :: thesis: ( R_Algebra_of_BoundedLinearOperators X is right_unital & R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to GROUP_1:def 3 :: thesis: (x * y) * z = x * (y * z)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus (x * y) * z = (FuncMult X) . ((xx * yy),zz) by Def4
.= (xx * yy) * zz by Def4
.= xx * (yy * zz) by Th7
.= (FuncMult X) . (xx,(yy * zz)) by Def4
.= x * (y * z) by Def4 ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is right_unital :: thesis: ( R_Algebra_of_BoundedLinearOperators X is right-distributive & R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def 4 :: thesis: x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x
reconsider xx = x as Element of BoundedLinearOperators (X,X) ;
thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is right-distributive :: thesis: ( R_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to VECTSP_1:def 2 :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider xx = x, yy = y, zz = z as Element of BoundedLinearOperators (X,X) ;
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . ((xx * yy),((FuncMult X) . (xx,zz))) by Def4
.= (x * y) + (x * z) by Def4 ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is vector-distributive :: thesis: ( R_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let a be Real; :: according to RLVECT_1:def 5 :: thesis: for b1, b2 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds a * (b1 + b2) = (a * b1) + (a * b2)
let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); :: thesis: a * (x + y) = (a * x) + (a * y)
reconsider f = x, g = y as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by RLVECT_1:def 5
.= (a * x) + (a * y) ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is scalar-distributive :: thesis: ( R_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let a, b be Real; :: according to RLVECT_1:def 6 :: thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds (a + b) * b1 = (a * b1) + (b * b1)
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: thesis: (a + b) * x = (a * x) + (b * x)
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by RLVECT_1:def 6
.= (a * x) + (b * x) ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is scalar-associative :: thesis: ( R_Algebra_of_BoundedLinearOperators X is vector-associative & R_Algebra_of_BoundedLinearOperators X is strict )
proof
let a, b be Real; :: according to RLVECT_1:def 7 :: thesis: for b1 being Element of the carrier of (R_Algebra_of_BoundedLinearOperators X) holds (a * b) * b1 = a * (b * b1)
let x be Element of (R_Algebra_of_BoundedLinearOperators X); :: thesis: (a * b) * x = a * (b * x)
reconsider f = x as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
thus (a * b) * x = (a * b) * f
.= a * (b * f) by RLVECT_1:def 7
.= a * (b * x) ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is vector-associative :: thesis: R_Algebra_of_BoundedLinearOperators X is strict
proof
let x, y be Element of (R_Algebra_of_BoundedLinearOperators X); :: according to FUNCSDOM:def 9 :: thesis: for b1 being object holds b1 * (x * y) = (b1 * x) * y
let a be Real; :: thesis: a * (x * y) = (a * x) * y
reconsider xx = x, yy = y as Element of BoundedLinearOperators (X,X) ;
thus a * (x * y) = a * (xx * yy) by Def4
.= (a * xx) * yy by Th12
.= (a * x) * y by Def4 ; :: thesis: verum
end;
thus R_Algebra_of_BoundedLinearOperators X is strict ; :: thesis: verum