:: The Field of Quotients over an Integral Domain
:: by Christoph Schwarzweller
::
:: Received May 4, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

definition
let I be non empty ZeroStr ;
func Q. I -> Subset of [: the carrier of I, the carrier of I:] means :Def1: :: 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 ) );
existence
ex b1 being Subset of [: the carrier of I, the carrier of I:] st
for u being set holds
( u in b1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) )
proof end;
uniqueness
for b1, b2 being Subset of [: the carrier of I, the carrier of I:] st ( for u being set holds
( u in b1 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) & ( for u being set holds
( u in b2 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Q. QUOFIELD:def 1 :
for I being non empty ZeroStr
for b2 being Subset of [: the carrier of I, the carrier of I:] holds
( b2 = Q. I iff for u being set holds
( u in b2 iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) );

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

registration
let I be non empty non degenerated multLoopStr_0 ;
cluster Q. I -> non empty ;
coherence
not Q. I is empty
by Th1;
end;

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

:: Definition and some Properties of Pair Addition and Multiplication
definition
let I be non empty non degenerated domRing-like 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))];
coherence
[(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Q. I
proof end;
end;

:: deftheorem defines padd QUOFIELD:def 2 :
for I being non empty non degenerated domRing-like doubleLoopStr
for u, v being Element of Q. I holds padd (u,v) = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))];

definition
let I be non empty non degenerated domRing-like 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))];
coherence
[((u `1) * (v `1)),((u `2) * (v `2))] is Element of Q. I
proof end;
end;

:: deftheorem defines pmult QUOFIELD:def 3 :
for I being non empty non degenerated domRing-like doubleLoopStr
for u, v being Element of Q. I holds pmult (u,v) = [((u `1) * (v `1)),((u `2) * (v `2))];

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

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

definition
let I be non empty non degenerated Abelian add-associative associative commutative distributive domRing-like doubleLoopStr ;
let u, v be Element of Q. I;
:: original: padd
redefine func padd (u,v) -> Element of Q. I;
commutativity
for u, v being Element of Q. I holds padd (u,v) = padd (v,u)
proof end;
end;

definition
let I be non empty non degenerated Abelian associative commutative domRing-like doubleLoopStr ;
let u, v be Element of Q. I;
:: original: pmult
redefine func pmult (u,v) -> Element of Q. I;
commutativity
for u, v being Element of Q. I holds pmult (u,v) = pmult (v,u)
proof end;
end;

:: Definition of Classes of Pairs
definition
let I be non empty non degenerated multLoopStr_0 ;
let u be Element of Q. I;
func QClass. u -> Subset of (Q. I) means :Def4: :: QUOFIELD:def 4
for z being Element of Q. I holds
( z in it iff (z `1) * (u `2) = (z `2) * (u `1) );
existence
ex b1 being Subset of (Q. I) st
for z being Element of Q. I holds
( z in b1 iff (z `1) * (u `2) = (z `2) * (u `1) )
proof end;
uniqueness
for b1, b2 being Subset of (Q. I) st ( for z being Element of Q. I holds
( z in b1 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) & ( for z being Element of Q. I holds
( z in b2 iff (z `1) * (u `2) = (z `2) * (u `1) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines QClass. QUOFIELD:def 4 :
for I being non empty non degenerated multLoopStr_0
for u being Element of Q. I
for b3 being Subset of (Q. I) holds
( b3 = QClass. u iff for z being Element of Q. I holds
( z in b3 iff (z `1) * (u `2) = (z `2) * (u `1) ) );

theorem Th5: :: QUOFIELD:5
for I being non empty non degenerated commutative multLoopStr_0
for u being Element of Q. I holds u in QClass. u
proof end;

registration
let I be non empty non degenerated commutative multLoopStr_0 ;
let u be Element of Q. I;
cluster QClass. u -> non empty ;
coherence
not QClass. u is empty
by Th5;
end;

definition
let I be non empty non degenerated multLoopStr_0 ;
func Quot. I -> Subset-Family of (Q. I) means :Def5: :: 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 );
existence
ex b1 being Subset-Family of (Q. I) st
for A being Subset of (Q. I) holds
( A in b1 iff ex u being Element of Q. I st A = QClass. u )
proof end;
uniqueness
for b1, b2 being Subset-Family of (Q. I) st ( for A being Subset of (Q. I) holds
( A in b1 iff ex u being Element of Q. I st A = QClass. u ) ) & ( for A being Subset of (Q. I) holds
( A in b2 iff ex u being Element of Q. I st A = QClass. u ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Quot. QUOFIELD:def 5 :
for I being non empty non degenerated multLoopStr_0
for b2 being Subset-Family of (Q. I) holds
( b2 = Quot. I iff for A being Subset of (Q. I) holds
( A in b2 iff ex u being Element of Q. I st A = QClass. u ) );

theorem Th6: :: QUOFIELD:6
for I being non empty non degenerated multLoopStr_0 holds not Quot. I is empty
proof end;

registration
let I be non empty non degenerated multLoopStr_0 ;
cluster Quot. I -> non empty ;
coherence
not Quot. I is empty
by Th6;
end;

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

theorem Th8: :: QUOFIELD:8
for I being non degenerated commutative domRing-like Ring
for u, v being Element of Quot. I st u meets v holds
u = v
proof end;

begin

definition
let I be non degenerated commutative domRing-like Ring;
let u, v be Element of Quot. I;
func qadd (u,v) -> Element of Quot. I means :Def6: :: 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))) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 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))) ) )
proof end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 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))) ) ) ) & ( for z being Element of Q. I holds
( z in b2 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))) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines qadd QUOFIELD:def 6 :
for I being non degenerated commutative domRing-like Ring
for u, v, b4 being Element of Quot. I holds
( b4 = qadd (u,v) iff for z being Element of Q. I holds
( z in b4 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))) ) ) );

definition
let I be non degenerated commutative domRing-like Ring;
let u, v be Element of Quot. I;
func qmult (u,v) -> Element of Quot. I means :Def7: :: 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)) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 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)) ) )
proof end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 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)) ) ) ) & ( for z being Element of Q. I holds
( z in b2 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)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines qmult QUOFIELD:def 7 :
for I being non degenerated commutative domRing-like Ring
for u, v, b4 being Element of Quot. I holds
( b4 = qmult (u,v) iff for z being Element of Q. I holds
( z in b4 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)) ) ) );

definition
let I be non empty non degenerated multLoopStr_0 ;
let u be Element of Q. I;
:: original: QClass.
redefine func QClass. u -> Element of Quot. I;
coherence
QClass. u is Element of Quot. I
by Def5;
end;

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

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

:: Properties of Quotient Field Addition and Multiplication
definition
let I be non degenerated commutative domRing-like Ring;
func q0. I -> Element of Quot. I means :Def8: :: QUOFIELD:def 8
for z being Element of Q. I holds
( z in it iff z `1 = 0. I );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I )
proof end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I ) ) & ( for z being Element of Q. I holds
( z in b2 iff z `1 = 0. I ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines q0. QUOFIELD:def 8 :
for I being non degenerated commutative domRing-like Ring
for b2 being Element of Quot. I holds
( b2 = q0. I iff for z being Element of Q. I holds
( z in b2 iff z `1 = 0. I ) );

definition
let I be non degenerated commutative domRing-like Ring;
func q1. I -> Element of Quot. I means :Def9: :: QUOFIELD:def 9
for z being Element of Q. I holds
( z in it iff z `1 = z `2 );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = z `2 )
proof end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff z `1 = z `2 ) ) & ( for z being Element of Q. I holds
( z in b2 iff z `1 = z `2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines q1. QUOFIELD:def 9 :
for I being non degenerated commutative domRing-like Ring
for b2 being Element of Quot. I holds
( b2 = q1. I iff for z being Element of Q. I holds
( z in b2 iff z `1 = z `2 ) );

definition
let I be non degenerated commutative domRing-like Ring;
let u be Element of Quot. I;
func qaddinv u -> Element of Quot. I means :Def10: :: 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)) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )
proof end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) & ( for z being Element of Q. I holds
( z in b2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines qaddinv QUOFIELD:def 10 :
for I being non degenerated commutative domRing-like Ring
for u, b3 being Element of Quot. I holds
( b3 = qaddinv u iff for z being Element of Q. I holds
( z in b3 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) );

definition
let I be non degenerated commutative domRing-like Ring;
let u be Element of Quot. I;
assume A1: u <> q0. I ;
func qmultinv u -> Element of Quot. I means :Def11: :: 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) ) );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) )
proof end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) & ( for z being Element of Q. I holds
( z in b2 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines qmultinv QUOFIELD:def 11 :
for I being non degenerated commutative domRing-like Ring
for u being Element of Quot. I st u <> q0. I holds
for b3 being Element of Quot. I holds
( b3 = qmultinv u iff for z being Element of Q. I holds
( z in b3 iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) );

theorem Th11: :: QUOFIELD:11
for I being non degenerated commutative domRing-like 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) )
proof end;

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

