Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Operations on Submodules in Right Module over Associative Ring

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

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCSDOM, VECTSP_2, LMOD_4, VECTSP_1, RLVECT_1, RLSUB_1, BOOLE, ARYTM_1, FUNCT_1, RELAT_1, RLSUB_2, MCART_1, BINOP_1, LATTICES, RMOD_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1, STRUCT_0, LATTICES, RLVECT_1, DOMAIN_1, FUNCSDOM, VECTSP_2, RMOD_2; constructors BINOP_1, LATTICES, DOMAIN_1, RMOD_2, MEMBERED, XBOOLE_0; clusters LATTICES, VECTSP_2, RMOD_2, STRUCT_0, RLSUB_2, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve R for Ring, V for RightMod of R, W,W1,W2,W3 for Submodule of V, u,u1,u2,v,v1,v2 for Vector of V, x,y,y1,y2 for set; definition let R; let V; let W1,W2; func W1 + W2 -> strict Submodule of V means :: RMOD_3:def 1 the carrier of it = {v + u : v in W1 & u in W2}; end; definition let R; let V; let W1,W2; func W1 /\ W2 -> strict Submodule of V means :: RMOD_3:def 2 the carrier of it = (the carrier of W1) /\ (the carrier of W2); end; canceled 4; theorem :: RMOD_3:5 x in W1 + W2 iff (ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2); theorem :: RMOD_3:6 v in W1 or v in W2 implies v in W1 + W2; theorem :: RMOD_3:7 x in W1 /\ W2 iff x in W1 & x in W2; theorem :: RMOD_3:8 for W being strict Submodule of V holds W + W = W; theorem :: RMOD_3:9 W1 + W2 = W2 + W1; theorem :: RMOD_3:10 W1 + (W2 + W3) = (W1 + W2) + W3; theorem :: RMOD_3:11 W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2; theorem :: RMOD_3:12 for W2 being strict Submodule of V holds W1 is Submodule of W2 iff W1 + W2 = W2; theorem :: RMOD_3:13 for W being strict Submodule of V holds (0).V + W = W & W + (0).V = W; theorem :: RMOD_3:14 for V being strict RightMod of R holds (0).V + (Omega).V = V & (Omega).V + (0).V = V; theorem :: RMOD_3:15 for V being RightMod of R, W being Submodule of V holds (Omega).V + W = the RightModStr of V & W + (Omega). V = the RightModStr of V; theorem :: RMOD_3:16 for V being strict RightMod of R holds (Omega).V + (Omega).V = V; theorem :: RMOD_3:17 for W being strict Submodule of V holds W /\ W = W; theorem :: RMOD_3:18 W1 /\ W2 = W2 /\ W1; theorem :: RMOD_3:19 W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3; theorem :: RMOD_3:20 W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2; theorem :: RMOD_3:21 (for W1 being strict Submodule of V holds W1 is Submodule of W2 implies W1 /\ W2 = W1) & for W1 st W1 /\ W2 = W1 holds W1 is Submodule of W2; theorem :: RMOD_3:22 W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3; theorem :: RMOD_3:23 W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3; theorem :: RMOD_3:24 W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule of W2 /\ W3; theorem :: RMOD_3:25 (0).V /\ W = (0).V & W /\ (0).V = (0).V; canceled; theorem :: RMOD_3:27 for W being strict Submodule of V holds (Omega).V /\ W = W & W /\ (Omega).V = W; theorem :: RMOD_3:28 for V being strict RightMod of R holds (Omega).V /\ (Omega).V = V; theorem :: RMOD_3:29 W1 /\ W2 is Submodule of W1 + W2; theorem :: RMOD_3:30 for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2; theorem :: RMOD_3:31 for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1; theorem :: RMOD_3:32 (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3); theorem :: RMOD_3:33 W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3); theorem :: RMOD_3:34 W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3); theorem :: RMOD_3:35 W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3); theorem :: RMOD_3:36 for W1 being strict Submodule of V holds W1 is Submodule of W3 implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3; theorem :: RMOD_3:37 for W1,W2 being strict Submodule of V holds W1 + W2 = W2 iff W1 /\ W2 = W1; theorem :: RMOD_3:38 for W2,W3 being strict Submodule of V holds W1 is Submodule of W2 implies W1 + W3 is Submodule of W2 + W3; theorem :: RMOD_3:39 W1 is Submodule of W2 implies W1 is Submodule of W2 + W3; theorem :: RMOD_3:40 W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is Submodule of W3; theorem :: RMOD_3:41 (ex W st the carrier of W = (the carrier of W1) \/ (the carrier of W2)) iff W1 is Submodule of W2 or W2 is Submodule of W1; definition let R; let V; func Submodules(V) -> set means :: RMOD_3:def 3 for x holds x in it iff ex W being strict Submodule of V st W = x; end; definition let R; let V; cluster Submodules(V) -> non empty; end; canceled 2; theorem :: RMOD_3:44 for V being strict RightMod of R holds V in Submodules(V); definition let R; let V; let W1,W2; pred V is_the_direct_sum_of W1,W2 means :: RMOD_3:def 4 the RightModStr of V = W1 + W2 & W1 /\ W2 = (0).V; end; canceled; theorem :: RMOD_3:46 V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2,W1; theorem :: RMOD_3:47 for V being strict RightMod of R holds V is_the_direct_sum_of (0).V,(Omega).V & V is_the_direct_sum_of (Omega).V,(0).V; reserve C1 for Coset of W1; reserve C2 for Coset of W2; theorem :: RMOD_3:48 C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2; theorem :: RMOD_3:49 for V being RightMod of R, W1,W2 being Submodule of V holds V is_the_direct_sum_of W1,W2 iff for C1 being Coset of W1, C2 being Coset of W2 ex v being Vector of V st C1 /\ C2 = {v}; theorem :: RMOD_3:50 for V being strict RightMod of R, W1,W2 being Submodule of V holds W1 + W2 = V iff for v being Vector of V ex v1,v2 being Vector of V st v1 in W1 & v2 in W2 & v = v1 + v2; theorem :: RMOD_3:51 for V being RightMod of R, W1,W2 being Submodule of V, v,v1,v2,u1,u2 being Vector of V holds V is_the_direct_sum_of W1,W2 & v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 implies v1 = u1 & v2 = u2; theorem :: RMOD_3:52 V = W1 + W2 & (ex v st for v1,v2,u1,u2 st v = v1 + v2 & v = u1 + u2 & v1 in W1 & u1 in W1 & v2 in W2 & u2 in W2 holds v1 = u1 & v2 = u2) implies V is_the_direct_sum_of W1,W2; definition let R; let V be RightMod of R; let v be Vector of V; let W1,W2 be Submodule of V; assume V is_the_direct_sum_of W1,W2; func v |-- (W1,W2) -> Element of [:the carrier of V, the carrier of V:] means :: RMOD_3:def 5 v = it`1 + it`2 & it`1 in W1 & it`2 in W2; end; canceled 4; theorem :: RMOD_3:57 V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1))`2; theorem :: RMOD_3:58 V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`2 = (v |-- (W2,W1))`1; reserve A1,A2,B for Element of Submodules(V); definition let R; let V; func SubJoin(V) -> BinOp of Submodules(V) means :: RMOD_3:def 6 for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 + W2; end; definition let R; let V; func SubMeet(V) -> BinOp of Submodules(V) means :: RMOD_3:def 7 for A1,A2,W1,W2 st A1 = W1 & A2 = W2 holds it.(A1,A2) = W1 /\ W2; end; canceled 4; theorem :: RMOD_3:63 LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice; theorem :: RMOD_3:64 LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 0_Lattice; theorem :: RMOD_3:65 for V being RightMod of R holds LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 1_Lattice; theorem :: RMOD_3:66 for V being RightMod of R holds LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 01_Lattice; theorem :: RMOD_3:67 LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is M_Lattice;

Back to top