let V be Z_Module; :: thesis: 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; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: Sum lq = (MorphsZQ V) . (Sum l)

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; :: thesis: 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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: Sum lq = (MorphsZQ V) . (Sum l)

per cases
( I is empty or not I is empty )
;

end;

suppose A3:
I is empty
; :: thesis: Sum lq = (MorphsZQ V) . (Sum l)

then
IQ = {} the carrier of (Z_MQ_VectSp V)
by AS0;

then lq = ZeroLC (Z_MQ_VectSp V) by VECTSP_6:6;

then A6: Sum lq = 0. (Z_MQ_VectSp V) by VECTSP_6:15;

I = {} the carrier of V by A3;

then l = ZeroLC V by ZMODUL02:12;

then Sum l = 0. V by ZMODUL02:19;

hence Sum lq = (MorphsZQ V) . (Sum l) by A6, defMorph, AS0; :: thesis: verum

end;then lq = ZeroLC (Z_MQ_VectSp V) by VECTSP_6:6;

then A6: Sum lq = 0. (Z_MQ_VectSp V) by VECTSP_6:15;

I = {} the carrier of V by A3;

then l = ZeroLC V by ZMODUL02:12;

then Sum l = 0. V by ZMODUL02:19;

hence Sum lq = (MorphsZQ V) . (Sum l) by A6, defMorph, AS0; :: thesis: verum

suppose E1:
not I is empty
; :: thesis: 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

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 )

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;

end;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

proof

consider Gq being FinSequence of (Z_MQ_VectSp V) such that
let u be Vector of V; :: thesis: ( u in I implies F . ((MorphsZQ V) . u) = u )

assume AS8: u in I ; :: thesis: F . ((MorphsZQ V) . u) = u

hence F . ((MorphsZQ V) . u) = F . (g . u) by FUNCT_1:49

.= u by FUNCT_1:34, AS8, AX2A, AX1 ;

:: thesis: verum

end;assume AS8: u in I ; :: thesis: F . ((MorphsZQ V) . u) = u

hence F . ((MorphsZQ V) . u) = F . (g . u) by FUNCT_1:49

.= u by FUNCT_1:34, AS8, AX2A, AX1 ;

:: thesis: verum

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

then
rng FGq = Carrier l
by TARSKI:2;
let x be object ; :: thesis: ( x in rng FGq iff x in Carrier l )

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; :: thesis: verum

end;hereby :: thesis: ( x in Carrier l implies x in rng FGq )

assume A20:
x in Carrier l
; :: thesis: x in rng FGqassume
x in rng FGq
; :: thesis: x in Carrier l

then 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; :: thesis: verum

end;then 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; :: thesis: verum

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; :: thesis: verum

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 :: thesis: 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 )

hence
Sum lq = (MorphsZQ V) . (Sum l)
by A9, A27, A29, A30, AS0, XThSum; :: thesis: verumex si being VECTOR of V st

( si = (l (#) FGq) . i & (lq (#) Gq) . i = (MorphsZQ V) . si )

let i be Element of NAT ; :: thesis: ( 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) ; :: thesis: 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 ) :: thesis: verum

end;( si = (l (#) FGq) . i & (lq (#) Gq) . i = (MorphsZQ V) . si ) )

assume A31: i in dom (l (#) FGq) ; :: thesis: 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 ) :: thesis: verum