proposition: Lemma directv_sumP {Us : I -> {vspace vT}} : reflect (forall i, P i -> Us i :&: (\sum_(j | P j && (j != i)) Us j) = 0)%VS (directv (\sum_(i | P i) Us i)).
proof: Proof. rewrite directvE /= /dimv vs2mx_sum -mxdirectE; apply: (equivP mxdirect_sumsP). by do [split=> dxU i /dxU; rewrite -vs2mx_sum -vs2mxI -vs2mx0] => [/val_inj|->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)