:: by Christoph Schwarzweller

::

:: Received May 4, 1998

:: Copyright (c) 1998-2012 Association of Mizar Users

begin

definition

let I be non empty ZeroStr ;

ex b_{1} being Subset of [: the carrier of I, the carrier of I:] st

for u being set holds

( u in b_{1} iff ex a, b being Element of I st

( u = [a,b] & b <> 0. I ) )

for b_{1}, b_{2} being Subset of [: the carrier of I, the carrier of I:] st ( for u being set holds

( u in b_{1} iff ex a, b being Element of I st

( u = [a,b] & b <> 0. I ) ) ) & ( for u being set holds

( u in b_{2} iff ex a, b being Element of I st

( u = [a,b] & b <> 0. I ) ) ) holds

b_{1} = b_{2}

end;
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 for u being set holds

( u in it iff ex a, b being Element of I st

( u = [a,b] & b <> 0. I ) );

ex b

for u being set holds

( u in b

( u = [a,b] & b <> 0. I ) )

proof end;

uniqueness for b

( u in b

( u = [a,b] & b <> 0. I ) ) ) & ( for u being set holds

( u in b

( u = [a,b] & b <> 0. I ) ) ) holds

b

proof end;

:: deftheorem Def1 defines Q. QUOFIELD:def 1 :

for I being non empty ZeroStr

for b_{2} being Subset of [: the carrier of I, the carrier of I:] holds

( b_{2} = Q. I iff for u being set holds

( u in b_{2} iff ex a, b being Element of I st

( u = [a,b] & b <> 0. I ) ) );

for I being non empty ZeroStr

for b

( b

( u in b

( u = [a,b] & b <> 0. I ) ) );

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

[(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Q. I

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

[(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] is Element of Q. I

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

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;

coherence

[((u `1) * (v `1)),((u `2) * (v `2))] is Element of Q. I

end;
let u, v be Element of Q. I;

coherence

[((u `1) * (v `1)),((u `2) * (v `2))] is Element of Q. I

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

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)

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)

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)

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

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)

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

:: Definition of Classes of Pairs

definition

let I be non empty non degenerated multLoopStr_0 ;

let u be Element of Q. I;

ex b_{1} being Subset of (Q. I) st

for z being Element of Q. I holds

( z in b_{1} iff (z `1) * (u `2) = (z `2) * (u `1) )

for b_{1}, b_{2} being Subset of (Q. I) st ( for z being Element of Q. I holds

( z in b_{1} iff (z `1) * (u `2) = (z `2) * (u `1) ) ) & ( for z being Element of Q. I holds

( z in b_{2} iff (z `1) * (u `2) = (z `2) * (u `1) ) ) holds

b_{1} = b_{2}

end;
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 for z being Element of Q. I holds

( z in it iff (z `1) * (u `2) = (z `2) * (u `1) );

ex b

for z being Element of Q. I holds

