let A, B be non degenerated commutative Ring; for S being non empty multiplicatively-closed without_zero Subset of A
for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
f = (Univ_Map (S,f)) * (canHom S)
let S be non empty multiplicatively-closed without_zero Subset of A; for f being Function of A,B st f is RingHomomorphism & f .: S c= Unit_Set B holds
f = (Univ_Map (S,f)) * (canHom S)
let f be Function of A,B; ( f is RingHomomorphism & f .: S c= Unit_Set B implies f = (Univ_Map (S,f)) * (canHom S) )
set h = canHom S;
set g = Univ_Map (S,f);
set g1 = (Univ_Map (S,f)) * (canHom S);
assume A1:
( f is RingHomomorphism & f .: S c= Unit_Set B )
; f = (Univ_Map (S,f)) * (canHom S)
A2:
dom (canHom S) = [#] A
by FUNCT_2:def 1;
A3: dom ((Univ_Map (S,f)) * (canHom S)) =
the carrier of A
by FUNCT_2:def 1
.=
dom f
by FUNCT_2:def 1
;
for x being object st x in dom f holds
f . x = ((Univ_Map (S,f)) * (canHom S)) . x
proof
set g1 =
(Univ_Map (S,f)) * (canHom S);
let x be
object ;
( x in dom f implies f . x = ((Univ_Map (S,f)) * (canHom S)) . x )
assume
x in dom f
;
f . x = ((Univ_Map (S,f)) * (canHom S)) . x
then reconsider x =
x as
Element of
A ;
A7:
(canHom S) . x =
Class (
(EqRel S),
((frac1 S) . x))
by Def7
.=
Class (
(EqRel S),
[x,(1. A)])
by Def4
;
(frac1 S) . x = [x,(1. A)]
by Def4;
then reconsider x1 =
[x,(1. A)] as
Element of
Frac S ;
reconsider hx =
(canHom S) . x as
Element of
(S ~ A) ;
consider a1,
s1 being
Element of
A such that A9:
s1 in S
and A10:
hx = Class (
(EqRel S),
[a1,s1])
and A11:
(Univ_Map (S,f)) . hx = (f . a1) * ((f . s1) ["])
by A1, Def8;
reconsider as1 =
[a1,s1] as
Element of
Frac S by A9, Def3;
as1,
x1 Fr_Eq S
by A7, A10, Th26;
then consider s0 being
Element of
A such that A13:
s0 in S
and A14:
(((as1 `1) * (x1 `2)) - ((x1 `1) * (as1 `2))) * s0 = 0. A
;
f . s0 is
Unit of
B
by A1, A13, Th56;
then A15:
f . s0 in Unit_Set B
;
f . s1 is
Unit of
B
by A1, A9, Th56;
then A16:
f . s1 in Unit_Set B
;
0. B =
f . (0. A)
by A1, QUOFIELD:50
.=
(f . (a1 - (x * s1))) * (f . s0)
by A1, A14, GROUP_6:def 6
;
then 0. B =
((f . (a1 - (x * s1))) * (f . s0)) * ((f . s0) ["])
.=
(f . (a1 - (x * s1))) * ((f . s0) * ((f . s0) ["]))
by GROUP_1:def 3
.=
(f . (a1 - (x * s1))) * (1. B)
by A15, Def2
.=
(f . a1) - (f . (x * s1))
by A1, RING_2:8
;
then A19:
f . a1 =
f . (x * s1)
by VECTSP_1:27
.=
(f . x) * (f . s1)
by A1, GROUP_6:def 6
;
(f . a1) * ((f . s1) ["]) =
(f . x) * ((f . s1) * ((f . s1) ["]))
by A19, GROUP_1:def 3
.=
(f . x) * (1. B)
by A16, Def2
.=
f . x
;
hence
f . x = ((Univ_Map (S,f)) * (canHom S)) . x
by A2, A11, FUNCT_1:13;
verum
end;
hence
f = (Univ_Map (S,f)) * (canHom S)
by A3; verum