Library Ssreflect.vector

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop.
Require Import finfun tuple ssralg matrix mxalgebra zmodp.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Local Scope ring_scope.

Reserved Notation "{ 'vspace' T }" (at level 0, format "{ 'vspace' T }").
Reserved Notation "\dim A" (at level 10, A at level 8, format "\dim A").
Reserved Notation "v %:VS" (at level 2, format "v %:VS").
Reserved Notation "''Hom' ( V , W )" (at level 0, format "''Hom' ( V , W )").
Reserved Notation "''End' ( V )" (at level 0, format "''End' ( V )").
Reserved Notation "f \^-1" (at level 24).

Delimit Scope vspace_scope with VS.

Import GRing.Theory.

Module VectorType.

Section ClassDef.
Variable R : ringType.
Implicit Type phR : phant R.

Structure mixin_of (V : lmodType R) : Type := Mixin {
               dim : nat;
  v2rv_isomorphism : V-> 'rV[R]_dim;
                 _ : linear v2rv_isomorphism;
                 _ : bijective v2rv_isomorphism
}.

Structure class_of (V : Type) : Type := Class {
  base : GRing.Lmodule.class_of R V;
  mixin : mixin_of (GRing.Lmodule.Pack _ base V)
}.
Local Coercion base : class_of >-> GRing.Lmodule.class_of.

Structure type phR : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition class phR (cT : type phR):=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phR T cT c of phant_id (@class phR cT) c := @Pack phR T c T.

Definition pack phR V V0 (m0 : mixin_of (@GRing.Lmodule.Pack R _ V V0 V)) :=
  fun bT b & phant_id (@GRing.Lmodule.class _ phR bT) b =>
  fun m & phant_id m0 m => Pack phR (@Class V b m) V.

Definition eqType phR cT := Equality.Pack (@class phR cT) cT.
Definition choiceType phR cT := Choice.Pack (@class phR cT) cT.
Definition zmodType phR cT := GRing.Zmodule.Pack (@class phR cT) cT.
Definition lmodType phR cT := GRing.Lmodule.Pack phR (@class phR cT) cT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> GRing.Lmodule.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType: type >-> Equality.type.
Bind Scope ring_scope with sort.
Canonical Structure eqType.
Coercion choiceType: type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType: type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion lmodType: type>-> GRing.Lmodule.type.
Canonical Structure lmodType.
Notation vectType R := (@type _ (Phant R)).
Notation VectType R m :=
   (@pack _ (Phant R) _ _ m _ _ id _ id).
Notation VectMixin := Mixin.
End Exports.

End VectorType.
Import VectorType.Exports.

Section VectorTypeTheory.

Variable (R : ringType) (V : vectType R).

Definition vdim := (VectorType.dim (VectorType.class V)).

Definition v2rv_isomorphism :=
 (@VectorType.v2rv_isomorphism _ _
    (@VectorType.mixin _ _ (VectorType.class V))).
Local Notation v2rv := v2rv_isomorphism.

Lemma v2rv_linear_proof : linear v2rv.
Proof. by rewrite /v2rv_isomorphism; case:(VectorType.class V)=> ? []. Qed.
Canonical Structure v2rv_linear := Linear v2rv_linear_proof.

Lemma v2rv_bij : bijective v2rv.
Proof.
by rewrite /v2rv_isomorphism; case:(VectorType.class V)=> ? [] . Qed.

Lemma v2rv_inj : injective v2rv.
Proof. by apply:(bij_inj v2rv_bij ). Qed.

Fact rv2v_proof : forall (rv :'rV[R]_vdim), exists v, rv == v2rv v.
Proof.
by move => rv; case:v2rv_bij => g Hg Hf;by exists (g rv);rewrite Hf.
Qed.

Definition rv2v_isomorphism := fun rv => xchoose (rv2v_proof rv).
Local Notation rv2v := rv2v_isomorphism.

Lemma rv2vK : cancel rv2v_isomorphism v2rv.
Proof.
by move => x; case/xchooseP:(rv2v_proof x);move /eqP => H;apply sym_equal.
Qed.

Lemma v2rvK : cancel v2rv rv2v.
Proof. by move=> v;apply:v2rv_inj;rewrite rv2vK. Qed.

Lemma rv2v_bij : bijective rv2v.
Proof. by apply:(bij_can_bij v2rv_bij); apply:v2rvK. Qed.

Lemma rv2v_inj : injective rv2v.
Proof. by apply:(bij_inj rv2v_bij ). Qed.

Lemma rv2v_linear_proof : linear rv2v.
Proof.
move => a v w;apply:v2rv_inj. rewrite rv2vK.
by rewrite !linearP /= !rv2vK.
Qed.
Canonical Structure rv2v_linear := Linear rv2v_linear_proof.

Variables m n : nat.

Lemma mxvec_bij : bijective (@mxvec R m n).
Proof. exists vec_mx; [exact: mxvecK | exact: vec_mxK]. Qed.

Definition matrixVectMixin := VectMixin (@mxvec_is_linear R m n) mxvec_bij.
Canonical Structure matrixVectType := VectType R matrixVectMixin.

End VectorTypeTheory.

Canonical Structure matrixVectType.


Section VSpaceDef.
Variable (K : fieldType) (V : vectType K).
Implicit Type u v : V.

Let n := vdim V.

Local Notation v2rv := (@v2rv_isomorphism _ V).
Local Notation rv2v := (@rv2v_isomorphism _ V).

Lemma v2rv_isom : exists f', [/\ cancel v2rv f', cancel f' v2rv & linear f'].
Proof.
by exists rv2v; split;
  [apply: v2rvK | apply: rv2vK | move=> a u v; rewrite linearP].
Qed.

Structure vspace : Type := VSpace {
    vs2mx : 'M[K]_n;
        _ : <<vs2mx>>%MS == vs2mx
}.

Definition vspace_of of phant V := vspace.
Local Notation "{ 'vspace' T }" := (vspace_of (Phant T)) : type_scope.

Canonical Structure vspace_subType :=
  Eval hnf in [subType for vs2mx by vspace_rect].
Canonical Structure vspace_eqMixin := [eqMixin of vspace by <:].
Canonical Structure vspace_eqType := Eval hnf in EqType vspace vspace_eqMixin.
Definition vspace_choiceMixin := [choiceMixin of vspace by <:].
Canonical Structure vspace_choiceType :=
  Eval hnf in ChoiceType vspace vspace_choiceMixin.

Canonical Structure vspace_of_subType := Eval hnf in [subType of {vspace V}].
Canonical Structure vspace_of_eqType := Eval hnf in [eqType of {vspace V}].
Canonical Structure vspace_for_choiceType :=
  Eval hnf in [choiceType of {vspace V}].

Implicit Type vs : {vspace V}.

Lemma vspace_ax: forall vs, <<vs2mx vs>>%MS == vs2mx vs.
Proof. by case. Qed.

