The abstract of the Mizar article:

Group and Field Definitions

by

Jozef Bialas

Received October 27, 1989

MML identifier: REALSET1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, BOOLE, BINOP_1, RLVECT_1, VECTSP_1, FUNCT_3,
      QC_LANG1, REALSET1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
      BINOP_1, FUNCT_3, STRUCT_0, RLVECT_1, VECTSP_1;
 constructors BINOP_1, FUNCT_3, VECTSP_1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, RLVECT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

canceled 9;

theorem :: REALSET1:10
   for X,x being set holds
   for F being Function of [:X,X:],X holds
   x in [:X,X:] implies F.x in X;

theorem :: REALSET1:11
   for X being set,
       F being BinOp of X
   ex A being Subset of X st
   for x being set holds x in [:A,A:] implies F.x in A;

definition
   let X be set;
   let F be BinOp of X;
   let A be Subset of X;
   pred F is_in A means
:: REALSET1:def 1
     for x being set holds x in [:A,A:] implies F.x in A;
end;

definition
   let X be set;
   let F be BinOp of X;
   mode Preserv of F -> Subset of X means
:: REALSET1:def 2
for x being set holds x in [:it,it:] implies F.x in it;
end;

canceled 2;

theorem :: REALSET1:14
   for X being set,
       F being BinOp of X,
       A being Preserv of F holds F|([:A,A:]) is BinOp of A;

definition
   let X be set;
   let F be BinOp of X;
   let A be Preserv of F;
   func F||A -> BinOp of A equals
:: REALSET1:def 3
   F | [:A,A:];
end;

definition ::group
  let IT be LoopStr;
 canceled;

  attr IT is zeroed means
:: REALSET1:def 5
                 for a being Element of IT holds
                      (the add of IT).[a,the Zero of IT] = a &
                      (the add of IT).[the Zero of IT,a] = a;
  attr IT is complementable means
:: REALSET1:def 6
                 for a being Element of IT
                  ex b being Element of IT st
                      (the add of IT).[a,b] = the Zero of IT &
                      (the add of IT).[b,a] = the Zero of IT;
end;

definition let L be non empty LoopStr;
 redefine attr L is add-associative means
:: REALSET1:def 7
        for a,b,c being Element of L holds
                      (the add of L).[(the add of L).[a,b],c] =
                       (the add of L).[a,(the add of L).[b,c]];
  redefine attr L is Abelian means
:: REALSET1:def 8

     for a,b being Element of L holds
        (the add of L).[a,b] = (the add of L).[b,a];
end;

definition let X be non empty set, a be BinOp of X, Z be Element of X;
 cluster LoopStr(#X,a,Z#) -> non empty;
end;

definition
 cluster strict Abelian add-associative zeroed
                        complementable (non empty LoopStr);
end;

definition ::group
   mode Group is Abelian add-associative zeroed complementable
    (non empty LoopStr);
end;

definition
 let IT be set;
 canceled 3;

 attr IT is trivial means
:: REALSET1:def 12
  IT is empty or ex x being set st IT = {x};
end;

definition
 cluster trivial non empty set;
 cluster non trivial non empty set;
 cluster non trivial -> non empty set;
end;

canceled 17;

theorem :: REALSET1:32
  for X being non empty set holds
   X is non trivial iff for x being set holds X\{x} is non empty set;

theorem :: REALSET1:33
  ex A being non empty set st for z being Element of A holds
A \ {z} is non empty set;

theorem :: REALSET1:34
  for X being non empty set
   st for x being Element of X holds X\{x} is non empty set
  holds X is non trivial;

definition
  let IT be 1-sorted;
  attr IT is trivial means
:: REALSET1:def 13
    the carrier of IT is trivial;
end;

definition
 cluster trivial 1-sorted;
end;

theorem :: REALSET1:35
      for A being non empty set st
    (for x being Element of A holds A\{x} is non empty set) holds
    A is non trivial set;

definition
 cluster non trivial strict doubleLoopStr;
end;

definition ::field operator
   let A be non trivial set;
   let od,om be BinOp of A;
   let nd be Element of A;
   let nm be Element of A\{nd};
   func field(A,od,om,nd,nm) -> non trivial strict doubleLoopStr means
:: REALSET1:def 14
   A = the carrier of it &
        od = the add of it &
        om = the mult of it &
        nd = the Zero of it &
        nm = the unity of it;
end;

definition
   let X be non trivial set;
   let F be BinOp of X;
   let x be Element of X;
   pred F is_Bin_Op_Preserv x means
:: REALSET1:def 15
       (X\{x} is Preserv of F) &
          F|[:X\{x},X\{x}:] is BinOp of X\{x};
end;

canceled 3;

theorem :: REALSET1:39
    for X being set holds
    for A being Subset of X holds
    ex F being BinOp of X st
    for x being set holds x in [:A,A:] implies F.x in A;

definition
    let X be set;
    let A be Subset of X;
    mode Presv of X,A -> BinOp of X means
:: REALSET1:def 16
for x being set holds x in [:A,A:] implies it.x in A;
end;

canceled;

theorem :: REALSET1:41
   for X being set,
       A being Subset of X,
       F being Presv of X,A holds
   F|([:A,A:]) is BinOp of A;

definition
   let X be set;
   let A be Subset of X;
   let F be Presv of X,A;
   func F|||A -> BinOp of A equals
:: REALSET1:def 17
    F | [:A,A:];
end;

canceled;

theorem :: REALSET1:43
    for A being non trivial set holds
    for x being Element of A holds
    ex F being BinOp of A st
    for y being set holds y in [:A\{x},A\{x}:] implies F.y in A\{x};

definition
    let A be non trivial set;
    let x be Element of A;
    mode DnT of x,A -> BinOp of A means
:: REALSET1:def 18
 for y being set holds y in [:A\{x},A\{x}:] implies it.y in A\{x};
end;

canceled;

theorem :: REALSET1:45
   for A being non trivial set holds
   for x being Element of A holds
   for F being DnT of x,A holds
   F|[:A\{x},A\{x}:] is BinOp of A\{x};

definition
   let A be non trivial set;
   let x be Element of A;
   let F be DnT of x,A;
func F!(A,x) -> BinOp of A\{x} equals
:: REALSET1:def 19
   F | [:A\{x},A\{x}:];
end;

definition
 let IT be 1-sorted;
 redefine attr IT is trivial means
:: REALSET1:def 20
    for x,y being Element of IT holds x = y;
end;