let X be non empty set ; :: thesis: for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL ,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let d1, d2 be Element of X; :: thesis: for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL ,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let A be BinOp of X; :: thesis: for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL ,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let M be Function of [:X,X:],X; :: thesis: for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL ,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let V be Algebra; :: thesis: for V1 being Subset of V
for MR being Function of [:REAL ,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let V1 be Subset of V; :: thesis: for MR being Function of [:REAL ,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let MR be Function of [:REAL ,X:],X; :: thesis: ( V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL ,V1:] & V1 is having-inverse implies AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V )
assume that
A1: V1 = X and
A2: d1 = 0. V and
A3: d2 = 1. V and
A4: A = the addF of V || V1 and
A5: M = the multF of V || V1 and
A6: MR = the Mult of V | [:REAL ,V1:] and
A7: for v being Element of V st v in V1 holds
- v in V1 ; :: according to C0SP1:def 1 :: thesis: AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
reconsider W = AlgebraStr(# X,M,A,MR,d2,d1 #) as non empty AlgebraStr ;
A8: now
let x, y be Element of W; :: thesis: x + y = the addF of V . x,y
x + y = the addF of V . [x,y] by A1, A4, FUNCT_1:72;
hence x + y = the addF of V . x,y ; :: thesis: verum
end;
A9: now
let a, x be VECTOR of W; :: thesis: a * x = the multF of V . a,x
a * x = the multF of V . [a,x] by A1, A5, FUNCT_1:72;
hence a * x = the multF of V . a,x ; :: thesis: verum
end;
A10: now
let a be Real; :: thesis: for x being VECTOR of W holds a * x = the Mult of V . a,x
let x be VECTOR of W; :: thesis: a * x = the Mult of V . a,x
a * x = the Mult of V . [a,x] by A1, A6, FUNCT_1:72;
hence a * x = the Mult of V . a,x ; :: thesis: verum
end;
A11: ( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is Algebra-like )
proof
set Mv = the multF of V;
set MV = the Mult of V;
set Av = the addF of V;
hereby :: according to RLVECT_1:def 5 :: thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is Algebra-like )
let x, y be VECTOR of W; :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
( x + y = x1 + y1 & y + x = y1 + x1 ) by A8;
hence x + y = y + x ; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 6 :: thesis: ( W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is Algebra-like )
let x, y, z be VECTOR of W; :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;
x + (y + z) = the addF of V . x1,(y + z) by A8;
then A12: x + (y + z) = x1 + (y1 + z1) by A8;
(x + y) + z = the addF of V . (x + y),z1 by A8;
then (x + y) + z = (x1 + y1) + z1 by A8;
hence (x + y) + z = x + (y + z) by A12, RLVECT_1:def 6; :: thesis: verum
end;
hereby :: according to RLVECT_1:def 7 :: thesis: ( W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is Algebra-like )
let x be VECTOR of W; :: thesis: x + (0. W) = x
reconsider y = x, z = 0. W as VECTOR of V by A1, TARSKI:def 3;
thus x + (0. W) = y + (0. V) by A2, A8
.= x by RLVECT_1:10 ; :: thesis: verum
end;
thus W is right_complementable :: thesis: ( W is commutative & W is associative & W is right_unital & W is right-distributive & W is Algebra-like )
proof
let x be Element of W; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 = x as Element of V by A1, TARSKI:def 3;
consider v being Element of V such that
A13: x1 + v = 0. V by ALGSTR_0:def 11;
v = - x1 by A13, VECTSP_1:63;
then reconsider y = v as Element of W by A1, A7;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. W
thus x + y = 0. W by A2, A8, A13; :: thesis: verum
end;
hereby :: according to GROUP_1:def 16 :: thesis: ( W is associative & W is right_unital & W is right-distributive & W is Algebra-like )
let v, w be Element of W; :: thesis: v * w = w * v
reconsider v1 = v, w1 = w as Element of V by A1, TARSKI:def 3;
( v * w = v1 * w1 & w * v = w1 * v1 ) by A9;
hence v * w = w * v ; :: thesis: verum
end;
hereby :: according to GROUP_1:def 4 :: thesis: ( W is right_unital & W is right-distributive & W is Algebra-like )
let a, b, x be Element of W; :: thesis: (a * b) * x = a * (b * x)
reconsider y = x, a1 = a, b1 = b as Element of V by A1, TARSKI:def 3;
a * (b * x) = the multF of V . a,(b * x) by A9;
then A14: a * (b * x) = a1 * (b1 * y) by A9;
a * b = a1 * b1 by A9;
then (a * b) * x = (a1 * b1) * y by A9;
hence (a * b) * x = a * (b * x) by A14, GROUP_1:def 4; :: thesis: verum
end;
hereby :: according to VECTSP_1:def 13 :: thesis: ( W is right-distributive & W is Algebra-like )
let v be Element of W; :: thesis: v * (1. W) = v
reconsider v1 = v as Element of V by A1, TARSKI:def 3;
v * (1. W) = v1 * (1. V) by A3, A9;
hence v * (1. W) = v by VECTSP_1:def 13; :: thesis: verum
end;
hereby :: according to VECTSP_1:def 11 :: thesis: W is Algebra-like
let x, y, z be Element of W; :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider x1 = x, y1 = y, z1 = z as Element of V by A1, TARSKI:def 3;
y + z = y1 + z1 by A8;
then x * (y + z) = x1 * (y1 + z1) by A9;
then A15: x * (y + z) = (x1 * y1) + (x1 * z1) by VECTSP_1:def 11;
( x * y = x1 * y1 & x * z = x1 * z1 ) by A9;
hence x * (y + z) = (x * y) + (x * z) by A8, A15; :: thesis: verum
end;
thus W is Algebra-like :: thesis: verum
proof
let x, y, z be Element of W; :: according to FUNCSDOM:def 20 :: thesis: for b1, b2 being Element of REAL holds
( b1 * (x * y) = (b1 * x) * y & b1 * (x + y) = (b1 * x) + (b1 * y) & (b1 + b2) * x = (b1 * x) + (b2 * x) & (b1 * b2) * x = b1 * (b2 * x) )
reconsider x1 = x, y1 = y as Element of V by A1, TARSKI:def 3;
let a, b be Real; :: thesis: ( 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) )
A16: a * x = a * x1 by A10;
x * y = x1 * y1 by A9;
then a * (x * y) = a * (x1 * y1) by A10;
then a * (x * y) = (a * x1) * y1 by FUNCSDOM:def 20;
hence a * (x * y) = (a * x) * y by A9, A16; :: thesis: ( a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
x + y = x1 + y1 by A8;
then a * (x + y) = a * (x1 + y1) by A10;
then A17: a * (x + y) = (a * x1) + (a * y1) by FUNCSDOM:def 20;
a * y = a * y1 by A10;
hence a * (x + y) = (a * x) + (a * y) by A8, A16, A17; :: thesis: ( (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) )
A18: b * x = b * x1 by A10;
(a + b) * x = (a + b) * x1 by A10;
then (a + b) * x = (a * x1) + (b * x1) by FUNCSDOM:def 20;
hence (a + b) * x = (a * x) + (b * x) by A8, A16, A18; :: thesis: (a * b) * x = a * (b * x)
(a * b) * x = (a * b) * x1 by A10;
then (a * b) * x = a * (b * x1) by FUNCSDOM:def 20;
hence (a * b) * x = a * (b * x) by A10, A18; :: thesis: verum
end;
end;
( 0. W = 0. V & 1. W = 1. V ) by A2, A3;
hence AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V by A1, A4, A5, A6, A11, Def9; :: thesis: verum