let F be Field; for V, W being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
let V, W be VectSp of F; for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V 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; for A being Subset of V
for B being Basis of V 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 st A is Basis of (ker T) & A c= B holds
T | (B \ A) is one-to-one
let B be Basis of V; ( 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:
x1 in B \ A
by A3;
A8:
not x1 in A9 \/ {x2}
A10:
x2 in B \ A
by A4;
then A11:
(T | (B \ A)) . x2 = T . x2
by FUNCT_1:49;
reconsider A = A as Basis of (ker T) by A1;
A12:
ker T = Lin A
by VECTSP_7:def 3;
(T | (B \ A)) . x1 = T . x1
by A7, FUNCT_1:49;
then
x1 - x2 in ker T
by A5, A11, Th17;
then
x1 - x2 in Lin A9
by A12, VECTSP_9:17;
then A13:
x1 in Lin (A9 \/ {x2})
by Th18;
{x2} \/ {x1} = {x1,x2}
by ENUMSET1:1;
then A14:
(A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2}
by XBOOLE_1:4;
{x1,x2} c= B
then A16:
A9 \/ {x1,x2} c= B
by A2, XBOOLE_1:8;
B is linearly-independent
by VECTSP_7:def 3;
hence
contradiction
by A13, A14, A8, A16, Th21, VECTSP_7:1; verum