The abstract of the Mizar article:

Groups, Rings, Left- and Right-Modules

by

Michal Muzalewski, and

Wojciech Skaba

Received October 22, 1990

MML identifier: MOD_1

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, VECTSP_1, ARYTM_1, FUNCSDOM, VECTSP_2, RELAT_1, MOD_1,
      BINOP_1, LATTICES, ALGSTR_2;
 notation STRUCT_0, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2;
 constructors VECTSP_2, XBOOLE_0;
 clusters VECTSP_1, VECTSP_2, ZFMISC_1, XBOOLE_0;


begin

definition
  mode AddGroup is add-associative right_zeroed right_complementable
                        (non empty LoopStr);
end;

canceled 12;

theorem :: MOD_1:13
  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 :: MOD_1:14
  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 left_unital right_unital distributive
      (non empty doubleLoopStr),
         F for non degenerated Field-like Ring,
         x for Scalar of F,
         V for add-associative right_zeroed right_complementable
               VectSp-like (non empty VectSpStr over F),
         v for Vector of V;

canceled 10;

theorem :: MOD_1:25
   x*v = 0.V iff x = 0.F or v = 0.V;

theorem :: MOD_1:26
   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;

canceled 10;

theorem :: MOD_1:37
  v*(0.R) = 0.V & v*(-1_ R) = -v & (0.V)*x = 0.V;

theorem :: MOD_1:38
  -v*x = v*(-x) & w - v*x = w + v*(-x);

theorem :: MOD_1:39
  (-v)*x = -v*x;

theorem :: MOD_1:40
  (v - w)*x = v*x - w*x;

 reserve F for non degenerated Field-like 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;

canceled;

theorem :: MOD_1:42
  v*x = 0.V iff x = 0.F or v = 0.V;

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