let R be Ring; :: thesis: for M, N being LeftMod of R
for f being Homomorphism of R,M,N holds
( f is one-to-one iff ker f = {(0. M)} )
let M, N be LeftMod of R; :: thesis: for f being Homomorphism of R,M,N holds
( f is one-to-one iff ker f = {(0. M)} )
let f be Homomorphism of R,M,N; :: thesis: ( f is one-to-one iff ker f = {(0. M)} )
A1: f . (0. M) = f . ((0. M) + (0. M)) by RLVECT_1:4
.= (f . (0. M)) + (f . (0. M)) by Def10, VECTSP_1:def 20 ;
then A2: f . (0. M) = 0. N by RLVECT_1:9;
A3: 0. M in ker f by A2;
thus ( f is one-to-one implies ker f = {(0. M)} ) :: thesis: ( ker f = {(0. M)} implies f is one-to-one )

proof

assume A5: f is one-to-one ; :: thesis: ker f = {(0. M)}
for x being object holds
( x in ker f iff x in {(0. M)} )

proof

let x be object ; :: thesis: ( x in ker f iff x in {(0. M)} )
( x in ker f implies x in {(0. M)} )

proof

assume x in ker f ; :: thesis: x in {(0. M)}
then consider x1 being Element of M such that
A7: ( x1 = x & f . x1 = 0. N ) ;
A8: f . x1 = f . (0. M) by A1, A7, RLVECT_1:9;
dom f = the carrier of M by FUNCT_2:def 1;
then x = 0. M by A5, A8, A7;
hence x in {(0. M)} by TARSKI:def 1; :: thesis: verum

end;

hence ( x in ker f iff x in {(0. M)} ) by A3, TARSKI:def 1; :: thesis: verum

end;

hence ker f = {(0. M)} by TARSKI:2; :: thesis: verum

end;

assume A10: ker f = {(0. M)} ; :: thesis: f is one-to-one
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A11: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then reconsider x1 = x1, x2 = x2 as Element of M ;
A12: - (f . x2) = (- (1. R)) * (f . x2) by VECTSP_1:14
.= f . ((- (1. R)) * x2) by Def10, MOD_2:def 2
.= f . (- x2) by VECTSP_1:14 ;
0. N = (f . x1) + (f . (- x2)) by A12, A11, RLVECT_1:5
.= f . (x1 + (- x2)) by Def10, VECTSP_1:def 20 ;
then x1 - x2 in ker f ;
then x1 - x2 = 0. M by A10, TARSKI:def 1;
hence x1 = x2 by VECTSP_1:19; :: thesis: verum

end;

hence f is one-to-one ; :: thesis: verum