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
Univ_Map (S,f) is unity-preserving
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
Univ_Map (S,f) is unity-preserving
let f be Function of A,B; ( f is RingHomomorphism & f .: S c= Unit_Set B implies Univ_Map (S,f) is unity-preserving )
set F = Univ_Map (S,f);
assume A1:
( f is RingHomomorphism & f .: S c= Unit_Set B )
; Univ_Map (S,f) is unity-preserving
(Univ_Map (S,f)) . (1. (S ~ A)) = 1. B
proof
consider a1,
s1 being
Element of
A such that A3:
s1 in S
and A4:
1. (S ~ A) = Class (
(EqRel S),
[a1,s1])
and A5:
(Univ_Map (S,f)) . (1. (S ~ A)) = (f . a1) * ((f . s1) ["])
by A1, Def8;
reconsider as1 =
[a1,s1] as
Element of
Frac S by A3, Def3;
Class (
(EqRel S),
(1. (A,S)))
= Class (
(EqRel S),
as1)
by A4, Def6;
then A6:
as1,
1. (
A,
S)
Fr_Eq S
by Th26;
consider s0 being
Element of
A such that A7:
s0 in S
and A8:
(((as1 `1) * ((1. (A,S)) `2)) - (((1. (A,S)) `1) * (as1 `2))) * s0 = 0. A
by A6;
A9:
0. B =
f . (0. A)
by A1, QUOFIELD:50
.=
(f . (a1 - s1)) * (f . s0)
by A1, A8, GROUP_6:def 6
;
f . s0 is
Unit of
B
by A1, A7, Th56;
then A10:
f . s0 in Unit_Set B
;
A11:
0. B =
((f . (a1 - s1)) * (f . s0)) * ((f . s0) ["])
by A9
.=
(f . (a1 - s1)) * ((f . s0) * ((f . s0) ["]))
by GROUP_1:def 3
.=
(f . (a1 - s1)) * (1. B)
by A10, Def2
.=
(f . a1) - (f . s1)
by A1, RING_2:8
;
f . s1 is
Unit of
B
by A1, A3, Th56;
then A12:
f . s1 in Unit_Set B
;
(Univ_Map (S,f)) . (1. (S ~ A)) =
(f . s1) * ((f . s1) ["])
by A5, A11, VECTSP_1:27
.=
1. B
by A12, Def2
;
hence
(Univ_Map (S,f)) . (1. (S ~ A)) = 1. B
;
verum
end;
hence
Univ_Map (S,f) is unity-preserving
; verum