:: QUOFIELD semantic presentation

definition

let c₁ be non empty ZeroStr ;
func Q. c₁ -> Subset of [:the carrier of a₁,the carrier of a₁:] means :Def1: :: QUOFIELD:def 1
for b₁ being set holds
( b₁ in a₂ iff ex b₂, b₃ being Element of a₁ st
( b₁ = [b₂,b₃] & b₃ <> 0. a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th1: :: QUOFIELD:1

for b₁ being non empty non degenerated multLoopStr_0 holds not Q. b₁ is empty

proof end;

registration

let c₁ be non empty non degenerated multLoopStr_0 ;
cluster Q. a₁ -> non empty ;
coherence by Th1;

end;

theorem Th2: :: QUOFIELD:2

for b₁ being non empty non degenerated multLoopStr_0
for b₂ being Element of Q. b₁ holds b₂ `2 <> 0. b₁

proof end;

Lemma4: for b₁ being non empty non degenerated multLoopStr_0
for b₂ being Element of Q. b₁ holds
( b₂ `1 is Element of b₁ & b₂ `2 is Element of b₁ )
;

definition

let c₁ be non empty non degenerated multLoopStr_0 ;
let c₂ be Element of Q. c₁;
redefine func `1 as c₂ `1 -> Element of a₁;
coherence by Lemma4;
redefine func `2 as c₂ `2 -> Element of a₁;
coherence by Lemma4;

end;

definition

let c₁ be non empty non degenerated domRing-like doubleLoopStr ;
let c₂, c₃ be Element of Q. c₁;
func padd c₂,c₃ -> Element of Q. a₁ equals :: QUOFIELD:def 2
[(((a₂ `1 ) * (a₃ `2 )) + ((a₃ `1 ) * (a₂ `2 ))),((a₂ `2 ) * (a₃ `2 ))];
coherence

proof end;

end;

:: deftheorem Def2 defines padd QUOFIELD:def 2 :

definition

let c₁ be non empty non degenerated domRing-like doubleLoopStr ;
let c₂, c₃ be Element of Q. c₁;
func pmult c₂,c₃ -> Element of Q. a₁ equals :: QUOFIELD:def 3
[((a₂ `1 ) * (a₃ `1 )),((a₂ `2 ) * (a₃ `2 ))];
coherence

proof end;

end;

:: deftheorem Def3 defines pmult QUOFIELD:def 3 :

theorem Th3: :: QUOFIELD:3

canceled;

theorem Th4: :: QUOFIELD:4

for b₁ being non empty Abelian add-associative associative commutative distributive non degenerated domRing-like doubleLoopStr
for b₂, b₃, b₄ being Element of Q. b₁ holds
( padd b₂,(padd b₃,b₄) = padd (padd b₂,b₃),b₄ & padd b₂,b₃ = padd b₃,b₂ )

proof end;

theorem Th5: :: QUOFIELD:5

for b₁ being non empty Abelian associative commutative non degenerated domRing-like doubleLoopStr
for b₂, b₃, b₄ being Element of Q. b₁ holds
( pmult b₂,(pmult b₃,b₄) = pmult (pmult b₂,b₃),b₄ & pmult b₂,b₃ = pmult b₃,b₂ )

proof end;

definition

let c₁ be non empty Abelian add-associative associative commutative distributive non degenerated domRing-like doubleLoopStr ;
let c₂, c₃ be Element of Q. c₁;
redefine func padd as padd c₂,c₃ -> Element of Q. a₁;
commutativity by Th4;

end;

definition

let c₁ be non empty Abelian associative commutative non degenerated domRing-like doubleLoopStr ;
let c₂, c₃ be Element of Q. c₁;
redefine func pmult as pmult c₂,c₃ -> Element of Q. a₁;
commutativity by Th5;

end;

definition

let c₁ be non empty non degenerated multLoopStr_0 ;
let c₂ be Element of Q. c₁;
func QClass. c₂ -> Subset of (Q. a₁) means :Def4: :: QUOFIELD:def 4
for b₁ being Element of Q. a₁ holds
( b₁ in a₃ iff (b₁ `1 ) * (a₂ `2 ) = (b₁ `2 ) * (a₂ `1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines QClass. QUOFIELD:def 4 :

theorem Th6: :: QUOFIELD:6

for b₁ being non empty commutative non degenerated multLoopStr_0
for b₂ being Element of Q. b₁ holds b₂ in QClass. b₂

proof end;

registration

let c₁ be non empty commutative non degenerated multLoopStr_0 ;
let c₂ be Element of Q. c₁;
cluster QClass. a₂ -> non empty ;
coherence by Th6;

end;

definition

let c₁ be non empty non degenerated multLoopStr_0 ;
func Quot. c₁ -> Subset-Family of (Q. a₁) means :Def5: :: QUOFIELD:def 5
for b₁ being Subset of (Q. a₁) holds
( b₁ in a₂ iff ex b₂ being Element of Q. a₁ st b₁ = QClass. b₂ );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th7: :: QUOFIELD:7

for b₁ being non empty non degenerated multLoopStr_0 holds not Quot. b₁ is empty

proof end;

registration

let c₁ be non empty non degenerated multLoopStr_0 ;
cluster Quot. a₁ -> non empty ;
coherence by Th7;

end;

theorem Th8: :: QUOFIELD:8

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of Q. b₁ st ex b₄ being Element of Quot. b₁ st
( b₂ in b₄ & b₃ in b₄ ) holds
(b₂ `1 ) * (b₃ `2 ) = (b₃ `1 ) * (b₂ `2 )

proof end;

theorem Th9: :: QUOFIELD:9

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of Quot. b₁ st b₂ meets b₃ holds
b₂ = b₃

proof end;

definition

let c₁ be commutative non degenerated domRing-like Ring;
let c₂, c₃ be Element of Quot. c₁;
func qadd c₂,c₃ -> Element of Quot. a₁ means :Def6: :: QUOFIELD:def 6
for b₁ being Element of Q. a₁ holds
( b₁ in a₄ iff ex b₂, b₃ being Element of Q. a₁ st
( b₂ in a₂ & b₃ in a₃ & (b₁ `1 ) * ((b₂ `2 ) * (b₃ `2 )) = (b₁ `2 ) * (((b₂ `1 ) * (b₃ `2 )) + ((b₃ `1 ) * (b₂ `2 ))) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines qadd QUOFIELD:def 6 :

definition

let c₁ be commutative non degenerated domRing-like Ring;
let c₂, c₃ be Element of Quot. c₁;
func qmult c₂,c₃ -> Element of Quot. a₁ means :Def7: :: QUOFIELD:def 7
for b₁ being Element of Q. a₁ holds
( b₁ in a₄ iff ex b₂, b₃ being Element of Q. a₁ st
( b₂ in a₂ & b₃ in a₃ & (b₁ `1 ) * ((b₂ `2 ) * (b₃ `2 )) = (b₁ `2 ) * ((b₂ `1 ) * (b₃ `1 )) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines qmult QUOFIELD:def 7 :

definition

let c₁ be non empty non degenerated multLoopStr_0 ;
let c₂ be Element of Q. c₁;
redefine func QClass. as QClass. c₂ -> Element of Quot. a₁;
coherence by Def5;

end;

theorem Th10: :: QUOFIELD:10

canceled;

theorem Th11: :: QUOFIELD:11

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of Q. b₁ holds qadd (QClass. b₂),(QClass. b₃) = QClass. (padd b₂,b₃)

proof end;

theorem Th12: :: QUOFIELD:12

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of Q. b₁ holds qmult (QClass. b₂),(QClass. b₃) = QClass. (pmult b₂,b₃)

proof end;

definition

let c₁ be commutative non degenerated domRing-like Ring;
func q0. c₁ -> Element of Quot. a₁ means :Def8: :: QUOFIELD:def 8
for b₁ being Element of Q. a₁ holds
( b₁ in a₂ iff b₁ `1 = 0. a₁ );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be commutative non degenerated domRing-like Ring;
func q1. c₁ -> Element of Quot. a₁ means :Def9: :: QUOFIELD:def 9
for b₁ being Element of Q. a₁ holds
( b₁ in a₂ iff b₁ `1 = b₁ `2 );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be commutative non degenerated domRing-like Ring;
let c₂ be Element of Quot. c₁;
func qaddinv c₂ -> Element of Quot. a₁ means :Def10: :: QUOFIELD:def 10
for b₁ being Element of Q. a₁ holds
( b₁ in a₃ iff ex b₂ being Element of Q. a₁ st
( b₂ in a₂ & (b₁ `1 ) * (b₂ `2 ) = (b₁ `2 ) * (- (b₂ `1 )) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines qaddinv QUOFIELD:def 10 :

definition

let c₁ be commutative non degenerated domRing-like Ring;
let c₂ be Element of Quot. c₁;
assume E20: c₂ <> q0. c₁ ;
func qmultinv c₂ -> Element of Quot. a₁ means :Def11: :: QUOFIELD:def 11
for b₁ being Element of Q. a₁ holds
( b₁ in a₃ iff ex b₂ being Element of Q. a₁ st
( b₂ in a₂ & (b₁ `1 ) * (b₂ `1 ) = (b₁ `2 ) * (b₂ `2 ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines qmultinv QUOFIELD:def 11 :

theorem Th13: :: QUOFIELD:13

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds
( qadd b₂,(qadd b₃,b₄) = qadd (qadd b₂,b₃),b₄ & qadd b₂,b₃ = qadd b₃,b₂ )

proof end;

theorem Th14: :: QUOFIELD:14

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ holds
( qadd b₂,(q0. b₁) = b₂ & qadd (q0. b₁),b₂ = b₂ )

proof end;

theorem Th15: :: QUOFIELD:15

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds
( qmult b₂,(qmult b₃,b₄) = qmult (qmult b₂,b₃),b₄ & qmult b₂,b₃ = qmult b₃,b₂ )

proof end;

theorem Th16: :: QUOFIELD:16

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ holds
( qmult b₂,(q1. b₁) = b₂ & qmult (q1. b₁),b₂ = b₂ )

proof end;

theorem Th17: :: QUOFIELD:17

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds qmult (qadd b₂,b₃),b₄ = qadd (qmult b₂,b₄),(qmult b₃,b₄)

proof end;

theorem Th18: :: QUOFIELD:18

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds qmult b₂,(qadd b₃,b₄) = qadd (qmult b₂,b₃),(qmult b₂,b₄)

proof end;

theorem Th19: :: QUOFIELD:19

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ holds
( qadd b₂,(qaddinv b₂) = q0. b₁ & qadd (qaddinv b₂),b₂ = q0. b₁ )

proof end;

theorem Th20: :: QUOFIELD:20

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ st b₂ <> q0. b₁ holds
( qmult b₂,(qmultinv b₂) = q1. b₁ & qmult (qmultinv b₂),b₂ = q1. b₁ )

proof end;

theorem Th21: :: QUOFIELD:21

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

proof end;

definition

let c₁ be commutative non degenerated domRing-like Ring;
func quotadd c₁ -> BinOp of Quot. a₁ means :Def12: :: QUOFIELD:def 12
for b₁, b₂ being Element of Quot. a₁ holds a₂ . b₁,b₂ = qadd b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines quotadd QUOFIELD:def 12 :

definition

let c₁ be commutative non degenerated domRing-like Ring;
func quotmult c₁ -> BinOp of Quot. a₁ means :Def13: :: QUOFIELD:def 13
for b₁, b₂ being Element of Quot. a₁ holds a₂ . b₁,b₂ = qmult b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines quotmult QUOFIELD:def 13 :

definition

let c₁ be commutative non degenerated domRing-like Ring;
func quotaddinv c₁ -> UnOp of Quot. a₁ means :Def14: :: QUOFIELD:def 14
for b₁ being Element of Quot. a₁ holds a₂ . b₁ = qaddinv b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines quotaddinv QUOFIELD:def 14 :

definition

let c₁ be commutative non degenerated domRing-like Ring;
func quotmultinv c₁ -> UnOp of Quot. a₁ means :Def15: :: QUOFIELD:def 15
for b₁ being Element of Quot. a₁ holds a₂ . b₁ = qmultinv b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines quotmultinv QUOFIELD:def 15 :

theorem Th22: :: QUOFIELD:22

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds (quotadd b₁) . ((quotadd b₁) . b₂,b₃),b₄ = (quotadd b₁) . b₂,((quotadd b₁) . b₃,b₄)

proof end;

theorem Th23: :: QUOFIELD:23

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of Quot. b₁ holds (quotadd b₁) . b₂,b₃ = (quotadd b₁) . b₃,b₂

proof end;

theorem Th24: :: QUOFIELD:24

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ holds
( (quotadd b₁) . b₂,(q0. b₁) = b₂ & (quotadd b₁) . (q0. b₁),b₂ = b₂ )

proof end;

theorem Th25: :: QUOFIELD:25

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds (quotmult b₁) . ((quotmult b₁) . b₂,b₃),b₄ = (quotmult b₁) . b₂,((quotmult b₁) . b₃,b₄)

proof end;

theorem Th26: :: QUOFIELD:26

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of Quot. b₁ holds (quotmult b₁) . b₂,b₃ = (quotmult b₁) . b₃,b₂

proof end;

theorem Th27: :: QUOFIELD:27

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ holds
( (quotmult b₁) . b₂,(q1. b₁) = b₂ & (quotmult b₁) . (q1. b₁),b₂ = b₂ )

proof end;

theorem Th28: :: QUOFIELD:28

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds (quotmult b₁) . ((quotadd b₁) . b₂,b₃),b₄ = (quotadd b₁) . ((quotmult b₁) . b₂,b₄),((quotmult b₁) . b₃,b₄)

proof end;

theorem Th29: :: QUOFIELD:29

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of Quot. b₁ holds (quotmult b₁) . b₂,((quotadd b₁) . b₃,b₄) = (quotadd b₁) . ((quotmult b₁) . b₂,b₃),((quotmult b₁) . b₂,b₄)

proof end;

theorem Th30: :: QUOFIELD:30

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ holds
( (quotadd b₁) . b₂,((quotaddinv b₁) . b₂) = q0. b₁ & (quotadd b₁) . ((quotaddinv b₁) . b₂),b₂ = q0. b₁ )

proof end;

theorem Th31: :: QUOFIELD:31

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of Quot. b₁ st b₂ <> q0. b₁ holds
( (quotmult b₁) . b₂,((quotmultinv b₁) . b₂) = q1. b₁ & (quotmult b₁) . ((quotmultinv b₁) . b₂),b₂ = q1. b₁ )

proof end;

definition

let c₁ be commutative non degenerated domRing-like Ring;
func the_Field_of_Quotients c₁ -> strict doubleLoopStr equals :: QUOFIELD:def 16
doubleLoopStr(# (Quot. a₁),(quotadd a₁),(quotmult a₁),(q1. a₁),(q0. a₁) #);
correctness ;

end;

:: deftheorem Def16 defines the_Field_of_Quotients QUOFIELD:def 16 :

registration

let c₁ be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th32: :: QUOFIELD:32

for b₁ being commutative non degenerated domRing-like Ring holds
( the carrier of (the_Field_of_Quotients b₁) = Quot. b₁ & the add of (the_Field_of_Quotients b₁) = quotadd b₁ & the mult of (the_Field_of_Quotients b₁) = quotmult b₁ & the Zero of (the_Field_of_Quotients b₁) = q0. b₁ & the unity of (the_Field_of_Quotients b₁) = q1. b₁ ) ;

theorem Th33: :: QUOFIELD:33

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds (quotadd b₁) . b₂,b₃ is Element of (the_Field_of_Quotients b₁)

proof end;

theorem Th34: :: QUOFIELD:34

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) holds (quotaddinv b₁) . b₂ is Element of (the_Field_of_Quotients b₁)

proof end;

theorem Th35: :: QUOFIELD:35

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds (quotmult b₁) . b₂,b₃ is Element of (the_Field_of_Quotients b₁)

proof end;

theorem Th36: :: QUOFIELD:36

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) holds (quotmultinv b₁) . b₂ is Element of (the_Field_of_Quotients b₁)

proof end;

theorem Th37: :: QUOFIELD:37

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds b₂ + b₃ = (quotadd b₁) . b₂,b₃ ;

Lemma47: for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of (the_Field_of_Quotients b₁) holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

Lemma48: for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds b₂ + b₃ = b₃ + b₂

proof end;

Lemma49: for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) holds b₂ + (0. (the_Field_of_Quotients b₁)) = b₂

proof end;

Lemma50: for b₁ being commutative non degenerated domRing-like Ring holds
( the_Field_of_Quotients b₁ is add-associative & the_Field_of_Quotients b₁ is right_zeroed & the_Field_of_Quotients b₁ is right_complementable )

proof end;

registration

let c₁ be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients a₁ -> non empty add-associative right_zeroed right_complementable strict ;
coherence by Lemma50;

end;

theorem Th38: :: QUOFIELD:38

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) holds - b₂ = (quotaddinv b₁) . b₂

proof end;

theorem Th39: :: QUOFIELD:39

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds b₂ * b₃ = (quotmult b₁) . b₂,b₃ ;

Lemma51: for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds b₂ * b₃ = b₃ * b₂
by Th26;

Lemma52: for b₁ being commutative non degenerated domRing-like Ring holds the_Field_of_Quotients b₁ is non empty commutative doubleLoopStr

proof end;

registration

let c₁ be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients a₁ -> non empty add-associative right_zeroed right_complementable commutative strict ;
coherence by Lemma52;

end;

Lemma53: for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) st b₃ = q1. b₁ holds
( b₃ * b₂ = b₂ & b₂ * b₃ = b₂ )
by Th27;

Lemma54: for b₁ being commutative non degenerated domRing-like Ring holds the_Field_of_Quotients b₁ is unital

proof end;

Lemma55: for b₁ being commutative non degenerated domRing-like Ring holds 1. (the_Field_of_Quotients b₁) = q1. b₁

proof end;

Lemma56: for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) holds (1. (the_Field_of_Quotients b₁)) * b₂ = b₂

