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:
canHom F is RingMonomorphism
by Th60;
then A4:
canHom F is RingHomomorphism
by Def23;
canHom F is RingEpimorphism
proof
A5:
for
x being
set st
x in rng (canHom F) holds
x in the
carrier of
(the_Field_of_Quotients F)
;
for
x being
set st
x in the
carrier of
(the_Field_of_Quotients F) holds
x in rng (canHom F)
proof
let x be
set ;
:: 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 A6:
x = QClass. u
by Def5;
consider a,
b being
Element of
F such that A7:
(
u = [a,b] &
b <> 0. F )
by Def1;
consider z being
Element of
F such that A8:
z * b = 1. F
by A7, VECTSP_1:def 20;
reconsider t =
[(a * z),(1. F)] as
Element of
Q. F by A1, Def1;
A9:
QClass. t = QClass. u
(canHom F) . (a * z) =
QClass. (quotient (a * z),(1. F))
by Def28
.=
x
by A1, A6, A9, Def27
;
hence
x in rng (canHom F)
by A2, FUNCT_1:def 5;
:: thesis: verum
end;
then
rng (canHom F) = the
carrier of
(the_Field_of_Quotients F)
by A5, TARSKI:2;
hence
canHom F is
RingEpimorphism
by A4, Def22;
:: thesis: verum
end;
then
canHom F is RingIsomorphism
by A3;
hence
F is_ringisomorph_to the_Field_of_Quotients F
by Def26; :: thesis: verum