:: The Field of Quotients over an Integral Domain
:: by Christoph Schwarzweller
::
:: Received May 4, 1998
:: Copyright (c) 1998-2011 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 b₁ being Subset of [: the carrier of I, the carrier of I:] st
for u being set holds
( u in b₁ iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) )

proof end;

uniqueness
for b₁, b₂ being Subset of [: the carrier of I, the carrier of I:] st ( for u being set holds
( u in b₁ iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) & ( for u being set holds
( u in b₂ iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Q. QUOFIELD:def 1 :
for I being non empty ZeroStr
for b₂ being Subset of [: the carrier of I, the carrier of I:] holds
( b₂ = Q. I iff for u being set holds
( u in b₂ 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;

Lm1: for I being non empty non degenerated multLoopStr_0
for u being Element of Q. I holds
( u `1 is Element of I & u `2 is Element of I )
;

definition

let I be non empty non degenerated multLoopStr_0 ;
let u be Element of Q. I;
:: original: `1
redefine func u `1 -> Element of I;
coherence
u `1 is Element of I by Lm1;
:: original: `2
redefine func u `2 -> Element of I;
coherence
u `2 is Element of I by Lm1;

end;

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 :: QUOFIELD:3

canceled;

theorem Th4: :: QUOFIELD:4

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 Th5: :: QUOFIELD:5

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

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 b₁ being Subset of (Q. I) st
for z being Element of Q. I holds
( z in b₁ iff (z `1) * (u `2) = (z `2) * (u `1) )

proof end;

uniqueness
for b₁, b₂ being Subset of (Q. I) st ( for z being Element of Q. I holds
( z in b₁ iff (z `1) * (u `2) = (z `2) * (u `1) ) ) & ( for z being Element of Q. I holds
( z in b₂ iff (z `1) * (u `2) = (z `2) * (u `1) ) ) holds
b₁ = b₂

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 b₃ being Subset of (Q. I) holds
( b₃ = QClass. u iff for z being Element of Q. I holds
( z in b₃ iff (z `1) * (u `2) = (z `2) * (u `1) ) );

theorem Th6: :: QUOFIELD:6

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 Th6;

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 b₁ being Subset-Family of (Q. I) st
for A being Subset of (Q. I) holds
( A in b₁ iff ex u being Element of Q. I st A = QClass. u )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of (Q. I) st ( for A being Subset of (Q. I) holds
( A in b₁ iff ex u being Element of Q. I st A = QClass. u ) ) & ( for A being Subset of (Q. I) holds
( A in b₂ iff ex u being Element of Q. I st A = QClass. u ) ) holds
b₁ = b₂

proof end;

end;

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

theorem Th7: :: QUOFIELD:7

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 Th7;

end;

theorem Th8: :: QUOFIELD:8

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 Th9: :: QUOFIELD:9

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 b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ 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 b₁, b₂ being Element of Quot. I st ( for z being Element of Q. I holds
( z in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

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

proof end;

end;

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

canceled;

theorem Th11: :: QUOFIELD:11

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 Th12: :: QUOFIELD:12

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;

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 b<sub>1</sub> being Element of Quot. I st
for z being Element of Q. I holds
( z in b<sub>1</sub> iff z `1 = 0. I )

proof end;

uniqueness
for b₁, b₂ being Element of Quot. I st ( for z being Element of Q. I holds
( z in b₁ iff z `1 = 0. I ) ) & ( for z being Element of Q. I holds
( z in b<sub>2</sub> iff z `1 = 0. I ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines q0. QUOFIELD:def 8 :
for I being non degenerated commutative domRing-like Ring
for b₂ being Element of Quot. I holds
( b₂ = q0. I iff for z being Element of Q. I holds
( z in b₂ 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 b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ iff z `1 = z `2 )

proof end;

uniqueness
for b₁, b₂ being Element of Quot. I st ( for z being Element of Q. I holds
( z in b₁ iff z `1 = z `2 ) ) & ( for z being Element of Q. I holds
( z in b₂ iff z `1 = z `2 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines q1. QUOFIELD:def 9 :
for I being non degenerated commutative domRing-like Ring
for b₂ being Element of Quot. I holds
( b₂ = q1. I iff for z being Element of Q. I holds
( z in b₂ 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 b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )

proof end;

uniqueness
for b₁, b₂ being Element of Quot. I st ( for z being Element of Q. I holds
( z in b₁ 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 b₂ iff ex a being Element of Q. I st
( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines qaddinv QUOFIELD:def 10 :
for I being non degenerated commutative domRing-like Ring
for u, b₃ being Element of Quot. I holds
( b₃ = qaddinv u iff for z being Element of Q. I holds
( z in b₃ 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 b₁ being Element of Quot. I st
for z being Element of Q. I holds
( z in b₁ iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) )

proof end;

uniqueness
for b₁, b₂ being Element of Quot. I st ( for z being Element of Q. I holds
( z in b₁ 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 b₂ iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) holds
b₁ = b₂

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 b₃ being Element of Quot. I holds
( b₃ = qmultinv u iff for z being Element of Q. I holds
( z in b₃ iff ex a being Element of Q. I st
( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) );

theorem Th13: :: QUOFIELD:13

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 Th14: :: QUOFIELD:14

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 Th15: :: QUOFIELD:15

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 Th16: :: QUOFIELD:16

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 Th17: :: QUOFIELD:17

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 Th18: :: QUOFIELD:18

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 Th19: :: QUOFIELD:19

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 Th20: :: QUOFIELD:20

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 Th21: :: QUOFIELD:21

for I being non degenerated commutative domRing-like Ring holds q1. I <> q0. I

proof end;

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 b₁ being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b₁ . (u,v) = qadd (u,v)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b₁ . (u,v) = qadd (u,v) ) & ( for u, v being Element of Quot. I holds b₂ . (u,v) = qadd (u,v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines quotadd QUOFIELD:def 12 :
for I being non degenerated commutative domRing-like Ring
for b₂ being BinOp of (Quot. I) holds
( b₂ = quotadd I iff for u, v being Element of Quot. I holds b₂ . (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 b₁ being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b₁ . (u,v) = qmult (u,v)

proof end;

uniqueness
for b₁, b₂ being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b₁ . (u,v) = qmult (u,v) ) & ( for u, v being Element of Quot. I holds b₂ . (u,v) = qmult (u,v) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines quotmult QUOFIELD:def 13 :
for I being non degenerated commutative domRing-like Ring
for b₂ being BinOp of (Quot. I) holds
( b₂ = quotmult I iff for u, v being Element of Quot. I holds b₂ . (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 b₁ being UnOp of (Quot. I) st
for u being Element of Quot. I holds b₁ . u = qaddinv u

proof end;

uniqueness
for b₁, b₂ being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b₁ . u = qaddinv u ) & ( for u being Element of Quot. I holds b₂ . u = qaddinv u ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines quotaddinv QUOFIELD:def 14 :
for I being non degenerated commutative domRing-like Ring
for b₂ being UnOp of (Quot. I) holds
( b₂ = quotaddinv I iff for u being Element of Quot. I holds b₂ . 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 b₁ being UnOp of (Quot. I) st
for u being Element of Quot. I holds b₁ . u = qmultinv u

proof end;

uniqueness
for b₁, b₂ being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b₁ . u = qmultinv u ) & ( for u being Element of Quot. I holds b₂ . u = qmultinv u ) holds
b₁ = b₂

proof end;

end;

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

theorem Th22: :: QUOFIELD:22

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 Th23: :: QUOFIELD:23

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 Th24: :: QUOFIELD:24

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 Th25: :: QUOFIELD:25

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 Th26: :: QUOFIELD:26

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 Th27: :: QUOFIELD:27

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 Th28: :: QUOFIELD:28

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 Th29: :: QUOFIELD:29

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 Th30: :: QUOFIELD:30

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 Th31: :: QUOFIELD:31

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:32

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:33

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 Th34: :: QUOFIELD:34

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:35

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:36

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:37

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:38

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:39

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:40

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:41

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 Th22;

theorem :: QUOFIELD:42

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 Th23;

theorem :: QUOFIELD:43

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 Th24;

theorem :: QUOFIELD:44

canceled;

theorem :: QUOFIELD:45

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 Th27;

theorem :: QUOFIELD:46

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:47

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 Th25;

theorem Th48: :: QUOFIELD:48

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 Th49: :: QUOFIELD:49

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 Th49;

end;

theorem Th50: :: QUOFIELD:50

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;

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 doubleLoopStr ;
coherence
for b₁ being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds
( b₁ is domRing-like & b₁ 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 doubleLoopStr ;
existence
ex b₁ being non empty doubleLoopStr st
( b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is Abelian & b₁ is commutative & b₁ is associative & b₁ is left_unital & b₁ is distributive & b₁ is almost_left_invertible & not b₁ 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 Th51: :: QUOFIELD:51

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 Th52: :: QUOFIELD:52

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;
canceled;
canceled;
canceled;
attr f is RingHomomorphism means :Def21: :: QUOFIELD:def 21
( f is additive & f is multiplicative & f is unity-preserving );

end;

:: deftheorem QUOFIELD:def 18 :
canceled;

:: deftheorem QUOFIELD:def 19 :
canceled;

:: deftheorem QUOFIELD:def 20 :
canceled;

:: deftheorem Def21 defines RingHomomorphism QUOFIELD:def 21 :
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 -> additive unity-preserving multiplicative Element of bool [: the carrier of R, the carrier of S:];
coherence
for b₁ being Function of R,S st b₁ is RingHomomorphism holds
( b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving ) by Def21;
cluster Function-like quasi_total additive unity-preserving multiplicative -> RingHomomorphism Element of bool [: the carrier of R, the carrier of S:];
coherence
for b₁ being Function of R,S st b₁ is additive & b₁ is multiplicative & b₁ is unity-preserving holds
b₁ is RingHomomorphism by Def21;

end;

definition

let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
attr f is RingEpimorphism means :Def22: :: QUOFIELD:def 22
( f is RingHomomorphism & rng f = the carrier of S );
attr f is RingMonomorphism means :Def23: :: QUOFIELD:def 23
( f is RingHomomorphism & f is one-to-one );

end;

:: deftheorem Def22 defines RingEpimorphism QUOFIELD:def 22 :
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 Def23 defines RingMonomorphism QUOFIELD:def 23 :
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 :Def24: :: QUOFIELD:def 24
( f is RingMonomorphism & f is RingEpimorphism );

end;

:: deftheorem Def24 defines RingIsomorphism QUOFIELD:def 24 :
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 Element of bool [: the carrier of R, the carrier of S:];
coherence
for b₁ being Function of R,S st b₁ is RingIsomorphism holds
( b₁ is RingMonomorphism & b₁ is RingEpimorphism ) by Def24;
cluster Function-like quasi_total RingEpimorphism RingMonomorphism -> RingIsomorphism Element of bool [: the carrier of R, the carrier of S:];
coherence
for b₁ being Function of R,S st b₁ is RingMonomorphism & b₁ is RingEpimorphism holds
b₁ is RingIsomorphism by Def24;

end;

theorem Th53: :: QUOFIELD:53

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 Th54: :: QUOFIELD:54

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 Th55: :: QUOFIELD:55

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 Th56: :: QUOFIELD:56

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 Th57: :: QUOFIELD:57

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 Th58: :: QUOFIELD:58

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 Th58;

end;

definition

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

end;

:: deftheorem Def25 defines is_embedded_in QUOFIELD:def 25 :
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 :Def26: :: QUOFIELD:def 26
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 Def26 defines is_ringisomorph_to QUOFIELD:def 26 :
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 :Def27: :: QUOFIELD:def 27
[x,y];
coherence
[x,y] is Element of Q. I by A1, Def1;

end;

:: deftheorem Def27 defines quotient QUOFIELD:def 27 :
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 :Def28: :: QUOFIELD:def 28
for x being Element of I holds it . x = QClass. (quotient (x,(1. I)));
existence
ex b₁ being Function of I,(the_Field_of_Quotients I) st
for x being Element of I holds b₁ . x = QClass. (quotient (x,(1. I)))

proof end;

uniqueness
for b₁, b₂ being Function of I,(the_Field_of_Quotients I) st ( for x being Element of I holds b₁ . x = QClass. (quotient (x,(1. I))) ) & ( for x being Element of I holds b₂ . x = QClass. (quotient (x,(1. I))) ) holds
b₁ = b₂

proof end;

end;

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

theorem Th59: :: QUOFIELD:59

for I being non degenerated commutative domRing-like Ring holds canHom I is RingHomomorphism

proof end;

theorem Th60: :: QUOFIELD:60

for I being non degenerated commutative domRing-like Ring holds canHom I is RingMonomorphism

proof end;

theorem :: QUOFIELD:61

for I being non degenerated commutative domRing-like Ring holds I is_embedded_in the_Field_of_Quotients I

proof end;

theorem Th62: :: QUOFIELD:62

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:63

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 Th62;

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 :Def29: :: QUOFIELD:def 29
( 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 Def29 defines has_Field_of_Quotients_Pair QUOFIELD:def 29 :
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:64

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:65

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;