theorem Th13: :: QUOFIELD:13
for I being non degenerated commutative domRing-like 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) )
proof end;

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

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

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

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

theorem Th18: :: QUOFIELD:18
for I being non degenerated commutative domRing-like 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 )
proof end;

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

:: Redefinition of the Operations' Types
definition
let I be non degenerated commutative domRing-like Ring;
func quotadd I -> BinOp of (Quot. I) means :Def12: :: QUOFIELD:def 12
for u, v being Element of Quot. I holds it . (u,v) = qadd (u,v);
existence
ex b1 being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v)
proof end;
uniqueness
for b1, b2 being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v) ) & ( for u, v being Element of Quot. I holds b2 . (u,v) = qadd (u,v) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines quotadd QUOFIELD:def 12 :
for I being non degenerated commutative domRing-like Ring
for b2 being BinOp of (Quot. I) holds
( b2 = quotadd I iff for u, v being Element of Quot. I holds b2 . (u,v) = qadd (u,v) );

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

:: deftheorem Def13 defines quotmult QUOFIELD:def 13 :
for I being non degenerated commutative domRing-like Ring
for b2 being BinOp of (Quot. I) holds
( b2 = quotmult I iff for u, v being Element of Quot. I holds b2 . (u,v) = qmult (u,v) );

definition
let I be non degenerated commutative domRing-like Ring;
func quotaddinv I -> UnOp of (Quot. I) means :Def14: :: QUOFIELD:def 14
for u being Element of Quot. I holds it . u = qaddinv u;
existence
ex b1 being UnOp of (Quot. I) st
for u being Element of Quot. I holds b1 . u = qaddinv u
proof end;
uniqueness
for b1, b2 being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b1 . u = qaddinv u ) & ( for u being Element of Quot. I holds b2 . u = qaddinv u ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines quotaddinv QUOFIELD:def 14 :
for I being non degenerated commutative domRing-like Ring
for b2 being UnOp of (Quot. I) holds
( b2 = quotaddinv I iff for u being Element of Quot. I holds b2 . u = qaddinv u );

definition
let I be non degenerated commutative domRing-like Ring;
func quotmultinv I -> UnOp of (Quot. I) means :Def15: :: QUOFIELD:def 15
for u being Element of Quot. I holds it . u = qmultinv u;
existence
ex b1 being UnOp of (Quot. I) st
for u being Element of Quot. I holds b1 . u = qmultinv u
proof end;
uniqueness
for b1, b2 being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b1 . u = qmultinv u ) & ( for u being Element of Quot. I holds b2 . u = qmultinv u ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines quotmultinv QUOFIELD:def 15 :
for I being non degenerated commutative domRing-like Ring
for b2 being UnOp of (Quot. I) holds
( b2 = quotmultinv I iff for u being Element of Quot. I holds b2 . u = qmultinv u );

theorem Th20: :: QUOFIELD:20
for I being non degenerated commutative domRing-like 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)))
proof end;

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

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

