:: QUOFIELD semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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

theorem Th1: :: QUOFIELD:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: QUOFIELD:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty Abelian add-associative associative commutative distributive non degenerated domRing-like doubleLoopStr
for u, v, w being Element of Q. I holds
( padd u,(padd v,w) = padd (padd u,v),w & padd u,v = padd v,u )
proof end;

theorem Th5: :: QUOFIELD:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty Abelian associative commutative non degenerated domRing-like doubleLoopStr
for u, v, w being Element of Q. I holds
( pmult u,(pmult v,w) = pmult (pmult u,v),w & pmult u,v = pmult v,u )
proof end;

definition
let I be non empty Abelian add-associative associative commutative distributive non degenerated 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 by Th4;
end;

definition
let I be non empty Abelian associative commutative non degenerated 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 by Th5;
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 b1 being Subset of (Q. I) st
for z being Element of Q. I holds
( z in b1 iff (z `1 ) * (u `2 ) = (z `2 ) * (u `1 ) )
proof end;
uniqueness
for b1, b2 being Subset of (Q. I) st ( for z being Element of Q. I holds
( z in b1 iff (z `1 ) * (u `2 ) = (z `2 ) * (u `1 ) ) ) & ( for z being Element of Q. I holds
( z in b2 iff (z `1 ) * (u `2 ) = (z `2 ) * (u `1 ) ) ) holds
b1 = b2
proof end;
end;

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

theorem Th6: :: QUOFIELD:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being non empty commutative non degenerated multLoopStr_0
for u being Element of Q. I holds u in QClass. u
proof end;

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

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

theorem Th7: :: QUOFIELD:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u, v being Element of Quot. I st u meets v holds
u = v
proof end;

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

:: deftheorem Def6 defines qadd QUOFIELD:def 6 :
for I being commutative non degenerated domRing-like Ring
for u, v, b4 being Element of Quot. I holds
( b4 = qadd u,v iff for z being Element of Q. I holds
( z in b4 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * (((a `1 ) * (b `2 )) + ((b `1 ) * (a `2 ))) ) ) );

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

:: deftheorem Def7 defines qmult QUOFIELD:def 7 :
for I being commutative non degenerated domRing-like Ring
for u, v, b4 being Element of Quot. I holds
( b4 = qmult u,v iff for z being Element of Q. I holds
( z in b4 iff ex a, b being Element of Q. I st
( a in u & b in v & (z `1 ) * ((a `2 ) * (b `2 )) = (z `2 ) * ((a `1 ) * (b `1 )) ) ) );

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

