The abstract of the Mizar article:

The Field of Quotients Over an Integral Domain

by

Christoph Schwarzweller

Received May 4, 1998

MML identifier: QUOFIELD

[ Mizar article, MML identifier index ]

environ

 vocabulary RLVECT_1, VECTSP_1, MCART_1, VECTSP_2, BINOP_1, LATTICES, SETFAM_1,
      FUNCSDOM, ARYTM_3, BOOLE, ARYTM_1, FUNCT_1, RELAT_1, PRE_TOPC, GRCAT_1,
      COHSP_1, ENDALG, SUBSET_1, QUOFIELD;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MCART_1, FUNCT_1,
      FUNCT_2, SETFAM_1, DOMAIN_1, STRUCT_0, RLVECT_1, VECTSP_2, VECTSP_1,
      BINOP_1, PRE_TOPC, TOPS_2, FUNCSDOM, GRCAT_1, ENDALG, GCD_1;
 constructors DOMAIN_1, BINOP_1, GCD_1, TOPS_2, GRCAT_1, ENDALG, ALGSTR_2;
 clusters STRUCT_0, RELSET_1, SUBSET_1, GCD_1, ALGSTR_1, VECTSP_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

::: Definition of Pairs

definition
let I be non empty ZeroStr;
func Q.I -> Subset of [:the carrier of I,the carrier of I:] means
:: QUOFIELD:def 1
 for u being set holds
 u in it iff ex a,b being Element of I st
            (u = [a,b] & b <> 0.I);
end;

theorem :: QUOFIELD:1
for I being non degenerated non empty multLoopStr_0 holds Q.I is non empty;

definition let I be non degenerated non empty multLoopStr_0;
  cluster Q.I -> non empty;
end;

