:: Construction of Rings and Left-, Right-, and Bi-Modules over a Ring
::  by Micha{\l} Muzalewski
::
:: Received June 20, 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 XBOOLE_0, ALGSTR_0, VECTSP_1, MESFUNC1, GROUP_1, SUBSET_1,
      RELAT_1, STRUCT_0, RLVECT_1, LATTICES, FUNCSDOM, BINOP_1, SUPINF_2,
      ARYTM_3, ARYTM_1, FUNCT_1, ZFMISC_1, FUNCT_5, MCART_1, VECTSP_2, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_2, BINOP_1,
      FUNCT_5, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FUNCSDOM,
      FUNCT_3;
 constructors FUNCT_3, VECTSP_1, FUNCSDOM, FUNCT_5, NUMBERS, GROUP_1;
 registrations XBOOLE_0, STRUCT_0, VECTSP_1, ALGSTR_0;
 requirements SUBSET, BOOLE;


begin :: 1. RING

reserve FS for non empty doubleLoopStr;
reserve F for Field;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
    unital distributive for non empty doubleLoopStr;
end;

definition
  let IT be non empty multLoopStr_0;

  attr IT is domRing-like means
:: VECTSP_2:def 1

  for x,y being Element of IT holds x*y = 0.IT implies x = 0.IT or y = 0.IT;
end;

registration
  cluster strict non degenerated commutative almost_left_invertible
    domRing-like for Ring;
end;

definition
  mode comRing is commutative Ring;
end;

definition
  mode domRing is domRing-like non degenerated comRing;
end;

theorem :: VECTSP_2:1
  F is domRing;

:: 10. AXIOMS OF SKEW-FIELD

registration
  cluster commutative left_unital -> well-unital for non empty multLoopStr;
  cluster commutative right_unital -> well-unital for non empty multLoopStr;
end;

:: 11. SOME PROPERTIES OF RING

reserve R for Abelian add-associative right_zeroed right_complementable non
  empty addLoopStr,
  x, y, z for Scalar of R;

theorem :: VECTSP_2:2
  (x + y = z iff x = z - y) & (x + y = z iff y = z - x);

theorem :: VECTSP_2:3
  for R being add-associative right_zeroed right_complementable
  non empty addLoopStr, x being Element of R holds x=0.R iff -x=0.R;

theorem :: VECTSP_2:4
  for R being add-associative right_zeroed Abelian right_complementable
non empty addLoopStr for x,y being Element of R ex z being Element of R st x
  = y+z & x = z+y;

:: 12. SOME PROPERTIES OF SKEW-FIELD

reserve SF for Skew-Field,
  x, y, z for Scalar of SF;

theorem :: VECTSP_2:5
  for F being add-associative right_zeroed right_complementable
  distributive non degenerated non empty doubleLoopStr for x, y being Element
  of F holds x*y = 1.F implies x<>0.F & y<>0.F;

theorem :: VECTSP_2:6
  for SF being non degenerated almost_left_invertible associative
add-associative right_zeroed right_complementable well-unital distributive non
  empty doubleLoopStr, x being Element of SF holds x<>0.SF implies ex y being
  Element of SF st x*y = 1.SF;

theorem :: VECTSP_2:7
  for SF being add-associative right_zeroed right_complementable
  distributive non degenerated almost_left_invertible associative well-unital
non empty doubleLoopStr for x,y being Element of SF st y*x = 1.SF holds x*y =
  1.SF;

theorem :: VECTSP_2:8
  for SF being non degenerated almost_left_invertible associative
  Abelian add-associative right_zeroed right_complementable well-unital
distributive non empty doubleLoopStr, x,y,z being Element of SF holds x * y =
  x * z & x<>0.SF implies y = z;

notation
  let SF be non degenerated almost_left_invertible associative add-associative
  right_zeroed right_complementable well-unital distributive non empty
  doubleLoopStr, x be Element of SF;
  synonym x" for /x;
end;

definition
  let SF be non degenerated almost_left_invertible associative add-associative
  right_zeroed right_complementable well-unital distributive non empty
   doubleLoopStr, x be Element of SF;
  assume
 x<>0.SF;

  redefine func x" means
:: VECTSP_2:def 2

  it * x = 1.SF;
end;

:: definition
::   let SF,x,y;
::   func x/y -> Scalar of SF equals
::   x * y";
::   correctness;
:: end;

::$CD

theorem :: VECTSP_2:9
  x<>0.SF implies x * x" = 1.SF & x" * x = 1.SF;

theorem :: VECTSP_2:10
  y*x = 1_SF implies x = y" & y = x";

theorem :: VECTSP_2:11
  x<>0.SF & y<>0.SF implies x"*y"=(y*x)";

theorem :: VECTSP_2:12
  x*y = 0.SF implies x = 0.SF or y = 0.SF;

theorem :: VECTSP_2:13
  x<>0.SF implies x"<>0.SF;

theorem :: VECTSP_2:14
  x<>0.SF implies x""=x;

theorem :: VECTSP_2:15
  x<>0.SF implies (1_SF)/x=x" & (1_SF)/x"=x;