theorem :: QUOFIELD:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th11: :: QUOFIELD:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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 commutative non degenerated domRing-like Ring;
func q0. I -> Element of Quot. I means :Def8: :: QUOFIELD:def 8
for z being Element of Q. I holds
( z in it iff z `1 = 0. I );
existence
ex b1 being Element of Quot. I st
for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I )
proof end;
uniqueness
for b1, b2 being Element of Quot. I st ( for z being Element of Q. I holds
( z in b1 iff z `1 = 0. I ) ) & ( for z being Element of Q. I holds
( z in b2 iff z `1 = 0. I ) ) holds
b1 = b2
proof end;
end;

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

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

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

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

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

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

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

theorem Th13: :: QUOFIELD:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring holds q1. I <> q0. I
proof end;

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

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

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

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

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

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

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

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

theorem Th22: :: QUOFIELD:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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 commutative non degenerated 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 commutative non degenerated domRing-like Ring holds the_Field_of_Quotients I = doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #);

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

theorem :: QUOFIELD:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring holds
( the carrier of (the_Field_of_Quotients I) = Quot. I & the add of (the_Field_of_Quotients I) = quotadd I & the mult of (the_Field_of_Quotients I) = quotmult I & the Zero of (the_Field_of_Quotients I) = q0. I & the unity of (the_Field_of_Quotients I) = q1. I ) ;

theorem Th33: :: QUOFIELD:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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 Th35: :: QUOFIELD:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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 commutative non degenerated domRing-like Ring
for u, v, w being Element of (the_Field_of_Quotients I) holds (u + v) + w = u + (v + w)
proof end;

Lm3: for I being commutative non degenerated domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u + v = v + u
proof end;

Lm4: for I being commutative non degenerated domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds u + (0. (the_Field_of_Quotients I)) = u
proof end;

Lm5: for I being commutative non degenerated 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 commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients I -> non empty add-associative right_zeroed right_complementable strict ;
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 Lm5;
end;

theorem :: QUOFIELD:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds - u = (quotaddinv I) . u
proof end;

theorem :: QUOFIELD:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u * v = (quotmult I) . u,v ;

Lm6: for I being commutative non degenerated domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u * v = v * u
by Th26;

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

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

Lm8: for I being commutative non degenerated domRing-like Ring
for h, e being Element of (the_Field_of_Quotients I) st e = q1. I holds
( e * h = h & h * e = h )
by Th27;

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

Lm10: for I being commutative non degenerated domRing-like Ring holds 1. (the_Field_of_Quotients I) = q1. I
proof end;

Lm11: for I being commutative non degenerated domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds (1. (the_Field_of_Quotients I)) * u = u
proof end;

registration
let I be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients I -> non empty add-associative right_zeroed right_complementable unital commutative strict ;
coherence
the_Field_of_Quotients I is unital by Lm9;
end;

theorem :: QUOFIELD:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring holds
( 1. (the_Field_of_Quotients I) = q1. I & 0. (the_Field_of_Quotients I) = q0. I ) by Lm10;

theorem :: QUOFIELD:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u, v, w being Element of (the_Field_of_Quotients I) holds (u + v) + w = u + (v + w) by Lm2;

theorem :: QUOFIELD:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u + v = v + u by Lm3;

theorem :: QUOFIELD:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds u + (0. (the_Field_of_Quotients I)) = u by Lm4;

theorem :: QUOFIELD:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: QUOFIELD:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u being Element of (the_Field_of_Quotients I) holds (1. (the_Field_of_Quotients I)) * u = u by Lm11;

theorem :: QUOFIELD:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds u * v = v * u ;

theorem Th47: :: QUOFIELD:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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;

Lm12: for I being commutative non degenerated domRing-like Ring
for u, v, w being Element of (the_Field_of_Quotients I) holds
( u * (v + w) = (u * v) + (u * w) & (u + v) * w = (u * w) + (v * w) )
proof end;

theorem Th49: :: QUOFIELD:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring holds the_Field_of_Quotients I is non empty Abelian add-associative right_zeroed right_complementable unital associative distributive Field-like non degenerated doubleLoopStr
proof end;

registration
let I be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients I -> non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict distributive Field-like non degenerated ;
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 Field-like & not the_Field_of_Quotients I is degenerated ) by Th49;
end;

theorem Th50: :: QUOFIELD:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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 add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated -> non empty add-associative right_zeroed right_complementable associative commutative right_unital distributive left_unital Field-like non degenerated domRing-like doubleLoopStr ;
coherence
for b1 being non empty add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr holds
( b1 is domRing-like & b1 is right_unital )
proof end;
end;

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

definition
let F be non empty associative commutative distributive left_unital Field-like 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 associative commutative distributive left_unital Field-like doubleLoopStr
for x, y being Element of F holds x / y = x * (y " );

theorem Th51: :: QUOFIELD:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being commutative Field-like non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being commutative Field-like non degenerated 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;

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 RingHomomorphism -> additive unity-preserving multiplicative M4(the carrier of R,the carrier of S);
coherence
for b1 being Function of R,S st b1 is RingHomomorphism holds
( b1 is additive & b1 is multiplicative & b1 is unity-preserving ) by Def21;
cluster additive unity-preserving multiplicative -> RingHomomorphism M4(the carrier of R,the carrier of S);
coherence
for b1 being Function of R,S st b1 is additive & b1 is multiplicative & b1 is unity-preserving holds
b1 is RingHomomorphism by 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 f;
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 RingIsomorphism -> RingEpimorphism RingMonomorphism M4(the carrier of R,the carrier of S);
coherence
for b1 being Function of R,S st b1 is RingIsomorphism holds
( b1 is RingMonomorphism & b1 is RingEpimorphism ) by Def24;
cluster RingEpimorphism RingMonomorphism -> RingIsomorphism M4(the carrier of R,the carrier of S);
coherence
for b1 being Function of R,S st b1 is RingMonomorphism & b1 is RingEpimorphism holds
b1 is RingIsomorphism by Def24;
end;

theorem Th53: :: QUOFIELD:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being commutative Field-like non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being commutative Field-like non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being non empty doubleLoopStr holds id R is RingHomomorphism
proof end;

registration
let R be non empty doubleLoopStr ;
cluster id R -> additive unity-preserving multiplicative 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 );

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 commutative non degenerated 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 b1 being Function of I,(the_Field_of_Quotients I) st
for x being Element of I holds b1 . x = QClass. (quotient x,(1. I))
proof end;
uniqueness
for b1, b2 being Function of I,(the_Field_of_Quotients I) st ( for x being Element of I holds b1 . x = QClass. (quotient x,(1. I)) ) & ( for x being Element of I holds b2 . x = QClass. (quotient x,(1. I)) ) holds
b1 = b2
proof end;
end;

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

theorem Th59: :: QUOFIELD:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring holds canHom I is RingHomomorphism
proof end;

theorem Th60: :: QUOFIELD:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring holds canHom I is RingMonomorphism
proof end;

theorem :: QUOFIELD:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring holds I is_embedded_in the_Field_of_Quotients I
proof end;

theorem Th62: :: QUOFIELD:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being commutative Field-like non degenerated domRing-like Ring holds F is_ringisomorph_to the_Field_of_Quotients F
proof end;

registration
let I be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients I -> non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict right-distributive right_unital distributive Field-like non degenerated 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated 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 F' being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for f' being Function of I,F' st f' is RingMonomorphism holds
ex h being Function of F,F' st
( h is RingHomomorphism & h * f = f' & ( for h' being Function of F,F' st h' is RingHomomorphism & h' * f = f' holds
h' = 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 F' being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for f' being Function of I,F' st f' is RingMonomorphism holds
ex h being Function of F,F' st
( h is RingHomomorphism & h * f = f' & ( for h' being Function of F,F' st h' is RingHomomorphism & h' * f = f' holds
h' = h ) ) ) ) );

theorem :: QUOFIELD:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative non degenerated domRing-like Ring ex F being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr ex f being Function of I,F st I has_Field_of_Quotients_Pair F,f
proof end;

theorem :: QUOFIELD:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being commutative domRing-like Ring
for F, F' being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for f being Function of I,F
for f' being Function of I,F' st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F',f' holds
F is_ringisomorph_to F'
proof end;