theorem :: QUOFIELD:2
for I being non degenerated non empty multLoopStr_0
for u being Element of Q.I holds u`2 <> 0.I;

definition
let I be non degenerated non empty multLoopStr_0;
let u be Element of Q.I;
 redefine func u`1 -> Element of I;
 redefine func u`2 -> Element of I;
end;

::: Definition and some Properties of Pair Addition and Multiplication

definition
let I be non degenerated domRing-like (non empty doubleLoopStr);
let u,v be Element of Q.I;
func padd(u,v) -> Element of Q.I equals
:: QUOFIELD:def 2
  [u`1 * v`2 + v`1 * u`2, u`2 * v`2];
end;

definition
let I be non degenerated domRing-like (non empty doubleLoopStr);
let u,v be Element of Q.I;
func pmult(u,v) -> Element of Q.I equals
:: QUOFIELD:def 3
  [u`1 * v`1, u`2 * v`2];
end;

canceled;

theorem :: QUOFIELD:4
for I being non degenerated domRing-like associative commutative
   Abelian add-associative distributive (non empty doubleLoopStr)
for u,v,w being Element of Q.I holds
padd(u,padd(v,w)) = padd(padd(u,v),w) & padd(u,v) = padd(v,u);

theorem :: QUOFIELD:5
for I being non degenerated domRing-like associative commutative
   Abelian (non empty doubleLoopStr)
for u,v,w being Element of Q.I holds
pmult(u,pmult(v,w)) = pmult(pmult(u,v),w) & pmult(u,v) = pmult(v,u);

definition let I be non degenerated domRing-like associative commutative
             Abelian add-associative distributive (non empty doubleLoopStr);
           let u, v be Element of Q.I;
  redefine func padd(u,v);
  commutativity;
end;

definition let I be non degenerated domRing-like associative commutative
             Abelian (non empty doubleLoopStr);
           let u, v be Element of Q.I;
  redefine func pmult(u,v);
  commutativity;
end;

::: Definition of Classes of Pairs

definition
let I be non degenerated non empty multLoopStr_0;
let u be Element of Q.I;
func QClass.u -> Subset of Q.I means
:: QUOFIELD:def 4
 for z being Element of Q.I holds z in it iff z`1 * u`2 = z`2 * u`1;
end;

theorem :: QUOFIELD:6
for I being non degenerated commutative (non empty multLoopStr_0)
for u being Element of Q.I holds u in QClass.u;

definition let I be non degenerated commutative (non empty multLoopStr_0);
           let u be Element of Q.I;
  cluster QClass.u -> non empty;
end;

definition
let I be non degenerated non empty multLoopStr_0;
func Quot.I -> Subset-Family of Q.I means
:: QUOFIELD:def 5
 for A being Subset of Q.I holds
 A in it iff (ex u being Element of Q.I st A = QClass.u);
end;

theorem :: QUOFIELD:7
for I being non degenerated non empty multLoopStr_0 holds
Quot.I is non empty;

definition let I be non degenerated non empty multLoopStr_0;
  cluster Quot.I -> non empty;
end;

theorem :: QUOFIELD:8
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Q.I holds
(ex w being Element of Quot.I st u in w & v in w) implies u`1 * v`2 = v`1 * u`2
;

theorem :: QUOFIELD:9
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Quot.I holds u meets v implies u = v;

::: Definition of Quotient Field Addition and Multiplication

begin

definition
let I be non degenerated domRing-like commutative Ring;
let u,v be Element of Quot.I;
func qadd(u,v) -> Element of Quot.I means
:: QUOFIELD:def 6
 for z being Element of Q.I holds
 z in it iff
 (ex a,b being Element of Q.I st
  a in u & b in v & z`1 * (a`2 * b`2) = z`2 * (a`1 * b`2 + b`1 * a`2));
end;

definition
let I be non degenerated domRing-like commutative Ring;
let u,v be Element of Quot.I;
func qmult(u,v) -> Element of Quot.I means
:: QUOFIELD:def 7
 for z being Element of Q.I holds
 z in it iff
 (ex a,b being Element of Q.I st
  a in u & b in v & z`1 * (a`2 * b`2) = z`2 * (a`1 * b`1));
end;

definition let I be non degenerated non empty multLoopStr_0;
           let u be Element of Q.I;
  redefine func QClass.u -> Element of Quot.I;
end;

canceled;

theorem :: QUOFIELD:11
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Q.I holds
qadd(QClass.u,QClass.v) = QClass.(padd(u,v));

theorem :: QUOFIELD:12
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Q.I holds
qmult(QClass.u,QClass.v) = QClass.(pmult(u,v));

::: Properties of Quotient Field Addition and Multiplication

definition
let I be non degenerated domRing-like commutative Ring;
func q0.I -> Element of Quot.I means
:: QUOFIELD:def 8
 for z being Element of Q.I holds z in it iff z`1 = 0.I;
end;

definition
let I be non degenerated domRing-like commutative Ring;
func q1.I -> Element of Quot.I means
:: QUOFIELD:def 9
 for z being Element of Q.I holds z in it iff z`1 = z`2;
end;

definition
let I be non degenerated domRing-like commutative Ring;
let u be Element of Quot.I;
func qaddinv(u) -> Element of Quot.I means
:: QUOFIELD:def 10
 for z being Element of Q.I holds
 z in it iff
 (ex a being Element of Q.I st (a in u & z`1 * a`2 = z`2 * (-(a`1))));
end;

definition
let I be non degenerated domRing-like commutative Ring;
let u be Element of Quot.I;
assume  u <> q0.I;
func qmultinv(u) -> Element of Quot.I means
:: QUOFIELD:def 11
 for z being Element of Q.I holds
 z in it iff
 (ex a being Element of Q.I st (a in u & z`1 * a`1 = z`2 * a`2));
end;

theorem :: QUOFIELD:13
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
qadd(u,qadd(v,w)) = qadd(qadd(u,v),w) & qadd(u,v) = qadd(v,u);