proof end;

registration

let c₁ be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients a₁ -> non empty add-associative right_zeroed right_complementable unital commutative strict ;
coherence by Lemma54;

end;

theorem Th40: :: QUOFIELD:40

for b₁ being commutative non degenerated domRing-like Ring holds
( 1. (the_Field_of_Quotients b₁) = q1. b₁ & 0. (the_Field_of_Quotients b₁) = q0. b₁ ) by Lemma55;

theorem Th41: :: QUOFIELD:41

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of (the_Field_of_Quotients b₁) holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) by Lemma47;

theorem Th42: :: QUOFIELD:42

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds b₂ + b₃ = b₃ + b₂ by Lemma48;

theorem Th43: :: QUOFIELD:43

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) holds b₂ + (0. (the_Field_of_Quotients b₁)) = b₂ by Lemma49;

theorem Th44: :: QUOFIELD:44

canceled;

theorem Th45: :: QUOFIELD:45

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) holds (1. (the_Field_of_Quotients b₁)) * b₂ = b₂ by Lemma56;

theorem Th46: :: QUOFIELD:46

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃ being Element of (the_Field_of_Quotients b₁) holds b₂ * b₃ = b₃ * b₂ ;

theorem Th47: :: QUOFIELD:47

for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of (the_Field_of_Quotients b₁) holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) by Th25;