theorem Th23: :: QUOFIELD:23
for I being non degenerated commutative domRing-like 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)))
proof end;

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

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

theorem Th26: :: QUOFIELD:26
for I being non degenerated commutative domRing-like 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)))
proof end;

theorem Th27: :: QUOFIELD:27
for I being non degenerated commutative domRing-like 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)))
proof end;

theorem Th28: :: QUOFIELD:28
for I being non degenerated commutative domRing-like 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 )
proof end;

theorem Th29: :: QUOFIELD:29
for I being non degenerated commutative domRing-like 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 )
proof end;

begin

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

:: deftheorem defines the_Field_of_Quotients QUOFIELD:def 16 :
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I = doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #);

registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> non empty strict ;
coherence
not the_Field_of_Quotients I is empty
;
end;

theorem :: QUOFIELD:30
for I being non degenerated commutative domRing-like Ring holds
( the carrier of (the_Field_of_Quotients I) = Quot. I & the addF of (the_Field_of_Quotients I) = quotadd I & the multF of (the_Field_of_Quotients I) = quotmult I & 0. (the_Field_of_Quotients I) = q0. I & 1. (the_Field_of_Quotients I) = q1. I ) ;

theorem :: QUOFIELD:31
for I being non degenerated commutative domRing-like 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)
proof end;

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

theorem :: QUOFIELD:33
for I being non degenerated commutative domRing-like 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)
proof end;

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

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

Lm2: for I being non degenerated commutative domRing-like Ring holds
( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )

proof end;

registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> right_complementable strict add-associative right_zeroed ;
coherence
( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )
by Lm2;
end;

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

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

Lm3: for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty commutative doubleLoopStr
proof end;

registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> strict commutative ;
coherence
the_Field_of_Quotients I is commutative
by Lm3;
end;

Lm4: for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is well-unital
proof end;

registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> strict well-unital ;
coherence
the_Field_of_Quotients I is well-unital
by Lm4;
end;

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

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

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

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

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

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

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

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

theorem Th46: :: QUOFIELD:46
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative distributive doubleLoopStr
proof end;

registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> non degenerated almost_left_invertible strict Abelian associative distributive ;
coherence
( the_Field_of_Quotients I is Abelian & the_Field_of_Quotients I is associative & the_Field_of_Quotients I is distributive & the_Field_of_Quotients I is almost_left_invertible & not the_Field_of_Quotients I is degenerated )
by Th46;
end;

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

:: Field is Integral Domain
registration
cluster non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive -> non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative right_unital well-unital distributive domRing-like for doubleLoopStr ;
coherence
for b1 being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds
( b1 is domRing-like & b1 is right_unital )
proof end;
end;

registration
cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative distributive left_unital for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is left_unital & b1 is distributive & b1 is almost_left_invertible & not b1 is degenerated )
proof end;
end;

definition
let F be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let x, y be Element of F;
func x / y -> Element of F equals :: QUOFIELD:def 17
x * (y ");
correctness
coherence
x * (y ") is Element of F
;
;
end;

:: deftheorem defines / QUOFIELD:def 17 :
for F being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x, y being Element of F holds x / y = x * (y ");

theorem Th48: :: QUOFIELD:48
for F being non degenerated almost_left_invertible 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)
proof end;

theorem Th49: :: QUOFIELD:49
for F being non degenerated almost_left_invertible 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)
proof end;

begin

definition
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
attr f is RingHomomorphism means :Def18: :: QUOFIELD:def 18
( f is additive & f is multiplicative & f is unity-preserving );
end;

:: deftheorem Def18 defines RingHomomorphism QUOFIELD:def 18 :
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingHomomorphism iff ( f is additive & f is multiplicative & f is unity-preserving ) );

registration
let R, S be non empty doubleLoopStr ;
cluster Function-like quasi_total RingHomomorphism -> unity-preserving multiplicative additive for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is RingHomomorphism holds
( b1 is additive & b1 is multiplicative & b1 is unity-preserving )
by Def18;
cluster Function-like quasi_total unity-preserving multiplicative additive -> RingHomomorphism for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is additive & b1 is multiplicative & b1 is unity-preserving holds
b1 is RingHomomorphism
by Def18;
end;

