The abstract of the Mizar article:

Ternary Fields

by

Michal Muzalewski, and

Wojciech Skaba

Received October 15, 1990

MML identifier: ALGSTR_3

[ Mizar article, MML identifier index ]

environ

 vocabulary VECTSP_1, MULTOP_1, FUNCT_1, ARYTM_1, RLVECT_1, ARYTM_3, ALGSTR_3;
 notation XBOOLE_0, SUBSET_1, NUMBERS, STRUCT_0, RLVECT_1, REAL_1, MULTOP_1;
 constructors RLVECT_1, REAL_1, MULTOP_1, MEMBERED, XBOOLE_0;
 clusters STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, SUBSET, ARITHM;


begin

:: TERNARY FIELDS

:: This few lines define the basic algebraic structure (F, 0, 1, T)
:: used in the whole article.

definition
  struct(ZeroStr) TernaryFieldStr (# carrier -> set,
                      Zero, unity -> Element of the carrier,
                          ternary -> TriOp of the carrier #);
end;

definition
 cluster non empty TernaryFieldStr;
end;

reserve F for non empty TernaryFieldStr;

:: The following definitions let us simplify the notation

definition let F;
  mode Scalar of F is Element of F;
end;

reserve a,b,c for Scalar of F;

definition let F,a,b,c;
  func Tern(a,b,c) -> Scalar of F equals
:: ALGSTR_3:def 1
   (the ternary of F).(a,b,c);
end;

definition let F;
 canceled;
  func 1_ F -> Scalar of F equals
:: ALGSTR_3:def 3
   the unity of F;
end;

:: The following definition specifies a ternary operation that
:: will be used in the forthcoming example: TernaryFieldEx
:: as its TriOp function.

definition
  func ternaryreal -> TriOp of REAL means
:: ALGSTR_3:def 4
  for a,b,c being Real holds it.(a,b,c) = a*b + c;
end;

:: Now comes the definition of example structure called: TernaryFieldEx.
:: This example will be used to prove the existence of the Ternary-Field mode.

definition
  func TernaryFieldEx -> strict TernaryFieldStr equals
:: ALGSTR_3:def 5
   TernaryFieldStr (# REAL, 0, 1, ternaryreal #);
end;

definition
 cluster TernaryFieldEx -> non empty;
end;

:: On the contrary to the Tern() (starting with uppercase), this definition
:: allows for the use of the currently specified example ternary field.

definition
  let a,b,c be Scalar of TernaryFieldEx;
  func tern(a,b,c) -> Scalar of TernaryFieldEx equals
:: ALGSTR_3:def 6
     (the ternary of TernaryFieldEx).(a,b,c);
end;

canceled 2;

theorem :: ALGSTR_3:3
 for u,u',v,v' being Real holds
  u <> u' implies ex x being Real st u*x+v = u'*x+v';

canceled;

theorem :: ALGSTR_3:5
 for u,a,v being Scalar of TernaryFieldEx
        for z,x,y being Real holds
           u=z & a=x & v=y implies Tern(u,a,v) = z*x + y;

theorem :: ALGSTR_3:6
 0 = 0.TernaryFieldEx;

:: The 1 defined in TeranaryFieldEx structure is equal to
:: the ordinary 1 of real numbers.

theorem :: ALGSTR_3:7
 1 = 1_ TernaryFieldEx;

definition let IT be non empty TernaryFieldStr;
  attr IT is Ternary-Field-like means
:: ALGSTR_3:def 7
    (0.IT <> 1_ IT)
  & (for a        being Scalar of IT holds Tern(a, 1_ IT, 0.IT) = a)
  & (for a        being Scalar of IT holds Tern(1_ IT, a, 0.IT) = a)
  & (for a,b      being Scalar of IT holds Tern(a, 0.IT, b ) = b)
  & (for a,b      being Scalar of IT holds Tern(0.IT, a, b ) = b)
  & (for u,a,b    being Scalar of IT ex v being Scalar of IT st
     Tern(u,a,v) = b)
  & (for u,a,v,v' being Scalar of IT holds Tern(u,a,v) = Tern(u,a,v')
     implies v = v')
  & (for a,a'     being Scalar of IT holds
     a <> a' implies
       for b,b' being Scalar of IT
         ex u,v being Scalar of IT st
                Tern(u,a,v) = b & Tern(u,a',v) = b')
  & (for u,u'     being Scalar of IT holds
     u <> u' implies
       for v,v' being Scalar of IT
           ex a being Scalar of IT st
                Tern(u,a,v) = Tern(u',a,v'))
  & (for a,a',u,u',v,v' being Scalar of IT holds
     Tern(u,a,v) = Tern(u',a,v') & Tern(u,a',v) = Tern(u',a',v')
     implies a = a' or u = u');
end;

definition
 cluster strict Ternary-Field-like (non empty TernaryFieldStr);
end;

definition
  mode Ternary-Field is Ternary-Field-like (non empty TernaryFieldStr);
end;

reserve F for Ternary-Field;
reserve a,a',b,c,x,x',u,u',v,v',z for Scalar of F;

theorem :: ALGSTR_3:8
    a<>a' & Tern(u,a,v) = Tern(u',a,v')
        & Tern(u,a',v) = Tern(u',a',v')
  implies u=u' & v=v';

canceled 2;

theorem :: ALGSTR_3:11
      a<>0.F implies for b,c ex x st Tern(a,x,b) = c;

theorem :: ALGSTR_3:12
      a<>0.F & Tern(a,x,b) = Tern(a,x',b) implies x=x';

theorem :: ALGSTR_3:13
      a<>0.F implies for b,c ex x st Tern(x,a,b) = c;

theorem :: ALGSTR_3:14
      a<>0.F & Tern(x,a,b) = Tern(x',a,b) implies x=x';