theorem Th48: :: QUOFIELD:48

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) st b₂ <> 0. (the_Field_of_Quotients b₁) holds
ex b₃ being Element of (the_Field_of_Quotients b₁) st b₂ * b₃ = 1. (the_Field_of_Quotients b₁)

proof end;

Lemma59: for b₁ being commutative non degenerated domRing-like Ring
for b₂, b₃, b₄ being Element of (the_Field_of_Quotients b₁) holds
( b₂ * (b₃ + b₄) = (b₂ * b₃) + (b₂ * b₄) & (b₂ + b₃) * b₄ = (b₂ * b₄) + (b₃ * b₄) )

proof end;

theorem Th49: :: QUOFIELD:49

for b₁ being commutative non degenerated domRing-like Ring holds the_Field_of_Quotients b₁ is non empty Abelian add-associative right_zeroed right_complementable unital associative distributive Field-like non degenerated doubleLoopStr

proof end;

registration

let c₁ be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients a₁ -> non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict distributive Field-like non degenerated ;
coherence by Th49;

end;

theorem Th50: :: QUOFIELD:50

for b₁ being commutative non degenerated domRing-like Ring
for b₂ being Element of (the_Field_of_Quotients b₁) st b₂ <> 0. (the_Field_of_Quotients b₁) holds
for b₃ being Element of b₁ st b₃ <> 0. b₁ holds
for b₄ being Element of Q. b₁ st b₂ = QClass. b₄ & b₄ = [b₃,(1. b₁)] holds
for b₅ being Element of Q. b₁ st b₅ = [(1. b₁),b₃] holds
b₂ " = QClass. b₅

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

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