theorem :: QUOFIELD:14
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds qadd(u,q0.I) = u & qadd(q0.I,u) = u;

theorem :: QUOFIELD:15
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
qmult(u,qmult(v,w)) = qmult(qmult(u,v),w) & qmult(u,v) = qmult(v,u);

theorem :: QUOFIELD:16
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds qmult(u,q1.I) = u & qmult(q1.I,u) = u;

theorem :: QUOFIELD:17
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
qmult(qadd(u,v),w) = qadd(qmult(u,w),qmult(v,w));

theorem :: QUOFIELD:18
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
qmult(u,qadd(v,w)) = qadd(qmult(u,v),qmult(u,w));

theorem :: QUOFIELD:19
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds
qadd(u,qaddinv(u)) = q0.I & qadd(qaddinv(u),u) = q0.I;

theorem :: QUOFIELD:20
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I st u <> q0.I holds
qmult(u,qmultinv(u)) = q1.I & qmult(qmultinv(u),u) = q1.I;

theorem :: QUOFIELD:21
for I being non degenerated domRing-like commutative Ring holds
  q1.I <> q0.I;

::: Redefinition of the Operations' Types

definition
let I be non degenerated domRing-like commutative Ring;
func quotadd(I) -> BinOp of Quot.I means
:: QUOFIELD:def 12
 for u,v being Element of Quot.I holds it.(u,v) = qadd(u,v);
end;

definition
let I be non degenerated domRing-like commutative Ring;
func quotmult(I) -> BinOp of Quot.I means
:: QUOFIELD:def 13
 for u,v being Element of Quot.I holds it.(u,v) = qmult(u,v);
end;

definition
let I be non degenerated domRing-like commutative Ring;
func quotaddinv(I) -> UnOp of Quot.I means
:: QUOFIELD:def 14
 for u being Element of Quot.I holds it.(u) = qaddinv(u);
end;

definition
let I be non degenerated domRing-like commutative Ring;
func quotmultinv(I) -> UnOp of Quot.I means
:: QUOFIELD:def 15
 for u being Element of Quot.I holds it.(u) = qmultinv(u);
end;

theorem :: QUOFIELD:22
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
(quotadd(I)).((quotadd(I)).(u,v),w) = (quotadd(I)).(u,(quotadd(I)).(v,w));

theorem :: QUOFIELD:23
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Quot.I holds (quotadd(I)).(u,v) = (quotadd(I)).(v,u);

theorem :: QUOFIELD:24
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds
(quotadd(I)).(u,q0.I) = u & (quotadd(I)).(q0.I,u) = u;

theorem :: QUOFIELD:25
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
(quotmult(I)).((quotmult(I)).(u,v),w) = (quotmult(I)).(u,(quotmult(I)).(v,w));

theorem :: QUOFIELD:26
for I being non degenerated domRing-like commutative Ring
for u,v being Element of Quot.I holds (quotmult(I)).(u,v)=(quotmult(I)).(v,u);

theorem :: QUOFIELD:27
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds
(quotmult(I)).(u,q1.I) = u & (quotmult(I)).(q1.I,u) = u;

theorem :: QUOFIELD:28
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
(quotmult(I)).((quotadd(I)).(u,v),w) =
(quotadd(I)).((quotmult(I)).(u,w),(quotmult(I)).(v,w));

theorem :: QUOFIELD:29
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of Quot.I holds
(quotmult(I)).(u,(quotadd(I)).(v,w)) =
(quotadd(I)).((quotmult(I)).(u,v),(quotmult(I)).(u,w));

theorem :: QUOFIELD:30
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I holds
(quotadd(I)).(u,(quotaddinv(I)).(u)) = q0.I &
(quotadd(I)).((quotaddinv(I)).(u),u) = q0.I;

