let V be Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)
let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)
let IQ be Subset of (Z_MQ_VectSp V); :: thesis: for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)
let lq be Linear_Combination of IQ; :: thesis: for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)
let m be Integer; :: thesis: for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)
let a be Element of F_Rat; :: thesis: for l being Linear_Combination of I st V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds
a * (Sum lq) = (MorphsZQ V) . (Sum l)
let l be Linear_Combination of I; :: thesis: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) implies a * (Sum lq) = (MorphsZQ V) . (Sum l) )
assume AS: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) ) ; :: thesis: a * (Sum lq) = (MorphsZQ V) . (Sum l)
reconsider lqa = a * lq as Linear_Combination of IQ by VECTSP_6:31;
thus a * (Sum lq) = Sum lqa by VECTSP_6:45
.= (MorphsZQ V) . (Sum l) by AS, XThSum1 ; :: thesis: verum