theorem :: VECTSP_2:16
  x<>0.SF implies x*((1_SF)/x)=1_SF & ((1_SF)/x)*x=1_SF;

theorem :: VECTSP_2:17
  x<>0.SF implies x/x = 1_SF;

theorem :: VECTSP_2:18
  y<>0.SF & z<>0.SF implies x/y=(x*z)/(y*z);

theorem :: VECTSP_2:19
  y<>0.SF implies -x/y=(-x)/y & x/(-y)=-x/y;

theorem :: VECTSP_2:20
  z<>0.SF implies x/z + y/z = (x+y)/z & x/z - y/z = (x-y)/z;

theorem :: VECTSP_2:21
  y<>0.SF & z<>0.SF implies x/(y/z)=(x*z)/y;

theorem :: VECTSP_2:22
  y<>0.SF implies x/y*y=x;

:: 13. LEFT-, RIGHT-, AND BI-MODULE STRUCTURE

definition
  let FS be 1-sorted;
  struct(addLoopStr) RightModStr over FS (# carrier -> set, addF -> BinOp of
    the carrier, ZeroF -> Element of the carrier, rmult -> Function of [: the
    carrier, the carrier of FS:], the carrier #);
end;

registration
  let FS be 1-sorted;
  cluster non empty for RightModStr over FS;
end;

registration
  let FS be 1-sorted;
  let A be non empty set, a be BinOp of A, Z be Element of A, r be Function of
  [:A,the carrier of FS:],A;
  cluster RightModStr(#A,a,Z,r#) -> non empty;
end;

definition
  let FS;
  let RMS be non empty RightModStr over FS;
  mode Scalar of RMS is Element of FS;
  mode Vector of RMS is Element of RMS;
end;

definition
  let FS1,FS2 be 1-sorted;
  struct (ModuleStr over FS1, RightModStr over FS2) BiModStr over FS1,FS2 (#
carrier -> set, addF -> BinOp of the carrier, ZeroF -> Element of the carrier,
lmult -> Function of [:the carrier of FS1, the carrier:], the carrier, rmult ->
    Function of [:the carrier, the carrier of FS2:], the carrier #);
end;

registration
  let FS1,FS2 be 1-sorted;
  cluster non empty for BiModStr over FS1,FS2;
end;

registration
  let FS1,FS2 be 1-sorted;
  let A be non empty set, a be BinOp of A, Z be Element of A, l be Function of
  [:the carrier of FS1,A:],A, r be Function of [:A,the carrier of FS2:],A;
  cluster BiModStr(#A,a,Z,l,r#) -> non empty;
end;

:: 14. PREDE LEFT-MODULE OF RING

reserve R, R1, R2 for Ring;

definition
  let R be Abelian add-associative right_zeroed right_complementable non
  empty addLoopStr;
  func AbGr R -> strict AbGroup equals
:: VECTSP_2:def 4
  addLoopStr (#the carrier of R, the addF
    of R, 0.R#);
end;

registration
  let R;
  cluster Abelian add-associative right_zeroed right_complementable strict for

    non empty ModuleStr over R;
end;

definition
  let R;

  func LeftModule R -> Abelian add-associative right_zeroed
  right_complementable strict non empty ModuleStr over R equals
:: VECTSP_2:def 5
  ModuleStr (#
    the carrier of R, the addF of R, 0.R, the multF of R #);
end;

registration let R;
  cluster Abelian add-associative right_zeroed right_complementable strict for

    non empty RightModStr over R;
end;

definition let R;

  func RightModule R -> Abelian add-associative right_zeroed
  right_complementable strict non empty RightModStr over R equals
:: VECTSP_2:def 6
  RightModStr
  (# the carrier of R, the addF of R, 0.R, the multF of R #);
end;

definition
  let R be non empty 1-sorted, V be non empty RightModStr over R;
  let x be Element of R;
  let v be Element of V;
  func v*x -> Element of V equals
:: VECTSP_2:def 7
  (the rmult of V).(v,x);
end;

registration let R1,R2;
  cluster Abelian add-associative right_zeroed right_complementable strict for

    non empty BiModStr over R1,R2;
end;

definition let R1,R2;

  func BiModule(R1,R2) -> Abelian add-associative right_zeroed
  right_complementable strict non empty BiModStr over R1,R2 equals
:: VECTSP_2:def 8
  BiModStr (#{0},op2,op0,
    pr2(the carrier of R1, {0}), pr1({0},the carrier of R2) #);
end;

theorem :: VECTSP_2:23
  for x,y being Scalar of R for v,w being Vector of LeftModule R
  holds x*(v+w) = x*v+x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v) & (1.R)*v = v
;

registration
  let R;
  cluster vector-distributive scalar-distributive scalar-associative
    scalar-unital Abelian add-associative right_zeroed
    right_complementable strict for non empty ModuleStr over R;
end;

definition
  let R;
  mode LeftMod of R is Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital non empty ModuleStr over R;
end;

registration let R;
  cluster LeftModule R -> Abelian add-associative right_zeroed
    right_complementable strict vector-distributive scalar-distributive
    scalar-associative scalar-unital;
end;

:: 18. AXIOMS OF LEFT MODULE OF RING

theorem :: VECTSP_2:24
  for x,y being Scalar of R for v,w being Vector of RightModule R
  holds (v+w)*x = v*x+w*x & v*(x+y) = v*x+v*y & v*(y*x) = (v*y)*x & v*(1_R) = v
;

definition
  let R be non empty doubleLoopStr;
  let IT be non empty RightModStr over R;

  attr IT is RightMod-like means
:: VECTSP_2:def 9

  for x,y being Scalar of R for v,w
being Vector of IT holds (v+w)*x = v*x+w*x & v*(x+y) = v*x+v*y & v*(y*x) = (v*y
  )*x & v*(1_R) = v;
end;

registration let R;
  cluster Abelian add-associative right_zeroed right_complementable
    RightMod-like strict for non empty RightModStr over R;
end;

definition
  let R;
  mode RightMod of R is Abelian add-associative right_zeroed
    right_complementable RightMod-like non empty RightModStr over R;
end;

registration let R;
  cluster RightModule R -> Abelian add-associative right_zeroed
    right_complementable RightMod-like;
end;

definition let R1,R2;
  let IT be non empty BiModStr over R1,R2;
  attr IT is BiMod-like means
:: VECTSP_2:def 10

  for x being Scalar of R1 for p being
  Scalar of R2 for v being Vector of IT holds x*(v*p) = (x*v)*p;
end;

registration let R1,R2;
  cluster Abelian add-associative right_zeroed right_complementable
RightMod-like vector-distributive scalar-distributive scalar-associative
scalar-unital BiMod-like strict for non empty BiModStr over R1,R2;
end;

definition let R1,R2;
  mode BiMod of R1,R2 is Abelian add-associative right_zeroed
right_complementable RightMod-like vector-distributive scalar-distributive
scalar-associative scalar-unital BiMod-like non empty BiModStr
    over R1,R2;
end;

theorem :: VECTSP_2:25
  for V being non empty BiModStr over R1,R2 holds (for x,y being Scalar
of R1 for p,q being Scalar of R2 for v,w being Vector of V holds x*(v+w) = x*v+
x*w & (x+y)*v = x*v+y*v & (x*y)*v = x*(y*v) & (1_R1)*v = v & (v+w)*p = v*p+w*p
& v*(p+q) = v*p+v*q & v*(q*p) = (v*q)*p & v*(1_R2) = v & x*(v*p) = (x*v)*p) iff
  V is RightMod-like vector-distributive scalar-distributive
  scalar-associative scalar-unital BiMod-like;

theorem :: VECTSP_2:26
  BiModule(R1,R2) is BiMod of R1,R2;

registration let R1,R2;
  cluster BiModule(R1,R2) -> Abelian add-associative right_zeroed
    right_complementable RightMod-like vector-distributive scalar-distributive
    scalar-associative scalar-unital BiMod-like;
end;

theorem :: VECTSP_2:27
  for L being non empty multLoopStr st L is well-unital holds 1.(L) =
  1_L;

begin :: MOD_1

theorem :: VECTSP_2:28
  for K be add-associative right_zeroed right_complementable
right-distributive right_unital non empty doubleLoopStr for a be Element of K
  holds a * (- 1.K) = - a;

theorem :: VECTSP_2:29
  for K be add-associative right_zeroed right_complementable
  left-distributive left_unital non empty doubleLoopStr for a be Element of K
  holds (- 1.K) * a = - a;

reserve R for Abelian add-associative right_zeroed right_complementable
  associative well-unital right_unital distributive non empty doubleLoopStr,
  F for non degenerated almost_left_invertible Ring,
  x for Scalar of F,
  V for add-associative right_zeroed right_complementable vector-distributive
  scalar-distributive scalar-associative scalar-unital
   non empty
  ModuleStr over F,
  v for Vector of V;

theorem :: VECTSP_2:30
  x*v = 0.V iff x = 0.F or v = 0.V;

theorem :: VECTSP_2:31
  x<>0.F implies x"*(x*v)=v;

reserve V for add-associative right_zeroed right_complementable RightMod-like
  non empty RightModStr over R;
reserve x for Scalar of R;
reserve v,w for Vector of V;

theorem :: VECTSP_2:32
  v*(0.R) = 0.V & v*(-1_R) = -v & (0.V)*x = 0.V;

theorem :: VECTSP_2:33
  -v*x = v*(-x) & w - v*x = w + v*(-x);

theorem :: VECTSP_2:34
  (-v)*x = -v*x;

theorem :: VECTSP_2:35
  (v - w)*x = v*x - w*x;

reserve F for non degenerated almost_left_invertible Ring;
reserve x for Scalar of F;
reserve V for add-associative right_zeroed right_complementable RightMod-like
  non empty RightModStr over F;
reserve v for Vector of V;

theorem :: VECTSP_2:36
  v*x = 0.V iff x = 0.F or v = 0.V;

theorem :: VECTSP_2:37
  x<>0.F implies (v*x)*x"=v;

registration
  cluster almost_left_invertible -> domRing-like for associative well-unital
add-associative right_zeroed right_complementable right-distributive non empty
    doubleLoopStr;
end;