theorem :: QUOFIELD:31
for I being non degenerated domRing-like commutative Ring
for u being Element of Quot.I st u <> q0.I holds
(quotmult(I)).(u,(quotmultinv(I)).(u)) = q1.I &
(quotmult(I)).((quotmultinv(I)).(u),u) = q1.I;

::: Definition of Quotient Field

begin

definition
let I be non degenerated domRing-like commutative Ring;
func the_Field_of_Quotients(I) -> strict doubleLoopStr equals
:: QUOFIELD:def 16
  doubleLoopStr (# Quot.I,quotadd(I),quotmult(I),q1.I,q0.I #);
end;

definition
let I be non degenerated domRing-like commutative Ring;
 cluster the_Field_of_Quotients(I) -> non empty;
end;

theorem :: QUOFIELD:32
for I being non degenerated domRing-like commutative Ring holds
the carrier of the_Field_of_Quotients(I) = Quot.I &
the add of the_Field_of_Quotients(I) = quotadd(I) &
the mult of the_Field_of_Quotients(I) = quotmult(I) &
the Zero of the_Field_of_Quotients(I) = q0.I &
the unity of the_Field_of_Quotients(I) = q1.I;

theorem :: QUOFIELD:33
for I being non degenerated domRing-like commutative Ring
for u,v being Element of the_Field_of_Quotients(I) holds
(quotadd(I)).(u,v) is Element of the_Field_of_Quotients(I);

theorem :: QUOFIELD:34
for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I) holds
(quotaddinv(I)).(u) is Element of the_Field_of_Quotients(I);

theorem :: QUOFIELD:35
for I being non degenerated domRing-like commutative Ring
for u,v being Element of the_Field_of_Quotients(I) holds
(quotmult(I)).(u,v) is Element of the_Field_of_Quotients(I);

theorem :: QUOFIELD:36
for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I) holds
(quotmultinv(I)).(u) is Element of the_Field_of_Quotients(I);

theorem :: QUOFIELD:37
for I being non degenerated domRing-like commutative Ring
for u,v being Element of the_Field_of_Quotients(I) holds
u + v = (quotadd(I)).(u,v);

definition let I be non degenerated domRing-like commutative Ring;
 cluster the_Field_of_Quotients(I) -> add-associative right_zeroed
                   right_complementable;
end;

theorem :: QUOFIELD:38
  for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I) holds
-u = (quotaddinv(I)).(u);

theorem :: QUOFIELD:39
for I being non degenerated domRing-like commutative Ring
for u,v being Element of the_Field_of_Quotients(I) holds
u * v = (quotmult(I)).(u,v);

theorem :: QUOFIELD:40
 for I being non degenerated domRing-like commutative Ring holds
1_ the_Field_of_Quotients(I) = q1.I & 0.the_Field_of_Quotients(I) = q0.I;

theorem :: QUOFIELD:41
  for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of the_Field_of_Quotients(I) holds
(u + v) + w = u + (v + w);

theorem :: QUOFIELD:42
 for I being non degenerated domRing-like commutative Ring
for u,v being Element of the_Field_of_Quotients(I) holds
u + v = v + u;

theorem :: QUOFIELD:43
  for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I) holds
u + 0.the_Field_of_Quotients(I) = u;

canceled;

theorem :: QUOFIELD:45
for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I) holds
1_ the_Field_of_Quotients(I) * u = u;

theorem :: QUOFIELD:46
for I being non degenerated domRing-like commutative Ring
for u,v being Element of the_Field_of_Quotients(I) holds
u * v = v * u;

theorem :: QUOFIELD:47
for I being non degenerated domRing-like commutative Ring
for u,v,w being Element of the_Field_of_Quotients(I) holds
(u * v) * w = u * (v * w);

theorem :: QUOFIELD:48
for I being non degenerated domRing-like commutative Ring
for u being Element of the_Field_of_Quotients(I)
st u <> 0.the_Field_of_Quotients(I)
ex v being Element of the_Field_of_Quotients(I)
st u * v = 1_ the_Field_of_Quotients(I);