proof end;

end;

definition

let c₁ be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let c₂, c₃ be Element of c₁;
func c₂ / c₃ -> Element of a₁ equals :: QUOFIELD:def 17
a₂ * (a₃ " );
correctness ;

end;

:: deftheorem Def17 defines / QUOFIELD:def 17 :

theorem Th51: :: QUOFIELD:51

for b₁ being commutative Field-like non degenerated Ring
for b₂, b₃, b₄, b₅ being Element of b₁ st b₃ <> 0. b₁ & b₅ <> 0. b₁ holds
(b₂ / b₃) * (b₄ / b₅) = (b₂ * b₄) / (b₃ * b₅)

proof end;

theorem Th52: :: QUOFIELD:52

for b₁ being commutative Field-like non degenerated Ring
for b₂, b₃, b₄, b₅ being Element of b₁ st b₃ <> 0. b₁ & b₅ <> 0. b₁ holds
(b₂ / b₃) + (b₄ / b₅) = ((b₂ * b₅) + (b₄ * b₃)) / (b₃ * b₅)

proof end;

definition

let c₁, c₂ be non empty doubleLoopStr ;
let c₃ be Function of c₁,c₂;
canceled;
canceled;
canceled;
attr a₃ is RingHomomorphism means :Def21: :: QUOFIELD:def 21
( a₃ is additive & a₃ is multiplicative & a₃ is unity-preserving );

end;

:: deftheorem Def18 QUOFIELD:def 18 :

:: deftheorem Def19 QUOFIELD:def 19 :

:: deftheorem Def20 QUOFIELD:def 20 :

:: deftheorem Def21 defines RingHomomorphism QUOFIELD:def 21 :

registration

let c₁, c₂ be non empty doubleLoopStr ;
cluster RingHomomorphism -> additive unity-preserving multiplicative M4(the carrier of a₁,the carrier of a₂);
coherence by Def21;
cluster additive unity-preserving multiplicative -> RingHomomorphism M4(the carrier of a₁,the carrier of a₂);
coherence by Def21;

end;

definition

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

end;

:: deftheorem Def22 defines RingEpimorphism QUOFIELD:def 22 :

:: deftheorem Def23 defines RingMonomorphism QUOFIELD:def 23 :

notation

let c₁, c₂ be non empty doubleLoopStr ;
let c₃ be Function of c₁,c₂;
synonym embedding c₃ for RingMonomorphism c₃;

end;

definition

let c₁, c₂ be non empty doubleLoopStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is RingIsomorphism means :Def24: :: QUOFIELD:def 24
( a₃ is RingMonomorphism & a₃ is RingEpimorphism );

end;

:: deftheorem Def24 defines RingIsomorphism QUOFIELD:def 24 :

registration

let c₁, c₂ be non empty doubleLoopStr ;
cluster RingIsomorphism -> RingEpimorphism RingMonomorphism M4(the carrier of a₁,the carrier of a₂);
coherence by Def24;
cluster RingEpimorphism RingMonomorphism -> RingIsomorphism M4(the carrier of a₁,the carrier of a₂);
coherence by Def24;

end;

theorem Th53: :: QUOFIELD:53

for b₁, b₂ being Ring
for b₃ being Function of b₁,b₂ st b₃ is RingHomomorphism holds
b₃ . (0. b₁) = 0. b₂

proof end;

theorem Th54: :: QUOFIELD:54

for b₁, b₂ being Ring
for b₃ being Function of b₁,b₂ st b₃ is RingMonomorphism holds
for b₄ being Element of b₁ holds
( b₃ . b₄ = 0. b₂ iff b₄ = 0. b₁ )

proof end;

theorem Th55: :: QUOFIELD:55

for b₁, b₂ being commutative Field-like non degenerated Ring
for b₃ being Function of b₁,b₂ st b₃ is RingHomomorphism holds
for b₄ being Element of b₁ st b₄ <> 0. b₁ holds
b₃ . (b₄ " ) = (b₃ . b₄) "

proof end;

theorem Th56: :: QUOFIELD:56

for b₁, b₂ being commutative Field-like non degenerated Ring
for b₃ being Function of b₁,b₂ st b₃ is RingHomomorphism holds
for b₄, b₅ being Element of b₁ st b₅ <> 0. b₁ holds
b₃ . (b₄ * (b₅ " )) = (b₃ . b₄) * ((b₃ . b₅) " )

proof end;

theorem Th57: :: QUOFIELD:57

for b₁, b₂, b₃ being Ring
for b₄ being Function of b₁,b₂ st b₄ is RingHomomorphism holds
for b₅ being Function of b₂,b₃ st b₅ is RingHomomorphism holds
b₅ * b₄ is RingHomomorphism

proof end;

theorem Th58: :: QUOFIELD:58

for b₁ being non empty doubleLoopStr holds id b₁ is RingHomomorphism

proof end;

registration

let c₁ be non empty doubleLoopStr ;
cluster id a₁ -> additive unity-preserving multiplicative RingHomomorphism ;
coherence by Th58;

end;

definition

let c₁, c₂ be non empty doubleLoopStr ;
pred c₁ is_embedded_in c₂ means :Def25: :: QUOFIELD:def 25
ex b₁ being Function of a₁,a₂ st b₁ is RingMonomorphism;

end;

:: deftheorem Def25 defines is_embedded_in QUOFIELD:def 25 :

definition

let c₁, c₂ be non empty doubleLoopStr ;
pred c₁ is_ringisomorph_to c₂ means :Def26: :: QUOFIELD:def 26
ex b₁ being Function of a₁,a₂ st b₁ is RingIsomorphism;
symmetry

proof end;

end;

:: deftheorem Def26 defines is_ringisomorph_to QUOFIELD:def 26 :

definition

let c₁ be non empty ZeroStr ;
let c₂, c₃ be Element of c₁;
assume E76: c₃ <> 0. c₁ ;
func quotient c₂,c₃ -> Element of Q. a₁ equals :Def27: :: QUOFIELD:def 27
[a₂,a₃];
coherence by E76, Def1;

end;

:: deftheorem Def27 defines quotient QUOFIELD:def 27 :

definition

let c₁ be commutative non degenerated domRing-like Ring;
func canHom c₁ -> Function of a₁,(the_Field_of_Quotients a₁) means :Def28: :: QUOFIELD:def 28
for b₁ being Element of a₁ holds a₂ . b₁ = QClass. (quotient b₁,(1. a₁));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def28 defines canHom QUOFIELD:def 28 :

theorem Th59: :: QUOFIELD:59

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

proof end;

theorem Th60: :: QUOFIELD:60

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

proof end;

theorem Th61: :: QUOFIELD:61

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

proof end;

theorem Th62: :: QUOFIELD:62

for b₁ being commutative Field-like non degenerated domRing-like Ring holds b₁ is_ringisomorph_to the_Field_of_Quotients b₁

proof end;

registration

let c₁ be commutative non degenerated domRing-like Ring;
cluster the_Field_of_Quotients a₁ -> 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 ;

end;

theorem Th63: :: QUOFIELD:63

for b₁ being commutative non degenerated domRing-like Ring holds the_Field_of_Quotients (the_Field_of_Quotients b₁) is_ringisomorph_to the_Field_of_Quotients b₁ by Th62;

definition

let c₁, c₂ be non empty doubleLoopStr ;
let c₃ be Function of c₁,c₂;
pred c₁ has_Field_of_Quotients_Pair c₂,c₃ means :Def29: :: QUOFIELD:def 29
( a₃ is RingMonomorphism & ( for b₁ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for b₂ being Function of a₁,b₁ st b₂ is RingMonomorphism holds
ex b₃ being Function of a₂,b₁ st
( b₃ is RingHomomorphism & b₃ * a₃ = b₂ & ( for b₄ being Function of a₂,b₁ st b₄ is RingHomomorphism & b₄ * a₃ = b₂ holds
b₄ = b₃ ) ) ) );

end;

:: deftheorem Def29 defines has_Field_of_Quotients_Pair QUOFIELD:def 29 :

theorem Th64: :: QUOFIELD:64

for b₁ being commutative non degenerated domRing-like Ring ex b₂ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr ex b₃ being Function of b₁,b₂ st b₁ has_Field_of_Quotients_Pair b₂,b₃

proof end;

theorem Th65: :: QUOFIELD:65

for b₁ being commutative domRing-like Ring
for b₂, b₃ being non empty Abelian add-associative right_zeroed right_complementable associative commutative distributive left_unital Field-like non degenerated doubleLoopStr
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st b₁ has_Field_of_Quotients_Pair b₂,b₄ & b₁ has_Field_of_Quotients_Pair b₃,b₅ holds
b₂ is_ringisomorph_to b₃

proof end;