let X be RealNormSpace; for x, y, z being Element of (R_Algebra_of_BoundedLinearOperators X)
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
let x, y, z be Element of (R_Algebra_of_BoundedLinearOperators X); for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
let a, b be Real; ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
set RBLOP = R_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators (X,X);
set ADD = Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)));
set MULT = FuncMult X;
set UNIT = FuncUnit 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)))) #);
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 =
f + g
.=
y + x
by RLVECT_1:2
; ( (x + y) + z = x + (y + z) & x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (x + y) + z =
(f + g) + h
.=
f + (g + h)
by RLVECT_1:def 3
.=
x + (y + z)
; ( x + (0. (R_Algebra_of_BoundedLinearOperators X)) = x & ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
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
; ( ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X) & (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus
ex t being Element of (R_Algebra_of_BoundedLinearOperators X) st x + t = 0. (R_Algebra_of_BoundedLinearOperators X)
( (x * y) * z = x * (y * z) & x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )proof
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
;
x + t = 0. (R_Algebra_of_BoundedLinearOperators X)
thus
x + t = 0. (R_Algebra_of_BoundedLinearOperators X)
by A1;
verum
end;
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
; ( x * (1. (R_Algebra_of_BoundedLinearOperators X)) = x & (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus x * (1. (R_Algebra_of_BoundedLinearOperators X)) =
xx * (FuncUnit X)
by Def4
.=
x
by Th8
; ( (1. (R_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 * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (1. (R_Algebra_of_BoundedLinearOperators X)) * x =
(FuncUnit X) * xx
by Def4
.=
x
by Th8
; ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
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
; ( (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
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
; ( a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus a * (x * y) =
a * (xx * yy)
by Def4
.=
(a * xx) * yy
by Th12
.=
(a * x) * y
by Def4
; ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus a * (x + y) =
a * (f + g)
.=
(a * f) + (a * g)
by RLVECT_1:def 5
.=
(a * x) + (a * y)
; ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (a + b) * x =
(a + b) * f
.=
(a * f) + (b * f)
by RLVECT_1:def 6
.=
(a * x) + (b * x)
; ( (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) )
thus (a * b) * x =
(a * b) * f
.=
a * (b * f)
by RLVECT_1:def 7
.=
a * (b * x)
; (a * b) * (x * y) = (a * x) * (b * y)
thus (a * b) * (x * y) =
(a * b) * (xx * yy)
by Def4
.=
(a * xx) * (b * yy)
by Th11
.=
(a * x) * (b * y)
by Def4
; verum