let F be Field; for V, W being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let V, W be VectSp of F; for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let T be linear-transformation of V,W; for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let X be Subset of V; for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let l be Linear_Combination of T .: X; ( T | X is one-to-one implies T @ (T # l) = l )
assume A1:
T | X is one-to-one
; T @ (T # l) = l
let w be Element of W; FUNCT_2:def 8 (T @ (T # l)) . w = l . w
set m = T @ (T # l);
per cases
( w in Carrier l or not w in Carrier l )
;
suppose A2:
w in Carrier l
;
(T @ (T # l)) . w = l . wthen A3:
l . w <> 0. F
by VECTSP_6:2;
A4:
dom (T # l) = [#] V
by FUNCT_2:92;
Carrier l c= T .: X
by VECTSP_6:def 4;
then consider v being
object such that A5:
v in dom T
and A6:
v in X
and A7:
w = T . v
by A2, FUNCT_1:def 6;
reconsider v =
v as
Element of
V by A5;
consider B being
Subset of
V such that A8:
B misses X
and A9:
T " {(T . v)} = {v} \/ B
by A1, A6, Th34;
A10:
(T # l) . v = l . (T . v)
by A1, A6, Th42;
A11:
(T # l) .: {v} =
Im (
(T # l),
v)
.=
{((T # l) . v)}
by A4, FUNCT_1:59
;
A12:
(T @ (T # l)) . w =
Sum ((T # l) .: (T " {(T . v)}))
by A7, Def5
.=
Sum ({(l . (T . v))} \/ ((T # l) .: B))
by A9, A10, A11, RELAT_1:120
;
end;