proposition: Lemma memv_sumP {P} {Us : I -> {vspace vT}} {v} : reflect (exists2 vs, forall i, P i -> vs i \in Us i & v = \sum_(i | P i) vs i) (v \in \sum_(i | P i) Us i)%VS.
proof: Proof. apply: (iffP idP) => [|[vs Uv ->]]; last exact: memv_sumr. rewrite memvK vs2mx_sum => /sub_sumsmxP[r /(canRL v2rK)->]. pose f i := r2v (r i *m vs2mx (Us i)); rewrite linear_sum /=. by exists f => //= i _; rewrite mem_r2v submxMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)