let L be Z_Lattice; :: thesis: for v, u being Vector of (DivisibleMod L)
for l being Linear_Combination of {u} holds SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))
let v, u be Vector of (DivisibleMod L); :: thesis: for l being Linear_Combination of {u} holds SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))
let l be Linear_Combination of {u}; :: thesis: SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))
per cases ( Carrier l = {} or Carrier l = {u} ) by ZFMISC_1:33, VECTSP_6:def 4;
suppose Carrier l = {} ; :: thesis: SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))
then A2: l = ZeroLC (DivisibleMod L) by VECTSP_6:def 3;
hence SumSc (v,l) = 0. F_Real by LmSumScDM11
.= (ScProductDM L) . (v,(0. (DivisibleMod L))) by ZMODLAT2:14
.= (ScProductDM L) . (v,((0. INT.Ring) * u)) by VECTSP_1:14
.= (ScProductDM L) . (v,((l . u) * u)) by A2, VECTSP_6:3 ;
:: thesis: verum
end;
suppose Carrier l = {u} ; :: thesis: SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u))
then consider F being FinSequence of (DivisibleMod L) such that
A3: ( F is one-to-one & rng F = {u} & SumSc (v,l) = Sum (ScFS (v,l,F)) ) by defSumScDM;
F = <*u*> by A3, FINSEQ_3:97;
then ScFS (v,l,F) = <*((ScProductDM L) . (v,((l . u) * u)))*> by ThScFSDM3;
hence SumSc (v,l) = (ScProductDM L) . (v,((l . u) * u)) by A3, RLVECT_1:44; :: thesis: verum
end;
end;