let A be domRing; the_Field_of_Quotients A is_ringisomorph_to Total-Quotient-Ring A
set S = Non_ZeroDiv_Set A;
set B = the_Field_of_Quotients A;
set f = canHom A;
A1:
canHom A is RingHomomorphism
by QUOFIELD:56;
A2:
canHom A is RingMonomorphism
by QUOFIELD:57;
A3:
(canHom A) .: (Non_ZeroDiv_Set A) c= Unit_Set (the_Field_of_Quotients A)
reconsider S = Non_ZeroDiv_Set A as non empty multiplicatively-closed without_zero Subset of A by Lm63;
A11:
Univ_Map (S,(canHom A)) is RingHomomorphism
by A3, QUOFIELD:56, Th57, Th58, Th59;
A12:
Total-Quotient-Ring A is Field
by Th65;
set g = Univ_Map (S,(canHom A));
set h = canHom S;
A13:
dom (Univ_Map (S,(canHom A))) = [#] (S ~ A)
by FUNCT_2:def 1;
A14:
for y being object st y in [#] (the_Field_of_Quotients A) holds
y in rng (Univ_Map (S,(canHom A)))
proof
let y be
object ;
( y in [#] (the_Field_of_Quotients A) implies y in rng (Univ_Map (S,(canHom A))) )
assume
y in [#] (the_Field_of_Quotients A)
;
y in rng (Univ_Map (S,(canHom A)))
then reconsider y =
y as
Element of
Quot. A by QUOFIELD:30;
consider y12 being
Element of
Q. A such that A16:
y = QClass. y12
by QUOFIELD:def 5;
consider y1,
y2 being
Element of
A such that A17:
y12 = [y1,y2]
and A18:
y2 <> 0. A
by QUOFIELD:def 1;
A19:
y2 in Non_ZeroDiv_Set A
by A18, Th64;
then A20:
[y1,y2] in Frac S
by Def3;
reconsider yy12 =
y12 as
Element of
Frac S by A17, A19, Def3;
reconsider x =
Class (
(EqRel S),
yy12) as
Element of
(S ~ A) by Lm41;
A21:
1. A <> 0. A
;
then reconsider p1 =
[y1,(1. A)] as
Element of
Q. A by QUOFIELD:def 1;
reconsider p2 =
[y2,(1. A)] as
Element of
Q. A by A21, QUOFIELD:def 1;
reconsider q =
[(1. A),y2] as
Element of
Q. A by A18, QUOFIELD:def 1;
reconsider r12 =
[y1,y2] as
Element of
Q. A by A18, QUOFIELD:def 1;
quotient (
y1,
(1. A))
= p1
by A21, QUOFIELD:def 24;
then A24:
(canHom A) . y1 = QClass. p1
by QUOFIELD:def 25;
quotient (
y2,
(1. A))
= p2
by A21, QUOFIELD:def 24;
then A25:
(canHom A) . y2 = QClass. p2
by QUOFIELD:def 25;
then A26:
QClass. p2 <> 0. (the_Field_of_Quotients A)
by A2, A18, QUOFIELD:51;
then A27:
((canHom A) . y2) " = QClass. q
by A18, A25, QUOFIELD:47;
A28:
pmult (
p1,
q) =
[((p1 `1) * (q `1)),((p1 `2) * (q `2))]
by QUOFIELD:def 3
.=
[y1,y2]
;
A29:
r12 in QClass. r12
by QUOFIELD:5;
(r12 `1) * (y12 `2) = (r12 `2) * (y12 `1)
by A17;
then
r12 in QClass. y12
by QUOFIELD:def 4;
then A30:
r12 in (QClass. r12) /\ (QClass. y12)
by A29, XBOOLE_0:def 4;
A31:
((canHom A) . y1) * (((canHom A) . y2) ") =
(quotmult A) . (
((canHom A) . y1),
(((canHom A) . y2) "))
by QUOFIELD:37
.=
qmult (
(QClass. p1),
(QClass. q))
by A24, A27, QUOFIELD:def 13
.=
QClass. r12
by A28, QUOFIELD:10
.=
y
by QUOFIELD:8, XBOOLE_0:4, A30, A16
;
reconsider x =
Class (
(EqRel S),
[y1,y2]) as
Element of
(S ~ A) by A20, Lm41;
consider x1,
x2 being
Element of
A such that A32:
x2 in S
and
x = Class (
(EqRel S),
[x1,x2])
and
(Univ_Map (S,(canHom A))) . x = ((canHom A) . x1) * (((canHom A) . x2) ["])
by A1, A3, Def8;
reconsider x12 =
[x1,x2] as
Element of
Frac S by Def3, A32;
A33:
dom (canHom S) = [#] A
by FUNCT_2:def 1;
A34:
(canHom S) . y2 =
Class (
(EqRel S),
((frac1 S) . y2))
by Def7
.=
Class (
(EqRel S),
[y2,(1. A)])
by Def4
;
then
(canHom S) . y2 is
Unit of
(S ~ A)
by A19, Lm46;
then A35:
(canHom S) . y2 in Unit_Set (S ~ A)
;
A36:
(canHom A) . y2 =
((Univ_Map (S,(canHom A))) * (canHom S)) . y2
by Th61, QUOFIELD:56, A3
.=
(Univ_Map (S,(canHom A))) . ((canHom S) . y2)
by A33, FUNCT_1:13
;
A37:
Univ_Map (
S,
(canHom A)) is
unity-preserving
by QUOFIELD:56, A3, Th59;
((canHom A) . y2) * ((Univ_Map (S,(canHom A))) . (((canHom S) . y2) ["])) =
(Univ_Map (S,(canHom A))) . (((canHom S) . y2) * (((canHom S) . y2) ["]))
by A11, A36, GROUP_6:def 6
.=
1. (the_Field_of_Quotients A)
by A37, A35, Def2
;
then A39:
((canHom A) . y2) " =
(((canHom A) . y2) ") * (((canHom A) . y2) * ((Univ_Map (S,(canHom A))) . (((canHom S) . y2) ["])))
.=
((((canHom A) . y2) ") * ((canHom A) . y2)) * ((Univ_Map (S,(canHom A))) . (((canHom S) . y2) ["]))
by GROUP_1:def 3
.=
(1. (the_Field_of_Quotients A)) * ((Univ_Map (S,(canHom A))) . (((canHom S) . y2) ["]))
by A25, A26, VECTSP_1:def 10
.=
(Univ_Map (S,(canHom A))) . (((canHom S) . y2) ["])
;
A40:
(canHom S) . y1 =
Class (
(EqRel S),
((frac1 S) . y1))
by Def7
.=
Class (
(EqRel S),
[y1,(1. A)])
by Def4
;
A41:
1. A in S
by C0SP1:def 4;
then reconsider zz1 =
[y1,(1. A)] as
Element of
Frac S by Def3;
reconsider zz2 =
[y2,(1. A)] as
Element of
Frac S by A41, Def3;
reconsider zz2inv =
[(1. A),y2] as
Element of
Frac S by A19, Def3;
reconsider z1 =
Class (
(EqRel S),
zz1) as
Element of
(S ~ A) by Lm41;
reconsider z2 =
Class (
(EqRel S),
zz2) as
Element of
(S ~ A) by Lm41;
reconsider z2inv =
Class (
(EqRel S),
zz2inv) as
Element of
(S ~ A) by Lm41;
Class (
(EqRel S),
[y2,(1. A)]) is
Unit of
(S ~ A)
by A19, Lm46;
then A43:
z2 in Unit_Set (S ~ A)
;
A44:
z2inv * z2 =
Class (
(EqRel S),
(zz2inv * zz2))
by Th33
.=
Class (
(EqRel S),
(1. (A,S)))
by A19, Th30, Th26
.=
1. (S ~ A)
by Def6
;
z2 ["] =
(z2inv * z2) * (z2 ["])
by A44
.=
z2inv * (z2 * (z2 ["]))
by GROUP_1:def 3
.=
z2inv * (1. (S ~ A))
by A43, Def2
.=
z2inv
;
then A46:
z1 * (z2 ["]) =
Class (
(EqRel S),
(zz1 * zz2inv))
by Th33
.=
Class (
(EqRel S),
[y1,y2])
;
(canHom A) . y1 =
((Univ_Map (S,(canHom A))) * (canHom S)) . y1
by Th61, QUOFIELD:56, A3
.=
(Univ_Map (S,(canHom A))) . ((canHom S) . y1)
by A33, FUNCT_1:13
;
then A49:
y = (Univ_Map (S,(canHom A))) . (Class ((EqRel S),[y1,y2]))
by A40, A34, A46, A11, A39, A31, GROUP_6:def 6;
Class (
(EqRel S),
[y1,y2]) is
Element of
(S ~ A)
by A20, Lm41;
hence
y in rng (Univ_Map (S,(canHom A)))
by A13, A49, FUNCT_1:def 3;
verum
end;
[#] (the_Field_of_Quotients A) c= rng (Univ_Map (S,(canHom A)))
by A14;
then
Univ_Map (S,(canHom A)) is onto
by XBOOLE_0:def 10;
hence
the_Field_of_Quotients A is_ringisomorph_to Total-Quotient-Ring A
by A11, A12, QUOFIELD:def 23; verum