let X be ComplexNormSpace; :: thesis: for x, y, z being Element of (C_Normed_Algebra_of_BoundedLinearOperators X)
for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )
let x, y, z be Element of (C_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: for a, b being Complex holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )
let a, b be Complex; :: thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )
set RBLOP = C_Normed_Algebra_of_BoundedLinearOperators X;
set BLOP = BoundedLinearOperators X,X;
set ADD = Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X);
set MULT = FuncMult X;
set UNIT = FuncUnit X;
set RRL = CLSStruct(# (BoundedLinearOperators X,X),(Zero_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) #);
reconsider f = x, g = y, h = z as Element of CLSStruct(# (BoundedLinearOperators X,X),(Zero_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) #) ;
thus x + y = f + g
.= y + x by RLVECT_1:5 ; :: thesis: ( (x + y) + z = x + (y + z) & x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )
thus (x + y) + z = (f + g) + h
.= f + (g + h) by RLVECT_1:def 6
.= x + (y + z) ; :: thesis: ( x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )
thus x + (0. (C_Normed_Algebra_of_BoundedLinearOperators X)) = f + (0. CLSStruct(# (BoundedLinearOperators X,X),(Zero_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) #))
.= x by RLVECT_1:def 7 ; :: thesis: ( x is right_complementable & (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )
thus ex t being Element of (C_Normed_Algebra_of_BoundedLinearOperators X) st x + t = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) :: according to ALGSTR_0:def 11 :: thesis: ( (x * y) * z = x * (y * z) & x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )

proof

consider s being Element of CLSStruct(# (BoundedLinearOperators X,X),(Zero_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) #) such that
A1: f + s = 0. CLSStruct(# (BoundedLinearOperators X,X),(Zero_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) #) by ALGSTR_0:def 11;
reconsider t = s as Element of (C_Normed_Algebra_of_BoundedLinearOperators X) ;
take t ; :: thesis: x + t = 0. (C_Normed_Algebra_of_BoundedLinearOperators X)
thus x + t = 0. (C_Normed_Algebra_of_BoundedLinearOperators X) by A1; :: thesis: 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 ; :: thesis: ( x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = x & (1. (C_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) & 1r * x = x )
thus x * (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) = xx * (FuncUnit X) by Def4
.= x by Th8 ; :: thesis: ( (1. (C_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) & 1r * x = x )
thus (1. (C_Normed_Algebra_of_BoundedLinearOperators X)) * x = (FuncUnit X) * xx by Def4
.= x by Th8 ; :: thesis: ( 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) & 1r * x = x )
thus x * (y + z) = xx * (yy + zz) by Def4
.= (xx * yy) + (xx * zz) by Th9
.= (Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . (xx * yy),((FuncMult X) . xx,zz) by Def4
.= (x * y) + (x * z) by Def4 ; :: thesis: ( (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) & 1r * x = x )
thus (y + z) * x = (yy + zz) * xx by Def4
.= (yy * xx) + (zz * xx) by Th10
.= (Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) . (yy * xx),((FuncMult X) . zz,xx) by Def4
.= (y * x) + (z * x) by Def4 ; :: thesis: ( 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) & 1r * x = x )
thus a * (x * y) = a * (xx * yy) by Def4
.= (a * xx) * yy by Th12
.= (a * x) * y by Def4 ; :: thesis: ( (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) & 1r * x = x )
thus (a * b) * (x * y) = (a * b) * (xx * yy) by Def4
.= (a * xx) * (b * yy) by Th11
.= (a * x) * (b * y) by Def4 ; :: thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1r * x = x )
thus a * (x + y) = a * (f + g)
.= (a * f) + (a * g) by CLVECT_1:def 2
.= (a * x) + (a * y) ; :: thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & 1r * x = x )
thus (a + b) * x = (a + b) * f
.= (a * f) + (b * f) by CLVECT_1:def 2
.= (a * x) + (b * x) ; :: thesis: ( (a * b) * x = a * (b * x) & 1r * x = x )
thus (a * b) * x = (a * b) * f
.= a * (b * f) by CLVECT_1:def 2
.= a * (b * x) ; :: thesis: 1r * x = x
thus 1r * x = 1r * f
.= x by CLVECT_1:def 2 ; :: thesis: verum