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 multiplicative
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 multiplicative
let f be Function of A,B; ( f is RingHomomorphism & f .: S c= Unit_Set B implies Univ_Map (S,f) is multiplicative )
set F = Univ_Map (S,f);
assume A1:
( f is RingHomomorphism & f .: S c= Unit_Set B )
; Univ_Map (S,f) is multiplicative
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 Th33, 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 * a2) * s3))) * (f . s0)
by A15, A1, 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 . s1 is
unital Element of
B )
;
f . s2 is
Unit of
B
by A1, A6, Th56;
then A19:
(
f . s2 in Unit_Set B &
f . s2 is
unital Element of
B )
;
f . s3 is
Unit of
B
by A1, A9, Th56;
then A20:
f . s3 in Unit_Set B
;
s1 * s2 is
Element of
S
by A3, A6, C0SP1:def 4;
then
f . (s1 * s2) is
Unit of
B
by A1, Th56;
then A21:
f . (s1 * s2) in Unit_Set B
;
A22:
(f . (s1 * s2)) * (((f . s2) ["]) * ((f . s1) ["])) =
((f . s1) * (f . s2)) * (((f . s2) ["]) * ((f . s1) ["]))
by A1, GROUP_6:def 6
.=
(((f . s1) * (f . s2)) * ((f . s2) ["])) * ((f . s1) ["])
by GROUP_1:def 3
.=
((f . s1) * ((f . s2) * ((f . s2) ["]))) * ((f . s1) ["])
by GROUP_1:def 3
.=
((f . s1) * (1. B)) * ((f . s1) ["])
by A19, Def2
.=
1. B
by A18, Def2
;
A23:
0. B =
((f . ((a3 * (s1 * s2)) - ((a1 * a2) * s3))) * (f . s0)) * ((f . s0) ["])
by A16
.=
(f . ((a3 * (s1 * s2)) - ((a1 * a2) * s3))) * ((f . s0) * ((f . s0) ["]))
by GROUP_1:def 3
.=
(f . ((a3 * (s1 * s2)) - ((a1 * a2) * s3))) * (1. B)
by A17, Def2
.=
(f . (a3 * (s1 * s2))) - (f . ((a1 * a2) * s3))
by A1, RING_2:8
;
A24:
(f . a3) * (f . (s1 * s2)) =
f . (a3 * (s1 * s2))
by A1, GROUP_6:def 6
.=
f . ((a1 * a2) * s3)
by A23, VECTSP_1:27
.=
(f . (a1 * a2)) * (f . s3)
by A1, GROUP_6:def 6
;
A25:
((f . a3) * ((f . s3) ["])) * (f . (s1 * s2)) =
((f . a3) * (f . (s1 * s2))) * ((f . s3) ["])
by GROUP_1:def 3
.=
(f . (a1 * a2)) * ((f . s3) * ((f . s3) ["]))
by A24, GROUP_1:def 3
.=
(f . (a1 * a2)) * (1. B)
by A20, Def2
.=
(f . a1) * (f . a2)
by A1, GROUP_6:def 6
;
A26:
(f . (s1 * s2)) ["] =
((f . (s1 * s2)) ["]) * ((f . (s1 * s2)) * (((f . s2) ["]) * ((f . s1) ["])))
by A22
.=
(((f . (s1 * s2)) ["]) * (f . (s1 * s2))) * (((f . s2) ["]) * ((f . s1) ["]))
by GROUP_1:def 3
.=
(1. B) * (((f . s2) ["]) * ((f . s1) ["]))
by A21, Def2
.=
((f . s2) ["]) * ((f . s1) ["])
;
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 ;
reconsider fs1s2 =
f . (s1 * s2) as
Element of
B ;
(Univ_Map (S,f)) . (x * y) =
(fa3 * (fs3 ["])) * (1. B)
by A11
.=
(fa3 * (fs3 ["])) * (fs1s2 * (fs1s2 ["]))
by A21, Def2
.=
(fa1 * fa2) * ((fs2 ["]) * (fs1 ["]))
by A26, A25, GROUP_1:def 3
.=
((fa1 * fa2) * (fs1 ["])) * (fs2 ["])
by GROUP_1:def 3
.=
((fa1 * (fs1 ["])) * fa2) * (fs2 ["])
by GROUP_1:def 3
.=
((Univ_Map (S,f)) . x) * ((Univ_Map (S,f)) . y)
by A5, A8, GROUP_1:def 3
;
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 multiplicative
; verum