let F be Ring; :: thesis: for V, W being VectSp of F

for T being linear-transformation of V,W st T is one-to-one holds

ker T = (0). V

let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W st T is one-to-one holds

ker T = (0). V

let T be linear-transformation of V,W; :: thesis: ( T is one-to-one implies ker T = (0). V )

reconsider Z = (0). V as Subspace of ker T by VECTSP_4:39;

assume A1: T is one-to-one ; :: thesis: ker T = (0). V

for v being Element of (ker T) holds v in Z

for T being linear-transformation of V,W st T is one-to-one holds

ker T = (0). V

let V, W be VectSp of F; :: thesis: for T being linear-transformation of V,W st T is one-to-one holds

ker T = (0). V

let T be linear-transformation of V,W; :: thesis: ( T is one-to-one implies ker T = (0). V )

reconsider Z = (0). V as Subspace of ker T by VECTSP_4:39;

assume A1: T is one-to-one ; :: thesis: ker T = (0). V

for v being Element of (ker T) holds v in Z

proof

hence
ker T = (0). V
by VECTSP_4:32; :: thesis: verum
let v be Element of (ker T); :: thesis: v in Z

A2: v in ker T ;

assume not v in Z ; :: thesis: contradiction

then A3: not v = 0. V by VECTSP_4:35;

A4: ( T . (0. V) = 0. W & dom T = [#] V ) by Th7, Th9;

reconsider v = v as Element of V by VECTSP_4:10;

T . v = 0. W by A2, Th10;

hence contradiction by A1, A3, A4; :: thesis: verum

end;A2: v in ker T ;

assume not v in Z ; :: thesis: contradiction

then A3: not v = 0. V by VECTSP_4:35;

A4: ( T . (0. V) = 0. W & dom T = [#] V ) by Th7, Th9;

reconsider v = v as Element of V by VECTSP_4:10;

T . v = 0. W by A2, Th10;

hence contradiction by A1, A3, A4; :: thesis: verum