let A be non degenerated commutative Ring; for S being non empty multiplicatively-closed without_zero Subset of A st not 0. A in S holds
ker (canHom S) c= ZeroDiv_Set A
let S be non empty multiplicatively-closed without_zero Subset of A; ( not 0. A in S implies ker (canHom S) c= ZeroDiv_Set A )
assume A1:
not 0. A in S
; ker (canHom S) c= ZeroDiv_Set A
for o being object st o in ker (canHom S) holds
o in ZeroDiv_Set A
proof
let o be
object ;
( o in ker (canHom S) implies o in ZeroDiv_Set A )
assume
o in ker (canHom S)
;
o in ZeroDiv_Set A
then consider v1 being
Element of
A such that A3:
v1 = o
and A4:
(canHom S) . v1 = 0. (S ~ A)
;
1. A in S
by C0SP1:def 4;
then reconsider w =
[v1,(1. A)] as
Element of
Frac S by Def3;
Class (
(EqRel S),
(0. (A,S))) =
(canHom S) . v1
by A4, Def6
.=
Class (
(EqRel S),
((frac1 S) . v1))
by Def7
.=
Class (
(EqRel S),
w)
by Def4
;
then
0. (
A,
S),
w Fr_Eq S
by Th26;
then consider t1 being
Element of
A such that A5:
t1 in S
and A6:
((((0. (A,S)) `1) * (w `2)) - ((w `1) * ((0. (A,S)) `2))) * t1 = 0. A
;
A7:
0. A =
((- (1. A)) * v1) * t1
by A6, VECTSP_2:29
.=
(- (1. A)) * (v1 * t1)
by GROUP_1:def 3
.=
- (v1 * t1)
by VECTSP_2:29
;
A8:
0. A =
- (- (v1 * t1))
by A7
.=
v1 * t1
;
v1 is
zero_divisible
by A1, A5, A8;
hence
o in ZeroDiv_Set A
by A3;
verum
end;
hence
ker (canHom S) c= ZeroDiv_Set A
; verum