( z in b

proof end;

uniqueness for b

( z in b

( z in b

b

proof 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_{3} being Subset of (Q. I) holds

( b_{3} = QClass. u iff for z being Element of Q. I holds

( z in b_{3} iff (z `1) * (u `2) = (z `2) * (u `1) ) );

for I being non empty non degenerated multLoopStr_0

for u being Element of Q. I

for b

( b

( z in b

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

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;

coherence

not QClass. u is empty by Th5;

end;
let u be Element of Q. I;

coherence

not QClass. u is empty by Th5;

definition

let I be non empty non degenerated multLoopStr_0 ;

ex b_{1} being Subset-Family of (Q. I) st

for A being Subset of (Q. I) holds

( A in b_{1} iff ex u being Element of Q. I st A = QClass. u )

for b_{1}, b_{2} being Subset-Family of (Q. I) st ( for A being Subset of (Q. I) holds

( A in b_{1} iff ex u being Element of Q. I st A = QClass. u ) ) & ( for A being Subset of (Q. I) holds

( A in b_{2} iff ex u being Element of Q. I st A = QClass. u ) ) holds

b_{1} = b_{2}

end;
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 for A being Subset of (Q. I) holds

( A in it iff ex u being Element of Q. I st A = QClass. u );

ex b

for A being Subset of (Q. I) holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof end;

:: deftheorem Def5 defines Quot. QUOFIELD:def 5 :

for I being non empty non degenerated multLoopStr_0

for b_{2} being Subset-Family of (Q. I) holds

( b_{2} = Quot. I iff for A being Subset of (Q. I) holds

( A in b_{2} iff ex u being Element of Q. I st A = QClass. u ) );

for I being non empty non degenerated multLoopStr_0

for b

( b

( A in b

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

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

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;

ex b_{1} being Element of Quot. I st

for z being Element of Q. I holds

( z in b_{1} 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 b_{1}, b_{2} being Element of Quot. I st ( for z being Element of Q. I holds

( z in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for z being Element of Q. I holds

( z in b

( 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

( z in b

( 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

( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * (((a `1) * (b `2)) + ((b `1) * (a `2))) ) ) ) holds

b

proof end;

:: deftheorem Def6 defines qadd QUOFIELD:def 6 :

for I being non degenerated commutative domRing-like Ring

for u, v, b_{4} being Element of Quot. I holds

( b_{4} = qadd (u,v) iff for z being Element of Q. I holds

( z in b_{4} 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 I being non degenerated commutative domRing-like Ring

for u, v, b

( b

( z in b

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

ex b_{1} being Element of Quot. I st

for z being Element of Q. I holds

( z in b_{1} 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 b_{1}, b_{2} being Element of Quot. I st ( for z being Element of Q. I holds

( z in b_{1} 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_{2} 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_{1} = b_{2}

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

ex b

for z being Element of Q. I holds

( z in b

( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) )

proof end;

uniqueness for b

( z in b

( 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

( a in u & b in v & (z `1) * ((a `2) * (b `2)) = (z `2) * ((a `1) * (b `1)) ) ) ) holds

b

proof end;

:: deftheorem Def7 defines qmult QUOFIELD:def 7 :

for I being non degenerated commutative domRing-like Ring

for u, v, b_{4} being Element of Quot. I holds

( b_{4} = qmult (u,v) iff for z being Element of Q. I holds

( z in b_{4} 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 I being non degenerated commutative domRing-like Ring

for u, v, b

( b

( z in b

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

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

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

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;

ex b_{1} being Element of Quot. I st

for z being Element of Q. I holds

( z in b_{1} iff z `1 = 0. I )

for b_{1}, b_{2} being Element of Quot. I st ( for z being Element of Q. I holds

( z in b_{1} iff z `1 = 0. I ) ) & ( for z being Element of Q. I holds

( z in b_{2} iff z `1 = 0. I ) ) holds

b_{1} = b_{2}

end;
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 for z being Element of Q. I holds

( z in it iff z `1 = 0. I );

ex b

for z being Element of Q. I holds

( z in b

proof end;

uniqueness for b

( z in b

( z in b

b

proof end;

:: deftheorem Def8 defines q0. QUOFIELD:def 8 :

for I being non degenerated commutative domRing-like Ring

for b_{2} being Element of Quot. I holds

( b_{2} = q0. I iff for z being Element of Q. I holds

( z in b_{2} iff z `1 = 0. I ) );

for I being non degenerated commutative domRing-like Ring

for b

( b

( z in b

definition

let I be non degenerated commutative domRing-like Ring;

ex b_{1} being Element of Quot. I st

for z being Element of Q. I holds

( z in b_{1} iff z `1 = z `2 )

for b_{1}, b_{2} being Element of Quot. I st ( for z being Element of Q. I holds

( z in b_{1} iff z `1 = z `2 ) ) & ( for z being Element of Q. I holds

( z in b_{2} iff z `1 = z `2 ) ) holds

b_{1} = b_{2}

end;
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 for z being Element of Q. I holds

( z in it iff z `1 = z `2 );

ex b

for z being Element of Q. I holds

( z in b

proof end;

uniqueness for b

( z in b

( z in b

b

proof end;

:: deftheorem Def9 defines q1. QUOFIELD:def 9 :

for I being non degenerated commutative domRing-like Ring

for b_{2} being Element of Quot. I holds

( b_{2} = q1. I iff for z being Element of Q. I holds

( z in b_{2} iff z `1 = z `2 ) );

for I being non degenerated commutative domRing-like Ring

for b

( b

( z in b

definition

let I be non degenerated commutative domRing-like Ring;

let u be Element of Quot. I;

ex b_{1} being Element of Quot. I st

for z being Element of Q. I holds

( z in b_{1} iff ex a being Element of Q. I st

( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )

for b_{1}, b_{2} being Element of Quot. I st ( for z being Element of Q. I holds

( z in b_{1} 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_{2} iff ex a being Element of Q. I st

( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) holds

b_{1} = b_{2}

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

ex b

for z being Element of Q. I holds

( z in b

( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) )

proof end;

uniqueness for b

( z in b

( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) & ( for z being Element of Q. I holds

( z in b

( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) ) holds

b

proof end;

:: deftheorem Def10 defines qaddinv QUOFIELD:def 10 :

for I being non degenerated commutative domRing-like Ring

for u, b_{3} being Element of Quot. I holds

( b_{3} = qaddinv u iff for z being Element of Q. I holds

( z in b_{3} iff ex a being Element of Q. I st

( a in u & (z `1) * (a `2) = (z `2) * (- (a `1)) ) ) );

for I being non degenerated commutative domRing-like Ring

for u, b

( b

( z in b

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

ex b_{1} being Element of Quot. I st

for z being Element of Q. I holds

( z in b_{1} iff ex a being Element of Q. I st

( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) )

for b_{1}, b_{2} being Element of Quot. I st ( for z being Element of Q. I holds

( z in b_{1} 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_{2} iff ex a being Element of Q. I st

( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) holds

b_{1} = b_{2}

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

ex b

for z being Element of Q. I holds

( z in b

( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) )

proof end;

uniqueness for b

( z in b

( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) & ( for z being Element of Q. I holds

( z in b

( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) ) holds

b

proof 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_{3} being Element of Quot. I holds

( b_{3} = qmultinv u iff for z being Element of Q. I holds

( z in b_{3} iff ex a being Element of Q. I st

( a in u & (z `1) * (a `1) = (z `2) * (a `2) ) ) );

for I being non degenerated commutative domRing-like Ring

for u being Element of Quot. I st u <> q0. I holds

for b

( b

( z in b

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

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 )

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

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 )

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

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

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 )

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 )

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;

:: Redefinition of the Operations' Types

definition

let I be non degenerated commutative domRing-like Ring;

ex b_{1} being BinOp of (Quot. I) st

for u, v being Element of Quot. I holds b_{1} . (u,v) = qadd (u,v)

for b_{1}, b_{2} being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b_{1} . (u,v) = qadd (u,v) ) & ( for u, v being Element of Quot. I holds b_{2} . (u,v) = qadd (u,v) ) holds

b_{1} = b_{2}

end;
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 for u, v being Element of Quot. I holds it . (u,v) = qadd (u,v);

ex b

for u, v being Element of Quot. I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def12 defines quotadd QUOFIELD:def 12 :

for I being non degenerated commutative domRing-like Ring

for b_{2} being BinOp of (Quot. I) holds

( b_{2} = quotadd I iff for u, v being Element of Quot. I holds b_{2} . (u,v) = qadd (u,v) );

for I being non degenerated commutative domRing-like Ring

for b

( b

definition

let I be non degenerated commutative domRing-like Ring;

ex b_{1} being BinOp of (Quot. I) st

for u, v being Element of Quot. I holds b_{1} . (u,v) = qmult (u,v)

for b_{1}, b_{2} being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b_{1} . (u,v) = qmult (u,v) ) & ( for u, v being Element of Quot. I holds b_{2} . (u,v) = qmult (u,v) ) holds

b_{1} = b_{2}

end;
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 for u, v being Element of Quot. I holds it . (u,v) = qmult (u,v);

ex b

for u, v being Element of Quot. I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def13 defines quotmult QUOFIELD:def 13 :

for I being non degenerated commutative domRing-like Ring

for b_{2} being BinOp of (Quot. I) holds

( b_{2} = quotmult I iff for u, v being Element of Quot. I holds b_{2} . (u,v) = qmult (u,v) );

for I being non degenerated commutative domRing-like Ring

for b

( b

definition

let I be non degenerated commutative domRing-like Ring;

ex b_{1} being UnOp of (Quot. I) st

for u being Element of Quot. I holds b_{1} . u = qaddinv u

for b_{1}, b_{2} being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b_{1} . u = qaddinv u ) & ( for u being Element of Quot. I holds b_{2} . u = qaddinv u ) holds

b_{1} = b_{2}

end;
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 for u being Element of Quot. I holds it . u = qaddinv u;

ex b

for u being Element of Quot. I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines quotaddinv QUOFIELD:def 14 :

for I being non degenerated commutative domRing-like Ring

for b_{2} being UnOp of (Quot. I) holds

( b_{2} = quotaddinv I iff for u being Element of Quot. I holds b_{2} . u = qaddinv u );

for I being non degenerated commutative domRing-like Ring

for b

( b

definition

let I be non degenerated commutative domRing-like Ring;

ex b_{1} being UnOp of (Quot. I) st

for u being Element of Quot. I holds b_{1} . u = qmultinv u

for b_{1}, b_{2} being UnOp of (Quot. I) st ( for u being Element of Quot. I holds b_{1} . u = qmultinv u ) & ( for u being Element of Quot. I holds b_{2} . u = qmultinv u ) holds

b_{1} = b_{2}

end;
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 for u being Element of Quot. I holds it . u = qmultinv u;

ex b

for u being Element of Quot. I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines quotmultinv QUOFIELD:def 15 :

for I being non degenerated commutative domRing-like Ring

for b_{2} being UnOp of (Quot. I) holds

( b_{2} = quotmultinv I iff for u being Element of Quot. I holds b_{2} . u = qmultinv u );

for I being non degenerated commutative domRing-like Ring

for b

( b

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

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)

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 )

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

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)

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 )

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

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

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 )

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 )

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;

coherence

doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #) is strict doubleLoopStr ;

;

end;
func the_Field_of_Quotients I -> strict doubleLoopStr equals :: QUOFIELD:def 16

doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #);

correctness doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #);

coherence

doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #) is strict doubleLoopStr ;

;

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

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;

coherence

not the_Field_of_Quotients I is empty ;

end;
coherence

not the_Field_of_Quotients I is empty ;

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

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

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)

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)

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)

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

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;

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

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

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

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;

coherence

the_Field_of_Quotients I is commutative by Lm3;

end;
coherence

the_Field_of_Quotients I is commutative by Lm3;

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;

coherence

the_Field_of_Quotients I is well-unital by Lm4;

end;
coherence

the_Field_of_Quotients I is well-unital by Lm4;

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

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

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;

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;

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;

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 ;

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;

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)

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;

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

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

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

for b_{1} being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr holds

( b_{1} is domRing-like & b_{1} is right_unital )
end;

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

( b

proof end;

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is Abelian & b_{1} is commutative & b_{1} is associative & b_{1} is left_unital & b_{1} is distributive & b_{1} is almost_left_invertible & not b_{1} is degenerated )
end;

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

( b

proof end;

definition

let F be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;

let x, y be Element of F;

correctness

coherence

x * (y ") is Element of F;

;

end;
let x, y be Element of F;

correctness

coherence

x * (y ") is Element of F;

;

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

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)

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)

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;

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

( f is additive & f is multiplicative & f is unity-preserving );

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

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 ;

for b_{1} being Function of R,S st b_{1} is RingHomomorphism holds

( b_{1} is additive & b_{1} is multiplicative & b_{1} is unity-preserving )
by Def18;

for b_{1} being Function of R,S st b_{1} is additive & b_{1} is multiplicative & b_{1} is unity-preserving holds

b_{1} is RingHomomorphism
by Def18;

end;
cluster Function-like quasi_total RingHomomorphism -> unity-preserving multiplicative additive for Element of bool [: the carrier of R, the carrier of S:];

coherence for b

( b

cluster Function-like quasi_total unity-preserving multiplicative additive -> RingHomomorphism for Element of bool [: the carrier of R, the carrier of S:];

coherence for b

b

definition

let R, S be non empty doubleLoopStr ;

let f be Function of R,S;

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

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

( f is RingHomomorphism & f is one-to-one );

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

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

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;
let f be Function of R,S;

synonym embedding f for RingMonomorphism ;

definition

let R, S be non empty doubleLoopStr ;

let f be Function of R,S;

end;
let f be Function of R,S;

attr f is RingIsomorphism means :Def21: :: QUOFIELD:def 21

( f is RingMonomorphism & f is RingEpimorphism );

( f is RingMonomorphism & f is RingEpimorphism );

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

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 ;

for b_{1} being Function of R,S st b_{1} is RingIsomorphism holds

( b_{1} is RingMonomorphism & b_{1} is RingEpimorphism )
by Def21;

for b_{1} being Function of R,S st b_{1} is RingMonomorphism & b_{1} is RingEpimorphism holds

b_{1} is RingIsomorphism
by Def21;

end;
cluster Function-like quasi_total RingIsomorphism -> RingEpimorphism RingMonomorphism for Element of bool [: the carrier of R, the carrier of S:];

coherence for b

( b

cluster Function-like quasi_total RingEpimorphism RingMonomorphism -> RingIsomorphism for Element of bool [: the carrier of R, the carrier of S:];

coherence for b

b

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 )

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

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

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

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;

definition

let R, S be non empty doubleLoopStr ;

end;
pred R is_embedded_in S means :Def22: :: QUOFIELD:def 22

ex f being Function of R,S st f is RingMonomorphism ;

ex f being Function of R,S st f is RingMonomorphism ;

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

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 ;

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

end;
pred R is_ringisomorph_to S means :Def23: :: QUOFIELD:def 23

ex f being Function of R,S st f is RingIsomorphism ;

symmetry ex f being Function of R,S st f is RingIsomorphism ;

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;

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

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 ;

coherence

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

end;
let x, y be Element of I;

assume A1: y <> 0. I ;

coherence

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

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

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;

ex b_{1} being Function of I,(the_Field_of_Quotients I) st

for x being Element of I holds b_{1} . x = QClass. (quotient (x,(1. I)))

for b_{1}, b_{2} being Function of I,(the_Field_of_Quotients I) st ( for x being Element of I holds b_{1} . x = QClass. (quotient (x,(1. I))) ) & ( for x being Element of I holds b_{2} . x = QClass. (quotient (x,(1. I))) ) holds

b_{1} = b_{2}

end;
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 for x being Element of I holds it . x = QClass. (quotient (x,(1. I)));

ex b

for x being Element of I holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def25 defines canHom QUOFIELD:def 25 :

for I being non degenerated commutative domRing-like Ring

for b_{2} being Function of I,(the_Field_of_Quotients I) holds

( b_{2} = canHom I iff for x being Element of I holds b_{2} . x = QClass. (quotient (x,(1. I))) );

for I being non degenerated commutative domRing-like Ring

for b

( b

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;

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

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;

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

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

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

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

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;