definition
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
attr f is RingEpimorphism means :Def19: :: QUOFIELD:def 19
( f is RingHomomorphism & rng f = the carrier of S );
attr f is RingMonomorphism means :Def20: :: QUOFIELD:def 20
( f is RingHomomorphism & f is one-to-one );
end;

:: deftheorem Def19 defines RingEpimorphism QUOFIELD:def 19 :
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingEpimorphism iff ( f is RingHomomorphism & rng f = the carrier of S ) );

:: deftheorem Def20 defines RingMonomorphism QUOFIELD:def 20 :
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingMonomorphism iff ( f is RingHomomorphism & f is one-to-one ) );

notation
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
synonym embedding f for RingMonomorphism ;
end;

definition
let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
attr f is RingIsomorphism means :Def21: :: QUOFIELD:def 21
( f is RingMonomorphism & f is RingEpimorphism );
end;

:: deftheorem Def21 defines RingIsomorphism QUOFIELD:def 21 :
for R, S being non empty doubleLoopStr
for f being Function of R,S holds
( f is RingIsomorphism iff ( f is RingMonomorphism & f is RingEpimorphism ) );

registration
let R, S be non empty doubleLoopStr ;
cluster Function-like quasi_total RingIsomorphism -> RingEpimorphism RingMonomorphism for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is RingIsomorphism holds
( b1 is RingMonomorphism & b1 is RingEpimorphism )
by Def21;
cluster Function-like quasi_total RingEpimorphism RingMonomorphism -> RingIsomorphism for Element of bool [: the carrier of R, the carrier of S:];
coherence
for b1 being Function of R,S st b1 is RingMonomorphism & b1 is RingEpimorphism holds
b1 is RingIsomorphism
by Def21;
end;

theorem Th50: :: QUOFIELD:50
for R, S being Ring
for f being Function of R,S st f is RingHomomorphism holds
f . (0. R) = 0. S
proof end;

theorem Th51: :: QUOFIELD:51
for R, S being Ring
for f being Function of R,S st f is RingMonomorphism holds
for x being Element of R holds
( f . x = 0. S iff x = 0. R )
proof end;

