let V be Z_Module; for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds
Sum lq = (MorphsZQ V) . (Sum l)
let I be Subset of V; for IQ being Subset of (Z_MQ_VectSp V)
for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds
Sum lq = (MorphsZQ V) . (Sum l)
let IQ be Subset of (Z_MQ_VectSp V); for l being Linear_Combination of I
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds
Sum lq = (MorphsZQ V) . (Sum l)
let l be Linear_Combination of I; for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) holds
Sum lq = (MorphsZQ V) . (Sum l)
let lq be Linear_Combination of IQ; ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) implies Sum lq = (MorphsZQ V) . (Sum l) )
assume AS0:
( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & l = lq * (MorphsZQ V) )
; Sum lq = (MorphsZQ V) . (Sum l)
per cases
( I is empty or not I is empty )
;
suppose E1:
not
I is
empty
;
Sum lq = (MorphsZQ V) . (Sum l)then consider v0 being
object such that A7:
v0 in I
;
reconsider v0 =
v0 as
Vector of
V by A7;
(MorphsZQ V) . v0 in IQ
by A7, AS0, FUNCT_2:35;
then reconsider X =
IQ as non
empty Subset of
(Z_MQ_VectSp V) ;
reconsider g =
(MorphsZQ V) | I as
Function of
I,
IQ by FUNCT_2:101, AS0;
MorphsZQ V is
one-to-one
by defMorph, AS0;
then AX1:
g is
one-to-one
by FUNCT_1:52;
AX2:
rng g = IQ
by RELAT_1:115, AS0;
then reconsider F =
g " as
Function of
IQ,
I by FUNCT_2:25, AX1;
reconsider F =
F as
Function of
X, the
carrier of
V by E1, FUNCT_2:7;
X = IQ
;
then AX2A:
dom g = I
by FUNCT_2:def 1;
then AX3:
(
dom F = X &
rng F = I )
by AX1, AX2, FUNCT_1:33;
A8:
for
u being
Vector of
V st
u in I holds
F . ((MorphsZQ V) . u) = u
consider Gq being
FinSequence of
(Z_MQ_VectSp V) such that A9:
(
Gq is
one-to-one &
rng Gq = Carrier lq &
Sum lq = Sum (lq (#) Gq) )
by VECTSP_6:def 6;
set n =
len Gq;
A10:
dom Gq = Seg (len Gq)
by FINSEQ_1:def 3;
A11:
Carrier lq c= X
by VECTSP_6:def 4;
A12:
dom (F * Gq) = Seg (len Gq)
by A10, A9, AX3, RELAT_1:27, VECTSP_6:def 4;
A13:
rng (F * Gq) c= the
carrier of
V
;
F * Gq is
FinSequence
by AX3, A9, FINSEQ_1:16, VECTSP_6:def 4;
then reconsider FGq =
F * Gq as
FinSequence of
V by A13, FINSEQ_1:def 4;
for
x being
object holds
(
x in rng FGq iff
x in Carrier l )
proof
let x be
object ;
( x in rng FGq iff x in Carrier l )
hereby ( x in Carrier l implies x in rng FGq )
assume
x in rng FGq
;
x in Carrier lthen consider z being
object such that A14:
(
z in dom FGq &
x = FGq . z )
by FUNCT_1:def 3;
A15:
x = F . (Gq . z)
by A14, FUNCT_1:12;
A16:
(
z in dom Gq &
Gq . z in dom F )
by A14, FUNCT_1:11;
then consider u being
Vector of
V such that A17:
(
u in I &
Gq . z = (MorphsZQ V) . u )
by AS0, FUNCT_2:65;
A18:
F . (Gq . z) = u
by A8, A17;
consider w being
Element of
(Z_MQ_VectSp V) such that A19:
(
Gq . z = w &
lq . w <> 0. F_Rat )
by A9, A16, FUNCT_1:3, VECTSP_6:1;
l . u <> 0. F_Rat
by AS0, A17, A19, FUNCT_2:15;
hence
x in Carrier l
by A15, A18;
verum
end;
assume A20:
x in Carrier l
;
x in rng FGq
then reconsider u =
x as
Vector of
V ;
A21:
l . u <> 0
by A20, ZMODUL02:8;
A22:
Carrier l c= I
by VECTSP_6:def 4;
lq . ((MorphsZQ V) . u) <> 0
by AS0, A21, FUNCT_2:15;
then A23:
(MorphsZQ V) . u in rng Gq
by A9;
then consider z being
object such that A24:
(
z in dom Gq &
(MorphsZQ V) . u = Gq . z )
by FUNCT_1:def 3;
A25:
F . (Gq . z) = u
by A20, A22, A24, A8;
A26:
z in dom FGq
by A11, A9, A24, AX3, A23, FUNCT_1:11;
then
FGq . z = u
by A25, FUNCT_1:12;
hence
x in rng FGq
by A26, FUNCT_1:def 3;
verum
end; then
rng FGq = Carrier l
by TARSKI:2;
then A27:
Sum l = Sum (l (#) FGq)
by A9, AX1, VECTSP_6:def 6;
A28:
len (l (#) FGq) = len FGq
by VECTSP_6:def 5;
then A29:
len (l (#) FGq) = len Gq
by A12, FINSEQ_1:def 3;
A30:
len (lq (#) Gq) = len Gq
by VECTSP_6:def 5;
now for i being Element of NAT st i in dom (l (#) FGq) holds
ex si being VECTOR of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = (MorphsZQ V) . si )let i be
Element of
NAT ;
( i in dom (l (#) FGq) implies ex si being VECTOR of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = (MorphsZQ V) . si ) )assume A31:
i in dom (l (#) FGq)
;
ex si being VECTOR of V st
( si = (l (#) FGq) . i & (lq (#) Gq) . i = (MorphsZQ V) . si )then
i in Seg (len FGq)
by A28, FINSEQ_1:def 3;
then A32:
i in dom FGq
by FINSEQ_1:def 3;
then
FGq . i in rng FGq
by FUNCT_1:3;
then reconsider v =
FGq . i as
Element of
V ;
A33:
(l (#) FGq) . i = (l . v) * v
by A32, ZMODUL02:13;
i in Seg (len Gq)
by A29, A31, FINSEQ_1:def 3;
then A34:
i in dom Gq
by FINSEQ_1:def 3;
then A35:
Gq . i in rng Gq
by FUNCT_1:3;
reconsider w =
Gq . i as
Element of
(Z_MQ_VectSp V) by A35;
consider u being
Vector of
V such that A37:
(
u in I &
Gq . i = (MorphsZQ V) . u )
by AS0, A9, A11, A35, FUNCT_2:65;
A381:
F . (Gq . i) = u
by A8, A37;
then A38:
v = u
by A32, FUNCT_1:12;
A39:
w = (MorphsZQ V) . v
by A32, A37, A381, FUNCT_1:12;
A40:
lq . w = l . v
by AS0, A37, A38, FUNCT_2:15;
T1:
(lq . w) * w = (MorphsZQ V) . ((l . v) * v)
by defMorph, A39, A40, AS0;
thus
ex
si being
VECTOR of
V st
(
si = (l (#) FGq) . i &
(lq (#) Gq) . i = (MorphsZQ V) . si )
verum end; hence
Sum lq = (MorphsZQ V) . (Sum l)
by A9, A27, A29, A30, AS0, XThSum;
verum end;