let R be Ring; for V, W being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for T being linear-transformation of V,W
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let V, W be LeftMod of R; for A being Subset of V
for l being Linear_Combination of A
for T being linear-transformation of V,W
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let A be Subset of V; for l being Linear_Combination of A
for T being linear-transformation of V,W
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let l be Linear_Combination of A; for T being linear-transformation of V,W
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let T be linear-transformation of V,W; for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
let v be Element of V; ( T | A is one-to-one & v in A implies ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X ) )
assume that
A1:
T | A is one-to-one
and
A2:
v in A
; ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
set X = (T " {(T . v)}) \ {v};
A3:
(T " {(T . v)}) \ {v} misses A
proof
dom T = [#] V
by RANKNULL:7;
then A4:
dom (T | A) = A
by RELAT_1:62;
assume
(T " {(T . v)}) \ {v} meets A
;
contradiction
then consider x being
object such that A5:
x in (T " {(T . v)}) \ {v}
and A6:
x in A
by XBOOLE_0:3;
not
x in {v}
by A5, XBOOLE_0:def 5;
then A7:
x <> v
by TARSKI:def 1;
x in T " {(T . v)}
by A5, XBOOLE_0:def 5;
then
T . x in {(T . v)}
by FUNCT_1:def 7;
then A8:
T . x = T . v
by TARSKI:def 1;
T . x = (T | A) . x
by A6, FUNCT_1:49;
then
(T | A) . v = (T | A) . x
by A2, A8, FUNCT_1:49;
hence
contradiction
by A1, A2, A4, A6, A7, FUNCT_1:def 4;
verum
end;
take
(T " {(T . v)}) \ {v}
; ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
{v} c= T " {(T . v)}
hence
( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
by A3, XBOOLE_1:45; verum