The abstract of the Mizar article:

Rings and Modules --- Part II

by

Michal Muzalewski

Received October 18, 1991

MML identifier: MOD_2

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCSDOM, VECTSP_1, CLASSES2, GRCAT_1, RLVECT_1, BOOLE, MIDSP_1,
      VECTSP_2, FUNCT_3, FUNCT_1, PRE_TOPC, INCSP_1, ORDINAL4, CAT_1, RELAT_1,
      ARYTM_3, ORDINAL1, ARYTM_1, BINOP_1, LATTICES, FUNCT_2, MOD_2, ALGSTR_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, BINOP_1, FUNCT_2,
      STRUCT_0, ORDINAL1, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2, CLASSES2,
      PRE_TOPC, ALGSTR_1, MIDSP_1, GRCAT_1, FUNCT_3;
 constructors ENUMSET1, BINOP_1, VECTSP_2, GRCAT_1, TOPS_2, ALGSTR_1, MIDSP_1,
      MEMBERED, PARTFUN1, XBOOLE_0;
 clusters VECTSP_1, STRUCT_0, RELSET_1, SUBSET_1, ALGSTR_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

reserve x,y,z for set;
reserve D,D' for non empty set;
reserve R for Ring;
reserve G,H,S for non empty VectSpStr over R;


reserve UN for Universe;

definition let R;
 canceled;

 func TrivialLMod(R) -> strict LeftMod of R equals
