proposition: Lemma directv_sum_independent {Us : I -> {vspace vT}} : reflect (forall us, (forall i, P i -> us i \in Us i) -> \sum_(i | P i) us i = 0 -> (forall i, P i -> us i = 0)) (directv (\sum_(i | P i) Us i)).
proof: Proof. apply: (iffP directv_sumP) => [dxU us Uu u_0 i Pi | dxU i Pi]. apply/eqP; rewrite -memv0 -(dxU i Pi) memv_cap Uu //= -memvN -sub0r -{1}u_0. by rewrite (bigD1 i) //= addrC addKr memv_sumr // => j /andP[/Uu]. apply/eqP; rewrite -subv0; apply/subvP=> v. rewrite memv_cap memv0 => /andP[Uiv /memv_sumP[us Uu Dv]]. have: \sum_(j | P j) [eta us with i |-> - v] j = 0. rewrite (bigD1 i) //= eqxx {1}Dv addrC -sumrB big1 // => j /andP[_ i'j]. by rewrite (negPf i'j) subrr. move/dxU/(_ i Pi); rewrite /= eqxx -oppr_eq0 => -> // j Pj. by have [-> | i'j] := eqVneq; rewrite ?memvN // Uu ?Pj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)