Definition mx2vs m (v : 'M_(m,n)) : {vspace V} :=
  VSpace (@introTF _ _ true eqP (genmx_id v)).

Lemma vs2mxK : cancel vs2mx (@mx2vs n).
Proof. by move=> [mx Hmx]; apply/eqP. Qed.

Lemma mx2vsK : forall m (M : 'M_(m,n)), (vs2mx (mx2vs M) :=: M)%MS.
Proof. by move=> m M; apply/eqmxP; rewrite !genmxE !submx_refl. Qed.

Lemma vseq2mxeq : forall vs1 vs2, (vs1 == vs2) = (vs2mx vs1 == vs2mx vs2)%MS.
Proof.
move=> [m1 Hm1] [m2 Hm2]; rewrite /eq_op /= -{1}(eqP Hm1) -{1}(eqP Hm2).
apply/eqP/idP; first by move/genmxP.
by move=> H; apply/genmxP.
Qed.

Lemma mxeq2vseq: forall m1 m2 M1 M2,
   (M1 == M2)%MS = (@mx2vs m1 M1 == @mx2vs m2 M2).
Proof.
move=> m1 m2 M1 M2; rewrite /eq_op /=.
apply/idP/eqP; first by move/eqmxP; move/eq_genmx.
by move/genmxP.
Qed.

Definition subsetv vs1 vs2 := (submx (vs2mx vs1) (vs2mx vs2)).
Local Notation "A <= B" := (subsetv A B) : vspace_scope.

Lemma subv_refl : reflexive subsetv.
Proof. by move=> vs; exact: submx_refl. Qed.
Hint Resolve subv_refl.

Lemma subv_trans : transitive subsetv.
Proof. by move=> vs1 vs2 vs3; exact: submx_trans. Qed.

Lemma subv_anti : antisymmetric subsetv.
Proof. by move=> vs1 vs2 H; apply/eqP; rewrite vseq2mxeq. Qed.

Definition injv (v: V) : {vspace V} := mx2vs (v2rv v).

Local Notation "v %:VS" := (injv v) : ring_scope.

Canonical Structure vpredType := mkPredType (fun vs v => (v%:VS <= vs)%VS).

Lemma vs2mx0 : vs2mx 0%:VS = 0.
Proof. by rewrite /injv linear0 /= genmx0. Qed.

Lemma mx2vs0: forall m, mx2vs (0 : 'M_(m,n)) = 0%:VS.
Proof. by move=> m; apply/eqP; rewrite /eq_op /= linear0 !genmx0. Qed.

Lemma injvP : forall v1 v2, reflect (exists k, v1 = k *: v2) (v1 \in v2%:VS).
Proof.
move=> v1 v2; apply: (iffP idP); rewrite /in_mem /= /subsetv /injv !genmxE.
  by move/sub_rVP=> [k Hk]; exists k;apply: v2rv_inj; rewrite linearZ.
move=> [k ->]; rewrite linearZ;apply: scalemx_sub; apply submx_refl.
Qed.

Lemma mem0v : forall vs, 0 \in vs.
Proof. by move=> vs; rewrite /in_mem /= /subsetv vs2mx0 sub0mx. Qed.

Lemma memv_inj : forall v, v \in v%:VS.
Proof. by move=> x; apply/injvP; exists 1; rewrite scale1r. Qed.

Lemma memvD : forall vs v1 v2, v1 \in vs -> v2 \in vs -> v1 + v2 \in vs.
Proof.
move=> v1 v2 vs; rewrite /in_mem /= /subsetv /injv !mx2vsK => H1 H2.
by rewrite linearD addmx_sub.
Qed.

Lemma memvMn : forall vs v m, v \in vs -> v *+ m \in vs.
Proof.
move=> vs v m Hv; elim:m => [|m IH]; first by rewrite mulr0n mem0v.
by rewrite mulrS memvD.
Qed.

Lemma memvZl : forall vs k v, v \in vs -> k *: v \in vs.
Proof.
move=> vs k v; rewrite /in_mem /= /subsetv /injv /= !mx2vsK => Hvvs.
by rewrite linearZ scalemx_sub.
Qed.

Lemma memvZ : forall vs k v, (k *: v \in vs) = (k == 0) || (v \in vs).
Proof.
move=> vs k v; case: eqP=> Hk; first by rewrite Hk scale0r mem0v.
move/eqP: Hk=> Hk; apply/idP/idP=> Hi; last exact: memvZl.
by rewrite -[v](scalerK Hk) memvZl.
Qed.

Lemma memvNr : forall vs v, v \in vs -> -v \in vs.
Proof. move=> vs v Hv; rewrite -scaleN1r; exact: memvZl. Qed.

Lemma memvNl : forall vs v, -v \in vs -> v \in vs.
Proof. move=> vs v Hv; rewrite -[v]opprK; exact: memvNr. Qed.

Lemma memv_sub : forall vs v1 v2, v1 \in vs -> v2 \in vs -> v1 - v2 \in vs.
Proof. by move=> vs v1 v2 Hv1 Hv2; rewrite memvD // memvNr. Qed.

Lemma memvDl : forall vs v1 v2, v1 \in vs -> (v1 + v2 \in vs) = (v2 \in vs).
Proof.
move=> vs v1 v2 Hv1; apply/idP/idP=> Hv2; last exact: memvD.
rewrite -[v2](addKr v1); apply: memvD=> //; exact: memvNr.
Qed.

Lemma memvDr : forall vs v1 v2, v1 \in vs -> (v2 + v1 \in vs) = (v2 \in vs).
Proof. move=> vs v1 v2; rewrite addrC; exact: memvDl. Qed.

Lemma memvN : forall vs v, (-v \in vs) = (v \in vs).
Proof. move=> *; apply/idP/idP; [exact: memvNl | exact: memvNr]. Qed.

Lemma memv_subl : forall vs v1 v2, v1 \in vs -> (v1 - v2 \in vs) = (v2 \in vs).
Proof. move=> *; rewrite memvDl //; exact: memvN. Qed.

Lemma memv_subr : forall vs v1 v2, v1 \in vs -> (v2 - v1 \in vs) = (v2 \in vs).
Proof. move=> *; rewrite memvDr //; exact: memvNr. Qed.

Lemma memv_suml : forall (I : finType) (P : pred I) (vs_ : I -> V) vs,
  (forall i, P i -> vs_ i \in vs) -> \sum_(i | P i) vs_ i \in vs.
Proof.
move=> I P v_ vs Hp; apply big_prop => //; first by apply mem0v.
by exact: memvD.
Qed.

Lemma rv2v_iE : forall i vs,
      <<row i (vs2mx vs)>>%MS = vs2mx (rv2v (row i (vs2mx vs)))%:VS.
Proof.
by move=> i vs;rewrite /injv /=; congr genmx; rewrite rv2vK.
Qed.

Lemma subvP : forall vs1 vs2,
  reflect (forall v, v \in vs1 -> v \in vs2) (vs1 <= vs2)%VS.
Proof.
move=> vs1 vs2; apply: (iffP idP).
  rewrite /in_mem /= /subsetv; move=> Hvs1vs2 v.
  by rewrite /injv !genmxE => Hv1; apply: submx_trans Hvs1vs2.
move=> Hv; rewrite /subsetv;apply/row_subP=> i; rewrite -genmxE.
rewrite (rv2v_iE i vs1); apply: Hv.
rewrite /in_mem /= /subsetv -(rv2v_iE i vs1) genmxE.
move: i; apply/row_subP; apply submx_refl.
Qed.

Lemma vspaceP : forall vs1 vs2, reflect (vs1 =i vs2) (vs1 == vs2)%VS.
Proof.
move=> vs1 vs2; apply: (iffP eqP); first by move->.
by move=> Hs; apply: subv_anti; apply/andP; split; apply/subvP=> v;
  rewrite Hs.
Qed.


Lemma sub0v : forall vs, (0%:VS <= vs)%VS.
Proof. by move=> vs; rewrite /subsetv vs2mx0 sub0mx. Qed.

Lemma subv0 : forall vs, (vs <= 0%:VS)%VS = (vs == 0%:VS).
Proof.
by move=> vs; rewrite /subsetv /eq_op /= linear0 genmx0 submx0.
Qed.

Lemma memv0 : forall v, v \in 0%:VS = (v == 0).
Proof.
move=> v; apply/idP/eqP; last by move->; exact: mem0v.
by move/injvP=> [k ->]; rewrite scaler0.
Qed.

Definition fullv := mx2vs (1%:M).

Lemma vs2mxf : (vs2mx fullv :=: 1%:M)%MS.
Proof. by apply/eqmxP; rewrite mxeq2vseq vs2mxK. Qed.

Lemma mx2vsf : mx2vs (1%:M) = fullv.
Proof. done. Qed.

Lemma subvf : forall vs, (vs <= fullv)%VS.
Proof. by move=> vs; rewrite /subsetv mx2vsK submx1. Qed.

Lemma memvf : forall v, v \in fullv.
Proof. move=> v; exact: subvf. Qed.

Definition vpick vs : V :=
 if [pick i | row i (vs2mx vs) != 0] is Some i then
 (rv2v (row i (vs2mx vs))) else 0.

Lemma memv_pick : forall vs, vpick vs \in vs.
Proof.
move=> vs; rewrite /vpick; case: pickP=> [i|] Hi; last by exact: mem0v.
by rewrite /in_mem /= /subsetv -rv2v_iE genmxE row_sub.
Qed.

Lemma vpick0 : forall vs, (vpick vs == 0) = (vs == 0%:VS).
Proof.
move=>vs; apply/eqP/eqP; last first.
  move->; rewrite /vpick; case: pickP=> [i|] Hi //.
  case/negP: Hi; apply/eqP; apply/matrixP=> i1 j1.
  by rewrite vs2mx0 !mxE.
rewrite /vpick; case: pickP=> [i|] Hi //= => H1.
  by case/negP: Hi; rewrite -mxrank_eq0 -mxrank_gen rv2v_iE H1 vs2mx0 mxrank0.
apply/eqP; rewrite /eq_op /=; apply/eqP; apply/row_matrixP=> i.
by rewrite linear0 genmx0 row0; move/eqP: (Hi i).
Qed.

Definition addv vs1 vs2 := mx2vs (vs2mx vs1 + vs2mx vs2)%MS.
Arguments Scope addv [vspace_scope].
Local Notation "A + B" := (addv A B) : vspace_scope.
Local Notation "\sum_ ( i <- r | P ) B" := (\big[addv/0%:VS]_(i <- r | P) B%VS)
  : vspace_scope.
Local Notation "\sum_ ( i <- r ) B" := (\big[addv/0%:VS]_(i <- r) B%VS)
  : vspace_scope.
Local Notation "\sum_ ( i | P ) B" := (\big[addv/0%:VS]_(i | P) B%VS)
  : vspace_scope.
Local Notation "\sum_ ( i < n ) B" :=
  (\big[addv/0%:VS]_(i < n) B%VS) : vspace_scope.

Lemma mx2vsD : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 + M2)%MS = (mx2vs M1 + mx2vs M2)%VS.
Proof.
move=> m1 m2 M1 M2; apply/eqP; rewrite /mx2vs /eq_op /=.
by apply/eqP; apply: eq_genmx; apply: eqmx_sym; apply adds_eqmx; apply: genmxE.
Qed.

Lemma vs2mx_morph : {morph vs2mx : u v / (u + v)%VS >-> (u + v)%MS}.
Proof.
move=> u v.
rewrite /= /addsmx; case: addsmx_key=> /=; rewrite /addsmx_def.
do 2
  (case: eqP=> _; first by rewrite conform_mx_id; apply/eqP; apply: vspace_ax).
apply: genmx_id.
Qed.

Lemma vs2mx_sum : forall (I : finType) (P : pred I) (vs_ : I -> {vspace V}),
   (vs2mx (\sum_(i | P i) vs_ i))%VS = (\sum_(i | P i) (vs2mx (vs_ i)))%MS.
Proof.
by move=> I P vs_; apply: big_morph; [exact: vs2mx_morph | exact: vs2mx0].
Qed.

Lemma mx2vsDr : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 + vs2mx (mx2vs M2))%MS = mx2vs (M1 + M2)%MS.
Proof. by move=> m1 m2 M1 M2; rewrite !mx2vsD vs2mxK. Qed.

Lemma mx2vsDl : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (vs2mx (mx2vs M1) + M2)%MS = mx2vs (M1 + M2)%MS.
Proof. by move=> m1 m2 M1 M2; rewrite !mx2vsD vs2mxK. Qed.

Lemma subv_add : forall vs1 vs2 vs3,
  (vs1 + vs2 <= vs3)%VS = (vs1 <= vs3)%VS && (vs2 <= vs3)%VS.
Proof.
by move=> vs1 vs2 vs3; rewrite /subsetv vs2mx_morph; exact: addsmx_sub.
Qed.

Lemma addvSl : forall vs1 vs2, (vs1 <= vs1 + vs2)%VS.
Proof. by move=> vs1 vs2; rewrite /subsetv vs2mx_morph; exact: addsmxSl. Qed.

Lemma addvSr : forall vs1 vs2, (vs2 <= vs1 + vs2)%VS.
Proof. by move=> vs1 vs2; rewrite /subsetv vs2mx_morph; exact: addsmxSr. Qed.

Lemma addvKl : forall vs1 vs2, (vs1 <= vs2)%VS = (vs1 + vs2 == vs2)%VS.
Proof.
move=> vs1 vs2; apply/idP/eqP=> Hs; last first.
  by rewrite -Hs addvSl.
by apply subv_anti; rewrite subv_add Hs subv_refl addvSr.
Qed.

Lemma addvKr: forall vs1 vs2, (vs2 <= vs1)%VS = (vs1 + vs2 == vs1)%VS.
Proof.
move=> vs1 vs2; apply/idP/eqP=> Hs; last first.
  by rewrite -Hs addvSr.
by apply subv_anti; rewrite subv_add Hs subv_refl addvSl.
Qed.

Lemma addvC : commutative addv.
Proof.
by move=> vs1 vs2; apply/eqP; rewrite -mxeq2vseq addsmxC submx_refl.
Qed.

Lemma addvA : associative addv.
Proof.
move=> vs1 vs2 vs3.
rewrite /addv mx2vsDr mx2vsDl.
by apply/eqP; rewrite -mxeq2vseq addsmxA !submx_refl.
Qed.

Lemma addvS : forall vs1 vs2 vs3 vs4,
  (vs1 <= vs2 -> vs3 <= vs4 -> vs1 + vs3 <= vs2 + vs4)%VS.
Proof.
by move=> vs1 vs2 vs3 v4; rewrite /subsetv !vs2mx_morph; exact: addsmxS.
Qed.

Lemma addvv : idempotent addv.
Proof. by move=> x; apply/eqP; rewrite -addvKr. Qed.

Lemma sum0v : left_id 0%:VS addv.
Proof.
move=> vs; rewrite /addv vs2mx0 -{2}[vs]vs2mxK.
apply/eqP; rewrite -mxeq2vseq; apply/eqmxP; exact: adds0mx.
Qed.

Lemma addv0 : right_id 0%:VS addv.
Proof.
move=> vs; rewrite /addv vs2mx0 -{2}[vs]vs2mxK.
apply/eqP; rewrite -mxeq2vseq; apply/eqmxP; exact: addsmx0.
Qed.

Lemma sumfv : left_zero fullv addv.
Proof.
by move=> vs;apply:subv_anti;apply/andP;split;[apply:subvf|apply:addvSl].
Qed.

Lemma addvf : right_zero fullv addv.
Proof.
by move=> vs;apply: subv_anti;apply/andP;split;
     [apply: subvf|apply: addvSr].
Qed.

Lemma memv_add : forall v1 v2 vs1 vs2,
  v1 \in vs1 -> v2 \in vs2 -> v1 + v2 \in (vs1 + vs2)%VS.
Proof.
move=> v1 v2 vs1 vs2 Hv1 Hv2.
by apply memvD; [move: v1 Hv1| move: v2 Hv2];
   apply/subvP; rewrite (addvSr, addvSl).
Qed.

Lemma memv_addP : forall v vs1 vs2,
  reflect (exists v1, exists v2, [/\ v1 \in vs1, v2 \in vs2 & v = v1 + v2])
           (v \in (vs1 + vs2)%VS).
Proof.
move=> v vs1 vs2; apply: (iffP idP); last first.
  by move=> [v1 [v2 [Hv1 Hv2 ->]]]; apply: memv_add.
rewrite {1}/in_mem /= /subsetv /addv /= !genmxE addsmxE.
case/submxP; move=> x Hx.
exists (rv2v (lsubmx x *m vs2mx vs1)); exists (rv2v (rsubmx x *m vs2mx vs2));
   split.
- rewrite /in_mem /= /injv rv2vK /= /subsetv /= genmxE; apply/submxP.
  by exists(lsubmx x).
- rewrite /in_mem /= /injv rv2vK /= /subsetv /= genmxE; apply/submxP.
  by exists(rsubmx x).
by rewrite -linearD -mul_row_col hsubmxK -Hx /= v2rvK.
Qed.
Implicit Arguments memv_addP [v vs1 vs2].

Canonical Structure addv_monoid := Monoid.Law addvA sum0v addv0.
Canonical Structure addv_comoid := Monoid.ComLaw addvC.

Section BigSum.
Variable I : finType.
Implicit Type P : pred I.

Lemma sumv_sup : forall i0 P vs (vs_ : I -> {vspace V}),
  P i0 -> (vs <= vs_ i0)%VS ->
   (vs <= \sum_(i | P i) vs_ i)%VS.
Proof.
move=> i0 P vs vs_ Pi0 Hvs; apply: subv_trans Hvs _.
by rewrite (bigD1 i0) // addvSl.
Qed.

Implicit Arguments sumv_sup [P vs vs_].

Lemma subv_sumP : forall P (vs_ : I -> {vspace V}) vs,
  reflect (forall i, P i -> vs_ i <= vs)%VS
          (\sum_(i | P i) vs_ i <= vs)%VS.
Proof.
move=> P vs_ vs; apply: (iffP idP) => [Hvs i Pi | Hvs].
  by apply: subv_trans Hvs; apply: sumv_sup Pi _.
by apply big_prop => // [|vs1 vs2 Hvs1]; rewrite ?sub0v // subv_add Hvs1.
Qed.

Lemma memv_sumP : forall P (vs_ : I -> {vspace V}) v,
  reflect (exists v_ : I -> V,
            (forall i, P i -> v_ i \in vs_ i) /\
             v = \sum_(i | P i) v_ i)
          (v \in (\sum_(i | P i) vs_ i)%VS).
Proof.
move=> P vs_ v; elim: {P}_.+1 {-2}P v (ltnSn #|P|) => // n1 Hrec P v.
case: (pickP P) => [i Pi | P0 _]; last first.
  rewrite big_pred0 // memv0.
  apply: (iffP eqP)=> [-> | [v_ [H1v ->]]] //; last by rewrite big_pred0.
  exists (fun _ => 0); split; last by rewrite big_pred0.
  by move=> i; rewrite mem0v.
rewrite (cardD1x Pi) (bigD1 i) //=; move/Hrec=> {n1 Hrec} /= IHi.
apply: (iffP memv_addP) => [ [v1 [v2 [Hv1 Hv2 ->]]] | [v_ [H1v ->]]].
  case/IHi: Hv2=> v_ [H1v H2v].
  exists [eta v_ with i |-> v1]; split=> /=.
    move=> i1 Pi1; case: eqP; first by move->.
    by move/eqP=> Hi1; apply: H1v; rewrite Pi1.
  rewrite (bigD1 i) //= eqxx H2v.
  by congr (_ + _); apply: eq_big => j //; case: eqP; rewrite // andbF.
exists (v_ i); exists (\sum_(j | P j && (j != i)) v_ j); split;
    last by rewrite (bigD1 i).
  exact: H1v.
apply/IHi; exists v_; split=> //.
by move=> j; case/andP=> H1j H2j; exact: H1v.
Qed.

Lemma memv_sumr : forall P (vs_ : I -> V) (Vs_ : I -> {vspace V}),
  (forall i, P i -> vs_ i \in Vs_ i) ->
  \sum_(i | P i) vs_ i \in (\sum_(i | P i) Vs_ i)%VS.
Proof. by move => P vs_ Vs_ Hi; apply/memv_sumP; exists vs_. Qed.

End BigSum.

Definition capv vs1 vs2 := mx2vs (vs2mx vs1 :&: vs2mx vs2)%MS.
Local Notation "A :&: B" := (capv A B) : vspace_scope.
Local Notation "\bigcap_ ( i <- r | P ) B" := (\big[capv/fullv]_(i <- r | P) B)
  : vspace_scope.
Local Notation "\bigcap_ ( i | P ) B" := (\big[capv/fullv]_(i | P) B)
  : vspace_scope.

Lemma capv_mx2vs : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 :&: M2)%MS = (mx2vs M1 :&: mx2vs M2)%VS.
Proof.
move=> m1 m2 M1 M2; apply/eqP; rewrite /mx2vs /eq_op /=.
by apply/eqP; apply: eq_genmx; apply: eqmx_sym; apply cap_eqmx; apply: genmxE.
Qed.

Lemma capv_vs2mx : forall vs1 vs2,
 (vs2mx (vs1 :&: vs2)%VS :=: vs2mx vs1 :&: vs2mx vs2)%MS.
Proof.
by move=> vs1 vs2; apply/eqmxP; rewrite mxeq2vseq capv_mx2vs !vs2mxK.
Qed.

Lemma capv_mx2vsr : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 :&: vs2mx (mx2vs M2))%MS = mx2vs (M1 :&: M2)%MS.
Proof. by move=> m1 m2 M1 M2; rewrite !capv_mx2vs vs2mxK. Qed.

Lemma capv_mx2vsl : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (vs2mx (mx2vs M1) :&: M2)%MS = mx2vs (M1 :&: M2)%MS.
Proof. by move=> m1 m2 M1 M2; rewrite !capv_mx2vs vs2mxK. Qed.

Lemma subv_cap : forall vs1 vs2 vs3,
  (vs1 <= vs2 :&: vs3)%VS = (vs1 <= vs2)%VS && (vs1 <= vs3)%VS.
Proof.
by move=> vs1 vs2 vs3; rewrite /subsetv capv_vs2mx; exact: sub_capmx.
Qed.

Lemma capvSl : forall vs1 vs2, (vs1 :&: vs2 <= vs1)%VS.
Proof. by move=> vs1 vs2; rewrite /subsetv capv_vs2mx; exact: capmxSl. Qed.

Lemma capvSr : forall vs1 vs2, (vs1 :&: vs2 <= vs2)%VS.
Proof. by move=> vs1 vs2; rewrite /subsetv capv_vs2mx; exact: capmxSr. Qed.

Lemma capvKl : forall vs1 vs2, (vs1 <= vs2)%VS = (vs1 :&: vs2 == vs1)%VS.
Proof.
move=> vs1 vs2; apply/idP/eqP=> Hs; last first.
  by rewrite -Hs capvSr.
by apply subv_anti; rewrite subv_cap Hs subv_refl capvSl.
Qed.

Lemma capvKr : forall vs1 vs2, ((vs2 <= vs1) = (vs1 :&: vs2 == vs2))%VS.
Proof.
move=> vs1 vs2; apply/idP/eqP=> Hs; last first.
  by rewrite -Hs capvSl.
by apply subv_anti; rewrite subv_cap Hs subv_refl capvSr.
Qed.

Lemma capvv : idempotent capv.
Proof. by move=> x; apply/eqP; rewrite -capvKr. Qed.

Lemma capvC : commutative capv.
Proof.
by move=> vs1 vs2; apply/eqP; rewrite -mxeq2vseq capmxC !submx_refl.
Qed.

Lemma capvA : associative capv.
Proof.
move=> vs1 vs2 vs3; rewrite /capv capv_mx2vsr capv_mx2vsl.
by apply/eqP; rewrite -mxeq2vseq capmxA !submx_refl.
Qed.

Lemma capvS : forall vs1 vs2 vs3 vs4,
  (vs1 <= vs2 -> vs3 <= vs4 -> vs1 :&: vs3 <= vs2 :&: vs4)%VS.
Proof.
by move=> vs1 vs2 vs3 v4; rewrite /subsetv !capv_vs2mx; exact: capmxS.
Qed.

Lemma cap0v : left_zero 0%:VS capv.
Proof.
move=> vs;apply: subv_anti;apply/andP;split; [apply: capvSl| apply: sub0v].
Qed.