theorem Th52: :: QUOFIELD:52
for R, S being non degenerated almost_left_invertible commutative Ring
for f being Function of R,S st f is RingHomomorphism holds
for x being Element of R st x <> 0. R holds
f . (x ") = (f . x) "
proof end;

theorem Th53: :: QUOFIELD:53
for R, S being non degenerated almost_left_invertible commutative Ring
for f being Function of R,S st f is RingHomomorphism holds
for x, y being Element of R st y <> 0. R holds
f . (x * (y ")) = (f . x) * ((f . y) ")
proof end;

theorem Th54: :: QUOFIELD:54
for R, S, T being Ring
for f being Function of R,S st f is RingHomomorphism holds
for g being Function of S,T st g is RingHomomorphism holds
g * f is RingHomomorphism
proof end;

theorem Th55: :: QUOFIELD:55
for R being non empty doubleLoopStr holds id R is RingHomomorphism
proof end;

registration
let R be non empty doubleLoopStr ;
cluster id R -> RingHomomorphism ;
coherence
id R is RingHomomorphism
by Th55;
end;

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

:: deftheorem Def22 defines is_embedded_in QUOFIELD:def 22 :
for R, S being non empty doubleLoopStr holds
( R is_embedded_in S iff ex f being Function of R,S st f is RingMonomorphism );

definition
let R, S be non empty doubleLoopStr ;
pred R is_ringisomorph_to S means :Def23: :: QUOFIELD:def 23
ex f being Function of R,S st f is RingIsomorphism ;
symmetry
for R, S being non empty doubleLoopStr st ex f being Function of R,S st f is RingIsomorphism holds
ex f being Function of S,R st f is RingIsomorphism
proof end;
end;

:: deftheorem Def23 defines is_ringisomorph_to QUOFIELD:def 23 :
for R, S being non empty doubleLoopStr holds
( R is_ringisomorph_to S iff ex f being Function of R,S st f is RingIsomorphism );

begin

definition
let I be non empty ZeroStr ;
let x, y be Element of I;
assume A1: y <> 0. I ;
func quotient (x,y) -> Element of Q. I equals :Def24: :: QUOFIELD:def 24
[x,y];
coherence
[x,y] is Element of Q. I
by A1, Def1;
end;

:: deftheorem Def24 defines quotient QUOFIELD:def 24 :
for I being non empty ZeroStr
for x, y being Element of I st y <> 0. I holds
quotient (x,y) = [x,y];

definition
let I be non degenerated commutative domRing-like Ring;
func canHom I -> Function of I,(the_Field_of_Quotients I) means :Def25: :: QUOFIELD:def 25
for x being Element of I holds it . x = QClass. (quotient (x,(1. I)));
existence
ex b1 being Function of I,(the_Field_of_Quotients I) st
for x being Element of I holds b1 . x = QClass. (quotient (x,(1. I)))
proof end;
uniqueness
for b1, b2 being Function of I,(the_Field_of_Quotients I) st ( for x being Element of I holds b1 . x = QClass. (quotient (x,(1. I))) ) & ( for x being Element of I holds b2 . x = QClass. (quotient (x,(1. I))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines canHom QUOFIELD:def 25 :
for I being non degenerated commutative domRing-like Ring
for b2 being Function of I,(the_Field_of_Quotients I) holds
( b2 = canHom I iff for x being Element of I holds b2 . x = QClass. (quotient (x,(1. I))) );

theorem Th56: :: QUOFIELD:56
for I being non degenerated commutative domRing-like Ring holds canHom I is RingHomomorphism
proof end;

theorem Th57: :: QUOFIELD:57
for I being non degenerated commutative domRing-like Ring holds canHom I is embedding
proof end;

theorem :: QUOFIELD:58
for I being non degenerated commutative domRing-like Ring holds I is_embedded_in the_Field_of_Quotients I
proof end;

theorem Th59: :: QUOFIELD:59
for F being non degenerated almost_left_invertible commutative domRing-like Ring holds F is_ringisomorph_to the_Field_of_Quotients F
proof end;

registration
let I be non degenerated commutative domRing-like Ring;
cluster the_Field_of_Quotients I -> strict right-distributive right_unital domRing-like ;
coherence
( the_Field_of_Quotients I is domRing-like & the_Field_of_Quotients I is right_unital & the_Field_of_Quotients I is right-distributive )
;
end;

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

:: Universal Property of Fields of Quotients
definition
let I, F be non empty doubleLoopStr ;
let f be Function of I,F;
pred I has_Field_of_Quotients_Pair F,f means :Def26: :: QUOFIELD:def 26
( f is RingMonomorphism & ( for F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f9 being Function of I,F9 st f9 is RingMonomorphism holds
ex h being Function of F,F9 st
( h is RingHomomorphism & h * f = f9 & ( for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h ) ) ) );
end;

:: deftheorem Def26 defines has_Field_of_Quotients_Pair QUOFIELD:def 26 :
for I, F being non empty doubleLoopStr
for f being Function of I,F holds
( I has_Field_of_Quotients_Pair F,f iff ( f is RingMonomorphism & ( for F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f9 being Function of I,F9 st f9 is RingMonomorphism holds
ex h being Function of F,F9 st
( h is RingHomomorphism & h * f = f9 & ( for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h ) ) ) ) );

theorem :: QUOFIELD:61
for I being non degenerated commutative domRing-like Ring ex F being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ex f being Function of I,F st I has_Field_of_Quotients_Pair F,f
proof end;

theorem :: QUOFIELD:62
for I being commutative domRing-like Ring
for F, F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f being Function of I,F
for f9 being Function of I,F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,f9 holds
F is_ringisomorph_to F9
proof end;