let A be non degenerated commutative Ring; :: thesis: for S being non empty multiplicatively-closed without_zero Subset of A st not 0. A in S & A is domRing holds
( ker (canHom S) = {(0. A)} & canHom S is one-to-one )
let S be non empty multiplicatively-closed without_zero Subset of A; :: thesis: ( not 0. A in S & A is domRing implies ( ker (canHom S) = {(0. A)} & canHom S is one-to-one ) )
assume A1: ( not 0. A in S & A is domRing ) ; :: thesis: ( ker (canHom S) = {(0. A)} & canHom S is one-to-one )
then A2: ker (canHom S) c= ZeroDiv_Set A by Lm50;
A3: ZeroDiv_Set A = {(0. A)} by A1, Th4;
A4: (canHom S) . (0. A) = Class ((EqRel S),((frac1 S) . (0. A))) by Def7
.= Class ((EqRel S),(0. (A,S))) by Def4
.= 0. (S ~ A) by Def6 ;
A5: 0. A in ker (canHom S) by A4;
A6: {(0. A)} is Subset of (ker (canHom S)) by A5, SUBSET_1:33;
for x, y being object st x in dom (canHom S) & y in dom (canHom S) & (canHom S) . x = (canHom S) . y holds
x = y
proof
let x, y be object ; :: thesis: ( x in dom (canHom S) & y in dom (canHom S) & (canHom S) . x = (canHom S) . y implies x = y )
assume A8: ( x in dom (canHom S) & y in dom (canHom S) & (canHom S) . x = (canHom S) . y ) ; :: thesis: x = y
then reconsider a = x, b = y as Element of A ;
A9: 0. (S ~ A) = ((canHom S) . a) - ((canHom S) . b) by A8, RLVECT_1:15
.= (canHom S) . (a - b) by Lm49 ;
A10: a - b in ker (canHom S) by A9;
A11: 0. A = a + (- b) by A2, A3, A10, TARSKI:def 1;
a = - (- b) by A11, RLVECT_1:6
.= b ;
hence x = y ; :: thesis: verum
end;
hence ( ker (canHom S) = {(0. A)} & canHom S is one-to-one ) by A2, A3, A6, XBOOLE_0:def 10; :: thesis: verum