:: Operations on 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_2, RMOD_2, VECTSP_1, ARYTM_3, STRUCT_0,
      SUBSET_1, TARSKI, SUPINF_2, RLSUB_1, XBOOLE_0, ARYTM_1, ZFMISC_1,
      FUNCT_1, RELAT_1, RLSUB_2, FINSEQ_4, MCART_1, BINOP_1, LATTICES, EQREL_1,
      PBOOLE, RMOD_3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, FUNCT_1,
      STRUCT_0, LATTICES, RLVECT_1, DOMAIN_1, VECTSP_1, VECTSP_2, RMOD_2;
 constructors BINOP_1, DOMAIN_1, LATTICES, RMOD_2;
 registrations SUBSET_1, STRUCT_0, LATTICES, VECTSP_2, RMOD_2, RELAT_1,
      XTUPLE_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 object;

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;

theorem :: RMOD_3:1
  x in W1 + W2 iff ex v1,v2 st v1 in W1 & v2 in W2 & x = v1 + v2;

theorem :: RMOD_3:2
  v in W1 or v in W2 implies v in W1 + W2;

theorem :: RMOD_3:3
  x in W1 /\ W2 iff x in W1 & x in W2;

theorem :: RMOD_3:4
  for W being strict Submodule of V holds W + W = W;

theorem :: RMOD_3:5
  W1 + W2 = W2 + W1;

theorem :: RMOD_3:6
  W1 + (W2 + W3) = (W1 + W2) + W3;

theorem :: RMOD_3:7
  W1 is Submodule of W1 + W2 & W2 is Submodule of W1 + W2;

theorem :: RMOD_3:8
  for W2 being strict Submodule of V holds W1 is Submodule of W2
  iff W1 + W2 = W2;

theorem :: RMOD_3:9
  for W being strict Submodule of V holds (0).V + W = W & W + (0). V = W;

theorem :: RMOD_3:10
  for V being strict RightMod of R holds (0).V + (Omega).V = V &
  (Omega).V + (0).V = V;

theorem :: RMOD_3:11
  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:12
  for V being strict RightMod of R holds (Omega).V + (Omega).V = V;

theorem :: RMOD_3:13
  for W being strict Submodule of V holds W /\ W = W;

theorem :: RMOD_3:14
  W1 /\ W2 = W2 /\ W1;

theorem :: RMOD_3:15
  W1 /\ (W2 /\ W3) = (W1 /\ W2) /\ W3;

theorem :: RMOD_3:16
  W1 /\ W2 is Submodule of W1 & W1 /\ W2 is Submodule of W2;

theorem :: RMOD_3:17
  (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:18
  W1 is Submodule of W2 implies W1 /\ W3 is Submodule of W2 /\ W3;

theorem :: RMOD_3:19
  W1 is Submodule of W3 implies W1 /\ W2 is Submodule of W3;

theorem :: RMOD_3:20
  W1 is Submodule of W2 & W1 is Submodule of W3 implies W1 is Submodule
  of W2 /\ W3;

theorem :: RMOD_3:21
  (0).V /\ W = (0).V & W /\ (0).V = (0).V;

theorem :: RMOD_3:22
  for W being strict Submodule of V holds (Omega).V /\ W = W & W
  /\ (Omega).V = W;

theorem :: RMOD_3:23
  for V being strict RightMod of R holds (Omega).V /\ (Omega).V = V;

theorem :: RMOD_3:24
  W1 /\ W2 is Submodule of W1 + W2;

theorem :: RMOD_3:25
  for W2 being strict Submodule of V holds (W1 /\ W2) + W2 = W2;

theorem :: RMOD_3:26
  for W1 being strict Submodule of V holds W1 /\ (W1 + W2) = W1;

theorem :: RMOD_3:27
  (W1 /\ W2) + (W2 /\ W3) is Submodule of W2 /\ (W1 + W3);

theorem :: RMOD_3:28
  W1 is Submodule of W2 implies W2 /\ (W1 + W3) = (W1 /\ W2) + (W2 /\ W3
  );

theorem :: RMOD_3:29
  W2 + (W1 /\ W3) is Submodule of (W1 + W2) /\ (W2 + W3);

theorem :: RMOD_3:30
  W1 is Submodule of W2 implies W2 + (W1 /\ W3) = (W1 + W2) /\ (W2 + W3);

theorem :: RMOD_3:31
  for W1 being strict Submodule of V holds W1 is Submodule of W3
  implies W1 + (W2 /\ W3) = (W1 + W2) /\ W3;

theorem :: RMOD_3:32
  for W1,W2 being strict Submodule of V holds W1 + W2 = W2 iff W1 /\ W2 = W1;

theorem :: RMOD_3:33
  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:34
  W1 is Submodule of W2 implies W1 is Submodule of W2 + W3;

theorem :: RMOD_3:35
  W1 is Submodule of W3 & W2 is Submodule of W3 implies W1 + W2 is
  Submodule of W3;

theorem :: RMOD_3:36
  (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 being object
holds x in it iff ex W being strict Submodule of V st W = x;
end;

registration
  let R;
  let V;
  cluster Submodules(V) -> non empty;
end;

theorem :: RMOD_3:37
  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;

theorem :: RMOD_3:38
  V is_the_direct_sum_of W1,W2 implies V is_the_direct_sum_of W2, W1;

theorem :: RMOD_3:39
  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:40
  C1 meets C2 implies C1 /\ C2 is Coset of W1 /\ W2;

theorem :: RMOD_3:41
  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:42
  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:43
  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:44
  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;

theorem :: RMOD_3:45
  V is_the_direct_sum_of W1,W2 implies (v |-- (W1,W2))`1 = (v |-- (W2,W1 ))`2;

theorem :: RMOD_3:46
  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;

theorem :: RMOD_3:47
  LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is Lattice;

theorem :: RMOD_3:48
  LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is 0_Lattice;

theorem :: RMOD_3:49
  for V being RightMod of R holds LattStr (# Submodules(V),
    SubJoin(V), SubMeet(V) #) is 1_Lattice;

theorem :: RMOD_3:50
  for V being RightMod of R holds LattStr (# Submodules(V), SubJoin(V),
    SubMeet(V) #) is 01_Lattice;

theorem :: RMOD_3:51
  LattStr (# Submodules(V), SubJoin(V), SubMeet(V) #) is M_Lattice;