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

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;

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

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

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

Lm1: 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 Lm1;

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

Lm2: 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 Lm2;

end;

Lm3: for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is well-unital
by Th25;

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

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 ;

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

notation

let R, S be non empty doubleLoopStr ;
let f be Function of R,S;
synonym RingHomomorphism f for linear ;
synonym RingEpimorphism f for epimorphism ;
synonym RingMonomorphism f for monomorphism ;

end;

notation

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

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

for R being non empty doubleLoopStr holds id R is RingHomomorphism ;

registration

let R be non empty doubleLoopStr ;

cluster id R -> RingHomomorphism ;

coherence
id R is RingHomomorphism ;

end;

definition

let R, S be non empty doubleLoopStr ;

pred R is_embedded_in S means :: QUOFIELD:def 22
ex f being Function of R,S st f is RingMonomorphism ;

end;

:: deftheorem QUOFIELD:def 18 :
canceled;

:: deftheorem QUOFIELD:def 19 :
canceled;

:: deftheorem QUOFIELD:def 20 :
canceled;

:: deftheorem QUOFIELD:def 21 :
canceled;

:: deftheorem 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 :: 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 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 );

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 :Def20: :: QUOFIELD:def 24
[x,y];

coherence
[x,y] is Element of Q. I by A1, Def1;

end;

:: deftheorem Def20 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 :Def21: :: QUOFIELD:def 25
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 Def21 defines canHom QUOFIELD:def 25 :
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 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 :: 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 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;