let R be Ring; for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @* l) . (T . v) = l . v
let V, W be LeftMod of R; for l being Linear_Combination of V
for T being linear-transformation of V,W
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @* l) . (T . v) = l . v
let l be Linear_Combination of V; for T being linear-transformation of V,W
for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @* l) . (T . v) = l . v
let T be linear-transformation of V,W; for v being Element of V st T | (Carrier l) is one-to-one & v in Carrier l holds
(T @* l) . (T . v) = l . v
let v be Element of V; ( T | (Carrier l) is one-to-one & v in Carrier l implies (T @* l) . (T . v) = l . v )
assume that
A1:
T | (Carrier l) is one-to-one
and
A2:
v in Carrier l
; (T @* l) . (T . v) = l . v
v in the carrier of V
;
then A3:
v in dom l
by FUNCT_2:def 1;
A4:
dom T = the carrier of V
by FUNCT_2:def 1;
for x being object holds
( x in (T " {(T . v)}) /\ (Carrier l) iff x in {v} )
proof
let x be
object ;
( x in (T " {(T . v)}) /\ (Carrier l) iff x in {v} )
hereby ( x in {v} implies x in (T " {(T . v)}) /\ (Carrier l) )
assume
x in (T " {(T . v)}) /\ (Carrier l)
;
x in {v}then A5:
(
x in T " {(T . v)} &
x in Carrier l )
by XBOOLE_0:def 4;
then A6:
(
x in the
carrier of
V &
T . x in {(T . v)} )
by FUNCT_2:38;
A7:
(T | (Carrier l)) . x =
T . x
by A5, FUNCT_1:49
.=
T . v
by A6, TARSKI:def 1
.=
(T | (Carrier l)) . v
by A2, FUNCT_1:49
;
A8:
x in dom (T | (Carrier l))
by A4, A5, RELAT_1:57;
v in dom (T | (Carrier l))
by A2, A4, RELAT_1:57;
then
x = v
by A1, A7, A8, FUNCT_1:def 4;
hence
x in {v}
by TARSKI:def 1;
verum
end;
assume
x in {v}
;
x in (T " {(T . v)}) /\ (Carrier l)
then A9:
x = v
by TARSKI:def 1;
(
x in the
carrier of
V &
T . x in {(T . v)} )
by A9, TARSKI:def 1;
then
x in T " {(T . v)}
by FUNCT_2:38;
hence
x in (T " {(T . v)}) /\ (Carrier l)
by A2, A9, XBOOLE_0:def 4;
verum
end;
then
(T " {(T . v)}) /\ (Carrier l) = {v}
by TARSKI:2;
then
canFS ((T " {(T . v)}) /\ (Carrier l)) = <*v*>
by FINSEQ_1:94;
then
lCFST (l,T,(T . v)) = <*(l . v)*>
by A3, FINSEQ_2:34;
then
Sum (lCFST (l,T,(T . v))) = l . v
by RLVECT_1:44;
hence
(T @* l) . (T . v) = l . v
by LDef5; verum