Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Submodules and Cosets of Submodules in Right Module over Associative Ring

**by****Michal Muzalewski, and****Wojciech Skaba**- Received October 22, 1990
- MML identifier: RMOD_2

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCSDOM, VECTSP_1, VECTSP_2, RLSUB_1, BOOLE, RLVECT_1, ARYTM_1, LMOD_4, RELAT_1, FUNCT_1, BINOP_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, DOMAIN_1, RLVECT_1, BINOP_1, VECTSP_1, FUNCSDOM, VECTSP_2; constructors DOMAIN_1, BINOP_1, VECTSP_2, PARTFUN1, MEMBERED, XBOOLE_0; clusters FUNCT_1, VECTSP_2, STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve x,y,y1,y2 for set; 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 lineary-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; canceled 3; theorem :: RMOD_2:4 V1 <> {} & V1 is lineary-closed implies 0.V in V1; theorem :: RMOD_2:5 V1 is lineary-closed implies (for v st v in V1 holds - v in V1); theorem :: RMOD_2:6 V1 is lineary-closed implies (for v,u st v in V1 & u in V1 holds v - u in V1); theorem :: RMOD_2:7 {0.V} is lineary-closed; theorem :: RMOD_2:8 the carrier of V = V1 implies V1 is lineary-closed; theorem :: RMOD_2:9 V1 is lineary-closed & V2 is lineary-closed & V3 = {v + u : v in V1 & u in V2} implies V3 is lineary-closed; theorem :: RMOD_2:10 V1 is lineary-closed & V2 is lineary-closed implies V1 /\ V2 is lineary-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 & the Zero of it = the Zero of V & the add of it = (the add of V) | [:the carrier of it,the carrier of it:] & the rmult of it = (the rmult of V) | [:the carrier of it, the carrier of R:]; end; reserve W,W1,W2 for Submodule of V; reserve w,w1,w2 for Vector of W; canceled 5; theorem :: RMOD_2:16 x in W1 & W1 is Submodule of W2 implies x in W2; theorem :: RMOD_2:17 x in W implies x in V; theorem :: RMOD_2:18 w is Vector of V; theorem :: RMOD_2:19 0.W = 0.V; theorem :: RMOD_2:20 0.W1 = 0.W2; theorem :: RMOD_2:21 w1 = v & w2 = u implies w1 + w2 = v + u; theorem :: RMOD_2:22 w = v implies w * a = v * a; theorem :: RMOD_2:23 w = v implies - v = - w; theorem :: RMOD_2:24 w1 = v & w2 = u implies w1 - w2 = v - u; theorem :: RMOD_2:25 0.V in W; theorem :: RMOD_2:26 0.W1 in W2; theorem :: RMOD_2:27 0.W in V; theorem :: RMOD_2:28 u in W & v in W implies u + v in W; theorem :: RMOD_2:29 v in W implies v * a in W; theorem :: RMOD_2:30 v in W implies - v in W; theorem :: RMOD_2:31 u in W & v in W implies u - v in W; theorem :: RMOD_2:32 V is Submodule of V; theorem :: RMOD_2:33 for X,V being strict RightMod of R holds V is Submodule of X & X is Submodule of V implies V = X; definition let R,V; cluster strict Submodule of V; end; theorem :: RMOD_2:34 V is Submodule of X & X is Submodule of Y implies V is Submodule of Y; theorem :: RMOD_2:35 the carrier of W1 c= the carrier of W2 implies W1 is Submodule of W2; theorem :: RMOD_2:36 (for v st v in W1 holds v in W2) implies W1 is Submodule of W2; theorem :: RMOD_2:37 for W1,W2 being strict Submodule of V holds the carrier of W1 = the carrier of W2 implies W1 = W2; theorem :: RMOD_2:38 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:39 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:40 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:41 the carrier of W = V1 implies V1 is lineary-closed; theorem :: RMOD_2:42 V1 <> {} & V1 is lineary-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; canceled 3; theorem :: RMOD_2:46 x in (0).V iff x = 0.V; theorem :: RMOD_2:47 (0).W = (0).V; theorem :: RMOD_2:48 (0).W1 = (0).W2; theorem :: RMOD_2:49 (0).W is Submodule of V; theorem :: RMOD_2:50 (0).V is Submodule of W; theorem :: RMOD_2:51 (0).W1 is Submodule of W2; canceled; theorem :: RMOD_2:53 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; canceled 3; theorem :: RMOD_2:57 x in v + W iff ex u st u in W & x = v + u; theorem :: RMOD_2:58 0.V in v + W iff v in W; theorem :: RMOD_2:59 v in v + W; theorem :: RMOD_2:60 0.V + W = the carrier of W; theorem :: RMOD_2:61 v + (0).V = {v}; theorem :: RMOD_2:62 v + (Omega).V = the carrier of V; theorem :: RMOD_2:63 0.V in v + W iff v + W = the carrier of W; theorem :: RMOD_2:64 v in W iff v + W = the carrier of W; theorem :: RMOD_2:65 v in W implies (v * a) + W = the carrier of W; theorem :: RMOD_2:66 u in W iff v + W = (v + u) + W; theorem :: RMOD_2:67 u in W iff v + W = (v - u) + W; theorem :: RMOD_2:68 v in u + W iff u + W = v + W; theorem :: RMOD_2:69 u in v1 + W & u in v2 + W implies v1 + W = v2 + W; theorem :: RMOD_2:70 v in W implies v * a in v + W; theorem :: RMOD_2:71 v in W implies - v in v + W; theorem :: RMOD_2:72 u + v in v + W iff u in W; theorem :: RMOD_2:73 v - u in v + W iff u in W; canceled; theorem :: RMOD_2:75 u in v + W iff (ex v1 st v1 in W & u = v - v1); theorem :: RMOD_2:76 (ex v st v1 in v + W & v2 in v + W) iff v1 - v2 in W; theorem :: RMOD_2:77 v + W = u + W implies (ex v1 st v1 in W & v + v1 = u); theorem :: RMOD_2:78 v + W = u + W implies (ex v1 st v1 in W & v - v1 = u); theorem :: RMOD_2:79 for W1,W2 being strict Submodule of V holds v + W1 = v + W2 iff W1 = W2; theorem :: RMOD_2:80 for W1,W2 being strict Submodule of V holds v + W1 = u + W2 implies W1 = W2; theorem :: RMOD_2:81 ex C st v in C; theorem :: RMOD_2:82 C is lineary-closed iff C = the carrier of W; theorem :: RMOD_2:83 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:84 {v} is Coset of (0).V; theorem :: RMOD_2:85 V1 is Coset of (0).V implies (ex v st V1 = {v}); theorem :: RMOD_2:86 the carrier of W is Coset of W; theorem :: RMOD_2:87 the carrier of V is Coset of (Omega).V; theorem :: RMOD_2:88 V1 is Coset of (Omega).V implies V1 = the carrier of V; theorem :: RMOD_2:89 0.V in C iff C = the carrier of W; theorem :: RMOD_2:90 u in C iff C = u + W; theorem :: RMOD_2:91 u in C & v in C implies (ex v1 st v1 in W & u + v1 = v); theorem :: RMOD_2:92 u in C & v in C implies (ex v1 st v1 in W & u - v1 = v); theorem :: RMOD_2:93 (ex C st v1 in C & v2 in C) iff v1 - v2 in W; theorem :: RMOD_2:94 u in B & u in C implies B = C;

Back to top