The abstract of the Mizar article:

From Double Loops to Fields

by

Wojciech Skaba, and

Michal Muzalewski

Received September 27, 1990

MML identifier: ALGSTR_2

[ Mizar article, MML identifier index ]

environ

 vocabulary VECTSP_1, FUNCT_1, RLVECT_1, ALGSTR_1, VECTSP_2, ARYTM_1, LATTICES,
      BINOP_1, ALGSTR_2;
 notation REAL_1, BINOP_1, STRUCT_0, RLVECT_1, VECTSP_1, VECTSP_2, ALGSTR_1;
 constructors BINOP_1, ALGSTR_1, VECTSP_2, REAL_1, MEMBERED, XBOOLE_0;
 clusters VECTSP_1, ALGSTR_1, VECTSP_2, MEMBERED, ZFMISC_1, XBOOLE_0;


begin :: DOUBLE LOOPS

 reserve L for non empty doubleLoopStr;

:: Below is the basic definition of the mode of DOUBLE LOOP.
:: The F_Real example in accordance with the many theorems proved above
:: is used to prove the existence.

definition
  cluster F_Real -> multLoop_0-like;
end;

:: In the following part of this article the negation and minus functions
:: are defined. This is the only definition of both functions in this article
:: while some of their features are independently proved
:: for various structures.

definition
  let L be add-left-cancelable add-right-invertible (non empty LoopStr);
  let a be Element of L;
 canceled 6;

  func -a -> Element of L means
:: ALGSTR_2:def 7
    a+it = 0.L;
end;

definition
  let L be add-left-cancelable add-right-invertible (non empty LoopStr);
  let a,b be Element of L;
  func a-b -> Element of L equals
:: ALGSTR_2:def 8
    a+ -b;
end;

definition
 cluster strict Abelian add-associative commutative associative distributive
   non degenerated left_zeroed right_zeroed Loop-like well-unital
    multLoop_0-like (non empty doubleLoopStr);
end;

definition
  mode doubleLoop is left_zeroed right_zeroed Loop-like
     well-unital multLoop_0-like (non empty doubleLoopStr);
end;

definition
  mode leftQuasi-Field is Abelian add-associative
    right-distributive non degenerated doubleLoop;
end;

 reserve a,b,c,x,y,z for Element of L;

:: The following theorem shows that the basic set of axioms of the
:: left quasi-field may be replaced with the following one,
:: by just removing a few and adding some other axioms.

canceled 11;

theorem :: ALGSTR_2:12
     L is leftQuasi-Field iff
     (for a holds a + 0.L = a)
   & (for a ex x st a+x = 0.L)
   & (for a,b,c holds (a+b)+c = a+(b+c))
   & (for a,b holds a+b = b+a)
   & 0.L <> 1_ L
   & (for a holds a * 1_ L = a)
   & (for a holds 1_ L * a = a)
   & (for a,b st a<>0.L ex x st a*x=b)
   & (for a,b st a<>0.L ex x st x*a=b)
   & (for a,x,y st a<>0.L holds a*x=a*y implies x=y)
   & (for a,x,y st a<>0.L holds x*a=y*a implies x=y)
   & (for a holds a*0.L = 0.L)
   & (for a holds 0.L*a = 0.L)
   & (for a,b,c holds a*(b+c) = a*b + a*c);

canceled;

theorem :: ALGSTR_2:14
  for G being Abelian right-distributive doubleLoop,
      a,b being Element of G holds a*(-b) = -(a*b);

theorem :: ALGSTR_2:15
  for G being Abelian add-left-cancelable add-right-invertible
          (non empty LoopStr),
      a being Element of G holds -(-a) = a;

theorem :: ALGSTR_2:16
    for G being Abelian right-distributive doubleLoop holds
   (-1_ G)*(-1_ G) = 1_ G;

theorem :: ALGSTR_2:17
    for G being Abelian right-distributive doubleLoop,
      a,x,y being Element of G holds
  a*(x-y) = a*x - a*y;

:: RIGHT QUASI-FIELD

:: The next contemplated algebraic structure is so called right quasi-field.
:: This structure is defined as a DOUBLE LOOP augmented with three axioms.
:: The reasoning is similar to that of left quasi-field.

definition
  mode rightQuasi-Field is Abelian add-associative left-distributive
       non degenerated doubleLoop;
end;

canceled;

