let I be non degenerated commutative domRing-like Ring; :: thesis:

let F9 be non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; :: thesis:
let f9 be Function of I,F9; :: thesis:
set hh = { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } ;
A2: for u being object st u in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } holds
ex a, b being object st u = [a,b]

let u be object ; :: thesis:
assume u in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } ; :: thesis:
then ex a, b being Element of I st
( u = [[a,b],((f9 . a) * ((f9 . b) "))] & b <> 0. I ) ;
hence ex a, b being object st u = [a,b] ; :: thesis:

end;

for a, b1, b2 being object st [a,b1] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } & [a,b2] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } holds
b1 = b2

proof

let a, b1, b2 be object ; :: thesis:
assume that
A3: [a,b1] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } and
A4: [a,b2] in { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } ; :: thesis:
consider x1, x2 being Element of I such that
A5: [a,b1] = [[x1,x2],((f9 . x1) * ((f9 . x2) "))] and
x2 <> 0. I by A3;
consider y1, y2 being Element of I such that
A6: [a,b2] = [[y1,y2],((f9 . y1) * ((f9 . y2) "))] and
y2 <> 0. I by A4;
A7: a = [y1,y2] by A6, XTUPLE_0:1;
A8: a = [x1,x2] by A5, XTUPLE_0:1;
then A9: x2 = y2 by A7, XTUPLE_0:1;
x1 = y1 by A7, A8, XTUPLE_0:1;
then b1 = b2 by A5, A6, A9, XTUPLE_0:1;
hence b1 = b2 ; :: thesis:

end;

then reconsider hh = { [[a,b],((f9 . a) * ((f9 . b) "))] where a, b is Element of I : b <> 0. I } as Function by A2, FUNCT_1:def 1, RELAT_1:def 1;
A10: for x being object st x in dom hh holds
x in Q. I

proof

let x be object ; :: thesis:
assume x in dom hh ; :: thesis:
then consider y being object such that
A11: [x,y] in hh by XTUPLE_0:def 12;
consider a, b being Element of I such that
A12: [x,y] = [[a,b],((f9 . a) * ((f9 . b) "))] and
A13: b <> 0. I by A11;
x = [a,b] by A12, XTUPLE_0:1;
hence x in Q. I by A13, Def1; :: thesis:

end;

for x being object st x in Q. I holds
x in dom hh

proof

let x be object ; :: thesis:
assume x in Q. I ; :: thesis:
then consider a, b being Element of I such that
A14: x = [a,b] and
A15: b <> 0. I by Def1;
[[a,b],((f9 . a) * ((f9 . b) "))] in hh by A15;
hence x in dom hh by A14, XTUPLE_0:def 12; :: thesis:

end;

then A16: dom hh = Q. I by A10, TARSKI:2;
for y being object st y in rng hh holds
y in the carrier of F9

proof

let y be object ; :: thesis:
assume y in rng hh ; :: thesis:
then consider x being object such that
A17: [x,y] in hh by XTUPLE_0:def 13;
consider a, b being Element of I such that
A18: [x,y] = [[a,b],((f9 . a) * ((f9 . b) "))] and
b <> 0. I by A17;
y = (f9 . a) * ((f9 . b) ") by A18, XTUPLE_0:1;
hence y in the carrier of F9 ; :: thesis:

end;

then rng hh c= the carrier of F9 by TARSKI:def 3;
then reconsider hh = hh as Function of (Q. I), the carrier of F9 by A16, FUNCT_2:def 1, RELSET_1:4;
set h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ;
( 0. F9 <> 1. F9 & (1. F9) * (1. F9) = 1. F9 ) ;
then A19: (1. F9) " = 1. F9 by VECTSP_1:def 10;
assume A20: f9 is RingMonomorphism ; :: thesis:
then A21: f9 is RingHomomorphism ;
A22: for v being object st v in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } holds
ex a, b being object st v = [a,b]

proof

let v be object ; :: thesis:
assume v in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ; :: thesis:
then ex u being Element of Q. I st
( v = [(QClass. u),(hh . u)] & 1. I = 1. I ) ;
hence ex a, b being object st v = [a,b] ; :: thesis:

end;

A23: for x being Element of Q. I holds hh . x = (f9 . (x `1)) * ((f9 . (x `2)) ")

proof

let x be Element of Q. I; :: thesis:
consider a, b being Element of I such that
A24: x = [a,b] and
A25: b <> 0. I by Def1;
A26: [[a,b],((f9 . a) * ((f9 . b) "))] in hh by A25;
thus hh . x = (f9 . (x `1)) * ((f9 . (x `2)) ") by A16, A24, A26, FUNCT_1:def 2; :: thesis:

end;

for a, b1, b2 being object st [a,b1] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } & [a,b2] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } holds
b1 = b2

proof

let a, b1, b2 be object ; :: thesis:
assume that
A27: [a,b1] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } and
A28: [a,b2] in { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } ; :: thesis:
consider u1 being Element of Q. I such that
A29: [a,b1] = [(QClass. u1),(hh . u1)] and
1. I = 1. I by A27;
consider u2 being Element of Q. I such that
A30: [a,b2] = [(QClass. u2),(hh . u2)] and
1. I = 1. I by A28;
A31: a = QClass. u2 by A30, XTUPLE_0:1;
a = QClass. u1 by A29, XTUPLE_0:1;
then u1 in QClass. u2 by A31, Th5;
then A32: (u1 `1) * (u2 `2) = (u1 `2) * (u2 `1) by Def4;
u1 `2 <> 0. I by Th2;
then A33: f9 . (u1 `2) <> 0. F9 by A20, Th51;
u2 `2 <> 0. I by Th2;
then A34: f9 . (u2 `2) <> 0. F9 by A20, Th51;
A35: f9 is RingHomomorphism by A20;
A36: hh . u1 = (f9 . (u1 `1)) / (f9 . (u1 `2)) by A23
.= ((f9 . (u1 `1)) / (f9 . (u1 `2))) * (1. F9)
.= ((f9 . (u1 `1)) / (f9 . (u1 `2))) * ((f9 . (u2 `2)) / (f9 . (u2 `2))) by A34, VECTSP_1:def 10
.= ((f9 . (u1 `1)) * (f9 . (u2 `2))) / ((f9 . (u1 `2)) * (f9 . (u2 `2))) by A33, A34, Th48
.= (f9 . ((u1 `2) * (u2 `1))) / ((f9 . (u1 `2)) * (f9 . (u2 `2))) by A32, A35, GROUP_6:def 6
.= ((f9 . (u1 `2)) * (f9 . (u2 `1))) / ((f9 . (u1 `2)) * (f9 . (u2 `2))) by A35, GROUP_6:def 6
.= ((f9 . (u1 `2)) / (f9 . (u1 `2))) * ((f9 . (u2 `1)) / (f9 . (u2 `2))) by A33, A34, Th48
.= (1. F9) * ((f9 . (u2 `1)) * ((f9 . (u2 `2)) ")) by A33, VECTSP_1:def 10
.= (f9 . (u2 `1)) * ((f9 . (u2 `2)) ")
.= hh . u2 by A23 ;
b1 = hh . u2 by A36, A29, XTUPLE_0:1
.= b2 by A30, XTUPLE_0:1 ;
hence b1 = b2 ; :: thesis:

end;

then reconsider h = { [(QClass. u),(hh . u)] where u is Element of Q. I : 1. I = 1. I } as Function by A22, FUNCT_1:def 1, RELAT_1:def 1;
A37: for x being object st x in dom h holds
x in Quot. I

proof

let x be object ; :: thesis:
assume x in dom h ; :: thesis:
then consider y being object such that
A38: [x,y] in h by XTUPLE_0:def 12;
consider u being Element of Q. I such that
A39: [x,y] = [(QClass. u),(hh . u)] and
1. I = 1. I by A38;
x = QClass. u by A39, XTUPLE_0:1;
hence x in Quot. I ; :: thesis:

end;

for x being object st x in Quot. I holds
x in dom h

proof

let x be object ; :: thesis:
assume x in Quot. I ; :: thesis:
then consider u being Element of Q. I such that
A40: x = QClass. u by Def5;
[(QClass. u),(hh . u)] in h ;
hence x in dom h by A40, XTUPLE_0:def 12; :: thesis:

end;

then A41: dom h = Quot. I by A37, TARSKI:2;
for y being object st y in rng h holds
y in the carrier of F9

proof

let y be object ; :: thesis:
assume y in rng h ; :: thesis:
then consider x being object such that
A42: [x,y] in h by XTUPLE_0:def 13;
consider u being Element of Q. I such that
A43: [x,y] = [(QClass. u),(hh . u)] and
1. I = 1. I by A42;
y = hh . u by A43, XTUPLE_0:1;
hence y in the carrier of F9 ; :: thesis:

end;

then rng h c= the carrier of F9 by TARSKI:def 3;
then reconsider h = h as Function of (Quot. I), the carrier of F9 by A41, FUNCT_2:def 1, RELSET_1:4;
reconsider h = h as Function of (the_Field_of_Quotients I),F9 ;
A44: for x being Element of (the_Field_of_Quotients I)
for u being Element of Q. I st x = QClass. u holds
h . x = hh . u

proof

let x be Element of (the_Field_of_Quotients I); :: thesis:
let u be Element of Q. I; :: thesis:
A45: [(QClass. u),(hh . u)] in h ;
assume x = QClass. u ; :: thesis:
hence h . x = hh . u by A41, A45, FUNCT_1:def 2; :: thesis:

end;

A46: now :: thesis:

let h9 be Function of (the_Field_of_Quotients I),F9; :: thesis:
assume that
A47: h9 is RingHomomorphism and
A48: h9 * (canHom I) = f9 ; :: thesis:
A49: 0. I <> 1. I ;
for x being object st x in the carrier of (the_Field_of_Quotients I) holds
h9 . x = h . x

proof

let x be object ; :: thesis:
assume x in the carrier of (the_Field_of_Quotients I) ; :: thesis:
then reconsider x = x as Element of (the_Field_of_Quotients I) ;
reconsider x9 = x as Element of Quot. I ;
consider u being Element of Q. I such that
A50: x9 = QClass. u by Def5;
consider a, b being Element of I such that
A51: u = [a,b] and
A52: b <> 0. I by Def1;
reconsider a9 = [a,(1. I)], b9 = [b,(1. I)] as Element of Q. I by A49, Def1;
reconsider a99 = QClass. a9, b99 = QClass. b9 as Element of (the_Field_of_Quotients I) ;
reconsider bi = [(1. I),b] as Element of Q. I by A52, Def1;
reconsider aa = QClass. (quotient (a,(1. I))) as Element of (the_Field_of_Quotients I) ;
reconsider bb = QClass. (quotient (b,(1. I))) as Element of (the_Field_of_Quotients I) ;
reconsider bi9 = QClass. bi as Element of (the_Field_of_Quotients I) ;
A54: b99 <> 0. (the_Field_of_Quotients I)

proof

A55: b9 in b99 by Th5;
assume A56: b99 = 0. (the_Field_of_Quotients I) ; :: thesis:
b = [b,(1. I)] `1
.= 0. I by A56, A55, Def8 ;
hence contradiction by A52; :: thesis:

end;

A57: h . x = hh . u by A44, A50
.= ((h9 * (canHom I)) . (u `1)) * ((f9 . (u `2)) ") by A23, A48
.= (h9 . ((canHom I) . (u `1))) * (((h9 * (canHom I)) . (u `2)) ") by A48, FUNCT_2:15
.= (h9 . ((canHom I) . (u `1))) * ((h9 . ((canHom I) . (u `2))) ") by FUNCT_2:15 ;
A58: h9 . ((quotmult I) . (a99,bi9)) = h9 . (qmult ((QClass. a9),(QClass. bi))) by Def13
.= h9 . (QClass. (pmult (a9,bi))) by Th10 ;
(h9 . ((canHom I) . (u `1))) * ((h9 . ((canHom I) . (u `2))) ") = (h9 . ((canHom I) . a)) * ((h9 . ((canHom I) . (u `2))) ") by A51
.= (h9 . aa) * ((h9 . ((canHom I) . (u `2))) ") by Def21
.= (h9 . a99) * ((h9 . ((canHom I) . (u `2))) ") by A49, Def20
.= (h9 . a99) * ((h9 . ((canHom I) . b)) ") by A51
.= (h9 . a99) * ((h9 . bb) ") by Def21
.= (h9 . a99) * ((h9 . b99) ") by A49, Def20
.= h9 . (a99 * (b99 ")) by A47, A54, Th53 ;
hence h9 . x = h . x by A50, A51, A52, A57, A54, A58, Th47; :: thesis:

end;

hence h9 = h ; :: thesis:

end;

A59: 1_ F9 = 1. F9 ;
for x, y being Element of (the_Field_of_Quotients I) holds
( h . (x + y) = (h . x) + (h . y) & h . (x * y) = (h . x) * (h . y) & h . (1_ (the_Field_of_Quotients I)) = 1_ F9 )

proof

let x, y be Element of (the_Field_of_Quotients I); :: thesis:
reconsider x = x, y = y as Element of Quot. I ;
A60: 0. F9 <> 1. F9 ;
consider u being Element of Q. I such that
A61: x = QClass. u by Def5;
A62: u `2 <> 0. I by Th2;
then A63: f9 . (u `2) <> 0. F9 by A20, Th51;
consider v being Element of Q. I such that
A64: y = QClass. v by Def5;
A65: v `2 <> 0. I by Th2;
then A66: f9 . (v `2) <> 0. F9 by A20, Th51;
A67: (u `2) * (v `2) <> 0. I by A62, A65, VECTSP_2:def 1;
then reconsider t = [(((u `1) * (v `2)) + ((v `1) * (u `2))),((u `2) * (v `2))] as Element of Q. I by Def1;
reconsider x = x, y = y as Element of (the_Field_of_Quotients I) ;
reconsider x9 = x, y9 = y as Element of Quot. I ;
A68: h . (qadd (x9,y9)) = h . (QClass. (padd (u,v))) by A61, A64, Th9
.= h . (QClass. t) ;
A69: (h . x) + (h . y) = (hh . u) + (h . y) by A44, A61
.= (hh . u) + (hh . v) by A44, A64
.= ((f9 . (u `1)) * ((f9 . (u `2)) ")) + (hh . v) by A23
.= ((f9 . (u `1)) / (f9 . (u `2))) + ((f9 . (v `1)) / (f9 . (v `2))) by A23
.= (((f9 . (u `1)) * (f9 . (v `2))) + ((f9 . (v `1)) * (f9 . (u `2)))) / ((f9 . (u `2)) * (f9 . (v `2))) by A63, A66, Th49
.= ((f9 . ((u `1) * (v `2))) + ((f9 . (v `1)) * (f9 . (u `2)))) / ((f9 . (u `2)) * (f9 . (v `2))) by A21, GROUP_6:def 6
.= ((f9 . ((u `1) * (v `2))) + (f9 . ((v `1) * (u `2)))) / ((f9 . (u `2)) * (f9 . (v `2))) by A21, GROUP_6:def 6
.= ((f9 . ((u `1) * (v `2))) + (f9 . ((v `1) * (u `2)))) * ((f9 . ((u `2) * (v `2))) ") by A21, GROUP_6:def 6
.= (f9 . (((u `1) * (v `2)) + ((v `1) * (u `2)))) * ((f9 . ((u `2) * (v `2))) ") by A21, VECTSP_1:def 20
.= (f9 . (t `1)) * ((f9 . ((u `2) * (v `2))) ")
.= (f9 . (t `1)) * ((f9 . (t `2)) ")
.= hh . t by A23 ;
A70: h . (QClass. t) = hh . t by A44;
reconsider t = [((u `1) * (v `1)),((u `2) * (v `2))] as Element of Q. I by A67, Def1;
A71: (h . x) * (h . y) = (hh . u) * (h . y) by A44, A61
.= (hh . u) * (hh . v) by A44, A64
.= ((f9 . (u `1)) * ((f9 . (u `2)) ")) * (hh . v) by A23
.= ((f9 . (u `1)) / (f9 . (u `2))) * ((f9 . (v `1)) / (f9 . (v `2))) by A23
.= ((f9 . (u `1)) * (f9 . (v `1))) / ((f9 . (u `2)) * (f9 . (v `2))) by A63, A66, Th48
.= (f9 . ((u `1) * (v `1))) / ((f9 . (u `2)) * (f9 . (v `2))) by A21, GROUP_6:def 6
.= (f9 . ((u `1) * (v `1))) * ((f9 . ((u `2) * (v `2))) ") by A21, GROUP_6:def 6
.= (f9 . (t `1)) * ((f9 . ((u `2) * (v `2))) ")
.= (f9 . (t `1)) * ((f9 . (t `2)) ")
.= hh . t by A23 ;
reconsider x9 = x, y9 = y as Element of Quot. I ;
A72: h . (qmult (x9,y9)) = h . (QClass. (pmult (u,v))) by A61, A64, Th10
.= h . (QClass. t) ;
A73: h . (QClass. t) = hh . t by A44;
0. I <> 1. I ;
then reconsider t = [(1. I),(1. I)] as Element of Q. I by Def1;
A74: for u being object st u in QClass. t holds
u in q1. I

proof

let u be object ; :: thesis:
assume A75: u in QClass. t ; :: thesis:
then reconsider u = u as Element of Q. I ;
u `1 = (u `1) * (1. I)
.= (u `1) * (t `2)
.= (u `2) * (t `1) by A75, Def4
.= (u `2) * (1. I)
.= u `2 ;
hence u in q1. I by Def9; :: thesis:

end;

for u being object st u in q1. I holds
u in QClass. t

proof

let u be object ; :: thesis:
assume A76: u in q1. I ; :: thesis:
then reconsider u = u as Element of Q. I ;
(u `1) * (t `2) = (u `1) * (1. I)
.= u `1
.= u `2 by A76, Def9
.= (u `2) * (1. I)
.= (u `2) * (t `1) ;
hence u in QClass. t by Def4; :: thesis:

end;

then q1. I = QClass. t by A74, TARSKI:2;
then h . (1_ (the_Field_of_Quotients I)) = hh . t by A44
.= (f9 . (t `1)) * ((f9 . (t `2)) ") by A23
.= (f9 . (1. I)) * ((f9 . (t `2)) ")
.= (f9 . (1. I)) * ((f9 . (1. I)) ")
.= (1. F9) * ((f9 . (1_ I)) ") by A21, A59, GROUP_1:def 13
.= (1. F9) * ((1_ F9) ") by A21, GROUP_1:def 13
.= 1_ F9 by A60, VECTSP_1:def 10 ;
hence ( h . (x + y) = (h . x) + (h . y) & h . (x * y) = (h . x) * (h . y) & h . (1_ (the_Field_of_Quotients I)) = 1_ F9 ) by A69, A68, A70, A71, A72, A73, Def12, Def13; :: thesis:

end;

then A77: ( h is additive & h is multiplicative & h is unity-preserving ) by GROUP_1:def 13, GROUP_6:def 6;
A78: for x being object st x in dom f9 holds
( x in dom (canHom I) & (canHom I) . x in dom h )

proof

let x be object ; :: thesis:
assume x in dom f9 ; :: thesis:
then reconsider x = x as Element of I ;
dom h = the carrier of (the_Field_of_Quotients I) by FUNCT_2:def 1;
then ( x in the carrier of I & (canHom I) . x in dom h ) ;
hence ( x in dom (canHom I) & (canHom I) . x in dom h ) by FUNCT_2:def 1; :: thesis:

end;

A79: 0. I <> 1. I ;
A80: for x being object st x in dom f9 holds
f9 . x = h . ((canHom I) . x)

proof

let x be object ; :: thesis:
assume x in dom f9 ; :: thesis:
then reconsider x = x as Element of I ;
reconsider u = [x,(1. I)] as Element of Q. I by A79, Def1;
reconsider u9 = QClass. u as Element of (the_Field_of_Quotients I) ;
h . ((canHom I) . x) = h . (QClass. (quotient (x,(1. I)))) by Def21
.= h . u9 by Def20
.= hh . u by A44
.= (f9 . (u `1)) * ((f9 . (u `2)) ") by A23
.= (f9 . (u `1)) * ((f9 . (1_ I)) ")
.= (f9 . (u `1)) * (1_ F9) by A21, A19, GROUP_1:def 13
.= f9 . (u `1)
.= f9 . x ;
hence f9 . x = h . ((canHom I) . x) ; :: thesis:

end;

for x being object st x in dom (canHom I) & (canHom I) . x in dom h holds
x in dom f9

proof

let x be object ; :: thesis:
assume that
A81: x in dom (canHom I) and
(canHom I) . x in dom h ; :: thesis:
reconsider x = x as Element of I by A81;
x in the carrier of I ;
hence x in dom f9 by FUNCT_2:def 1; :: thesis:

end;

then h * (canHom I) = f9 by A78, A80, FUNCT_1:10;
hence ex h being Function of (the_Field_of_Quotients I),F9 st
( h is RingHomomorphism & h * (canHom I) = f9 & ( for h9 being Function of (the_Field_of_Quotients I),F9 st h9 is RingHomomorphism & h9 * (canHom I) = f9 holds
h9 = h ) ) by A77, A46; :: thesis:

end;

canHom I is embedding by Th57;
then I has_Field_of_Quotients_Pair the_Field_of_Quotients I, canHom I by A1;
hence 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 ; :: thesis: