begin
definition
let I be non
empty ZeroStr ;
func Q. I -> Subset of
[:the carrier of I,the carrier of I:] means :
Def1:
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 ) )
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
end;
:: deftheorem Def1 defines Q. QUOFIELD:def 1 :
theorem Th1:
theorem Th2:
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 )
;
:: deftheorem defines padd QUOFIELD:def 2 :
:: deftheorem defines pmult QUOFIELD:def 3 :
theorem
canceled;
theorem Th4:
theorem Th5:
:: deftheorem Def4 defines QClass. QUOFIELD:def 4 :
theorem Th6:
:: deftheorem Def5 defines Quot. QUOFIELD:def 5 :
theorem Th7:
theorem Th8:
theorem Th9:
begin
:: deftheorem Def6 defines qadd QUOFIELD:def 6 :
:: deftheorem Def7 defines qmult QUOFIELD:def 7 :
theorem
canceled;
theorem Th11:
theorem Th12:
:: deftheorem Def8 defines q0. QUOFIELD:def 8 :
:: deftheorem Def9 defines q1. QUOFIELD:def 9 :
:: deftheorem Def10 defines qaddinv QUOFIELD:def 10 :
:: deftheorem Def11 defines qmultinv QUOFIELD:def 11 :
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
definition
let I be non
degenerated commutative domRing-like Ring;
func quotadd I -> BinOp of
(Quot. I) means :
Def12:
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
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
end;
:: deftheorem Def12 defines quotadd QUOFIELD:def 12 :
definition
let I be non
degenerated commutative domRing-like Ring;
func quotmult I -> BinOp of
(Quot. I) means :
Def13:
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
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
end;
:: deftheorem Def13 defines quotmult QUOFIELD:def 13 :
:: deftheorem Def14 defines quotaddinv QUOFIELD:def 14 :
:: deftheorem Def15 defines quotmultinv QUOFIELD:def 15 :
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
begin
:: deftheorem defines the_Field_of_Quotients QUOFIELD:def 16 :
theorem
theorem
theorem Th34:
theorem
theorem
theorem
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 )
theorem
theorem
Lm3:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty commutative doubleLoopStr
Lm4:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is well-unital
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem Th48:
theorem Th49:
theorem Th50:
:: deftheorem defines / QUOFIELD:def 17 :
theorem Th51:
theorem Th52:
begin
:: deftheorem QUOFIELD:def 18 :
canceled;
:: deftheorem QUOFIELD:def 19 :
canceled;
:: deftheorem QUOFIELD:def 20 :
canceled;
:: deftheorem Def21 defines RingHomomorphism QUOFIELD:def 21 :
:: deftheorem Def22 defines RingEpimorphism QUOFIELD:def 22 :
:: deftheorem Def23 defines RingMonomorphism QUOFIELD:def 23 :
:: deftheorem Def24 defines RingIsomorphism QUOFIELD:def 24 :
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
:: deftheorem Def25 defines is_embedded_in QUOFIELD:def 25 :
:: deftheorem Def26 defines is_ringisomorph_to QUOFIELD:def 26 :
begin
:: deftheorem Def27 defines quotient QUOFIELD:def 27 :
:: deftheorem Def28 defines canHom QUOFIELD:def 28 :
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem
:: deftheorem Def29 defines has_Field_of_Quotients_Pair QUOFIELD:def 29 :
theorem
theorem