theorem :: ALGSTR_2:19
     L is rightQuasi-Field iff
     (for a holds a + 0.L = a)
   & (for a ex x st a+x = 0.L)
   & (for a,b,c holds (a+b)+c = a+(b+c))
   & (for a,b holds a+b = b+a)
   & 0.L <> 1_ L
   & (for a holds a * 1_ L = a)
   & (for a holds 1_ L * a = a)
   & (for a,b st a<>0.L ex x st a*x=b)
   & (for a,b st a<>0.L ex x st x*a=b)
   & (for a,x,y st a<>0.L holds a*x=a*y implies x=y)
   & (for a,x,y st a<>0.L holds x*a=y*a implies x=y)
   & (for a holds a*0.L = 0.L)
   & (for a holds 0.L*a = 0.L)
   & (for a,b,c holds (b+c)*a = b*a + c*a);

:: Below, the three features concerned with the - function,
:: numbered 20..22 are proved. Where necessary, a few additional
:: facts are included. They are independent of the similar proofs
:: performed for the left quasi-field.

 reserve G for left-distributive doubleLoop,
         a,b,x,y for Element of G;

canceled;

theorem :: ALGSTR_2:21
   (-b)*a = -(b*a);

canceled;

theorem :: ALGSTR_2:23
    for G being Abelian left-distributive doubleLoop holds
    (-1_ G)*(-1_ G) = 1_ G;

theorem :: ALGSTR_2:24
     (x-y)*a = x*a - y*a;

:: DOUBLE SIDED QUASI-FIELD

:: The next contemplated algebraic structure is so called double sided
:: quasi-field. This structure is also defined as a DOUBLE LOOP augmented
:: with four axioms, while its relevance to left/right quasi-field is
:: independently contemplated.
:: The reasoning is similar to that of left/right quasi-field.

definition
  mode doublesidedQuasi-Field is Abelian add-associative distributive
     non degenerated doubleLoop;
end;

 reserve a,b,c,x,y,z for Element of L;

canceled;

theorem :: ALGSTR_2:26
     L is doublesidedQuasi-Field iff
     (for a holds a + 0.L = a)
   & (for a ex x st a+x = 0.L)
   & (for a,b,c holds (a+b)+c = a+(b+c))
   & (for a,b holds a+b = b+a)
   & 0.L <> 1_ L
   & (for a holds a * 1_ L = a)
   & (for a holds 1_ L * a = a)
   & (for a,b st a<>0.L ex x st a*x=b)
   & (for a,b st a<>0.L ex x st x*a=b)
   & (for a,x,y st a<>0.L holds a*x=a*y implies x=y)
   & (for a,x,y st a<>0.L holds x*a=y*a implies x=y)
   & (for a holds a*0.L = 0.L)
   & (for a holds 0.L*a = 0.L)
   & (for a,b,c holds a*(b+c) = a*b + a*c)
   & (for a,b,c holds (b+c)*a = b*a + c*a);

:: SKEW FIELD
:: A Skew-Field is defined as a double sided quasi-field extended
:: with the associativity of multiplication.

definition
  mode _Skew-Field is associative doublesidedQuasi-Field;
end;

:: The following theorem shows that the basic set of axioms of the
:: skew field may be replaced with the following one,
:: by just removing a few and adding some other axioms.
:: A few theorems proved earlier are highly utilized.

canceled 5;

theorem :: ALGSTR_2:32
   L is _Skew-Field iff
     (for a holds a + 0.L = a)
   & (for a ex x st a+x = 0.L)
   & (for a,b,c holds (a+b)+c = a+(b+c))
   & (for a,b holds a+b = b+a)
   & 0.L <> 1_ L
   & (for a holds a * 1_ L = a)
   & (for a st a<>0.L ex x st a*x = 1_ L)
   & (for a holds a*0.L = 0.L)
   & (for a holds 0.L*a = 0.L)
   & (for a,b,c holds (a*b)*c = a*(b*c))
   & (for a,b,c holds a*(b+c) = a*b + a*c)
   & (for a,b,c holds (b+c)*a = b*a + c*a);

:: FIELD

:: A _Field is defined as a Skew-Field with the axiom of the commutativity
:: of multiplication.

definition
  mode _Field is commutative _Skew-Field;
end;

canceled;

theorem :: ALGSTR_2:34
     L is _Field iff
     (for a holds a + 0.L = a)
   & (for a ex x st a+x = 0.L)
   & (for a,b,c holds (a+b)+c = a+(b+c))
   & (for a,b holds a+b = b+a)
   & 0.L <> 1_ L
   & (for a holds a * 1_ L = a)
   & (for a st a<>0.L ex x st a*x = 1_ L)
   & (for a holds a*0.L = 0.L)
   & (for a,b,c holds (a*b)*c = a*(b*c))
   & (for a,b,c holds a*(b+c) = a*b + a*c)
   & (for a,b holds a*b = b*a);