Lemma capv0 : right_zero 0%:VS capv.
Proof.
move=> vs;apply: subv_anti; apply/andP; split;
                                     [apply: capvSr| apply: sub0v].
Qed.

Lemma capfv : left_id fullv capv.
Proof. by move=> vs; rewrite /capv /fullv capv_mx2vsl cap1mx vs2mxK. Qed.

Lemma capvf : right_id fullv capv.
Proof. by move=> vs; rewrite /capv /fullv capv_mx2vsr capmx1 vs2mxK. Qed.

Lemma memv_cap : forall v vs1 vs2,
  (v \in (vs1 :&: vs2)%VS) = (v \in vs1) && (v \in vs2).
Proof. by move=> v vs1 vs2; rewrite /in_mem /= subv_cap. Qed.

Lemma vspace_modl : forall vs1 vs2 vs3,
  (vs1 <= vs3 -> vs1 + (vs2 :&: vs3) = (vs1 + vs2) :&: vs3)%VS.
Proof.
move=> vs1 vs2 vs3; rewrite /subsetv /= => Hv.
rewrite /capv /addv !capv_mx2vsl mx2vsDr.
by apply/eqP; rewrite -mxeq2vseq; apply/eqmxP; apply: matrix_modl.
Qed.

Lemma vspace_modr : forall vs1 vs2 vs3,
  (vs3 <= vs1 -> (vs1 :&: vs2) + vs3 = vs1 :&: (vs2 + vs3))%VS.
Proof.
move=> vs1 vs2 vs3; rewrite /subsetv /= => Hv.
rewrite /capv /addv !capv_mx2vsr mx2vsDl.
by apply/eqP; rewrite -mxeq2vseq; apply/eqmxP; apply: matrix_modr.
Qed.

Canonical Structure capv_monoid := Monoid.Law capvA capfv capvf.
Canonical Structure capv_comoid := Monoid.ComLaw capvC.

Section BigCap.
Variable I : finType.
Implicit Type P : pred I.

Lemma bigcapv_inf : forall i0 P (vs_ : I -> {vspace V}) vs,
  P i0 -> (vs_ i0 <= vs -> \bigcap_(i | P i) vs_ i <= vs)%VS.
Proof.
move=> i0 P vs_ vs Pi0 Hvs; apply: subv_trans Hvs.
by rewrite (bigD1 i0) // capvSl.
Qed.

Lemma subv_bigcapP : forall P vs (vs_ : I -> {vspace V}),
  reflect (forall i, P i -> vs <= vs_ i)%VS
          (vs <= \bigcap_(i | P i) vs_ i)%VS.
Proof.
move=> P vs vs_; apply: (iffP idP) => [Hvs i Pi | Hvs].
  by apply: (subv_trans Hvs); rewrite (bigcapv_inf Pi).
by apply big_prop => // [|B C sAC]; rewrite ?subvf // subv_cap sAC.
Qed.

End BigCap.

Definition complv vs := mx2vs ((vs2mx vs) ^C)%MS.
Arguments Scope complv [vspace_scope].
Local Notation "A ^C" := (complv A) : vspace_scope.

Lemma addv_complf : forall vs, (vs + vs^C = fullv)%VS.
Proof.
move=> vs; rewrite /addv /complv mx2vsDr.
apply/eqP; rewrite -mxeq2vseq submx1 sub1mx.
exact: addsmx_compl_full.
Qed.

Lemma capv_compl : forall vs, (vs :&: vs^C)%VS = 0%:VS.
Proof.
move=> vs; rewrite /capv /complv capv_mx2vsr -(mx2vs0 n).
by apply/eqP; rewrite -mxeq2vseq capmx_compl submx_refl.
Qed.

Definition diffv vs1 vs2 := mx2vs (vs2mx vs1 :\: vs2mx vs2)%MS.
Local Notation "A :\: B" := (diffv A B) : vspace_scope.

Lemma diffvSl : forall vs1 vs2, (vs1 :\: vs2 <= vs1)%VS.
Proof. move=> vs1 vs2; rewrite /subsetv mx2vsK; exact: diffmxSl. Qed.

Lemma capv_diff : forall vs1 vs2, ((vs1 :\: vs2) :&: vs2 = 0%:VS )%VS.
Proof.
move=> vs1 vs2; rewrite /capv /diffv -(mx2vs0 n) capv_mx2vsl.
by apply/eqP; rewrite -mxeq2vseq capmx_diff submx_refl .
Qed.

Lemma addv_diff_cap_eq : forall vs1 vs2, (vs1 :\: vs2 + vs1 :&: vs2 = vs1)%VS.
Proof.
move=> vs1 vs2.
rewrite /capv /diffv /addv mx2vsDr mx2vsDl -{3}[vs1]vs2mxK.
apply/eqP; rewrite -mxeq2vseq; apply/eqmxP; exact: addsmx_diff_cap_eq.
Qed.

Definition dimv vs := \rank (vs2mx vs).
Arguments Scope dimv[vspace_scope].
Local Notation "\dim A" := (dimv A) : nat_scope.

Lemma dimv0 : \dim (0 %:VS) = 0%N.
Proof. by rewrite /dimv /= linear0 genmx0 mxrank0. Qed.

Lemma dimv_eq0 : forall vs, (\dim vs == 0%N) = (vs == 0%:VS).
Proof.
by move=> vs; rewrite /dimv /= mxrank_eq0 {2}/eq_op /= linear0 genmx0.
Qed.

Lemma dimvf : \dim fullv = vdim V.
Proof. by rewrite /dimv mxrank_gen mxrank1. Qed.

Lemma dim_injv : forall v, \dim (v %:VS) = (v != 0).
Proof.
move=> v; case: (_ =P _)=> Hv; first by rewrite Hv dimv0.
rewrite /dimv /= mxrank_gen /=.
case: mxrank (rank_leq_row (v2rv v)) (mxrank_eq0 (v2rv v)); last by case.
move=> _ Hu; have H1u: v2rv v = 0 by apply/eqP; rewrite -Hu eqxx.
case: Hv; by apply: v2rv_inj;rewrite linear0.
Qed.

Lemma dimvS : forall vs1 vs2, (vs1 <= vs2)%VS -> \dim vs1 <= \dim vs2.
Proof. move=> vs1 vs2; exact: mxrankS. Qed.

Lemma dimv_leqif_sup : forall vs1 vs2,
 (vs1 <= vs2)%VS -> \dim vs1 <= \dim vs2 ?= iff (vs2 <= vs1)%VS.
Proof. move=> vs1 vs2 H; exact: mxrank_leqif_sup. Qed.

Lemma dimv_leqif_eq : forall vs1 vs2,
 (vs1 <= vs2)%VS -> \dim vs1 <= \dim vs2 ?= iff (vs1 == vs2)%VS.
Proof. move=> vs1 vs2 H; rewrite vseq2mxeq; exact: mxrank_leqif_eq. Qed.

Lemma dimv_compl : forall vs, \dim vs^C = (n - \dim vs)%N.
Proof. move=> vs; rewrite /dimv mxrank_gen; exact: mxrank_compl. Qed.

Lemma dimv_disjoint_sum : forall vs1 vs2,
  (vs1 :&: vs2)%VS = 0%:VS -> \dim (vs1 + vs2)%VS = (\dim vs1 + \dim vs2)%N.
Proof.
move=> vs1 vs2; move/eqP.
rewrite vseq2mxeq /= /addv /capv /mx2vs /dimv /= !genmxE linear0.
move/eqmxP=> H; apply: mxrank_disjoint_sum.
by apply/eqP; rewrite -mxrank_eq0 H mxrank0.
Qed.

Lemma dimv_cap_compl : forall vs1 vs2,
  (\dim (vs1 :&: vs2) + \dim (vs1 :\: vs2))%N = \dim vs1.
Proof. move=> vs1 vs2; rewrite /dimv !mxrank_gen; exact: mxrank_cap_compl. Qed.

Lemma dimv_sum_cap : forall vs1 vs2,
  (\dim (vs1 + vs2) + \dim (vs1 :&: vs2) = \dim vs1 + \dim vs2)%N.
Proof. move=> vs1 vs2; rewrite /dimv !mxrank_gen; exact: mxrank_sum_cap. Qed.

Lemma dimv_sum_leqif : forall vs1 vs2,
  \dim (vs1 + vs2) <= \dim vs1 + \dim vs2 ?= iff (vs1 :&: vs2 <= 0 %:VS)%VS.
Proof.
move=> vs1 vs2.
rewrite /dimv /subsetv !mxrank_gen vs2mx0 genmxE.
exact: mxrank_adds_leqif.
Qed.

Lemma subv_diffv0 : forall vs1 vs2,
  ((vs1 <= vs2) = (vs1 :\: vs2 == 0%:VS))%VS.
Proof.
move => vs1 vs2.
by rewrite -dimv_eq0 -(eqn_addl (\dim (vs1 :&: vs2)%VS)) addn0 dimv_cap_compl
           eq_sym (dimv_leqif_eq (capvSl _ _)) capvKl.
Qed.

Section BigDim.
Variable I : finType.
Implicit Type P : pred I.

Lemma dimv_leq_sum : forall P (vs_ : I -> {vspace V}),
  \dim (\sum_(i | P i) vs_ i)%VS <= (\sum_(i | P i) \dim (vs_ i))%N.
