let V be Z_Module; :: thesis: for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:INT,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:INT,V1:] holds
Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
let V1 be Subset of V; :: thesis: for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:INT,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:INT,V1:] holds
Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
let D be non empty set ; :: thesis: for d1 being Element of D
for A being BinOp of D
for M being Function of [:INT,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:INT,V1:] holds
Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
let d1 be Element of D; :: thesis: for A being BinOp of D
for M being Function of [:INT,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:INT,V1:] holds
Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
let A be BinOp of D; :: thesis: for M being Function of [:INT,D:],D st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:INT,V1:] holds
Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
let M be Function of [:INT,D:],D; :: thesis: ( V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:INT,V1:] implies Z_ModuleStruct(# D,d1,A,M #) is Submodule of V )
assume that
A1: V1 = D and
A2: d1 = 0. V and
A3: A = the addF of V || V1 and
A4: M = the Mult of V | [:INT,V1:] ; :: thesis: Z_ModuleStruct(# D,d1,A,M #) is Submodule of V
set W = Z_ModuleStruct(# D,d1,A,M #);
A5: for a being Integer
for x being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds a * x = the Mult of V . (a,x)
proof
let a be Integer; :: thesis: for x being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds a * x = the Mult of V . (a,x)
let x be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: thesis: a * x = the Mult of V . (a,x)
reconsider a1 = a as Element of INT by INT_1:def 2;
thus a * x = the Mult of V . [a1,x] by A1, A4, FUNCT_1:49
.= the Mult of V . (a,x) ; :: thesis: verum
end;
A6: for x, y being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds x + y = the addF of V . (x,y)
proof
let x, y be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: thesis: x + y = the addF of V . (x,y)
thus x + y = the addF of V . [x,y] by A1, A3, FUNCT_1:49
.= the addF of V . (x,y) ; :: thesis: verum
end;
A7: ( Z_ModuleStruct(# D,d1,A,M #) is Abelian & Z_ModuleStruct(# D,d1,A,M #) is add-associative & Z_ModuleStruct(# D,d1,A,M #) is right_zeroed & Z_ModuleStruct(# D,d1,A,M #) is right_complementable & Z_ModuleStruct(# D,d1,A,M #) is vector-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-associative & Z_ModuleStruct(# D,d1,A,M #) is scalar-unital )
proof
set MV = the Mult of V;
set AV = the addF of V;
thus Z_ModuleStruct(# D,d1,A,M #) is Abelian :: thesis: ( Z_ModuleStruct(# D,d1,A,M #) is add-associative & Z_ModuleStruct(# D,d1,A,M #) is right_zeroed & Z_ModuleStruct(# D,d1,A,M #) is right_complementable & Z_ModuleStruct(# D,d1,A,M #) is vector-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-associative & Z_ModuleStruct(# D,d1,A,M #) is scalar-unital )
proof
let x, y be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
thus x + y = x1 + y1 by A6
.= y1 + x1
.= y + x by A6 ; :: thesis: verum
end;
thus Z_ModuleStruct(# D,d1,A,M #) is add-associative :: thesis: ( Z_ModuleStruct(# D,d1,A,M #) is right_zeroed & Z_ModuleStruct(# D,d1,A,M #) is right_complementable & Z_ModuleStruct(# D,d1,A,M #) is vector-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-associative & Z_ModuleStruct(# D,d1,A,M #) is scalar-unital )
proof
let x, y, z be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by A1, TARSKI:def 3;
thus (x + y) + z = the addF of V . ((x + y),z1) by A6
.= (x1 + y1) + z1 by A6
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= the addF of V . (x1,(y + z)) by A6
.= x + (y + z) by A6 ; :: thesis: verum
end;
thus Z_ModuleStruct(# D,d1,A,M #) is right_zeroed :: thesis: ( Z_ModuleStruct(# D,d1,A,M #) is right_complementable & Z_ModuleStruct(# D,d1,A,M #) is vector-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-associative & Z_ModuleStruct(# D,d1,A,M #) is scalar-unital )
proof
let x be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: according to RLVECT_1:def 4 :: thesis: x + (0. Z_ModuleStruct(# D,d1,A,M #)) = x
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus x + (0. Z_ModuleStruct(# D,d1,A,M #)) = y + (0. V) by A2, A6
.= x by RLVECT_1:4 ; :: thesis: verum
end;
thus Z_ModuleStruct(# D,d1,A,M #) is right_complementable :: thesis: ( Z_ModuleStruct(# D,d1,A,M #) is vector-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-associative & Z_ModuleStruct(# D,d1,A,M #) is scalar-unital )
proof
let x be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider x1 = x as VECTOR of V by A1, TARSKI:def 3;
consider v being VECTOR of V such that
A8: x1 + v = 0. V by ALGSTR_0:def 11;
v = - x1 by A8, RLVECT_1:def 10
.= (- 1) * x1 by Th2
.= (- 1) * x by A5 ;
then reconsider y = v as VECTOR of Z_ModuleStruct(# D,d1,A,M #) ;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. Z_ModuleStruct(# D,d1,A,M #)
thus x + y = 0. Z_ModuleStruct(# D,d1,A,M #) by A2, A6, A8; :: thesis: verum
end;
thus for a being Integer
for x, y being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds a * (x + y) = (a * x) + (a * y) :: according to ZMODUL01:def 2 :: thesis: ( Z_ModuleStruct(# D,d1,A,M #) is scalar-distributive & Z_ModuleStruct(# D,d1,A,M #) is scalar-associative & Z_ModuleStruct(# D,d1,A,M #) is scalar-unital )
proof
let a be Integer; :: thesis: for x, y being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds a * (x + y) = (a * x) + (a * y)
let x, y be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: thesis: a * (x + y) = (a * x) + (a * y)
reconsider x1 = x, y1 = y as VECTOR of V by A1, TARSKI:def 3;
reconsider a = a as Integer ;
a * (x + y) = the Mult of V . (a,(x + y)) by A5
.= a * (x1 + y1) by A6
.= (a * x1) + (a * y1) by Def2
.= the addF of V . (( the Mult of V . (a,x1)),(a * y)) by A5
.= the addF of V . ((a * x),(a * y)) by A5
.= (a * x) + (a * y) by A6 ;
hence a * (x + y) = (a * x) + (a * y) ; :: thesis: verum
end;
thus for a, b being Integer
for x being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds (a + b) * x = (a * x) + (b * x) :: according to ZMODUL01:def 3 :: thesis: ( Z_ModuleStruct(# D,d1,A,M #) is scalar-associative & Z_ModuleStruct(# D,d1,A,M #) is scalar-unital )
proof
let a, b be Integer; :: thesis: for x being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds (a + b) * x = (a * x) + (b * x)
let x be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: thesis: (a + b) * x = (a * x) + (b * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
reconsider a = a, b = b as Integer ;
(a + b) * x = (a + b) * y by A5
.= (a * y) + (b * y) by Def3
.= the addF of V . (( the Mult of V . (a,y)),(b * x)) by A5
.= the addF of V . ((a * x),(b * x)) by A5
.= (a * x) + (b * x) by A6 ;
hence (a + b) * x = (a * x) + (b * x) ; :: thesis: verum
end;
thus for a, b being Integer
for x being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds (a * b) * x = a * (b * x) :: according to ZMODUL01:def 4 :: thesis: Z_ModuleStruct(# D,d1,A,M #) is scalar-unital
proof
let a, b be Integer; :: thesis: for x being VECTOR of Z_ModuleStruct(# D,d1,A,M #) holds (a * b) * x = a * (b * x)
let x be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: thesis: (a * b) * x = a * (b * x)
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
reconsider a = a, b = b as Integer ;
(a * b) * x = (a * b) * y by A5
.= a * (b * y) by Def4
.= the Mult of V . (a,(b * x)) by A5
.= a * (b * x) by A5 ;
hence (a * b) * x = a * (b * x) ; :: thesis: verum
end;
let x be VECTOR of Z_ModuleStruct(# D,d1,A,M #); :: according to ZMODUL01:def 5 :: thesis: 1 * x = x
reconsider y = x as VECTOR of V by A1, TARSKI:def 3;
thus 1 * x = 1 * y by A5
.= x by Def5 ; :: thesis: verum
end;
0. Z_ModuleStruct(# D,d1,A,M #) = 0. V by A2;
hence Z_ModuleStruct(# D,d1,A,M #) is Submodule of V by A1, A3, A4, A7, Def9; :: thesis: verum