proposition: Lemma memv_mulP (K : fieldType) (aT : falgType K) (U V : {vspace aT}) w : reflect (exists n (us vs : n.-tuple aT), [/\ all (mem U) us, all (mem V) vs & w = \sum_(i < n) tnth us i * tnth vs i]) (w \in (U * V)%VS).
proof: Proof. apply: (iffP idP) => [|[b [us [vs [usU vsV ->]]]]]; last first. by rewrite rpred_sum// => i _; rewrite memv_mul//; apply/all_tnthP. rewrite unlock span_def big_tuple => /memv_sumP[/= w_ w_mem ->]. have wP_ i : exists2 uv, (uv.1 \in U) && (uv.2 \in V) & w_ i = uv.1 * uv.2. have /vlineP[k ->] := w_mem i isT; set UV := (X in tnth X _). have /allpairsP[[u v] [uP vP ->]] := mem_tnth i UV. by exists (k *: u, v); rewrite /= ?rpredZ ?vbasis_mem// scalerAl. pose d := (\dim U * \dim V)%N; pose uv i := (projT1 (sig2_eqW (wP_ i))). exists d, [tuple (uv i).1 | i < _], [tuple (uv i).2 | i < _]; rewrite /uv. split; do ?by apply/allP => _/mapP[i _ ->]; case: sig2_eqW => /= ? /andP[]. by apply: eq_bigr => i; rewrite !tnth_map/= tnth_ord_tuple; case: sig2_eqW. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)