Proof.
move=> P vs_; elim: {P}_.+1 {-2}P (ltnSn #|P|) => // n1 Hrec P.
case: (pickP P) => [i Pi | P0]; last first.
  by rewrite big_pred0 // dim_injv eqxx.
rewrite (cardD1x Pi) (bigD1 i) //=; move/Hrec=> {n1 Hrec} /= Hrec.
rewrite [(\sum_(i0 | P i0) _)%N](bigD1 i) //=.
apply: (leq_trans (dimv_sum_leqif _ _)).
by rewrite leq_add2l.
Qed.

End BigDim.

Section SumExpr.


Inductive addv_spec : {vspace V} -> nat -> Prop :=
 | TrivialSumv vs
    : @addv_spec vs (\dim vs)
 | ProperSumv T1 T2 d1 d2 of
      @addv_spec T1 d1 & @addv_spec T2 d2
    : addv_spec (T1 + T2)%VS (d1 + d2)%N.
Arguments Scope addv_spec [vspace_scope nat_scope].

Structure addv_expr := Sumv {
  addv_val :> wrapped {vspace V};
  addv_dim : wrapped nat;
  _ : addv_spec (unwrap addv_val) (unwrap addv_dim)
}.

Canonical Structure trivial_addv vs :=
  @Sumv (Wrap vs) (Wrap (\dim vs)) (TrivialSumv vs).

Structure proper_addv_expr := ProperSumvExpr {
  proper_addv_val :> {vspace V};
  proper_addv_dim : nat;
  _ : addv_spec proper_addv_val proper_addv_dim
}.

Definition proper_addvP (S : proper_addv_expr) :=
  let: ProperSumvExpr _ _ termS := S return addv_spec S (proper_addv_dim S)
  in termS.

Canonical Structure sum_addv (S : proper_addv_expr) :=
  @Sumv (wrap (S : {vspace V})) (wrap (proper_addv_dim S)) (proper_addvP S).

Section Vector.

Variable (v : V).

Fact vector_addv_proof : addv_spec (v%:VS) (v != 0).
Proof. rewrite -dim_injv; left. Qed.
Canonical Structure vector_addv_expr := ProperSumvExpr vector_addv_proof.
End Vector.

Section Binary.
Variable (S1 S2 : addv_expr).

Fact binary_addv_proof :
  addv_spec (unwrap S1 + unwrap S2)
             (unwrap (addv_dim S1) + unwrap (addv_dim S2)).
Proof. by case: S1 S2 => [A1 r1 A1P] [A2 r2 A2P]; right. Qed.
Canonical Structure binary_addv_expr := ProperSumvExpr binary_addv_proof.
End Binary.

Section Nary.

Variables (I : finType) (P : pred I) (S_ : I -> addv_expr).
Fact nary_addv_proof : forall r,
  addv_spec (\sum_(i <- r | P i) unwrap (S_ i))
             (\sum_(i <- r | P i) unwrap (addv_dim (S_ i))).
Proof.
elim => [|i e IHe].
  by move: (vector_addv_proof 0); rewrite eqxx !big_nil.
rewrite !big_cons; case: (P i)=> //.
right=> //; case: (S_ i) => A r; exact.
Qed.

Canonical Structure nary_addv_expr r := ProperSumvExpr (nary_addv_proof r).
End Nary.

Definition directv_def T of phantom {vspace V} (unwrap (addv_val T)) :=
  \dim (unwrap T) == unwrap (addv_dim T).

End SumExpr.

Notation directv A := (directv_def (Phantom {vspace _} A%VS)).

Lemma directvP : forall (S : proper_addv_expr),
  reflect (\dim S = proper_addv_dim S) (directv S).
Proof. move=> S; exact: eqnP. Qed.
Implicit Arguments directvP [S].

Lemma directv_trivial : forall vs, directv (unwrap (@trivial_addv vs)).
Proof. move=> vs; exact: eqxx. Qed.

Lemma dimv_sumw_leqif : forall (S : addv_expr),
  \dim (unwrap S) <= unwrap (addv_dim S) ?= iff directv (unwrap S).
Proof.
rewrite /directv_def => [[vs] [r] /= defvsr]; split=> //=.
elim: defvsr => // vs1 vs2 d1 d2 _ levsd1 _ levsd2.
by apply: leq_trans (leq_add levsd1 levsd2); rewrite dimv_sum_leqif.
Qed.

Lemma directvE : forall (S : addv_expr),
  directv (unwrap S) = (\dim (unwrap S) == unwrap (addv_dim S)).
Proof. by []. Qed.

Lemma directvEgeq : forall (S : addv_expr),
  directv (unwrap S) = (\dim (unwrap S) >= unwrap (addv_dim S)).
Proof.
by move=> S; rewrite leq_eqVlt ltnNge eq_sym !dimv_sumw_leqif orbF.
Qed.

Section BinaryDirect.

Lemma directv_addE : forall (S1 S2 : addv_expr),
   directv (unwrap S1 + unwrap S2)
    = [&& directv (unwrap S1), directv (unwrap S2)
        & unwrap S1 :&: unwrap S2 == 0%:VS]%VS.
Proof.
move=> S1 S2; rewrite directvE /directv_def /=.
have:= leqif_add (dimv_sumw_leqif S1) (dimv_sumw_leqif S2).
move/(leqif_trans (dimv_sum_leqif (unwrap S1) (unwrap S2)))=>->.
by rewrite /directv_def /= andbC -andbA subv0.
Qed.

Lemma directv_addP vs1 vs2 :
   reflect (vs1 :&: vs2 = 0%:VS)%VS (directv (vs1 + vs2)).
Proof. move=> *; rewrite directv_addE !directv_trivial; exact: eqP. Qed.

Lemma directv_add_unique : forall vs1 vs2,
   directv (vs1 + vs2) <->
   (forall u1 v1 u2 v2, u1 \in vs1 -> v1 \in vs1 ->
                        u2 \in vs2 -> v2 \in vs2 ->
                        u1 + u2 == v1 + v2 = ((u1,u2) == (v1,v2))).
Proof.
move => vs1 vs2; split.
 move/directv_addP => dv u1 u2 v1 v2 Hu1 Hu2 Hv1 Hv2.
 apply/idP/andP => /=; last by case; do 2 move/eqP ->.
 rewrite -[_ == u2]subr_eq0 -[_ == v2]subr_eq0 -!memv0 -dv !memv_cap.
 rewrite -subr_eq -addrA addrC eq_sym -subr_eq.
 rewrite -!(memvN _ (u1 - u2)) oppr_sub.
 move/eqP => Heq.
 move: (memv_sub Hu2 Hu1) (memv_sub Hv1 Hv2).
 by move: Heq => -> -> ->.
move => Hpair.
apply/directv_addP.
apply/eqP.
rewrite -subv0.
apply/subvP => v.
rewrite memv_cap memv0.
case/andP => Hv1 Hv2.
have: (v + 0 == 0 + v) by rewrite addr0 add0r.
rewrite Hpair ?mem0v //.
by case/andP => /=.
Qed.

End BinaryDirect.

Section NaryDirect.

Variables (I : finType) (P : pred I).

Let TIsum A_ i :=
  (A_ i :&: (\sum_(j | P j && (j != i)) A_ j) = 0%:VS :> {vspace V})%VS.

Let directv_sum_recP : forall S_ : I -> addv_expr,
  reflect (forall i, P i -> directv (unwrap (S_ i)) /\ TIsum (unwrap \o S_) i)
          (directv (\sum_(i | P i) (unwrap (S_ i)))).
Proof.
rewrite /TIsum => S_; apply: (iffP eqnP) => /= [dxS i Pi | dxS].
  set Si' := (\sum_(j | _) unwrap (S_ j))%VS.
  suffices: directv (unwrap (S_ i) + Si').
    by rewrite directv_addE; case/and3P=> -> _; move/eqP.
  by apply/eqnP; rewrite /= -!(bigD1 i).
elim: _.+1 {-2 4}P (subxx P) (ltnSn #|P|) => // m IHm Q; move/subsetP=> sQP.
case: (pickP Q) => [i Qi | Q0]; last by rewrite !big_pred0 ?dimv0.
rewrite (cardD1x Qi) !((bigD1 i) Q) //=.
move/IHm=> <- {IHm}/=; last by apply/subsetP=> j; case/andP; move/sQP.
case: (dxS i (sQP i Qi)); move/eqnP=> <- TiQ_0; rewrite dimv_disjoint_sum //.
apply/eqP; rewrite -subv0 -{2}TiQ_0 capvS //=; apply/subv_sumP=> j /=.
by case/andP => Qj Di'j; rewrite (@sumv_sup _ j) ?[P j]sQP // Di'j.
Qed.

Lemma directv_sumP : forall vs_ : I -> {vspace V},
  reflect (forall i,
            P i -> vs_ i :&: (\sum_(j | P j && (j != i)) vs_ j) = 0%:VS)%VS
          (directv (\sum_(i | P i) vs_ i)).
Proof.
move=> vs_; apply: (iffP (directv_sum_recP _)) => dxA i; case/dxA=> //.
intros HH; split; first by exact: directv_trivial.
by apply/eqP; rewrite /eq_op /=; apply/eqP.
Qed.

Lemma directv_sumE : forall (S_ : I -> addv_expr) (xunwrap := unwrap),
  reflect (and (forall i, P i -> directv (unwrap (S_ i)))
               (directv (\sum_(i | P i) (xunwrap (S_ i)))))
          (directv (\sum_(i | P i) (unwrap (S_ i)))).
Proof.
move=> S_; apply: (iffP (directv_sum_recP _)) => [dxS | [dxS_ dxS] i Pi].
  by do [split; last apply/directv_sumP] => i; case/dxS.
by split; [exact: dxS_ | exact: directv_sumP Pi].
Qed.

Lemma directv_sum_unique : forall vs_ : I -> {vspace V},
   directv (\sum_(i | P i) vs_ i) <->
   (forall (u_ v_ : I -> V), (forall i : I, P i -> u_ i \in vs_ i) ->
                             (forall i : I, P i -> v_ i \in vs_ i) ->
                             (\sum_(i | P i) u_ i == \sum_(i | P i) v_ i) =
                             (forallb i : I, P i ==> (u_ i == v_ i))).
Proof.
move => vs_; split.
 move/directv_sumP => dv u_ v_ Hu_ Hv_.
 apply/idP/forall_inP; last first.
  by move => E; apply/eqP; apply: eq_bigr => i Pi; apply/eqP; apply E.
 move => Hsum i Pi.
 move/(_ _ Pi): dv.
 move/directv_addP.
 move/directv_add_unique.
 move/(_ (u_ i) (v_ i)) => dv.
 move: Hsum.
 rewrite !(bigD1 _ Pi) /=.
 by (rewrite dv ?Hu_ ?Hv_ ?memv_sumr //; first by case/andP);
  move => ?; case/andP => ? _; [apply Hu_|apply Hv_].
move => Hall.
apply/directv_sumP => i Pi.
apply/eqP.
rewrite -subv0.
apply/subvP => v.
rewrite memv_cap memv0.
case/andP => Hv1.
case/memv_sumP => v2_ [Hv2_ Hv2_eq].
pose u_ j := if j == i then v else 0.
pose v_ j := if j == i then 0 else (v2_ j).
have: \sum_(j | P j) u_ j == \sum_(j | P j) v_ j.
 rewrite !(bigD1 _ Pi) /=.
 by rewrite big1 /u_;
  first (rewrite /v_(eq_refl i) addr0 add0r Hv2_eq
        ;apply/eqP
        ;apply: eq_bigr
        );
  move => j;
  case/andP => _;
  by move/negbTE ->.
rewrite Hall /u_ /v_ => [|j Pj|j Pj].
  by move/forall_inP; move/(_ _ Pi); rewrite eqxx.
  by case: ifP; rewrite ?mem0v //; move/eqP=> ->.
by case: ifP; rewrite ?mem0v //; move/negbT => nji; apply Hv2_; rewrite Pj nji.
Qed.

End NaryDirect.

Definition span (l : seq V) := (\sum_(i <- l) i%:VS)%VS.

Lemma span_nil : span [::] = 0%:VS.
Proof. by rewrite /span big_nil. Qed.

Lemma span_seq1: forall v, span [::v] = v%:VS.
Proof. by move=> v; rewrite /span big_cons big_nil addv0. Qed.

Lemma span_cons : forall v l, span (v::l) = (v%:VS + span l)%VS.
Proof. by move=> v l; rewrite /span big_cons. Qed.

Lemma span_cat : forall l1 l2, span (l1 ++ l2) = (span l1 + span l2)%VS.
Proof. by move=> l1 l2; rewrite /span big_cat. Qed.

Lemma memv_span : forall l v, v \in l -> v \in span l.
Proof.
move=> l v; case/(nthP 0)=> i Hi <-.
rewrite /span (big_nth 0) big_mkord.
by apply: (@sumv_sup _ (Ordinal Hi)).
Qed.

Lemma span_subset : forall (l1 l2 : seq V),
  {subset l1 <= l2} -> (span l1 <= span l2)%VS.
Proof.
move=> l1 l2 H.
rewrite /span !(big_nth 0) !big_mkord.
apply/subv_sumP=> i _.
have: l1`_i \in l2 by rewrite H //; apply/(nthP 0); exists i.
case/(nthP 0)=> j Hj <-.
by apply: (@sumv_sup _ (Ordinal Hj)).
Qed.

Lemma span_eq : forall (l1 l2 : seq V), l1 =i l2 -> span l1 = span l2.
Proof.
by move=> l1 l2 H; apply: subv_anti; rewrite !span_subset // => i;
   rewrite ?H // -H.
Qed.

Lemma dim_span : forall l, \dim (span l) <= size l.
Proof.
elim=> [|v l Hrec]; first by rewrite span_nil dimv0.
rewrite /span big_cons /=.
apply: (leq_trans (dimv_sum_leqif _ _).1).
apply: (@leq_add _ _ 1)=> //.
by rewrite dim_injv; case: (_ == _).
Qed.

Definition span_mx l := \matrix_(i < size l) (v2rv l`_i).

Lemma span_mx_row : forall l i, row i (span_mx l) = v2rv l`_i.
Proof.
move=> l i; apply/matrixP=> i1 j1; rewrite !mxE.
by suff->: i1 = 0; [done | case: i1=> [[|i1] H] //; apply/eqP].
Qed.

Lemma span_vs2mx : forall l, (vs2mx (span l) == span_mx l)%MS.
Proof.
move=> l; rewrite /span !(big_nth 0) !big_mkord vs2mx_sum.
apply/andP; split.
  by apply/sumsmx_subP=> i _; rewrite genmxE -span_mx_row row_sub.
apply/row_subP=> i; rewrite span_mx_row -genmxE.
by apply: (sumsmx_sup i).
Qed.

Lemma span_mulmx : forall (l : seq V) (s : 'I_(size l) -> K),
  \sum_(i < size l) s i *: l`_i =
     rv2v ((\row_(i < size l) (s i)) *m (span_mx l)).
Proof.
move=> l s; apply: v2rv_inj; rewrite rv2vK linear_sum mulmx_sum_row.
by apply: eq_big=> // i _; rewrite mxE span_mx_row linearZ.
Qed.

Definition coord (l : seq V) :=
  fun (v : V) =>
  [ffun i : 'I_(size l) => ((((v2rv v) *m pinvmx (span_mx l)) 0 i) : K^o)].

Lemma coord_is_linear : forall l, linear (coord l).
Proof.
move=> l k u v; apply/ffunP=> i.
by rewrite /coord !ffunE linearP mulmx_addl -scalemxAl !mxE.
Qed.
Canonical Structure coord_linear l := Linear (coord_is_linear l).

Lemma coord_sumE : forall l I r (P : pred I) (F : I -> V) i,
 coord l (\sum_(j <- r | P j) F j) i = \sum_(j <- r | P j) coord l (F j) i.
Proof.
move=> l I r P F i; rewrite linear_sum.
elim: r=> [|j t Hrec]; first by rewrite !big_nil ffunE.
by rewrite !big_cons; case: (P j); rewrite ?ffunE Hrec.
Qed.

Lemma coord_span :
  forall l v, v \in span l -> v = \sum_(i < size l) coord l v i *: l`_i.
Proof.
move=> l v Hv; apply: v2rv_inj; rewrite linear_sum.
suff->: v2rv v = \sum_i coord l v i *: (row i (span_mx l)).
  by apply: eq_big=> // i _; rewrite linearZ span_mx_row.
have: (v2rv v <= span_mx l)%MS.
  by move/eqmxP: (span_vs2mx l)<-; apply: submx_trans Hv; rewrite /= genmxE.
move/mulmxKpV=><-; rewrite mulmx_sum_row.
by apply: eq_big=> // i _; rewrite ffunE.
Qed.

Lemma span_subsetl : forall l vs,
  all (fun v => v \in vs) l = (span l <= vs)%VS.
Proof.
move => l vs; apply/allP/subvP=> H v.
  move/coord_span ->; apply: memv_suml => i _.
  by rewrite memvZl // H // mem_nth.
by move=>Hv; rewrite H // memv_span.
Qed.

Definition free l := \dim (span l) == size l.

Lemma free_span_mx : forall l, free l = row_free (span_mx l).
Proof.
by move=> l; move: (span_vs2mx l); rewrite /free /dimv; move/eqmxP->.
Qed.

Lemma free_nil : free [::].
Proof. by rewrite /free span_nil dimv0. Qed.

Lemma free_seq1 : forall v, v != 0 -> free [::v].
Proof.
by move=> v Hv; rewrite /free /span big_seq1 dim_injv (negPf Hv).
Qed.

Lemma free_perm_eq : forall (l1 l2 : seq V),
  perm_eq l1 l2 -> free l1 = free l2.
Proof.
by move=> l1 l2 H; rewrite /free (perm_eq_size H) (span_eq (perm_eq_mem H)).
Qed.

Lemma free_notin0 : forall v l, free l -> v \in l -> v != 0.
Proof.
move=> v l Hf Hv; apply/eqP=> Hv0; move: Hv; rewrite Hv0.
case/(nthP 0)=> i Hi Hi0.
pose l1 := take i l ++ drop i.+1 l.
have Hp: perm_eq l (l`_i :: l1).
  by rewrite -{1}[l](cat_take_drop i.+1) /l1 -cat_cons perm_cat2r
             (take_nth 0 Hi) perm_rcons perm_eq_refl.
move: Hf (dim_span l1).
rewrite (free_perm_eq Hp) /free Hi0 /span big_cons sum0v.
by move/eqP->; rewrite ltnn.
Qed.

Lemma freeP : forall l,
  reflect
    (forall s, \sum_(i < size l) s i *: l`_i = 0 -> s =1 fun _ => 0)
     (free l).
Proof.
move=> l; rewrite free_span_mx -kermx_eq0.
apply: (iffP rowV0P)=> Hs.
  move=> s; move/eqP; rewrite span_mulmx -(v2rvK 0) linear0.
  move/eqP; move/rv2v_inj; move/sub_kermxP; move/Hs=> H0 i.
  suff<-: (\row_i s i) 0 i = s i by rewrite H0 mxE.
  by rewrite mxE.
move=> v Hv; suff He: [eta v 0] =1 (fun _ => 0).
  apply/matrixP=> [] i j; suff->: i = 0 by rewrite He mxE.
  by apply/eqP; case: i=> [[]].
apply: Hs; rewrite span_mulmx.
apply: v2rv_inj; rewrite rv2vK linear0.
apply/sub_kermxP; apply: submx_trans Hv; apply: row_sub.
Qed.

Lemma free_coord : forall l i,
  free l -> coord l (l`_i) = [ffun j : 'I_(size l) => (i == j)%:R].
Proof.
move=> l i Hf; apply/ffunP=> j.
case: (@leqP (size l) i)=> Hi .
  rewrite nth_default // linear0 !ffunE /=.
  by case: eqP=> // Hij; move: Hi; rewrite {}Hij leqNgt; case: j=> j->.
have: l`_i = \sum_(j < size l) (i == j)%:R *: l`_j.
  rewrite (bigD1 (Ordinal Hi)) //= eqxx scale1r big1 ?addr0 // => [k].
  by rewrite eq_sym {1}/eq_op /=; case: eqP=> //; rewrite scale0r.
rewrite {1}(coord_span (memv_span (mem_nth _ Hi))).
move/eqP; rewrite -subr_eq0 -sumr_sub.
rewrite (eq_bigr (fun i0 => (coord l l`_i i0 - (i == i0)%:R) *: l`_i0)).
  move/eqP=> HH; move/freeP: Hf; move/(_ _ HH j).
  by move/eqP; rewrite subr_eq0; move/eqP->; rewrite ffunE.
by move=>*; rewrite !scaler_subl.
Qed.

Lemma free_coordE : forall l i j, free l -> coord l (l`_i) j = (i == j)%:R.
Proof. by move=> *; rewrite free_coord // ffunE. Qed.

Lemma free_catl : forall l2 l1, free (l1 ++ l2) -> free l1.
Proof.
move=> l2 l1; move/freeP; rewrite size_cat=> H; apply/freeP=> s Hs i.
pose s1 (i :'I_(size l1 + size l2)) :=
   match split i with inl i => s i | _ => 0 end.
have Fls: forall j, s1 (lshift (size l2) j) = s j.
  move=> [j Hj]; rewrite /s1; case: splitP=> [] [j1 Hj1] /=; move/eqP=> He.
    by have->: (Ordinal Hj) = (Ordinal Hj1) by apply/val_eqP.
  suff: false by done.
  by move: Hj; rewrite ltnNge (eqP He) leq_addr.
have Frs: forall j, s1 (rshift (size l1) j) = 0.
  move=> [j Hj]; rewrite /s1; case: splitP=> [] [j1 Hj1] /=; move/eqP=> He //.
  suff: false by done.
  by move: Hj1; rewrite ltnNge -(eqP He) leq_addr.
have: s1 =1 (fun _ => 0).
  apply: H; rewrite big_split_ord /=.
  rewrite -{5}[0]add0r; congr (_ + _).
    rewrite -{3}Hs; apply: eq_big => // j _.
    by rewrite Fls nth_cat (ltn_ord j).
  by apply: big1=> i1 _ //=; rewrite Frs scale0r.
by move/(_ (lshift (size l2) i)); rewrite Fls.
Qed.

Lemma free_catr : forall l1 l2, free (l1 ++ l2) -> free l2.
Proof.
move=> l1 l2 H; apply: (@free_catl l1).
rewrite -(@free_perm_eq (l1 ++ l2)) //.
apply/perm_eqlP; apply: perm_catC.
Qed.

Lemma free_filter : forall P (l: seq V),
  free l -> free (filter P l).
Proof.
move=> P l; move: (perm_eq_refl l); rewrite -(perm_filterC P).
by move/free_perm_eq<-; exact: free_catl.
Qed.

Lemma addv_free : forall l1 l2,
  directv (span l1 + span l2) -> free (l1 ++ l2) = free l1 && free l2.
Proof.
move=> l1 l2; move/directv_addP=> Hd; apply/idP/andP.
  by move=> Hf; split; [apply: free_catl Hf | apply: free_catr Hf].
case; rewrite /free size_cat.
by rewrite span_cat (dimv_disjoint_sum Hd); move/eqP->; move/eqP->.
Qed.

Definition is_span vs l := span l == vs.

Lemma is_span_nil : is_span 0%:VS [::].
Proof. by rewrite /is_span span_nil. Qed.

Lemma is_span_seq1 : forall v, v != 0 -> is_span v%:VS [::v].
Proof. by move=> v Hv; rewrite /is_span span_seq1. Qed.

Lemma memv_is_span : forall v vs l, is_span vs l -> v \in l -> v \in vs.
Proof.
by move=> v vs l; rewrite /is_span; move/eqP=> <- H1; apply: memv_span.
Qed.

Lemma is_span_span : forall vs l v,
  is_span vs l -> v \in vs -> v = \sum_i coord l v i *: l`_i.
Proof.
by move=> vs l v; rewrite /is_span; move/eqP=> <- H1; apply coord_span.
Qed.

Lemma addv_is_span : forall vs1 vs2 l1 l2,
  is_span vs1 l1 -> is_span vs2 l2 -> is_span (vs1 + vs2)%VS (l1 ++ l2).
Proof.
rewrite /is_span=> vs1 vs2 l1 l2 Hb1 Hb2.
by rewrite span_cat (eqP Hb1) (eqP Hb2).
Qed.

Definition is_basis vs l := is_span vs l && free l.

Lemma is_basis_span : forall vs l, is_basis vs l -> is_span vs l.
Proof. by move=> vs l; case/andP. Qed.

Lemma is_basis_free : forall vs l, is_basis vs l -> free l.
Proof. by move=> vs l; case/andP. Qed.

Lemma is_basis_nil : is_basis 0%:VS [::].
Proof. by rewrite /is_basis is_span_nil free_nil. Qed.

Lemma is_basis_seq1 : forall v, v != 0 -> is_basis v%:VS [::v].
Proof. by move=> v Hv; rewrite /is_basis is_span_seq1 // free_seq1. Qed.

Lemma is_basis_notin0 : forall v vs l, is_basis vs l -> v \in l -> v != 0.
Proof.
by move=> v vs l Hf Hi; apply: free_notin0 Hi; apply: is_basis_free Hf.
Qed.

Lemma memv_is_basis : forall v vs l, is_basis vs l -> v \in l -> v \in vs.
Proof.
by move=> v vs l Hf Hi; apply: memv_is_span Hi; apply: is_basis_span.
Qed.

Lemma addv_is_basis : forall vs1 vs2 l1 l2,
  directv (vs1 + vs2) -> is_basis vs1 l1 -> is_basis vs2 l2 ->
  is_basis (vs1 + vs2)%VS (l1 ++ l2).
Proof.
move=> vs1 vs2 l1 l2 Hd; case/andP=> Hb1 Hf1; case/andP=> Hb2 Hf2.
rewrite /is_basis addv_is_span // addv_free //; first by rewrite Hf1.
by move: Hb1 Hb2; rewrite /is_span; move/eqP->; move/eqP->.
Qed.

Lemma size_is_basis : forall vs l, is_basis vs l -> size l = \dim vs.
Proof.
by rewrite /is_basis /is_span /free; move => vs l; case/andP; do 2 move/eqP ->.
Qed.

Definition vbasis vs := (fix loop (m : nat) vs {struct m} :=
  if m is m'.+1 then
    vpick vs :: loop m' (vs :\: ((vpick vs)%:VS))%VS else [::])
  (\dim vs) vs.

Lemma vbasis0 : vbasis 0%:VS = [::].
Proof. by rewrite /vbasis dimv0. Qed.

Lemma is_basis_vbasis : forall vs, is_basis vs (vbasis vs).
Proof.
rewrite /vbasis.
move=> vs;elim: {vs}(\dim vs) {-2 4}vs (erefl (\dim vs)) => /= [|m Hrec] vs.
  move/eqP; rewrite dimv_eq0; move/eqP->; apply is_basis_nil.
move=> Hs.
have->: forall (a : V) l, a::l = [::a] ++ l by done.
rewrite -{1}(addv_diff_cap_eq vs (vpick vs)%:VS) addvC //.
apply: addv_is_basis => //.
- rewrite directv_addE /directv_def /= !eqxx !andTb.
  move: (memv_pick vs); rewrite /in_mem /= capvKr; move/eqP->.
  by rewrite capvC capv_diff.
- move: (memv_pick vs); rewrite /in_mem /= capvKr; move/eqP->.
  apply: is_basis_seq1; rewrite vpick0.
  by apply/eqP=> HH; rewrite HH dimv0 in Hs.
apply: Hrec.
apply/eqP; rewrite -eqSS -Hs -(dimv_cap_compl vs (vpick vs)%:VS).
- move: (memv_pick vs); rewrite /in_mem /= capvKr; move/eqP->.
suff ->: \dim (vpick vs)%:VS = 1%N by done.
rewrite dim_injv vpick0.
by case: eqP=> // HH; move: Hs; rewrite HH dimv0.
Qed.

Lemma memv_basis : forall v vs, v \in (vbasis vs) -> v \in vs.
Proof. move=> v vs; exact (memv_is_basis (is_basis_vbasis _)). Qed.

Lemma coord_basis : forall v vs, v \in vs ->
  v = \sum_(i < size (vbasis vs)) coord (vbasis vs) v i *: (vbasis vs)`_i.
Proof.
move=> v vs Hvs; apply: coord_span.
by case/andP: (is_basis_vbasis vs); rewrite/is_span; move/eqP->.
Qed.

Lemma size_basis : forall vs, size (vbasis vs) = \dim vs.
Proof. by move => vs; rewrite (size_is_basis (is_basis_vbasis _)). Qed.

Section BigSumBasis.

Variable I : finType.
Implicit Type P : pred I.

Lemma span_bigcat : forall P (l_ : I -> seq V),
  span (\big[cat/[::]]_(i | P i) l_ i) = (\sum_(i | P i) span (l_ i))%VS.
Proof.
move=> P l_.
elim: index_enum => [|t s Hrec]; first by rewrite !big_nil span_nil.
rewrite !big_cons; case Pt: (P t); last by apply: Hrec.
by rewrite span_cat Hrec.
Qed.

Lemma bigaddv_free : forall P (l_ : I -> seq V),
  (directv (\sum_(i | P i) span (l_ i)))%VS ->
  (forall i, P i -> free (l_ i)) -> free (\big[cat/[::]]_(i | P i) l_ i).
Proof.
move=> P l_; rewrite /free /directv_def /= => Hd Hi.
rewrite span_bigcat (eqP Hd) eq_sym.
have ->: (\sum_(i | P i) \dim (span (l_ i)) = \sum_(i | P i) size (l_ i))%N.
  by apply: eq_big => // i Pi; apply/eqP; apply Hi.
apply/eqP; apply: big_morph => //; exact: size_cat.
Qed.

Lemma bigaddv_is_span : forall P l_ (vs_ : I -> {vspace V}),
  (forall i, P i -> is_span (vs_ i) (l_ i)) ->
    is_span (\sum_(i | P i) vs_ i)%VS (\big[cat/[::]]_(i | P i) l_ i).
Proof.
move=> P k_ vs_; rewrite /directv_def /=.
elim: index_enum => [|t s Hrec]; first by rewrite !big_nil is_span_nil.
rewrite !big_cons; case Pt: (P t) => Hi; last by apply: Hrec.
by apply: addv_is_span; [apply: Hi | apply: Hrec].
Qed.

Lemma bigaddv_is_basis : forall P l_ (vs_ : I -> {vspace V}),
  let vs := (\sum_(i | P i) vs_ i)%VS in
  directv vs ->
  (forall i, P i -> is_basis (vs_ i) (l_ i)) ->
    is_basis vs (\big[cat/[::]]_(i | P i) l_ i).
Proof.
move=> P l_ vs_ vs Hd Hi; rewrite /is_basis.
rewrite bigaddv_is_span.
  apply: bigaddv_free.
    move: Hd; rewrite /directv_def /= -/vs.
    have<-: (\sum_(i | P i) span (l_ i) = vs)%VS.
      apply: eq_big => // i Pi; apply/eqP; exact: (is_basis_span (Hi _ Pi)).
    have<-: (\sum_(i | P i) \dim (span (l_ i)) = \sum_(i | P i) \dim (vs_ i))%N.
      apply: eq_big => // i Pi; apply/eqP.
      by move: (is_basis_span (Hi _ Pi)); rewrite /is_span; move/eqP->.
    by done.
  by move=> i Pi; apply: (is_basis_free (Hi _ Pi)).
by move=> i Pi; apply: (is_basis_span (Hi _ Pi)).
Qed.

End BigSumBasis.

End VSpaceDef.

Hint Resolve subv_refl.
Implicit Arguments subvP [K V vs1 vs2].
Implicit Arguments sumv_sup [K V I P vs vs_].
Implicit Arguments subv_sumP [K V I P vs_ vs].
Implicit Arguments bigcapv_inf [K V I P vs_ vs].
Implicit Arguments directvP [K V S].
Implicit Arguments directv_addP [K V vs1 vs2].
Implicit Arguments directv_sumP [K V I P vs_].
Implicit Arguments directv_sumE [K V I P S_].

Arguments Scope dimv [_ _ vspace_scope].
Arguments Scope complv [_ _ vspace_scope].
Arguments Scope subsetv [_ _ vspace_scope vspace_scope].
Arguments Scope addv [_ _ vspace_scope vspace_scope].
Arguments Scope capv [_ _ vspace_scope vspace_scope].
Arguments Scope diffv [_ _ vspace_scope vspace_scope].
Prenex Implicits dimv complv subsetv addv capv fullv.

Notation vspaceType K := (VectorType.type (Phant K)).
Notation "{ 'vspace' T }" := (vspace_of (Phant T)) : type_scope.
Notation "\dim A" := (dimv A) : nat_scope.
Notation "A ^C" := (complv A) : vspace_scope.
Notation "A <= B" := (subsetv A B) : vspace_scope.
Notation "A <= B <= C" := ((subsetv A B) && (subsetv B C)) : vspace_scope.
Notation "A + B" := (addv A B) : vspace_scope.
Notation "A :&: B" := (capv A B) : vspace_scope.
Notation "A :\: B" := (diffv A B) : vspace_scope.
Notation directv S := (directv_def (Phantom _ S%VS)).
Notation "v %:VS" := (injv v) : ring_scope.

Notation "\sum_ ( <- r | P ) B" :=
  (\big[addv/0%:VS]_(<- r | P%B) B%VS) : vspace_scope.
Notation "\sum_ ( i <- r | P ) B" :=
  (\big[addv/0%:VS]_(i <- r | P%B) B%VS) : vspace_scope.
Notation "\sum_ ( i <- r ) B" :=
  (\big[addv/0%:VS]_(i <- r) B%VS) : vspace_scope.
Notation "\sum_ ( m <= i < n | P ) B" :=
  (\big[addv/0%:VS]_(m <= i < n | P%B) B%VS) : vspace_scope.
Notation "\sum_ ( m <= i < n ) B" :=
  (\big[addv/0%:VS]_(m <= i < n) B%VS) : vspace_scope.
Notation "\sum_ ( i | P ) B" :=
  (\big[addv/0%:VS]_(i | P%B) B%VS) : vspace_scope.
Notation "\sum_ i B" :=
  (\big[addv/0%:VS]_i B%VS) : vspace_scope.
Notation "\sum_ ( i : t | P ) B" :=
  (\big[addv/0%:VS]_(i : t | P%B) B%VS) (only parsing) : vspace_scope.
Notation "\sum_ ( i : t ) B" :=
  (\big[addv/0%:VS]_(i : t) B%VS) (only parsing) : vspace_scope.
Notation "\sum_ ( i < n | P ) B" :=
  (\big[addv/0%:VS]_(i < n | P%B) B%VS) : vspace_scope.
Notation "\sum_ ( i < n ) B" :=
  (\big[addv/0%:VS]_(i < n) B%VS) : vspace_scope.
Notation "\sum_ ( i \in A | P ) B" :=
  (\big[addv/0%:VS]_(i \in A | P%B) B%VS) : vspace_scope.
Notation "\sum_ ( i \in A ) B" :=
  (\big[addv/0%:VS]_(i \in A) B%VS) : vspace_scope.

Notation "\bigcap_ ( <- r | P ) B" :=
  (\big[capv/(fullv _)]_(<- r | P%B) B%VS) : vspace_scope.
Notation "\bigcap_ ( i <- r | P ) B" :=
  (\big[capv/(fullv _)]_(i <- r | P%B) B%VS) : vspace_scope.
Notation "\bigcap_ ( i <- r ) B" :=
  (\big[capv/(fullv _)]_(i <- r) B%VS) : vspace_scope.
Notation "\bigcap_ ( m <= i < n | P ) B" :=
  (\big[capv/(fullv _)]_(m <= i < n | P%B) B%VS) : vspace_scope.
Notation "\bigcap_ ( m <= i < n ) B" :=
  (\big[capv/(fullv _)]_(m <= i < n) B%VS) : vspace_scope.
Notation "\bigcap_ ( i | P ) B" :=
  (\big[capv/(fullv _)]_(i | P%B) B%VS) : vspace_scope.
Notation "\bigcap_ i B" :=
  (\big[capv/(fullv _)]_i B%VS) : vspace_scope.
Notation "\bigcap_ ( i : t | P ) B" :=
  (\big[capv/(fullv _)]_(i : t | P%B) B%VS) (only parsing) : vspace_scope.
Notation "\bigcap_ ( i : t ) B" :=
  (\big[capv/(fullv _)]_(i : t) B%VS) (only parsing) : vspace_scope.
Notation "\bigcap_ ( i < n | P ) B" :=
  (\big[capv/(fullv _)]_(i < n | P%B) B%VS) : vspace_scope.
Notation "\bigcap_ ( i < n ) B" :=
  (\big[capv/(fullv _)]_(i < n) B%VS) : vspace_scope.
Notation "\bigcap_ ( i \in A | P ) B" :=
  (\big[capv/(fullv _)]_(i \in A | P%B) B%VS) : vspace_scope.
Notation "\bigcap_ ( i \in A ) B" :=
  (\big[capv/(fullv _)]_(i \in A) B%VS) : vspace_scope.

Section LinearApp.

Variable (R : ringType) (V W : vectType R).

Inductive linearApp : Type :=
  LinearApp of 'M[R]_(vdim V,vdim W).

Definition mx_of_lapp x := let: LinearApp mx := x in mx.

Local Notation v2rv V := (@v2rv_isomorphism _ V).
Local Notation rv2v V := (@rv2v_isomorphism _ V).

Definition fun_of_lapp f (x : V) : W := rv2v W ((v2rv V x) *m (mx_of_lapp f)).

Coercion fun_of_lapp : linearApp >-> Funclass.

Canonical Structure linearApp_subType :=
  Eval hnf in [newType for mx_of_lapp by linearApp_rect].
Canonical Structure lapp_eqMixin := [eqMixin of linearApp by <:].
Canonical Structure lapp_eqType := Eval hnf in EqType linearApp lapp_eqMixin.
Definition lapp_choiceMixin := [choiceMixin of linearApp by <:].
Canonical Structure lapp_choiceType :=
  Eval hnf in ChoiceType linearApp lapp_choiceMixin.

Lemma eq_lapp : forall (f g : linearApp), reflect (f =1 g) (f == g).
Proof.
move => [f] [g] /=; apply: (iffP eqP); first by move => ->.
rewrite /fun_of_lapp /eqfun /= => H.
rewrite (_:f = g) // -row_matrixP => i.
move: (H (rv2v_isomorphism (delta_mx 0 i))).
rewrite !rowE rv2vK.
by apply: (can_inj (@rv2vK _ _)).
Qed.

Definition zero_lapp := LinearApp (const_mx 0).
Local Notation "\0" := zero_lapp : vspace_scope.
Definition add_lapp f1 f2 := LinearApp (mx_of_lapp f1 + mx_of_lapp f2).
Local Notation "f1 \+ f2" := (add_lapp f1 f2) : vspace_scope.
Definition opp_lapp f := LinearApp (oppmx (mx_of_lapp f)).
Definition scale_lapp k f := LinearApp (k *: mx_of_lapp f).
Local Notation "k \*: f" := (scale_lapp k f) : vspace_scope.

Lemma lapp_addA : associative add_lapp.
Proof. move=> f1 f2 f3; congr LinearApp; exact: addmxA. Qed.

Lemma lapp_addC : commutative add_lapp.
Proof. move=> f1 f2; congr LinearApp; exact: addmxC. Qed.

Lemma lapp_add0 : left_id zero_lapp add_lapp.
Proof. move=> [m]; congr LinearApp; exact: add0mx. Qed.

Lemma lapp_addN : left_inverse zero_lapp opp_lapp add_lapp.
Proof. move=> f; congr LinearApp; exact: addNmx. Qed.

Definition lapp_zmodMixin := ZmodMixin lapp_addA lapp_addC lapp_add0 lapp_addN.

Lemma zero_lappE : forall x, (\0 x = 0)%VS.
Proof. by move => x; rewrite /fun_of_lapp /= mulmx0 linear0. Qed.

Lemma add_lappE : forall f g x, (f \+ g)%VS x = f x + g x.
Proof. by move => f g x; rewrite /fun_of_lapp mulmx_addr linearD. Qed.

Lemma opp_lappE : forall f x, (opp_lapp f) x = - f x.
Proof. by move=> f x; rewrite /fun_of_lapp mulmxN linearN. Qed.

Canonical Structure lapp_zmodType :=
  Eval hnf in ZmodType linearApp lapp_zmodMixin.

Lemma sum_lappE : forall I (r : seq I) (P : pred I) (F : I -> linearApp) x,
  (\big[+%R/0]_(i <- r | P i) F i) x = \big[+%R/0]_(i <- r | P i) (F i x).
Proof.
move=> I r P F x; elim: r=> [|i r Hrec]; first by rewrite !big_nil zero_lappE.
by rewrite !big_cons; case: (P i); rewrite // add_lappE Hrec.
Qed.

Lemma lapp_scaleA : forall k1 k2 f, (k1 \*: (k2 \*: f) = (k1 * k2) \*: f)%VS.
Proof. move=> k1 k2 f; congr LinearApp; exact: scalerA. Qed.
Lemma lapp_scale1 : forall f, (1 \*: f = f)%VS.
Proof. move=> [m]; congr LinearApp; exact: scale1r. Qed.

Lemma lapp_addr : forall k f1 f2,
  (k \*: (f1 \+ f2) = (k \*: f1) \+ (k \*: f2))%VS.
Proof. move=> k f1 f2; congr LinearApp; exact: scaler_addr. Qed.

Lemma lapp_addl : forall f k1 k2,
  ((k1 + k2) \*: f = (k1 \*: f) \+ (k2 \*: f))%VS.
Proof. move=> k1 k2 f; congr LinearApp; exact: scaler_addl. Qed.

Definition lapp_lmodMixin :=
  LmodMixin lapp_scaleA lapp_scale1 lapp_addr lapp_addl.

Canonical Structure lapp_lmodType :=
  Eval hnf in LmodType R linearApp lapp_lmodMixin.

Definition lapp_rep := mxvec \o mx_of_lapp.

Definition lapp_rep_is_linear : linear lapp_rep.
Proof. by move=> a x y; apply/rowP=> k; rewrite !(castmxE, mxE). Qed.
Canonical Structure lapp_rep_linear:= Linear lapp_rep_is_linear.

Lemma lapp_rep_bij : bijective lapp_rep.
Proof.
exists (LinearApp \o vec_mx); last by exact: vec_mxK.
by move=> [m]; congr LinearApp; exact: mxvecK.
Qed.

Definition linearMixin := VectMixin lapp_rep_is_linear lapp_rep_bij.
Canonical Structure linearVect (phV : phant V) (phW : phant W) :=
  VectType R linearMixin.

Variables (phV : phant V) (phW : phant W).

Lemma hom_is_linear : forall (f : linearVect phV phW), linear f.
Proof.
by move=> f a x y; rewrite /fun_of_lapp linearP mulmx_addl
                        -scalemxAl linearP.
Qed.
Canonical Structure hom_linear f := Linear (hom_is_linear f).

Definition lapp_of_fun f := LinearApp (lin1_mx ((v2rv W) \o f \o (rv2v V))).

Lemma fun_of_lappK : cancel fun_of_lapp lapp_of_fun.
Proof.
move=> [m]; congr LinearApp; apply/matrixP=> i j /=.
by rewrite /lin1_mx /= mxE !rv2vK /= -rowE mxE.
Qed.

Lemma lapp_of_funK : forall (f : V -> W), linear f -> lapp_of_fun f =1 f.
Proof.
move=> f Hf x; rewrite /fun_of_lapp /=.
set h := (v2rv W \o f) \o rv2v V.
suff h_proof: linear h.
  by rewrite (mul_rV_lin1 (Linear h_proof)) /h !v2rvK.
by move=> a u v; rewrite /h /= linearP Hf linearP.
Qed.

End LinearApp.
Notation "\0" := (zero_lapp _ _) : vspace_scope.
Notation "f1 \+ f2" := (add_lapp f1 f2) : vspace_scope.
Notation "k \*: f" := (scale_lapp k f) : vspace_scope.

Section ScaleLapp.

Variable (R : comRingType) (V W : vectType R).
Variable f : linearApp V W.

Lemma scale_lappE : forall a x, ((a \*: f) x)%VS = a *: f x.
Proof. by move => a x; rewrite /fun_of_lapp -scalemxAr linearZ. Qed.

End ScaleLapp.

Section UnitApp.

Variable (R : ringType) (V : vectType R).
Hypothesis vdim_nz : (vdim V != 0)%N.
Definition unit_lapp := LinearApp (1%:M: 'M_(vdim V, vdim V)).
Notation "\1" := unit_lapp : vspace_scope.

Lemma unit_lappE : forall x, (\1 x = x)%VS.
Proof. by move=> x; rewrite /fun_of_lapp mulmx1 v2rvK. Qed.

Lemma unit_nonzero_lapp : (\1 != \0)%VS.
Proof.
apply/eqP=> H; case/eqP: (matrix_nonzero1 R (vdim V).-1).
by case: H; case: vdim vdim_nz.
Qed.

End UnitApp.
Notation "\1" := (unit_lapp _) : vspace_scope.

Section CompLinearApp.

Variable (R : ringType) (V W Z : vectType R).
Implicit Type f : linearApp W Z.
Implicit Type g : linearApp V W.

Definition comp_lapp f g := LinearApp (mx_of_lapp g *m mx_of_lapp f).
Notation "f \o g" := (comp_lapp f g) : vspace_scope.

Lemma comp_lappE : forall f g, (f \o g)%VS =1 f \o g.
Proof.
by move=> [Mf] [Mg] x; rewrite /comp_lapp /fun_of_lapp !mulmxA /= rv2vK.
Qed.

End CompLinearApp.

Notation "f \o g" := (comp_lapp f g) : vspace_scope.

Section InvLinearApp.

Variable (K : fieldType) (V W : vectType K).
Implicit Type f : linearApp V W.

Definition inv_lapp f := LinearApp (pinvmx (mx_of_lapp f)).
Notation "f \^-1" := (inv_lapp f) : vspace_scope.

Lemma inv_lapp_def : forall f, (f \o (f \^-1 \o f) = f)%VS.
Proof.
move=> [Mf]; congr LinearApp; exact: (mulmxKpV (submx_refl Mf)).
Qed.

End InvLinearApp.
Notation "f \^-1" := (inv_lapp f) : vspace_scope.

Section LAlgLinearApp.

Variable (R : ringType) (V W Z T : vectType R).
Implicit Type h : linearApp V W.
Implicit Type g : linearApp W Z.
Implicit Type f : linearApp Z T.

Lemma comp_lappA : forall f g h, (f \o (g \o h) = (f \o g) \o h)%VS.
Proof. by move=> [mf] [mg] [mh]; congr LinearApp; rewrite !mulmxA. Qed.

Lemma comp_lapp_addl : forall f1 f2 g,
  ((f1 \+ f2) \o g = (f1 \o g) \+ (f2 \o g))%VS.
Proof. by move=> [mf1] [mf2] [mg]; congr LinearApp; exact: mulmx_addr. Qed.

Lemma comp_lapp_addr : forall f g1 g2,
  (f \o (g1 \+ g2) = (f \o g1) \+ (f \o g2))%VS.
Proof. move=> [mf] [mg1] [mg2]; congr LinearApp; exact: mulmx_addl. Qed.

Lemma comp_1lapp : forall f, (\1 \o f = f)%VS.
Proof. move=> [mf]; congr LinearApp; exact: mulmx1. Qed.

Lemma comp_lapp1 : forall f, (f \o \1)%VS = f.
Proof. move=> [mf]; congr LinearApp; exact: mul1mx. Qed.

Lemma scale_lapp_Ar : forall k f g, (k \*: (f \o g) = f \o (k \*: g))%VS.
Proof. move=> k [mf mg]; congr LinearApp; exact :scalemxAl. Qed.

End LAlgLinearApp.

Section AlgLinearApp.

Variable (R : comRingType) (V W Z : vectType R).
Implicit Type g : linearApp V W.
Implicit Type f : linearApp W Z.

Lemma scale_lapp_Al : forall k f g, (k \*: (f \o g) = (k \*: f) \o g)%VS.
Proof. move=> k [mf mg]; congr LinearApp; exact: scalemxAr. Qed.

End AlgLinearApp.

Module LApp.

Section LinearAppStruct.

Variable (R : comRingType) (V : vectType R).
Hypothesis dim_nz : (vdim V != 0)%N.

Definition ringMixin :=
  RingMixin (@comp_lappA _ V V V V) (@comp_1lapp _ V V) (@comp_lapp1 _ V V)
            (@comp_lapp_addl _ V V V) (@comp_lapp_addr _ V V V)
             (@unit_nonzero_lapp _ V dim_nz).

Definition ringType :=
  Eval hnf in RingType (@linearApp R V V) ringMixin.

Canonical Structure revRingType :=
  Eval hnf in RingType (@linearApp R V V) (GRing.converse_ringMixin ringType).

Canonical Structure lalgType :=
 Eval hnf in LalgType R (@linearApp R V V)
               (fun k x y => @scale_lapp_Ar R V V V k y x).

Canonical Structure algType :=
   Eval hnf in AlgType R (@linearApp R V V)
                 (fun k x y => @scale_lapp_Al R V V V k y x).

End LinearAppStruct.

End LApp.

Notation "''Hom' ( V , W )" := (linearVect (Phant V) (Phant W)) : type_scope.
Notation "''End' ( V )" := (linearVect (Phant V) (Phant V)) : type_scope.

Section LinearImage.

Variable (K : fieldType) (V W : vectType K).

Implicit Type f : 'Hom(V,W).
Implicit Type vs : {vspace V}.

Definition limg f := mx2vs (mx_of_lapp f).

Definition fun_of_limg f (vs : {vspace V}) :=
  (mx2vs ((vs2mx vs) *m (mx_of_lapp f))).

Definition lker f := mx2vs (kermx (mx_of_lapp f)).

Definition lpre_img f (vs : {vspace W}) :=
  let Mf := mx_of_lapp f in
  mx2vs (((vs2mx vs) :&: Mf) *m pinvmx Mf + kermx Mf)%MS.

Local Notation " f @: V " := (fun_of_limg f V) (at level 24) : vspace_scope.
Local Notation " f @^-1: V " := (lpre_img f V) (at level 24) : vspace_scope.

Lemma lkerE : forall f vs, (f @: vs == 0%:VS)%VS = (vs <= lker f)%VS.
Proof.
move=> f vs; rewrite /subsetv genmxE.
apply/idP/sub_kermxP; last by rewrite /fun_of_limg; move->; rewrite mx2vs0.
rewrite vseq2mxeq !mx2vsK linear0 !sub0mx andbT.
by move/submx0null.
Qed.

Lemma limgE : forall f, limg f = (f @: (fullv V))%VS.
move=> [Mf]; apply/eqP.
by rewrite -mxeq2vseq /= !(eqmxMr _ (genmxE _)) mul1mx submx_refl.
Qed.

Lemma limg_monotone : forall f vs1 vs2,
  (vs1 <= vs2)%VS -> (f @: vs1 <= f @: vs2)%VS.
Proof.
by move=> [Mf] vs1 vs2; rewrite /subsetv /= !genmxE ;apply: submxMr.
Qed.

Lemma limg_inj : forall f v, (f @: (v %:VS))%VS = (f v)%:VS.
Proof.
move=> [Mf] v; apply/eqP.
by rewrite vseq2mxeq /= rv2vK !genmxE !(eqmxMr _ (genmxE _)) submx_refl.
Qed.

Lemma lpre_img0 : forall f, (f @^-1: 0%:VS)%VS = lker f.
Proof.
move=> [Mf]; apply/eqP.
by rewrite vseq2mxeq /= linear0 genmx0 cap0mx mul0mx !genmxE
           !adds0mx !submx_refl.
Qed.

Lemma lpre_img_full : forall f (vs : {vspace W}),
  (f @^-1: (vs :&: limg f))%VS = (f @^-1: vs)%VS.
Proof.
move=> [Mf] vs; apply/eqP; rewrite vseq2mxeq /= mx2vsK !genmxE.
apply/eqmxP; apply: adds_eqmx=> //; apply: eqmxMr.
have F1: (vs2mx vs :&: Mf :&:Mf :=: vs2mx vs :&: Mf)%MS.
  rewrite -capmxA; apply: cap_eqmx=> //.
  by apply/eqmxP; rewrite sub_capmx capmxSr !submx_refl.
apply: eqmx_trans F1; apply: cap_eqmx=> //.
apply/eqmxP; rewrite !genmxE; apply/eqmxP.
apply: cap_eqmx=> //.
by apply/eqmxP; rewrite !genmxE !submx_refl.
Qed.

Lemma lpre_imgK : forall f (vs : {vspace W}),
  (vs <= limg f)%VS -> (f @: (f @^-1: vs))%VS = vs.
Proof.
move=> [Mf] vs Hvs; apply/eqP.
rewrite vseq2mxeq /= mx2vsK !genmxE !(eqmxMr _ (genmxE _)) !addsmxMr.
have->: (kermx Mf *m Mf = 0)%MS.
  by apply: sub_kermxP; apply: submx_refl.
rewrite !addsmx0 mulmxKpV ?submx_refl ?capmxSr //.
move: Hvs; rewrite /limg /subsetv /= !genmxE.
by move=> Hvs; rewrite capmxSl sub_capmx submx_refl.
Qed.

Lemma limg0 : forall f, (f @: (0 %:VS))%VS = 0%:VS.
Proof. by move=> f; rewrite limg_inj; rewrite linear0. Qed.

Lemma lim0g : forall vs, (0 @: vs)%VS = 0%:VS.
Proof. by move => vs; rewrite /fun_of_limg /= mulmx0 mx2vs0. Qed.

Lemma memv_img : forall f v vs, v \in vs -> f v \in (f @: vs)%VS.
Proof. by move=> f v vs Hv; rewrite /in_mem /= -limg_inj limg_monotone. Qed.

Lemma memv_ker : forall f v, (v \in lker f)%VS = (f v == 0).
Proof.
move=> f v; rewrite /in_mem /= -lkerE limg_inj.
apply/idP/idP; last by move/eqP->.
rewrite -memv0; move/eqP<-; exact: memv_inj.
Qed.

Lemma limg_add : forall f, {morph (fun_of_limg f) : u v / (u + v)%VS}.
Proof.
move=> [Mf] vs1 vs2; rewrite -mx2vsD; apply/eqP.
by rewrite -mxeq2vseq -!addsmxMr !(eqmxMr _ (genmxE _)) submx_refl.
Qed.

Lemma limg_sum : forall f (I : finType) (P : pred I) (vs_ : I -> {vspace V}),
  (f @: (\sum_(i | P i) vs_ i) = \sum_(i | P i) (f @: (vs_ i)))%VS.
Proof.
move=> I P v_; apply: big_morph; [exact: limg_add | exact: limg0].
Qed.

Lemma limg_cap : forall f vs1 vs2,
  (f @: (vs1 :&: vs2) <= f @: vs1 :&: f @: vs2)%VS.
Proof.
by move=> f vs1 vs2; (rewrite subv_cap; apply/andP;
                      split; apply: limg_monotone);
    [apply: capvSl | apply: capvSr].
Qed.

Lemma limg_bigcap :
  forall f (I : finType) (P : pred I) (vs_ : I -> {vspace V}),
  (f @: (\bigcap_(i | P i) vs_ i) <= \bigcap_(i | P i) (f @: (vs_ i)))%VS.
Proof.
move=> f I P vs_; elim: {P}_.+1 {-2}P (ltnSn #|P|) => // n1 Hrec P.
case: (pickP P) => [i Pi | P0]; last first.
  by rewrite !big_pred0 // => _; apply: subvf.
rewrite (cardD1x Pi) (bigD1 i) //=; move/Hrec=> {n1 Hrec} /= Hrec.
rewrite [(\bigcap_(i0 | P i0) _)%VS](bigD1 i) //=.
apply: (subv_trans (limg_cap _ _ _)).
apply: capvS => //; apply: subv_refl.
Qed.

Lemma limg_span : forall f l, (f @: span l)%VS = span (map f l).
Proof.
move=> f l; rewrite /span (big_nth 0) big_mkord limg_sum //.
rewrite big_map (big_nth 0) big_mkord; apply: eq_big => // i _.
by rewrite limg_inj.
Qed.

Lemma memv_imgP : forall f v vs,
  reflect (exists v1, v1 \in vs /\ v = f v1) (v \in f @: vs)%VS.
Proof.
move=> f v vs; apply: (iffP idP); last first.
 by move=> [v1 [Hiv1 ->]]; apply: memv_img.
case/andP: (is_basis_vbasis vs).
rewrite /is_span; move/eqP<-=> _.
rewrite limg_span; move/coord_span->.
exists (\sum_i (coord (map f (vbasis vs)) v i: K) *: (vbasis vs)`_i); split.
  apply: memv_suml=> [] [i Hi] _; apply: memvZl; apply: memv_span.
  by apply/(nthP 0); exists i; rewrite // -(size_map f).
rewrite linear_sum; apply: eq_big=> // [] [i Hi] _.
by rewrite linearZ (nth_map 0) // -(size_map f).
Qed.

Lemma limg_ker_compl : forall f vs, (f @: (vs :\: lker f))%VS = (f @: vs)%VS.
Proof.
move=> f vs; apply/eqP; apply/vspaceP=> i.
apply/memv_imgP/memv_imgP=> [] [v [Hv ->]].
  by exists v; split => //; apply: (subv_trans Hv); exact: diffvSl.
move: Hv; rewrite -{1}(addv_diff_cap_eq vs (lker f)).
case/memv_addP=> v1 [v2 [Hv1 Hv2 ->]]; exists v1; split => //.
rewrite linearD; move: Hv2; rewrite memv_cap; case/andP=> _.
by rewrite memv_ker /=; move/eqP->; rewrite addr0.
Qed.

Lemma limg_dim_eq : forall f vs,
  (vs :&: lker f)%VS = 0%:VS -> \dim (f @: vs) = \dim vs.
Proof.
move=> [Mf] vs; rewrite /dimv /lker /capv.
move/eqP;rewrite vseq2mxeq capv_mx2vsr /= !genmxE linear0.
rewrite -(mxrank_mul_ker (vs2mx vs) Mf).
by move/eqmx_rank; rewrite mxrank0 => ->; rewrite addn0.
Qed.

Lemma limg_is_basis : forall f vs l, (vs :&: lker f)%VS = 0%:VS ->
   (is_basis vs l -> is_basis (f @: vs)%VS (map f l)).
Proof.
move=> f vs l Hvs; case/andP=> Hs Hf.
have F1: is_span (f @: vs)%VS (map f l).
  by move: Hs; rewrite /is_span -limg_span; move/eqP<-.
rewrite /is_basis F1.
move: Hf; rewrite /free size_map; move/eqP<-.
move: F1; rewrite /is_span; move/eqP->.
rewrite limg_dim_eq //.
by move: Hs; rewrite /is_span; move/eqP->; rewrite eqxx.
Qed.

Lemma limg_ker_dim : forall f vs,
  (\dim (vs :&: lker f) + \dim (f @: vs) = \dim vs)%N.
Proof.
move=> f vs; rewrite -limg_ker_compl.
by rewrite limg_dim_eq; [exact: dimv_cap_compl | exact: capv_diff].
Qed.

Lemma lker0P : forall f, reflect (injective f) (lker f == 0%:VS).
Proof.
move => f; apply: (iffP idP).
  move => Hf x y; move/eqP.
  rewrite -GRing.subr_eq0 -linear_sub -memv_ker (eqP Hf) memv0 GRing.subr_eq0.
  by move/eqP.
by move=> Hf; apply/vspaceP=> x; rewrite memv0 memv_ker; apply/eqP/eqP=> Hi;
   try apply: Hf; rewrite Hi linear0.
Qed.

Lemma limg_ker0 : forall f vs ws,
 lker f == 0%:VS -> (f @: vs <= f @: ws)%VS = (vs <= ws)%VS.
Proof.
move=> f vs ws; move/lker0P=> Hf.
apply/idP/idP; last by apply limg_monotone.
move/subvP => Hvw; apply/subvP => z Hz.
case/memv_imgP: (Hvw _ (memv_img f Hz)) => y [Hy Hyz].
by rewrite (Hf _ _ Hyz).
Qed.

Lemma eq_limg_ker0 : forall f vs ws,
 lker f == 0%:VS -> (f @: vs == f @: ws)%VS = (vs == ws)%VS.
Proof.
move=> f vs ws Hf; apply/eqP/eqP => H; last by rewrite H.
by apply: subv_anti; rewrite -!(limg_ker0 _ _ Hf) H subv_refl.
Qed.

End LinearImage.

Notation " f @: V " := (fun_of_limg f V) (at level 24) : vspace_scope.
Notation " f @^-1: V " := (lpre_img f V) (at level 24) : vspace_scope.

Section UnitImage.

Variable (K : fieldType) (V : vectType K).

Lemma lim1g : forall vs, ((\1 : 'End(V)) @: vs = vs)%VS.
Proof. by move => vs; rewrite /unit_lapp /fun_of_limg mulmx1 vs2mxK. Qed.

End UnitImage.

Section CompImage.

Variable (K : fieldType) (V W Z : vectType K).

Lemma limg_comp : forall (f : 'Hom(V,W)) (g : 'Hom(W,Z)) vs,
 ((g \o f) @: vs = g @: (f @: vs))%VS.
Proof.
move => f g vs; apply/eqP; apply/vspaceP => v.
apply/memv_imgP/memv_imgP; move => [x [Hx ->]];
 [exists (f x)|move/memv_imgP: Hx => [y [Hy ->]];exists y];
 rewrite comp_lappE; split=>//.
by apply: memv_img.
Qed.

End CompImage.

Section LinearPreImage.

Variable (K : fieldType) (V W : vectType K).

Implicit Type f : 'Hom(V,W).
Implicit Type vs : {vspace V}.

Lemma lpre_imgE : forall f (vs : {vspace W}),
  (f @^-1: vs)%VS = (((f \^-1) @: (vs :&: limg f)%VS) + lker f)%VS.
Proof.
move=> [Mf] vs; apply/eqP; rewrite vseq2mxeq /= mx2vsK !genmxE.
apply/eqmxP; apply: adds_eqmx; apply/eqmxP; rewrite !genmxE; apply/eqmxP=>//.
apply: eqmxMr.
apply/eqmxP; rewrite !genmxE; apply/eqmxP.
by apply: cap_eqmx=> //; apply/eqmxP; rewrite !genmxE !submx_refl.
Qed.

Lemma lpre_img_monotone : forall f (vs1 vs2 : {vspace W}),
  (vs1 <= vs2)%VS-> (f @^-1: vs1 <= f @^-1: vs2)%VS.
Proof.
move=> f vs1 vs2 Hvs; rewrite !lpre_imgE.
apply: addvS; last by apply: subv_refl.
apply: limg_monotone.
by apply: capvS; last by apply: subv_refl.
Qed.

Lemma memv_pre_img : forall f v (vs : {vspace W}), (f v \in vs) = (v \in f @^-1: vs)%VS.
Proof.
move=> f v vs; apply/idP/idP; last first.
  rewrite -lpre_img_full; move/(memv_img f).
  rewrite lpre_imgK ?capvSr //.
  by move=> Hi; apply: (subv_trans Hi); exact: capvSl.
move=> Hv; pose v1 := inv_lapp f (f v).
have F1: v - v1 \in lker f.
 rewrite memv_ker linear_sub /v1.
 have F1: ((f \o (f \^-1 \o f)) v = f v)%VS.
   by rewrite inv_lapp_def.
by rewrite /= -{1}F1 comp_lappE /= comp_lappE /= addrN.
rewrite lpre_imgE; apply/memv_addP; exists v1; exists (v - v1); split=> //.
  apply: memv_img; rewrite memv_cap Hv.
  by rewrite limgE; apply: memv_img; apply: subvf.
by rewrite addrC -addrA addNr addr0.
Qed.

Lemma inv_lker0 : forall f, lker f == 0%:VS -> (f \^-1 \o f = \1)%VS.
Proof.
move=> [Mf] Hf.
congr LinearApp; rewrite /= /pinvmx /=.
rewrite -{1}(mulmx_ebase Mf) -!mulmxA.
rewrite mulKVmx ?row_ebase_unit //.
rewrite [pid_mx _ *m (_ *m _)]mulmxA mul_pid_mx minnn.
have Hr: \rank Mf = vdim V.
  apply: anti_leq.
  rewrite rank_leq_row row_leq_rank -kermx_eq0 -submx0.
  by move: Hf; rewrite -(@mx2vs0 _ _ (vdim V)) -mxeq2vseq; case/andP.
have: vdim V <= vdim W by rewrite -Hr rank_leq_col.
rewrite -{1}Hr -eqn_minr; move/eqP->.
by rewrite Hr pid_mx_1 mul1mx mulmxV // col_ebase_unit.
Qed.

End LinearPreImage.

Section Projection.

Variable (K : fieldType) (V : vectType K).
Implicit Types vs : {vspace V}.

Definition projv vs : 'End(V) := LinearApp (pinvmx (vs2mx vs) *m (vs2mx vs)).

Lemma projv_id : forall vs v, v \in vs -> projv vs v = v.
Proof.
move=> vs s Hv; rewrite /fun_of_lapp mulmxA mulmxKpV ?v2rvK //.
by move: Hv; rewrite /in_mem /= /subsetv /injv mx2vsK.
Qed.

Lemma lker_proj : forall vs, lker (projv vs) = (vs^C)%VS.
Proof.
move=> vs; apply: sym_equal; apply/eqP.
have: (vs^C <= lker (projv vs))%VS.
  rewrite /subsetv /= !genmxE; apply/sub_kermxP.
  by rewrite /complmx /pinvmx -!mulmxA [row_ebase _ *m _]mulmxA
            (mulmxV (row_ebase_unit _)) mul1mx mulmxA
           (mul_copid_mx_pid _ _ (rank_leq_col _)) mul0mx.
move/dimv_leqif_eq; move/leqifP; case: eqP=> // _; rewrite ltnNge; case/negP.
rewrite -(leq_add2r (\dim vs)) dimv_compl subnK -dimvf; last first.
  by rewrite dimvS // subvf.
rewrite -(limg_ker_dim (projv vs) (fullv _)) capfv -limgE leq_add2l dimvS //.
by apply/subvP=> v; move/projv_id<-; rewrite limgE memv_img // memvf.
Qed.

Lemma limg_proj : forall vs, limg (projv vs) = vs.
Proof.
move=> vs; apply: sym_equal; apply/eqP.
have: (vs <= limg (projv vs))%VS.
  by apply/subvP=> v; move/projv_id<-; rewrite limgE memv_img // memvf.
move/dimv_leqif_eq; move/leqifP; case: eqP=> // _; rewrite ltnNge; case/negP.
rewrite -(leq_add2l (\dim (vs^C))) -{1}lker_proj dimv_compl subnK -dimvf.
  by rewrite -(limg_ker_dim (projv vs) (fullv _)) capfv -limgE leqnn.
by rewrite dimvS // subvf.
Qed.

Lemma memv_proj : forall vs v, projv vs v \in vs.
Proof.
by move=> vs v; rewrite -{2}[vs]limg_proj limgE memv_img // memvf.
Qed.

Lemma memv_projC : forall vs v, v - projv vs v \in (vs^C)%VS.
Proof.
move=> vs v.
by rewrite -lker_proj memv_ker linear_sub /= (projv_id (memv_proj _ _)) subrr.
Qed.

Definition addv_pi1 vs1 vs2 : 'End(V) :=
 LinearApp (proj_mx (vs2mx vs1) (vs2mx vs2)).

Definition addv_pi2 vs1 vs2 : 'End(V) :=
 (projv vs2 \o (\1 - (addv_pi1 vs1 vs2)))%VS.

Lemma memv_pi1 : forall vs1 vs2 v, (addv_pi1 vs1 vs2) v \in vs1.
Proof.
move => vs1 vs2 v /=.
by rewrite /fun_of_lapp /in_mem /= /subsetv /injv rv2vK mx2vsK proj_mx_sub.
Qed.

Lemma memv_pi2 : forall vs1 vs2 v, (addv_pi2 vs1 vs2) v \in vs2.
Proof. by move => vs1 vs2 v; rewrite comp_lappE; apply: memv_proj. Qed.

Lemma addv_pi1_pi2 : forall vs1 vs2 v, v \in (vs1 + vs2)%VS ->
 v = ((addv_pi1 vs1 vs2) + (addv_pi2 vs1 vs2)) v.
Proof.
move => vs1 vs2 v Hv /=.
rewrite add_lappE comp_lappE /= add_lappE opp_lappE unit_lappE
        projv_id; first by rewrite addrC subrK.
move: Hv.
rewrite /fun_of_lapp /in_mem /= /subsetv /injv !mx2vsK linear_sub /= rv2vK.
move => Hv.
by rewrite proj_mx_compl_sub.
Qed.

Section Sumv_Pi.

Variable I : finType.
Variable V_ : I -> {vspace V}.
Variable P : pred I.

Let loop := fix loop (Vs : seq {vspace V}) : seq 'End(V) :=
 match Vs with
 | [::] => [::]
 | W :: Vs' => let pi := (addv_pi1 W (\sum_(V <- Vs') V)%VS) in
               pi :: (map (fun f => (f \o (\1 - pi))%VS) (loop Vs'))
 end.

Let size_loop : forall Vs, size (loop Vs) = size Vs.
Proof. by elim => // j js IH /=; rewrite size_map IH. Qed.

Definition sumv_pi (i : I) : 'End(V) :=
 nth \0%VS (loop (map V_ (enum P))) (index i (enum P)).

Lemma memv_sum_pi : forall i v, sumv_pi i v \in V_ i.
move => i v.
rewrite /sumv_pi -[loop _]map_id -(eq_map (fun x => comp_lapp1 x)).
elim: (enum P) \1%VS => /=.
 by rewrite zero_lappE mem0v.
move => j js IH F.
case: eqP => [->|_] /=.
 by rewrite comp_lappE; apply: memv_pi1.
by rewrite -map_comp /comp -(eq_map (fun x => comp_lappA x _ _)).
Qed.

Lemma sumv_sum_pi : forall v, v \in (\sum_(i | P i) V_ i)%VS ->
 v = (\sum_(i | P i) sumv_pi i) v.
Proof.
rewrite -big_filter -[\sum_(i | P i) _]big_filter /sumv_pi filter_index_enum.
elim: (enum P) (enum_uniq P) => [|j js IH] /=.
 by move => _ v; rewrite !big_nil memv0 zero_lappE; move/eqP.
case/andP => jnjs uniq v.
rewrite !big_cons /= (eq_refl j) /= big_map.
move/(addv_pi1_pi2) => Hv.
rewrite {1}Hv !add_lappE; congr (_ + _).
set V2 := (\sum_(j0 <- js) V_ j0)%VS.
rewrite (IH uniq _ (memv_pi2 (V_ j) V2 v))
        !(big_cond_seq (r := js) predT) !sum_lappE.
apply: eq_bigr => i.
case/andP => _.
case: eqP.
 by move => <- jjs; move: jnjs; rewrite jjs.
move => _ Hi /=.
by rewrite (nth_map \0%VS) ?size_loop ?size_map ?index_mem //
           comp_lappE /comp add_lappE opp_lappE unit_lappE {2}Hv add_lappE
           addrC addKr.
Qed.

End Sumv_Pi.

End Projection.

Section SubVectorType.

Variable (K : fieldType) (V : vectType K) (vs : {vspace V}).

Inductive subvect_of : predArgType := Subv x & x \in vs.
Definition sv_val u := let: Subv x _ := u in x.
Canonical Structure subvect_subType :=
  Eval hnf in [subType for sv_val by subvect_of_rect].
Definition subvect_eqMixin := Eval hnf in [eqMixin of subvect_of by <:].
Canonical Structure subvect_eqType :=
  Eval hnf in EqType subvect_of subvect_eqMixin.
Definition subvect_choiceMixin := [choiceMixin of subvect_of by <:].
Canonical Structure subvect_choiceType :=
  Eval hnf in ChoiceType subvect_of subvect_choiceMixin.

Lemma subvectP : forall u, sv_val u \in vs.
Proof. exact: valP. Qed.
Lemma subvect_inj : injective sv_val.
Proof. exact: val_inj. Qed.
Lemma congr_subv : forall u v, u = v -> sv_val u = sv_val v.
Proof. exact: congr1. Qed.

Definition subvect_zero := Subv (mem0v vs).
Definition subvect_opp u := Subv (memvNr (subvectP u)).
Definition subvect_add u v := Subv (memvD (subvectP u) (subvectP v)).

Lemma subvect_addA : associative subvect_add.
Proof. by move=> u v w; apply: val_inj; exact: addrA. Qed.
Lemma subvect_addC : commutative subvect_add.
Proof. by move=> u v; apply: val_inj; exact: addrC. Qed.
Lemma subvect_add0 : left_id subvect_zero subvect_add.
Proof. move=> u; apply: val_inj; exact: add0r. Qed.
Lemma subvect_addN : left_inverse subvect_zero subvect_opp subvect_add.
Proof. move=> u; apply: val_inj; exact: addNr. Qed.

Definition subvect_zmodMixin :=
  GRing.Zmodule.Mixin subvect_addA subvect_addC subvect_add0 subvect_addN.
Canonical Structure subvect_zmodType :=
  Eval hnf in ZmodType subvect_of subvect_zmodMixin.

Definition subvect_scale k (u : subvect_of) := Subv (memvZl k (valP u)).

Lemma subvect_scaleA : forall k1 k2 u,
  subvect_scale k1 (subvect_scale k2 u) = subvect_scale (k1 * k2) u.
Proof. by move=> *; apply: val_inj; exact: scalerA. Qed.
Lemma subvect_scale1 : left_id 1 subvect_scale.
Proof. by move=> *; apply: val_inj; exact: scale1r. Qed.
Lemma subvect_scale_addr : forall k, {morph (subvect_scale k) : x y / x + y}.
Proof. by move=> k u v; apply: val_inj; exact: scaler_addr. Qed.
Lemma subvect_scale_addl : forall u,
  {morph (subvect_scale)^~ u : k1 k2 / k1 + k2}.
Proof. by move=> u k1 k2; apply: val_inj; exact: scaler_addl. Qed.

Definition subvect_lmodMixin :=
  GRing.Lmodule.Mixin subvect_scaleA subvect_scale1
                      subvect_scale_addr subvect_scale_addl.
Canonical Structure subvect_lmodType :=
  Eval hnf in LmodType K subvect_of subvect_lmodMixin.

Definition subvect_v2rv (u : subvect_of) :=
  \row_(j < size(vbasis vs)) (coord (vbasis vs) (sv_val u) j).

Lemma subvect_is_linear : linear subvect_v2rv.
Proof.
move=> k u1 v1; apply: val_inj.
congr mx_val; apply/matrixP=> i j /=.
by rewrite !mxE linearD linearZ !ffunE.
Qed.

Canonical Structure subvect_linear := Linear subvect_is_linear.

Lemma subvect_bij : bijective subvect_v2rv.
Proof.
pose v (r : 'rV_(size (vbasis vs))) :=
  \sum_(i < size (vbasis vs)) (r 0 i *: (vbasis vs)`_i).
have v_in: forall r, v r \in vs.
  move=> r; apply: memv_suml=> i _; apply: memvZl.
  by apply: memv_basis; apply: mem_nth.
exists (fun r => Subv (v_in r)).
  move=> v1; apply: val_inj; rewrite /subvect_v2rv /v.
  have F1: sv_val v1 \in vs by case v1.
  by rewrite /= {2}(coord_basis F1); apply: eq_big=> // i _; rewrite mxE.
move=> v1; apply/rowP=> [] i.
rewrite /subvect_v2rv /v /= mxE coord_sumE.
rewrite (bigD1 i) //= linearZ ffunE
        (free_coordE _ _ (is_basis_free (is_basis_vbasis _)))
         eqxx /GRing.scale /= ?mulr1 big1 ?addr0 //.
move=> k.
rewrite linearZ ffunE (free_coordE _ _ (is_basis_free (is_basis_vbasis _))).
by rewrite {1}/eq_op /=; case: eqP=> //; rewrite /GRing.scale /= mulr0.
Qed.

Definition subvect_VectMixin := VectMixin subvect_is_linear subvect_bij.
Canonical Structure subvect_vectType := VectType K subvect_VectMixin.

End SubVectorType.

Definition lappE :=
  (zero_lappE, comp_lappE, scale_lappE, add_lappE, sum_lappE).

Section ProdVector.

Variable (K : fieldType) (V W : vectType K).

Definition prodVector := locked (matrixVectType K 1 (vdim V + vdim W)).

Local Notation v2rv V := (@v2rv_isomorphism _ V).
Local Notation rv2v V := (@rv2v_isomorphism _ V).

Definition p2pv : forall (vw: V * W), prodVector.
move=> vw; unlock prodVector.
exact (row_mx (v2rv V vw.1) (v2rv W vw.2)).
Defined.

Definition pv2p : forall (p : prodVector), V * W.
unlock prodVector=> p.
exact (rv2v V (lsubmx p), rv2v W (rsubmx p)).
Defined.

Lemma p2pvK : cancel p2pv pv2p.
Proof.
move=> [u v]; rewrite /p2pv /pv2p.
by unlock prodVector; rewrite row_mxKl row_mxKr !v2rvK.
Qed.

Lemma pv2pK : cancel pv2p p2pv.
Proof.
rewrite /cancel /pv2p /p2pv; unlock prodVector=> x /=.
by rewrite !rv2vK hsubmxK.
Qed.

Lemma pvaddE : forall p q : prodVector,
  pv2p (p + q) = ((pv2p p).1+(pv2p q).1,(pv2p p).2+(pv2p q).2).
Proof.
by rewrite /pv2p; unlock prodVector=> p q; rewrite !linearD.
Qed.

Lemma pvoppE : forall p : prodVector,
  pv2p (-p) = (-(pv2p p).1,-(pv2p p).2).
Proof.
by rewrite /pv2p; unlock prodVector=> p; rewrite !linearN.
Qed.

Lemma pvscaleE : forall (a: K) (p : prodVector),
  pv2p (a *: p) = (a *: (pv2p p).1, a *: (pv2p p).2).
Proof.
by rewrite /pv2p; unlock prodVector=> a p; rewrite !linearZ.
Qed.

Definition pvf f g : 'End(prodVector) :=
   lapp_of_fun (fun p => let (u,v) := pv2p p in p2pv (f u, g v)).

Lemma pvfK : forall (f : 'End(V)) (g : 'End(W)),
   pvf f g =1 (fun x : prodVector => p2pv (f (pv2p x).1 , g (pv2p x).2)).
Proof.
move=> f g p; rewrite /pvf lapp_of_funK; first by case pv2p.
move=> a.
rewrite /pv2p /p2pv; unlock prodVector=> x y /=.
rewrite !linearP.
by apply/matrixP=> i j; rewrite !mxE; case: split=> o; rewrite !mxE.
Qed.

End ProdVector.

Notation "A :+: B" := (prodVector A B) : type_scope.

Section ExpVector.

Variable (K : fieldType) (V : vectType K).

Fixpoint expVector (n : nat) {struct n} :=
  if n is n1.+1 then (V :+: (expVector n1)) else matrixVectType K 0 0.

Fixpoint l2ev (l : seq V) : expVector (size l) :=
 if l is (x :: l1) return expVector (size l) then p2pv (x, (l2ev l1))
 else 0.

Lemma l2ev_cons : forall x l, l2ev (x :: l) = p2pv (x, (l2ev l)).
Proof. by []. Qed.

Fixpoint ev2l (n : nat) : expVector n -> seq V :=
  if n is n1.+1 return (expVector n -> seq V) then
      fun p => let (u, p1) := pv2p p in u :: @ev2l n1 p1
  else fun _ => [::].

Fixpoint tuple_of_ev (n : nat) : expVector n -> n.-tuple V :=
  if n is n1.+1 return (expVector n -> n.-tuple V) then
      fun p =>
      [tuple of (pv2p p).1 :: tuple_of_ev (pv2p p).2]
  else fun _ => [tuple].

Fixpoint ev_of_tuple (n : nat) : n.-tuple V -> expVector n :=
  if n is n1.+1 return (n.-tuple V -> expVector n) then
      fun t =>
        p2pv (tnth t 0, ev_of_tuple (behead_tuple t))
  else fun _ => 0.

Let behead_tupleE : forall n u (v : n.-tuple V),
  behead_tuple [tuple of u :: v] = v.
Proof.
move=> n u v; apply: eq_from_tnth=> i.
by rewrite tnth_behead !(tnth_nth 0) inordK //; case: i.
Qed.

Lemma tuple_of_evK : forall n, cancel (@tuple_of_ev n) (@ev_of_tuple n).
Proof.
elim=> [|n Hrec] x; first by rewrite (thinmx0 x).
by rewrite /= behead_tupleE Hrec (tnth_nth 0) -surjective_pairing pv2pK.
Qed.

Lemma ev_of_tupleK : forall n, cancel (@ev_of_tuple n) (@tuple_of_ev n).
Proof.
elim=> [|n Hrec] x; first by rewrite (tuple0 x).
by rewrite (tuple_eta x) /= behead_tupleE (tnth_nth 0) p2pvK Hrec.
Qed.

Definition evf n (ft : n.-tuple (V -> V)) : 'Hom(V, expVector n) :=
  lapp_of_fun
    (fun p => ev_of_tuple (map_tuple (fun x => x p) ft)).

Let map_tupleE :
  forall (T1 T2 : Type) (f : T1 -> T2) (x : T1) n (t : n.-tuple T1),
   map_tuple f [tuple of x :: t] = [tuple of f x :: map f t].
Proof.
move=> T1 T2 f x n t.
by apply: eq_from_tnth=> i; rewrite !(tnth_nth (f x)).
Qed.

Lemma evfK : forall n (ft : n.-tuple (V -> V)),
  (forall i, linear (tnth ft i)) ->
  evf ft =1 (fun p => ev_of_tuple (map_tuple (fun x => x p) ft)).
Proof.
move=> n ft Hl x.
apply: lapp_of_funK=> a u v.
elim: n ft Hl => [|n Hrec] ft Hl.
  by rewrite [ft]tuple0 scaler0 add0r.
case/tupleP: ft Hl=> f ft Hl.
rewrite !map_tupleE /= !behead_tupleE Hrec; last first.
  by move=> i; move: (Hl (rshift 1 i)); rewrite !(tnth_nth (fun x => 0)).
move: (Hl 0);rewrite !tnth0=> ->.
rewrite /p2pv; unlock prodVector.
by apply/rowP=> i; rewrite !mxE; case: split=> o; rewrite /= linearP !mxE.
Qed.

End ExpVector.

Notation "V '^' n" := (expVector V n) : vspace_scope.

Section Solver.

Variable (K : fieldType) (V : vectType K).

Variable n : nat.
Variable feq : n.-tuple (V -> V).
Variable veq : n.-tuple V.
Variable feq_linear : forall i, linear (tnth feq i).

Definition vsolve_eq ms :=
  ((ev_of_tuple veq) \in (evf feq) @: ms)%VS.

Lemma vsolve_eqP : forall (ms : {vspace V}),
  reflect
      (exists u, u \in ms /\
         forall i : 'I_n, tnth feq i u = tnth veq i)
      (vsolve_eq ms).
Proof.
move=> ms.
apply: (iffP (memv_imgP _ _ _))=> [] [v [H1v H2v]]; exists v; split=> //.
  move=> i.
  by rewrite -[veq]ev_of_tupleK H2v (evfK feq_linear) ev_of_tupleK tnth_map.
rewrite (evfK feq_linear); congr (ev_of_tuple).
by apply: eq_from_tnth=> j; rewrite -H2v tnth_map.
Qed.

End Solver.

Export VectorType.Exports.