proposition: Lemma directv_sum_unique {Us : I -> {vspace vT}} : reflect (forall us vs, (forall i, P i -> us i \in Us i) -> (forall i, P i -> vs i \in Us i) -> (\sum_(i | P i) us i == \sum_(i | P i) vs i) = [forall (i | P i), us i == vs i]) (directv (\sum_(i | P i) Us i)).
proof: Proof. apply: (iffP directv_sum_independent) => [dxU us vs Uu Uv | dxU us Uu u_0 i Pi]. apply/idP/forall_inP=> [|eq_uv]; last by apply/eqP/eq_bigr => i /eq_uv/eqP. rewrite -subr_eq0 -sumrB => /eqP/dxU eq_uv i Pi. by rewrite -subr_eq0 eq_uv // => j Pj; apply: memvB; move: j Pj. apply/eqP; have:= esym (dxU us \0 Uu _); rewrite u_0 big1_eq eqxx. by move/(_ _)/forall_inP=> -> // j _; apply: mem0v. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)