Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Groups, Rings, Left- and Right-Modules

by
Michal Muzalewski, and
Wojciech Skaba

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
(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,
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;

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;
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;

```