:: MOD_2:def 2
   VectSpStr (#{{}},op2,op0,pr2(the carrier of R,{{}})#);
end;

theorem :: MOD_2:1
  for x being Vector of TrivialLMod(R) holds x = 0.TrivialLMod(R);

definition let R be non empty doubleLoopStr;
  let G,H be non empty VectSpStr over R; let f be map of G,H;
 canceled 2;

 attr f is linear means
:: MOD_2:def 5
  (for x,y being Vector of G holds f.(x+y) = f.x+f.y)
        & for a being Scalar of R, x being Vector of G holds f.(a*x) = a*f.x;
end;

canceled 2;

theorem :: MOD_2:4
 for f being map of G,H st f is linear holds f is additive;

canceled;

theorem :: MOD_2:6
 for f being map of G,H, g being map of H,S
      st f is linear & g is linear holds g*f is linear;

reserve R for Ring;
reserve G, H for LeftMod of R;

canceled;

theorem :: MOD_2:8
 ZeroMap(G,H) is linear;

                      ::
                      ::  Morphisms of Left Modules
                      ::

 reserve G1, G2, G3 for LeftMod of R;

definition let R;
  struct LModMorphismStr over R (# Dom,Cod -> LeftMod of R,
                                Fun -> map of the Dom, the Cod #);
end;

reserve f for LModMorphismStr over R;

definition let R,f;
 func dom(f) -> LeftMod of R equals
:: MOD_2:def 6
   the Dom of f;
 func cod(f) -> LeftMod of R equals
:: MOD_2:def 7
   the Cod of f;
end;

definition let R,f;
 func fun(f) -> map of dom(f),cod(f) equals
:: MOD_2:def 8
   the Fun of f;
end;

theorem :: MOD_2:9
  for f0 being map of G1,G2 st f = LModMorphismStr(#G1,G2,f0#)
      holds dom f = G1 & cod f = G2 & fun f = f0;

definition let R,G,H;
 func ZERO(G,H) -> strict LModMorphismStr over R equals
:: MOD_2:def 9
   LModMorphismStr(# G,H,ZeroMap(G,H)#);
end;

definition let R;
 let IT be LModMorphismStr over R;
 attr IT is LModMorphism-like means
:: MOD_2:def 10
  fun(IT) is linear;
end;

definition let R;
 cluster strict LModMorphism-like LModMorphismStr over R;
end;

definition let R;
 mode LModMorphism of R is LModMorphism-like LModMorphismStr over R;
end;

theorem :: MOD_2:10
 for F being LModMorphism of R holds the Fun of F is linear;

definition let R,G,H;
 cluster ZERO(G,H) -> LModMorphism-like;
end;

definition let R,G,H;
 mode Morphism of G,H -> LModMorphism of R means
:: MOD_2:def 11
  dom(it) = G & cod(it) = H;
end;

definition let R,G,H;
 cluster strict Morphism of G,H;
end;

theorem :: MOD_2:11
 for f being LModMorphismStr over R holds
   dom(f) = G & cod(f) = H & fun(f) is linear implies f is Morphism of G,H;

theorem :: MOD_2:12
 for f being map of G,H st f is linear
       holds LModMorphismStr (#G,H,f#) is strict Morphism of G,H;

theorem :: MOD_2:13
 id G is linear;

definition let R,G;
 func ID G -> strict Morphism of G,G equals
:: MOD_2:def 12
   LModMorphismStr(# G,G,id G#);
end;

definition let R,G,H;
 redefine func ZERO(G,H) -> strict Morphism of G,H;
end;

theorem :: MOD_2:14
 for F being Morphism of G,H ex f being map of G,H
       st the LModMorphismStr of F = LModMorphismStr(#G,H,f#) & f is linear;

theorem :: MOD_2:15
 for F being strict Morphism of G,H ex f being map of G,H
       st F = LModMorphismStr(#G,H,f#);

theorem :: MOD_2:16
 for F being LModMorphism of R ex G,H st F is Morphism of G,H;

theorem :: MOD_2:17
  for F being strict LModMorphism of R
 ex G,H being LeftMod of R, f being map of G,H
       st F is strict Morphism of G,H
        & F = LModMorphismStr(#G,H,f#)
        & f is linear;

theorem :: MOD_2:18
 for g,f being LModMorphism of R st dom(g) = cod(f)
       ex G1,G2,G3 st g is Morphism of G2,G3 &
                      f is Morphism of G1,G2;

definition let R; let G,F be LModMorphism of R;
 assume  dom(G) = cod(F);
 func G*F -> strict LModMorphism of R means
:: MOD_2:def 13
  for G1,G2,G3 being LeftMod of R,
           g being map of G2,G3, f being map of G1,G2
       st the LModMorphismStr of G = LModMorphismStr(#G2,G3,g#) &
          the LModMorphismStr of F = LModMorphismStr(#G1,G2,f#)
       holds it = LModMorphismStr(#G1,G3,g*f#);
end;

canceled;

theorem :: MOD_2:20
 for G being Morphism of G2,G3,
          F being Morphism of G1,G2
      holds G*F is strict Morphism of G1,G3;

definition let R,G1,G2,G3;
           let G be Morphism of G2,G3;
           let F be Morphism of G1,G2;
 func G*'F -> strict Morphism of G1,G3 equals
:: MOD_2:def 14
   G*F;
end;

theorem :: MOD_2:21
 for G being Morphism of G2,G3,
          F being Morphism of G1,G2,
          g being map of G2,G3, f being map of G1,G2
      st G = LModMorphismStr(#G2,G3,g#) & F = LModMorphismStr(#G1,G2,f#)
      holds G*'F = LModMorphismStr(#G1,G3,g*f#) & G*F = LModMorphismStr(#
G1,G3,g*f#);

 theorem :: MOD_2:22
  for f,g being strict LModMorphism of R st dom g = cod f holds
       ex G1,G2,G3 being LeftMod of R,
          f0 being map of G1,G2, g0 being map of G2,G3
          st f = LModMorphismStr(#G1,G2,f0#)
           & g = LModMorphismStr(#G2,G3,g0#)
           & g*f = LModMorphismStr(#G1,G3,g0*f0#);

 theorem :: MOD_2:23
  for f,g being strict LModMorphism of R st dom g = cod f holds
     dom(g*f) = dom f
   & cod (g*f) = cod g;

 theorem :: MOD_2:24
  for G1,G2,G3,G4 being LeftMod of R,
             f being strict Morphism of G1,G2,
             g being strict Morphism of G2,G3,
             h being strict Morphism of G3,G4
         holds h*(g*f) = (h*g)*f;

 theorem :: MOD_2:25
  for f,g,h being strict LModMorphism of R st dom h = cod g & dom g = cod f
        holds h*(g*f) = (h*g)*f;

 theorem :: MOD_2:26
     dom ID(G) = G & cod ID(G) = G
& (for f being strict LModMorphism of R st cod f = G holds (ID G)*f = f)
& (for g being strict LModMorphism of R st dom g = G holds g*(ID G) = g);

definition let x,y,z;
 cluster {x,y,z} -> non empty;
end;

canceled;

theorem :: MOD_2:28
 for u,v,w being Element of UN holds {u,v,w} is Element of UN;

theorem :: MOD_2:29
 for u being Element of UN holds succ u is Element of UN;

theorem :: MOD_2:30
 0 is Element of UN & 1 is Element of UN & 2 is Element of UN;

reserve a,b,c for Element of {0,1,2};

definition let a;
 func -a -> Element of {0,1,2} equals
:: MOD_2:def 15
    0 if a = 0,
             2 if a = 1,
             1 if a = 2;
           let b;
 func a+b -> Element of {0,1,2} equals
:: MOD_2:def 16
    b if a = 0,
           a if b = 0,
           2 if a = 1 & b = 1,
           0 if a = 1 & b = 2,
           0 if a = 2 & b = 1,
           1 if a = 2 & b = 2;
 func a*b -> Element of {0,1,2} equals
:: MOD_2:def 17
    0 if b = 0,
           0 if a = 0,
           a if b = 1,
           b if a = 1,
           1 if a = 2 & b = 2;
end;

definition
 func add3 -> BinOp of {0,1,2} means
:: MOD_2:def 18
   it.(a,b) = a+b;
 func mult3 -> BinOp of {0,1,2} means
:: MOD_2:def 19
   it.(a,b) = a*b;
 func compl3 -> UnOp of {0,1,2} means
:: MOD_2:def 20
   it.a = -a;
 func unit3 -> Element of {0,1,2} equals
:: MOD_2:def 21
   1;
 func zero3 -> Element of {0,1,2} equals
:: MOD_2:def 22
    0;
end;

definition
 func Z3 -> strict doubleLoopStr equals
:: MOD_2:def 23
   doubleLoopStr (#{0,1,2},add3,mult3,unit3,zero3#);
end;

definition
 cluster Z3 -> non empty;
end;

canceled;

theorem :: MOD_2:32
 0.Z3 = 0
  & 1_ Z3 = 1
  & 0.Z3 is Element of {0,1,2}
  & 1_ Z3 is Element of {0,1,2}
  & the add of Z3 = add3
  & the mult of Z3 = mult3;

definition
 cluster Z3 -> add-associative right_zeroed right_complementable;
end;

theorem :: MOD_2:33
 for x,y being Scalar of Z3, X,Y being Element of {0,1,2}
     st X=x & Y=y holds
        x+y = X+Y
      & x*y = X*Y
      & -x = -X;

theorem :: MOD_2:34
 for x,y,z being Scalar of Z3, X,Y,Z being Element of {0,1,2}
     st X=x & Y=y & Z=z holds
        (x+y)+z = (X+Y)+Z
      & x+(y+z) = X+(Y+Z)
      & (x*y)*z = (X*Y)*Z
      & x*(y*z) = X*(Y*Z);

theorem :: MOD_2:35
 for x,y,z,a,b being Element of {0,1,2} st a = 0 & b = 1 holds
            x+y = y+x &
            (x+y)+z = x+(y+z) &
            x+a = x &
            x+(-x) = a &
            x*y = y*x &
            (x*y)*z = x*(y*z) &
            b*x = x &
            (x<>a implies ex y be Element of {0,1,2} st x*y = b) &
            a <> b & x*(y+z) = x*y+x*z;

theorem :: MOD_2:36
 for F being non empty doubleLoopStr st for x,y,z being Scalar of F holds
            x+y = y+x &
            (x+y)+z = x+(y+z) &
            x+(0.F) = x &
            x+(-x) = (0.F) &
            x*y = y*x &
            (x*y)*z = x*(y*z) &
            1_ F*x = x &
            (x<>(0.F) implies ex y be Scalar of F st x*y = 1_ F) &
            0.F <> 1_ F &
            x*(y+z) = x*y+x*z holds F is Field;

theorem :: MOD_2:37
 Z3 is Fanoian Field;

definition
 cluster Z3 -> Fanoian add-associative right_zeroed right_complementable
    Abelian commutative associative left_unital distributive Field-like;
end;

theorem :: MOD_2:38
for f being Function of D,D' st D in UN & D' in UN holds f in UN;

canceled;

theorem :: MOD_2:40
    the carrier of Z3 in UN & the add of Z3 is Element of UN &
  comp Z3 is Element of UN & the Zero of Z3 is Element of UN &
  the mult of Z3 is Element of UN & the unity of Z3 is Element of UN;