:: Several Properties of Fields. Field Theory
::  by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies VECTSP_1, REALSET2, FUNCT_1, MESFUNC1, SUBSET_1, STRUCT_0,
      RELAT_1, ARYTM_1, ARYTM_3, SUPINF_2, ALGSTR_0, BINOP_1, ZFMISC_1,
      REALSET3;
 notations TARSKI, ZFMISC_1, SUBSET_1, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0,
      ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REALSET2;
 constructors BINOP_1, REALSET2, RELSET_1;
 registrations RELSET_1, STRUCT_0, REALSET2;
 requirements SUBSET, BOOLE;


begin

:: Properties of fields

theorem :: REALSET3:1
  for F being Field holds revf(F).1.F = 1.F;

theorem :: REALSET3:2
  for F being Field holds for a,b being Element of NonZero F holds
  revf(F).(omf(F).(a,revf(F).b)) = omf(F).(b,revf(F).a);

theorem :: REALSET3:3
  for F being Field, a,b being Element of NonZero F holds revf(F).(
  omf(F).(a,b)) = omf(F).(revf(F).a,revf(F).b);

theorem :: REALSET3:4
  for F being Field holds for a,b,c,d being Element
  of F holds a-b = c-d iff a+d = b+c;

theorem :: REALSET3:5
  for F being Field holds for a,c being Element of F
holds for b,d being Element of NonZero F holds omf(F).(a,revf(F).b) = omf(F).(c
  ,revf(F).d) iff omf(F).(a,d) = omf(F).(b,c);

theorem :: REALSET3:6
  for F being Field holds for a,b being Element of F
holds for c,d being Element of NonZero F holds omf(F).(omf(F).(a,revf(F).c),omf
  (F).(b,revf(F).d)) = omf(F).(omf(F).(a,b),revf(F).(omf(F).(c,d)));

theorem :: REALSET3:7
  for F being Field holds for a,b being Element of F
holds for c,d being Element of NonZero F holds (the addF of F).(omf(F).(a,revf(
F).c),omf(F).(b,revf(F).d)) = omf(F).((the addF of F).(omf(F).(a,d),omf(F).(b,c
  )),revf(F).(omf(F).(c,d)));

definition ::subtraction
  let F be Field;
  func osf(F) -> BinOp of the carrier of F means
:: REALSET3:def 1

  for x,y being Element of F holds it.(x,y) = (the addF of F).(x,(comp F).y);
end;

theorem :: REALSET3:8
  for F being Field holds for x being Element of F holds osf(F).(x,x) = 0.F;

theorem :: REALSET3:9
  for F being Field holds for a,b,c being Element
  of F holds omf(F).(a,osf(F).(b,c)) = osf(F).(omf(F).(a,b),omf(F).(a,c));

theorem :: REALSET3:10
  for F being Field holds for a,b,c being Element of F
  holds omf(F).(osf(F).(a,b),c) = osf(F).(omf(F).(a,c),omf(F).(b,c));

theorem :: REALSET3:11
  for F being Field holds for a,b being Element of F
  holds osf(F).(a,b) = (comp F).(osf(F).(b,a));

theorem :: REALSET3:12
  for F being Field holds for a,b being Element of F
  holds osf(F).((comp F).a,b) = (comp F).((the addF of F).(a,b));

theorem :: REALSET3:13
  for F being Field holds for a,b,c,d being Element
  of F holds osf(F).(a,b) = osf(F).(c,d) iff a+d = b+c;

theorem :: REALSET3:14
  for F being Field holds for a being Element of F holds
  osf(F).(0.F,a) = (comp F).a;

theorem :: REALSET3:15
  for F being Field holds for a being Element of F holds osf(F).(a,0.F) = a;

theorem :: REALSET3:16
  for F being Field holds for a,b,c being Element of F
  holds a+b = c iff osf(F).(c,a) = b;

theorem :: REALSET3:17
  for F being Field holds for a,b,c being Element of F
  holds a+b = c iff osf(F).(c,b) = a;

theorem :: REALSET3:18
  for F being Field holds for a,b,c being Element of F
  holds osf(F).(a,osf(F).(b,c)) = (the addF of F).(osf(F).(a,b),c);

theorem :: REALSET3:19
  for F being Field holds for a,b,c being Element of F
  holds osf(F).(a,(the addF of F).(b,c)) = osf(F).(osf(F).(a,b),c);

definition ::division.
  let F be Field;
  func ovf(F) -> Function of [:the carrier of F, NonZero F:],the carrier of F
  means
:: REALSET3:def 2

  for x being Element of F, y being Element of
  NonZero F holds it.(x,y) = omf(F).(x,revf(F).y);
end;

theorem :: REALSET3:20
  for F being Field holds for x being Element of NonZero F holds
  ovf(F).(x,x) = 1.F;

theorem :: REALSET3:21
  for F being Field holds for a,b being Element of
F holds for c being Element of NonZero F holds omf(F).(a,ovf(F).(b,c)) = ovf(F)
  .(omf(F).(a,b),c);

theorem :: REALSET3:22
  for F being Field holds for a being Element of NonZero F holds omf(F).
  (a,ovf(F).(1.F,a)) = 1.F & omf(F).(ovf(F).(1.F,a),a) = 1.F;

theorem :: REALSET3:23
  for F being Field holds for a,b being Element of NonZero F holds ovf(F
  ).(a,b) = revf(F).(ovf(F).(b,a));

theorem :: REALSET3:24
  for F being Field holds for a,b being Element of NonZero F holds ovf(F
  ).(revf(F).a,b) = revf(F).(omf(F).(a,b));

theorem :: REALSET3:25
  for F being Field holds for a,c being Element of
  F holds for b,d being Element of NonZero F holds ovf(F).(a,b) = ovf(F).(c,d)
  iff omf(F).(a,d) = omf(F).(b,c);

theorem :: REALSET3:26
  for F being Field holds for a being Element of NonZero F holds ovf(F).
  (1.F,a) = revf(F).a;

theorem :: REALSET3:27
  for F being Field holds for a being Element of F holds ovf(F).(a,1.F) = a;

theorem :: REALSET3:28
  for F being Field holds for a being Element of NonZero F holds for b,c
  being Element of F holds omf(F).(a,b) = c iff ovf(F).(c,a) = b;

theorem :: REALSET3:29
  for F being Field holds for a,c being Element of F
holds for b being Element of NonZero F holds omf(F).(a,b) = c iff ovf(F).(c,b)
  = a;

theorem :: REALSET3:30
  for F being Field holds for a being Element of F holds
for b,c being Element of NonZero F holds ovf(F).(a,ovf(F).(b,c)) = omf(F).(ovf(
  F).(a,b),c);

theorem :: REALSET3:31
  for F being Field holds for a being Element of F holds
for b,c being Element of NonZero F holds ovf(F).(a,omf(F).(b,c)) = ovf(F).(ovf(
  F).(a,b),c);