let W be Z_Module; for V being free finite-rank Z_Module
for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
let V be free finite-rank Z_Module; for A being Subset of V
for B being Basis of V
for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
let A be Subset of V; for B being Basis of V
for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
let B be Basis of V; for T being linear-transformation of V,W st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
let T be linear-transformation of V,W; ( A is Basis of (ker T) & A c= B implies T | (B \ A) is one-to-one )
assume that
A1:
A is Basis of (ker T)
and
A2:
A c= B
; T | (B \ A) is one-to-one
reconsider A9 = A as Subset of V ;
set f = T | (B \ A);
let x1, x2 be object ; FUNCT_1:def 4 ( not x1 in dom (T | (B \ A)) or not x2 in dom (T | (B \ A)) or not (T | (B \ A)) . x1 = (T | (B \ A)) . x2 or x1 = x2 )
assume that
A3:
x1 in dom (T | (B \ A))
and
A4:
x2 in dom (T | (B \ A))
and
A5:
(T | (B \ A)) . x1 = (T | (B \ A)) . x2
and
A6:
x1 <> x2
; contradiction
x2 in dom T
by A4, RELAT_1:57;
then reconsider x2 = x2 as Element of V ;
x1 in dom T
by A3, RELAT_1:57;
then reconsider x1 = x1 as Element of V ;
A7:
not x1 in A9 \/ {x2}
A9:
(T | (B \ A)) . x2 = T . x2
by A4, FUNCT_1:49;
reconsider A = A as Subset of (ker T) by A1;
reconsider A = A as Basis of (ker T) by A1;
A10:
ker T = Lin A
by VECTSP_7:def 3;
(T | (B \ A)) . x1 = T . x1
by A3, FUNCT_1:49;
then
x1 - x2 in ker T
by A5, A9, Th17;
then
x1 - x2 in Lin A9
by A10, ZMODUL03:20;
then A11:
x1 in Lin (A9 \/ {x2})
by Th18;
{x2} \/ {x1} = {x1,x2}
by ENUMSET1:1;
then A12:
(A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2}
by XBOOLE_1:4;
{x1,x2} c= B
then A14:
A9 \/ {x1,x2} c= B
by A2, XBOOLE_1:8;
B is linearly-independent
by VECTSP_7:def 3;
hence
contradiction
by A7, A11, A12, A14, Th21, ZMODUL02:56; verum