let F be non degenerated almost_left_invertible commutative domRing-like Ring; :: thesis: F is_ringisomorph_to the_Field_of_Quotients F
A1: 0. F <> 1. F ;
A2: dom (canHom F) = the carrier of F by FUNCT_2:def 1;
A3: for x being object st x in the carrier of (the_Field_of_Quotients F) holds
x in rng (canHom F)
proof
let x be object ; :: thesis: ( x in the carrier of (the_Field_of_Quotients F) implies x in rng (canHom F) )
assume x in the carrier of (the_Field_of_Quotients F) ; :: thesis: x in rng (canHom F)
then reconsider x = x as Element of Quot. F ;
consider u being Element of Q. F such that
A4: x = QClass. u by Def5;
consider a, b being Element of F such that
A5: u = [a,b] and
A6: b <> 0. F by Def1;
consider z being Element of F such that
A7: z * b = 1. F by A6, VECTSP_1:def 9;
reconsider t = [(a * z),(1. F)] as Element of Q. F by A1, Def1;
A8: for x being object st x in QClass. t holds
x in QClass. u
proof
let x be object ; :: thesis: ( x in QClass. t implies x in QClass. u )
assume A9: x in QClass. t ; :: thesis: x in QClass. u
then reconsider x = x as Element of Q. F ;
x `1 = (x `1) * (1. F)
.= (x `1) * (t `2)
.= (x `2) * (t `1) by A9, Def4
.= (x `2) * (a * z) ;
then (x `1) * (u `2) = ((x `2) * (a * z)) * b by A5
.= (x `2) * ((a * z) * b) by GROUP_1:def 3
.= (x `2) * (a * (1. F)) by A7, GROUP_1:def 3
.= (x `2) * a
.= (x `2) * (u `1) by A5 ;
hence x in QClass. u by Def4; :: thesis: verum
end;
for x being object st x in QClass. u holds
x in QClass. t
proof
let x be object ; :: thesis: ( x in QClass. u implies x in QClass. t )
assume A10: x in QClass. u ; :: thesis: x in QClass. t
then reconsider x = x as Element of Q. F ;
(x `1) * (t `2) = (x `1) * (b * z) by A7
.= ((x `1) * b) * z by GROUP_1:def 3
.= ((x `1) * (u `2)) * z by A5
.= ((x `2) * (u `1)) * z by A10, Def4
.= ((x `2) * a) * z by A5
.= (x `2) * (a * z) by GROUP_1:def 3
.= (x `2) * (t `1) ;
hence x in QClass. t by Def4; :: thesis: verum
end;
then A11: QClass. t = QClass. u by A8, TARSKI:2;
(canHom F) . (a * z) = QClass. (quotient ((a * z),(1. F))) by Def21
.= x by A1, A4, A11, Def20 ;
hence x in rng (canHom F) by A2, FUNCT_1:def 3; :: thesis: verum
end;
for x being object st x in rng (canHom F) holds
x in the carrier of (the_Field_of_Quotients F) ;
then rng (canHom F) = the carrier of (the_Field_of_Quotients F) by A3, TARSKI:2;
then A12: canHom F is onto ;
A13: canHom F is embedding by Th57;
then canHom F is RingHomomorphism ;
then canHom F is RingEpimorphism by A12;
hence F is_ringisomorph_to the_Field_of_Quotients F by A13; :: thesis: verum