theorem :: QUOFIELD:49
for I being non degenerated domRing-like commutative Ring holds
the_Field_of_Quotients(I) is add-associative right_zeroed right_complementable
    Abelian commutative associative left_unital distributive
      Field-like non degenerated (non empty doubleLoopStr);

definition let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) ->
    Abelian commutative associative left_unital distributive
      Field-like non degenerated;
end;

theorem :: QUOFIELD:50
for I being non degenerated domRing-like commutative Ring
for x being Element of the_Field_of_Quotients(I)
      st x <> 0.the_Field_of_Quotients(I)
for a being Element of I st a <> 0.I
for u being Element of Q.I st x = QClass.u & u = [a,1_ I]
for v being Element of Q.I st v = [1_ I,a] holds
x" = QClass.v;

::: Field is Integral Domain

definition
cluster -> domRing-like right_unital
   (add-associative right_zeroed right_complementable
        commutative associative left_unital
        distributive Field-like non degenerated(non empty doubleLoopStr));
end;

definition
cluster add-associative right_zeroed right_complementable
        Abelian commutative associative left_unital
        distributive Field-like non degenerated (non empty doubleLoopStr);
end;

definition
let F be commutative associative left_unital distributive
         Field-like (non empty doubleLoopStr);
let x, y be Element of F;
func x/y -> Element of F equals
:: QUOFIELD:def 17
  x * y";
end;

theorem :: QUOFIELD:51
for F being non degenerated Field-like commutative Ring
for a,b,c,d being Element of F st b <> 0.F & d <> 0.F holds
(a/b) * (c/d) = (a * c) / (b * d);

theorem :: QUOFIELD:52
for F being non degenerated Field-like commutative Ring
for a,b,c,d being Element of F st b <> 0.F & d <> 0.F holds
(a/b) + (c/d) = (a*d + c*b) / (b * d);

::: Definition of Ring Homomorphism

begin

definition let R,S be non empty doubleLoopStr;
  let f be map of R, S;
 canceled 3;

  attr f is RingHomomorphism means
:: QUOFIELD:def 21
   f is additive multiplicative unity-preserving;
end;

definition let R,S be non empty doubleLoopStr;
  cluster RingHomomorphism -> additive multiplicative unity-preserving
    map of R, S;
  cluster additive multiplicative unity-preserving -> RingHomomorphism
    map of R, S;
end;

definition let R,S be non empty doubleLoopStr;
  let f be map of R, S;
  attr f is RingEpimorphism means
:: QUOFIELD:def 22
   f is RingHomomorphism & rng f = the carrier of S;

  attr f is RingMonomorphism means
:: QUOFIELD:def 23
   f is RingHomomorphism & f is one-to-one;
  synonym f is embedding;
end;

definition let R,S be non empty doubleLoopStr;
  let f be map of R, S;
  attr f is RingIsomorphism means
:: QUOFIELD:def 24
   f is RingMonomorphism RingEpimorphism;
end;

definition let R,S be non empty doubleLoopStr;
  cluster RingIsomorphism -> RingMonomorphism RingEpimorphism map of R, S;
  cluster RingMonomorphism RingEpimorphism -> RingIsomorphism map of R, S;
end;

theorem :: QUOFIELD:53
for R,S being Ring
for f being map of R, S st f is RingHomomorphism holds
f.(0.R) = 0.S;

theorem :: QUOFIELD:54
for R,S being Ring
for f being map of R, S st f is RingMonomorphism
for x being Element of R holds
f.x = 0.S iff x = 0.R;

theorem :: QUOFIELD:55
for R,S being non degenerated Field-like commutative Ring
for f being map of R, S st f is RingHomomorphism
for x being Element of R st x <> 0.R holds
f.(x") = (f.x)";

theorem :: QUOFIELD:56
for R,S being non degenerated Field-like commutative Ring
for f being map of R, S st f is RingHomomorphism
for x,y being Element of R st y <> 0.R holds
f.(x * y") = f.x * (f.y)";

theorem :: QUOFIELD:57
for R,S,T being Ring
for f being map of R, S st f is RingHomomorphism
for g being map of S, T st g is RingHomomorphism holds
g*f is RingHomomorphism;

theorem :: QUOFIELD:58
for R being non empty doubleLoopStr
holds id R is RingHomomorphism;

definition let R be non empty doubleLoopStr;
  cluster id R -> RingHomomorphism;
end;

definition let R,S be non empty doubleLoopStr;
  pred R is_embedded_in S means
:: QUOFIELD:def 25
   ex f being map of R, S st f is RingMonomorphism;
end;

definition let R,S be non empty doubleLoopStr;
  pred R is_ringisomorph_to S means
:: QUOFIELD:def 26
   ex f being map of R, S st f is RingIsomorphism;
symmetry;
end;

::: Properties of the Field of Quotients

begin

definition let I be non empty ZeroStr;
  let x, y be Element of I;
  assume  y <> 0.I;
  func quotient(x,y) -> Element of Q.I equals
:: QUOFIELD:def 27
   [x,y];
end;

definition let I be non degenerated domRing-like commutative Ring;
func canHom(I) -> map of I, the_Field_of_Quotients(I) means
:: QUOFIELD:def 28
 for x being Element of I holds
 it.x = QClass.(quotient(x,1_ I));
end;

theorem :: QUOFIELD:59
for I being non degenerated domRing-like commutative Ring holds
canHom(I) is RingHomomorphism;

theorem :: QUOFIELD:60
for I being non degenerated domRing-like commutative Ring holds
canHom(I) is embedding;

theorem :: QUOFIELD:61
  for I being non degenerated domRing-like commutative Ring holds
I is_embedded_in the_Field_of_Quotients(I);

theorem :: QUOFIELD:62
for F being non degenerated Field-like domRing-like commutative Ring holds
F is_ringisomorph_to the_Field_of_Quotients(F);

definition let I be non degenerated domRing-like commutative Ring;
  cluster the_Field_of_Quotients(I) ->
     domRing-like right_unital right-distributive;
end;

theorem :: QUOFIELD:63
  for I being non degenerated domRing-like commutative Ring holds
the_Field_of_Quotients(the_Field_of_Quotients(I)) is_ringisomorph_to
the_Field_of_Quotients(I);

::: Universal Property of Fields of Quotients

definition let I, F be non empty doubleLoopStr;
           let f be map of I, F;
pred I has_Field_of_Quotients_Pair F,f means
:: QUOFIELD:def 29
 f is RingMonomorphism &
 for F' being add-associative right_zeroed right_complementable
              Abelian commutative associative left_unital distributive
              Field-like non degenerated (non empty doubleLoopStr)
 for f' being map of I, F' st f' is RingMonomorphism holds
   ex h being map of F, F' st h is RingHomomorphism &
           h*f = f' &
           for h' being map of F, F'
               st h' is RingHomomorphism & h'*f = f'
               holds h' = h;
end;

theorem :: QUOFIELD:64
  for I being non degenerated domRing-like commutative Ring holds
ex F being add-associative right_zeroed right_complementable
           Abelian commutative associative left_unital distributive
           Field-like non degenerated (non empty doubleLoopStr)
st ex f being map of I, F st I has_Field_of_Quotients_Pair F,f;

theorem :: QUOFIELD:65
  for I being domRing-like commutative Ring
for F,F' being add-associative right_zeroed right_complementable
    Abelian commutative associative left_unital distributive
      Field-like non degenerated (non empty doubleLoopStr)
for f being map of I, F
for f' being map of I, F'
st I has_Field_of_Quotients_Pair F,f &
   I has_Field_of_Quotients_Pair F',f'
holds F is_ringisomorph_to F';