let W be Z_Module; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: T | (B \ A) is one-to-one

reconsider A9 = A as Subset of V ;

set f = T | (B \ A);

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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}

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

B is linearly-independent by VECTSP_7:def 3;

hence contradiction by A7, A11, A12, A14, Th21, ZMODUL02:56; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: T | (B \ A) is one-to-one

reconsider A9 = A as Subset of V ;

set f = T | (B \ A);

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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}

proof

A9:
(T | (B \ A)) . x2 = T . x2
by A4, FUNCT_1:49;
assume A8:
x1 in A9 \/ {x2}
; :: thesis: contradiction

end;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

proof

then A14:
A9 \/ {x1,x2} c= B
by A2, XBOOLE_1:8;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x1,x2} or z in B )

assume A13: z in {x1,x2} ; :: thesis: z in B

end;assume A13: z in {x1,x2} ; :: thesis: z in B

B is linearly-independent by VECTSP_7:def 3;

hence contradiction by A7, A11, A12, A14, Th21, ZMODUL02:56; :: thesis: verum