:: Submodules and Cosets of Submodules in Right Module over Associative Ring
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 22, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCSDOM, VECTSP_1, VECTSP_2, SUBSET_1, RLSUB_1, ARYTM_3,
RELAT_1, XBOOLE_0, SUPINF_2, ARYTM_1, GROUP_1, STRUCT_0, TARSKI,
ALGSTR_0, ZFMISC_1, FUNCT_1, REALSET1, RLVECT_1, BINOP_1, RMOD_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
REALSET1, STRUCT_0, ALGSTR_0, DOMAIN_1, RLVECT_1, BINOP_1, GROUP_1,
VECTSP_1, VECTSP_2;
constructors PARTFUN1, BINOP_1, REALSET1, VECTSP_2, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, REALSET1, STRUCT_0, VECTSP_1,
VECTSP_2, RELAT_1, ALGSTR_0;
requirements SUBSET, BOOLE;
begin
reserve x,y,y1,y2 for object;
reserve R for Ring;
reserve a for Scalar of R;
reserve V,X,Y for RightMod of R;
reserve u,u1,u2,v,v1,v2 for Vector of V;
reserve V1,V2,V3 for Subset of V;
definition
let R, V, V1;
attr V1 is linearly-closed means
:: RMOD_2:def 1
(for v,u st v in V1 & u in V1 holds
v + u in V1) & for a,v st v in V1 holds v * a in V1;
end;
theorem :: RMOD_2:1
V1 <> {} & V1 is linearly-closed implies 0.V in V1;
theorem :: RMOD_2:2
V1 is linearly-closed implies for v st v in V1 holds - v in V1;
theorem :: RMOD_2:3
V1 is linearly-closed implies for v,u st v in V1 & u in V1 holds v - u in V1;
theorem :: RMOD_2:4
{0.V} is linearly-closed;
theorem :: RMOD_2:5
the carrier of V = V1 implies V1 is linearly-closed;
theorem :: RMOD_2:6
V1 is linearly-closed & V2 is linearly-closed & V3 = {v + u : v in V1
& u in V2} implies V3 is linearly-closed;
theorem :: RMOD_2:7
V1 is linearly-closed & V2 is linearly-closed implies V1 /\ V2 is
linearly-closed;
definition
let R;
let V;
mode Submodule of V -> RightMod of R means
:: RMOD_2:def 2
the carrier of it c= the
carrier of V & 0.it = 0.V & the addF of it = (the addF of V) | ([:the carrier
of it,the carrier of it:] qua set) & the rmult of it = (the rmult of V)|([:the
carrier of it, the carrier of R:] qua set);
end;
reserve W,W1,W2 for Submodule of V;
reserve w,w1,w2 for Vector of W;
theorem :: RMOD_2:8
x in W1 & W1 is Submodule of W2 implies x in W2;
theorem :: RMOD_2:9
x in W implies x in V;
theorem :: RMOD_2:10
w is Vector of V;
theorem :: RMOD_2:11
0.W = 0.V;
theorem :: RMOD_2:12
0.W1 = 0.W2;
theorem :: RMOD_2:13
w1 = v & w2 = u implies w1 + w2 = v + u;
theorem :: RMOD_2:14
w = v implies w * a = v * a;
theorem :: RMOD_2:15
w = v implies - v = - w;
theorem :: RMOD_2:16
w1 = v & w2 = u implies w1 - w2 = v - u;
theorem :: RMOD_2:17
0.V in W;
theorem :: RMOD_2:18
0.W1 in W2;
theorem :: RMOD_2:19
0.W in V;
theorem :: RMOD_2:20
u in W & v in W implies u + v in W;
theorem :: RMOD_2:21
v in W implies v * a in W;
theorem :: RMOD_2:22
v in W implies - v in W;
theorem :: RMOD_2:23
u in W & v in W implies u - v in W;
theorem :: RMOD_2:24
V is Submodule of V;
theorem :: RMOD_2:25
for X,V being strict RightMod of R holds V is Submodule of X & X
is Submodule of V implies V = X;
registration
let R,V;
cluster strict for Submodule of V;
end;
theorem :: RMOD_2:26
V is Submodule of X & X is Submodule of Y implies V is Submodule of Y;
theorem :: RMOD_2:27
the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2;
theorem :: RMOD_2:28
(for v st v in W1 holds v in W2) implies W1 is Submodule of W2;
theorem :: RMOD_2:29
for W1,W2 being strict Submodule of V holds the carrier of W1 =
the carrier of W2 implies W1 = W2;
theorem :: RMOD_2:30
for W1,W2 being strict Submodule of V holds (for v being Vector
of V holds v in W1 iff v in W2) implies W1 = W2;
theorem :: RMOD_2:31
for V being strict RightMod of R, W being strict Submodule of V holds
the carrier of W = the carrier of V implies W = V;
theorem :: RMOD_2:32
for V being strict RightMod of R, W being strict Submodule of V holds
(for v being Vector of V holds v in W) implies W = V;
theorem :: RMOD_2:33
the carrier of W = V1 implies V1 is linearly-closed;
theorem :: RMOD_2:34
V1 <> {} & V1 is linearly-closed implies ex W being strict
Submodule of V st V1 = the carrier of W;
definition
let R;
let V;
func (0).V -> strict Submodule of V means
:: RMOD_2:def 3
the carrier of it = {0.V};
end;
definition
let R;
let V;
func (Omega).V -> strict Submodule of V equals
:: RMOD_2:def 4
the RightModStr of V;
end;
theorem :: RMOD_2:35
x in (0).V iff x = 0.V;
theorem :: RMOD_2:36
(0).W = (0).V;
theorem :: RMOD_2:37
(0).W1 = (0).W2;
theorem :: RMOD_2:38
(0).W is Submodule of V;
theorem :: RMOD_2:39
(0).V is Submodule of W;
theorem :: RMOD_2:40
(0).W1 is Submodule of W2;
theorem :: RMOD_2:41
for V being strict RightMod of R holds V is Submodule of (Omega).V;
definition
let R;
let V;
let v,W;
func v + W -> Subset of V equals
:: RMOD_2:def 5
{v + u : u in W};
end;
definition
let R;
let V;
let W;
mode Coset of W -> Subset of V means
:: RMOD_2:def 6
ex v st it = v + W;
end;
reserve B,C for Coset of W;
theorem :: RMOD_2:42
x in v + W iff ex u st u in W & x = v + u;
theorem :: RMOD_2:43
0.V in v + W iff v in W;
theorem :: RMOD_2:44
v in v + W;
theorem :: RMOD_2:45
0.V + W = the carrier of W;
theorem :: RMOD_2:46
v + (0).V = {v};
theorem :: RMOD_2:47
v + (Omega).V = the carrier of V;
theorem :: RMOD_2:48
0.V in v + W iff v + W = the carrier of W;
theorem :: RMOD_2:49
v in W iff v + W = the carrier of W;
theorem :: RMOD_2:50
v in W implies (v * a) + W = the carrier of W;
theorem :: RMOD_2:51
u in W iff v + W = (v + u) + W;
theorem :: RMOD_2:52
u in W iff v + W = (v - u) + W;
theorem :: RMOD_2:53
v in u + W iff u + W = v + W;
theorem :: RMOD_2:54
u in v1 + W & u in v2 + W implies v1 + W = v2 + W;
theorem :: RMOD_2:55
v in W implies v * a in v + W;
theorem :: RMOD_2:56
v in W implies - v in v + W;
theorem :: RMOD_2:57
u + v in v + W iff u in W;
theorem :: RMOD_2:58
v - u in v + W iff u in W;
theorem :: RMOD_2:59
u in v + W iff ex v1 st v1 in W & u = v - v1;
theorem :: RMOD_2:60
(ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W;
theorem :: RMOD_2:61
v + W = u + W implies ex v1 st v1 in W & v + v1 = u;
theorem :: RMOD_2:62
v + W = u + W implies ex v1 st v1 in W & v - v1 = u;
theorem :: RMOD_2:63
for W1,W2 being strict Submodule of V holds v + W1 = v + W2 iff W1 = W2;
theorem :: RMOD_2:64
for W1,W2 being strict Submodule of V holds v + W1 = u + W2 implies W1 = W2;
theorem :: RMOD_2:65
ex C st v in C;
theorem :: RMOD_2:66
C is linearly-closed iff C = the carrier of W;
theorem :: RMOD_2:67
for W1,W2 being strict Submodule of V for C1 being Coset of W1, C2
being Coset of W2 holds C1 = C2 implies W1 = W2;
theorem :: RMOD_2:68
{v} is Coset of (0).V;
theorem :: RMOD_2:69
V1 is Coset of (0).V implies ex v st V1 = {v};
theorem :: RMOD_2:70
the carrier of W is Coset of W;
theorem :: RMOD_2:71
the carrier of V is Coset of (Omega).V;
theorem :: RMOD_2:72
V1 is Coset of (Omega).V implies V1 = the carrier of V;
theorem :: RMOD_2:73
0.V in C iff C = the carrier of W;
theorem :: RMOD_2:74
u in C iff C = u + W;
theorem :: RMOD_2:75
u in C & v in C implies ex v1 st v1 in W & u + v1 = v;
theorem :: RMOD_2:76
u in C & v in C implies ex v1 st v1 in W & u - v1 = v;
theorem :: RMOD_2:77
(ex C st v1 in C & v2 in C) iff v1 - v2 in W;
theorem :: RMOD_2:78
u in B & u in C implies B = C;