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 additive
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 additive
let f be Function of A,B; ( f is RingHomomorphism & f .: S c= Unit_Set B implies Univ_Map (S,f) is additive )
set F = Univ_Map (S,f);
assume A1:
( f is RingHomomorphism & f .: S c= Unit_Set B )
; Univ_Map (S,f) is additive
for x, y being Element of (S ~ A) holds (Univ_Map (S,f)) . (x + y) = ((Univ_Map (S,f)) . x) + ((Univ_Map (S,f)) . y)
proof
let x,
y be
Element of
(S ~ A);
(Univ_Map (S,f)) . (x + y) = ((Univ_Map (S,f)) . x) + ((Univ_Map (S,f)) . y)
consider a1,
s1 being
Element of
A such that A3:
s1 in S
and A4:
x = Class (
(EqRel S),
[a1,s1])
and A5:
(Univ_Map (S,f)) . x = (f . a1) * ((f . s1) ["])
by A1, Def8;
consider a2,
s2 being
Element of
A such that A6:
s2 in S
and A7:
y = Class (
(EqRel S),
[a2,s2])
and A8:
(Univ_Map (S,f)) . y = (f . a2) * ((f . s2) ["])
by A1, Def8;
reconsider as1 =
[a1,s1] as
Element of
Frac S by A3, Def3;
reconsider as2 =
[a2,s2] as
Element of
Frac S by A6, Def3;
reconsider z =
x + y as
Element of
(S ~ A) ;
consider a3,
s3 being
Element of
A such that A9:
s3 in S
and A10:
z = Class (
(EqRel S),
[a3,s3])
and A11:
(Univ_Map (S,f)) . z = (f . a3) * ((f . s3) ["])
by A1, Def8;
reconsider as3 =
[a3,s3] as
Element of
Frac S by A9, Def3;
Class (
(EqRel S),
as3)
= Class (
(EqRel S),
(as1 + as2))
by Th35, A4, A7, A10;
then
as3,
as1 + as2 Fr_Eq S
by Th26;
then consider s0 being
Element of
A such that A14:
s0 in S
and A15:
(((as3 `1) * ((as1 + as2) `2)) - (((as1 + as2) `1) * (as3 `2))) * s0 = 0. A
;
A16:
0. B =
f . (0. A)
by A1, QUOFIELD:50
.=
(f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * (f . s0)
by A1, A15, GROUP_6:def 6
;
f . s0 is
Unit of
B
by A1, A14, Th56;
then A17:
f . s0 in Unit_Set B
;
f . s1 is
Unit of
B
by A1, A3, Th56;
then A18:
f . s1 in Unit_Set B
;
f . s2 is
Unit of
B
by A1, A6, Th56;
then A19:
f . s2 in Unit_Set B
;
f . s3 is
Unit of
B
by A1, A9, Th56;
then A20:
f . s3 in Unit_Set B
;
A21:
0. B =
((f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * (f . s0)) * ((f . s0) ["])
by A16
.=
(f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * ((f . s0) * ((f . s0) ["]))
by GROUP_1:def 3
.=
(f . ((a3 * (s1 * s2)) - (((a1 * s2) + (a2 * s1)) * s3))) * (1. B)
by A17, Def2
.=
(f . (a3 * (s1 * s2))) - (f . (((a1 * s2) + (a2 * s1)) * s3))
by A1, RING_2:8
;
(f . a3) * ((f . s1) * (f . s2)) =
(f . a3) * (f . (s1 * s2))
by A1, GROUP_6:def 6
.=
f . (a3 * (s1 * s2))
by A1, GROUP_6:def 6
.=
f . (((a1 * s2) + (a2 * s1)) * s3)
by A21, VECTSP_1:27
.=
(f . ((a1 * s2) + (a2 * s1))) * (f . s3)
by A1, GROUP_6:def 6
;
then A23:
((f . a3) * ((f . s3) ["])) * ((f . s1) * (f . s2)) =
((f . ((a1 * s2) + (a2 * s1))) * (f . s3)) * ((f . s3) ["])
by GROUP_1:def 3
.=
(f . ((a1 * s2) + (a2 * s1))) * ((f . s3) * ((f . s3) ["]))
by GROUP_1:def 3
.=
(f . ((a1 * s2) + (a2 * s1))) * (1. B)
by A20, Def2
.=
(f . (a1 * s2)) + (f . (a2 * s1))
by A1, VECTSP_1:def 20
;
reconsider fa1 =
f . a1,
fa2 =
f . a2,
fa3 =
f . a3 as
Element of
B ;
reconsider fs1 =
f . s1,
fs2 =
f . s2,
fs3 =
f . s3 as
Element of
B ;
A24:
(fa3 * (fs3 ["])) * fs1 =
((fa3 * (fs3 ["])) * fs1) * (1. B)
.=
((fa3 * (fs3 ["])) * fs1) * (fs2 * (fs2 ["]))
by A19, Def2
.=
(((fa3 * (fs3 ["])) * fs1) * fs2) * (fs2 ["])
by GROUP_1:def 3
.=
((f . (a1 * s2)) + (f . (a2 * s1))) * ((f . s2) ["])
by A23, GROUP_1:def 3
.=
(((f . a1) * (f . s2)) + (f . (a2 * s1))) * ((f . s2) ["])
by A1, GROUP_6:def 6
.=
((fa1 * fs2) + (fa2 * fs1)) * (fs2 ["])
by A1, GROUP_6:def 6
.=
((fa1 * fs2) * (fs2 ["])) + ((fa2 * fs1) * (fs2 ["]))
by VECTSP_1:def 3
.=
(fa1 * (fs2 * (fs2 ["]))) + ((fa2 * fs1) * (fs2 ["]))
by GROUP_1:def 3
.=
(fa1 * (1. B)) + ((fa2 * fs1) * (fs2 ["]))
by A19, Def2
.=
fa1 + ((fa2 * (fs2 ["])) * fs1)
by GROUP_1:def 3
;
(Univ_Map (S,f)) . (x + y) =
(fa3 * (fs3 ["])) * (1. B)
by A11
.=
(fa3 * (fs3 ["])) * (fs1 * (fs1 ["]))
by A18, Def2
.=
(fa1 + ((fa2 * (fs2 ["])) * fs1)) * (fs1 ["])
by A24, GROUP_1:def 3
.=
(fa1 * (fs1 ["])) + (((fa2 * (fs2 ["])) * fs1) * (fs1 ["]))
by VECTSP_1:def 3
.=
(fa1 * (fs1 ["])) + ((fa2 * (fs2 ["])) * (fs1 * (fs1 ["])))
by GROUP_1:def 3
.=
(fa1 * (fs1 ["])) + ((fa2 * (fs2 ["])) * (1. B))
by A18, Def2
.=
((Univ_Map (S,f)) . x) + ((Univ_Map (S,f)) . y)
by A5, A8
;
hence
(Univ_Map (S,f)) . (x + y) = ((Univ_Map (S,f)) . x) + ((Univ_Map (S,f)) . y)
;
verum
end;
hence
Univ_Map (S,f) is additive
; verum