Library mathcomp.algebra.vector

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


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

Reserved Notation "{ 'vspace' T }" (at level 0, format "{ 'vspace' T }").
Reserved Notation "''Hom' ( T , rT )" (at level 8, format "''Hom' ( T , rT )").
Reserved Notation "''End' ( T )" (at level 8, format "''End' ( T )").
Reserved Notation "\dim A" (at level 10, A at level 8, format "\dim A").

Delimit Scope vspace_scope with VS.

Import GRing.Theory.

Module Vector.

Section ClassDef.
Variable R : ringType.

Definition axiom_def n (V : lmodType R) of phant V :=
  {v2r : V -> 'rV[R]_n | linear v2r & bijective v2r}.

Inductive mixin_of (V : lmodType R) := Mixin dim & axiom_def dim (Phant V).

Structure class_of V := 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 : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c T.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition dim := let: Mixin n _ := mixin class in n.

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

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition lmodType := @GRing.Lmodule.Pack R phR cT xclass xT.

End ClassDef.
Notation axiom n V := (axiom_def n (Phant V)).

Section OtherDefs.
Local Coercion sort : type >-> Sortclass.
Local Coercion dim : type >-> nat.
Inductive space (K : fieldType) (vT : type (Phant K)) (phV : phant vT) :=
  Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
Inductive hom (R : ringType) (vT wT : type (Phant R)) :=
  Hom of 'M[R]_(vT, wT).
End OtherDefs.

Module Import 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 eqType.
Coercion choiceType: type >-> Choice.type.
Canonical choiceType.
Coercion zmodType: type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion lmodType: type>-> GRing.Lmodule.type.
Canonical lmodType.
Notation vectType R := (@type _ (Phant R)).
Notation VectType R V mV :=
   (@pack _ (Phant R) V _ mV _ _ id _ id).
Notation VectMixin := Mixin.
Notation "[ 'vectType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'vectType' R 'of' T 'for' cT ]") : form_scope.
Notation "[ 'vectType' R 'of' T ]" := (@clone _ (Phant R) T _ _ idfun)
  (at level 0, format "[ 'vectType' R 'of' T ]") : form_scope.

Notation "{ 'vspace' vT }" := (space (Phant vT)) : type_scope.
Notation "''Hom' ( aT , rT )" := (hom aT rT) : type_scope.
Notation "''End' ( vT )" := (hom vT vT) : type_scope.

Prenex Implicits Hom.

Delimit Scope vspace_scope with VS.
Bind Scope vspace_scope with space.
Delimit Scope lfun_scope with VF.
Bind Scope lfun_scope with hom.

End Exports.

Module InternalTheory.

Section Iso.
Variables (R : ringType) (vT rT : vectType R).
Local Coercion dim : vectType >-> nat.

Fact v2r_subproof : axiom vT vT. Proof. by case: vT => T [bT []]. Qed.
Definition v2r := s2val v2r_subproof.

Let v2r_bij : bijective v2r := s2valP' v2r_subproof.
Fact r2v_subproof : {r2v | cancel r2v v2r}.
Proof.
have r2vP r: {v | v2r v = r}.
  by apply: sig_eqW; have [v _ vK] := v2r_bij; exists (v r).
by exists (fun r => sval (r2vP r)) => r; case: (r2vP r).
Qed.
Definition r2v := sval r2v_subproof.

Lemma r2vK : cancel r2v v2r. Proof. exact: (svalP r2v_subproof). Qed.
Lemma r2v_inj : injective r2v. Proof. exact: can_inj r2vK. Qed.
Lemma v2rK : cancel v2r r2v. Proof. by have/bij_can_sym:= r2vK; apply. Qed.
Lemma v2r_inj : injective v2r. Proof. exact: can_inj v2rK. Qed.

Canonical v2r_linear := Linear (s2valP v2r_subproof : linear v2r).
Canonical r2v_linear := Linear (can2_linear v2rK r2vK).
End Iso.

Section Vspace.
Variables (K : fieldType) (vT : vectType K).
Local Coercion dim : vectType >-> nat.

Definition b2mx n (X : n.-tuple vT) := \matrix_i v2r (tnth X i).
Lemma b2mxK n (X : n.-tuple vT) i : r2v (row i (b2mx X)) = X`_i.
Proof. by rewrite rowK v2rK -tnth_nth. Qed.

Definition vs2mx {phV} (U : @space K vT phV) := let: Space mx _ := U in mx.
Lemma gen_vs2mx (U : {vspace vT}) : <<vs2mx U>>%MS = vs2mx U.
Proof. by apply/eqP; rewrite /vs2mx; case: U. Qed.

Fact mx2vs_subproof m (A : 'M[K]_(m, vT)) : <<(<<A>>)>>%MS == <<A>>%MS.
Proof. by rewrite genmx_id. Qed.
Definition mx2vs {m} A : {vspace vT} := Space _ (@mx2vs_subproof m A).

Canonical space_subType := [subType for @vs2mx (Phant vT)].
Lemma vs2mxK : cancel vs2mx mx2vs.
Proof. by move=> v; apply: val_inj; rewrite /= gen_vs2mx. Qed.
Lemma mx2vsK m (M : 'M_(m, vT)) : (vs2mx (mx2vs M) :=: M)%MS.
Proof. exact: genmxE. Qed.
End Vspace.

Section Hom.
Variables (R : ringType) (aT rT : vectType R).
Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A.
Canonical hom_subType := [newType for f2mx].
End Hom.

Arguments mx2vs _ _ _%N _%MS.
Prenex Implicits v2r r2v v2rK r2vK b2mx vs2mx vs2mxK f2mx.

End InternalTheory.

End Vector.
Export Vector.Exports.
Import Vector.InternalTheory.

Section VspaceDefs.

Variables (K : fieldType) (vT : vectType K).
Implicit Types (u : vT) (X : seq vT) (U V : {vspace vT}).

Definition space_eqMixin := Eval hnf in [eqMixin of {vspace vT} by <:].
Canonical space_eqType := EqType {vspace vT} space_eqMixin.
Definition space_choiceMixin := Eval hnf in [choiceMixin of {vspace vT} by <:].
Canonical space_choiceType := ChoiceType {vspace vT} space_choiceMixin.

Definition dimv U := \rank (vs2mx U).
Definition subsetv U V := (vs2mx U <= vs2mx V)%MS.
Definition vline u := mx2vs (v2r u).

Definition pred_of_vspace phV (U : Vector.space phV) : pred_class :=
  fun v => (vs2mx (vline v) <= vs2mx U)%MS.
Canonical vspace_predType :=
  @mkPredType _ (unkeyed {vspace vT}) (@pred_of_vspace _).

Definition fullv : {vspace vT} := mx2vs 1%:M.
Definition addv U V := mx2vs (vs2mx U + vs2mx V).
Definition capv U V := mx2vs (vs2mx U :&: vs2mx V).
Definition complv U := mx2vs (vs2mx U)^C.
Definition diffv U V := mx2vs (vs2mx U :\: vs2mx V).
Definition vpick U := r2v (nz_row (vs2mx U)).
Fact span_key : unit. Proof. by []. Qed.
Definition span_expanded_def X := mx2vs (b2mx (in_tuple X)).
Definition span := locked_with span_key span_expanded_def.
Canonical span_unlockable := [unlockable fun span].
Definition vbasis_def U :=
  [tuple r2v (row i (row_base (vs2mx U))) | i < dimv U].
Definition vbasis := locked_with span_key vbasis_def.
Canonical vbasis_unlockable := [unlockable fun vbasis].


Definition free X := dimv (span X) == size X.
Definition basis_of U X := (span X == U) && free X.

End VspaceDefs.

Coercion pred_of_vspace : Vector.space >-> pred_class.
Notation "\dim U" := (dimv U) : nat_scope.
Notation "U <= V" := (subsetv U V) : vspace_scope.
Notation "U <= V <= W" := (subsetv U V && subsetv V W) : vspace_scope.
Notation "<[ v ] >" := (vline v) : vspace_scope.
Notation "<< X >>" := (span X) : vspace_scope.
Notation "0" := (vline 0) : vspace_scope.
Arguments fullv {K vT}.
Prenex Implicits subsetv addv capv complv diffv span free basis_of.

Notation "U + V" := (addv U V) : vspace_scope.
Notation "U :&: V" := (capv U V) : vspace_scope.
Notation "U ^C" := (complv U) (at level 8, format "U ^C") : vspace_scope.
Notation "U :\: V" := (diffv U V) : vspace_scope.
Notation "{ : vT }" := (@fullv _ vT) (only parsing) : vspace_scope.

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

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

Section VectorTheory.

Variables (K : fieldType) (vT : vectType K).
Implicit Types (a : K) (u v w : vT) (X Y : seq vT) (U V W : {vspace vT}).

Local Notation subV := (@subsetv K vT) (only parsing).
Local Notation addV := (@addv K vT) (only parsing).
Local Notation capV := (@capv K vT) (only parsing).


Fact vspace_key U : pred_key U. Proof. by []. Qed.
Canonical vspace_keyed U := KeyedPred (vspace_key U).

Lemma memvE v U : (v \in U) = (<[v]> <= U)%VS. Proof. by []. Qed.

Lemma vlineP v1 v2 : reflect (exists k, v1 = k *: v2) (v1 \in <[v2]>)%VS.
Proof.
apply: (iffP idP) => [|[k ->]]; rewrite memvK genmxE ?linearZ ?scalemx_sub //.
by case/sub_rVP=> k; rewrite -linearZ => /v2r_inj->; exists k.
Qed.

Fact memv_submod_closed U : submod_closed U.
Proof.
split=> [|a u v]; rewrite !memvK ?linear0 ?sub0mx // => Uu Uv.
by rewrite linearP addmx_sub ?scalemx_sub.
Qed.
Canonical memv_opprPred U := OpprPred (memv_submod_closed U).
Canonical memv_addrPred U := AddrPred (memv_submod_closed U).
Canonical memv_zmodPred U := ZmodPred (memv_submod_closed U).
Canonical memv_submodPred U := SubmodPred (memv_submod_closed U).

Lemma mem0v U : 0 \in U. Proof. exact : rpred0. Qed.
Lemma memvN U v : (- v \in U) = (v \in U). Proof. exact: rpredN. Qed.
Lemma memvD U : {in U &, forall u v, u + v \in U}. Proof. exact : rpredD. Qed.
Lemma memvB U : {in U &, forall u v, u - v \in U}. Proof. exact : rpredB. Qed.
Lemma memvZ U k : {in U, forall v, k *: v \in U}. Proof. exact : rpredZ. Qed.

Lemma memv_suml I r (P : pred I) vs U :
  (forall i, P i -> vs i \in U) -> \sum_(i <- r | P i) vs i \in U.
Proof. exact: rpred_sum. Qed.

Lemma memv_line u : u \in <[u]>%VS.
Proof. by apply/vlineP; exists 1; rewrite scale1r. Qed.

Lemma subvP U V : reflect {subset U <= V} (U <= V)%VS.
Proof.
apply: (iffP rV_subP) => sU12 u.
  by rewrite !memvE /subsetv !genmxE => /sU12.
by have:= sU12 (r2v u); rewrite !memvE /subsetv !genmxE r2vK.
Qed.

Lemma subvv U : (U <= U)%VS. Proof. exact/subvP. Qed.
Hint Resolve subvv.

Lemma subv_trans : transitive subV.
Proof. by move=> U V W /subvP sUV /subvP sVW; apply/subvP=> u /sUV/sVW. Qed.

Lemma subv_anti : antisymmetric subV.
Proof. by move=> U V; apply/vs2mxP. Qed.

Lemma eqEsubv U V : (U == V) = (U <= V <= U)%VS.
Proof. by apply/eqP/idP=> [-> | /subv_anti//]; rewrite subvv. Qed.

Lemma vspaceP U V : U =i V <-> U = V.
Proof.
split=> [eqUV | -> //]; apply/subv_anti/andP.
by split; apply/subvP=> v; rewrite eqUV.
Qed.

Lemma subvPn {U V} : reflect (exists2 u, u \in U & u \notin V) (~~ (U <= V)%VS).
Proof.
apply: (iffP idP) => [|[u Uu]]; last by apply: contra => /subvP->.
case/row_subPn=> i; set vi := row i _ => V'vi.
by exists (r2v vi); rewrite memvK r2vK ?row_sub.
Qed.

Lemma sub0v U : (0 <= U)%VS.
Proof. exact: mem0v. Qed.

Lemma subv0 U : (U <= 0)%VS = (U == 0%VS).
Proof. by rewrite eqEsubv sub0v andbT. Qed.

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


Lemma subvf U : (U <= fullv)%VS. Proof. by rewrite /subsetv vs2mxF submx1. Qed.
Lemma memvf v : v \in fullv. Proof. exact: subvf. Qed.

Lemma memv_pick U : vpick U \in U. Proof. by rewrite mem_r2v nz_row_sub. Qed.

Lemma vpick0 U : (vpick U == 0) = (U == 0%VS).
Proof. by rewrite -memv0 mem_r2v -subv0 /subV vs2mx0 !submx0 nz_row_eq0. Qed.

Lemma subv_add U V W : (U + V <= W)%VS = (U <= W)%VS && (V <= W)%VS.
Proof. by rewrite /subV vs2mxD addsmx_sub. Qed.

Lemma addvS U1 U2 V1 V2 : (U1 <= U2 -> V1 <= V2 -> U1 + V1 <= U2 + V2)%VS.
Proof. by rewrite /subV !vs2mxD; apply: addsmxS. Qed.

Lemma addvSl U V : (U <= U + V)%VS.
Proof. by rewrite /subV vs2mxD addsmxSl. Qed.

Lemma addvSr U V : (V <= U + V)%VS.
Proof. by rewrite /subV vs2mxD addsmxSr. Qed.

Lemma addvC : commutative addV.
Proof. by move=> U V; apply/vs2mxP; rewrite !vs2mxD addsmxC submx_refl. Qed.

Lemma addvA : associative addV.
Proof. by move=> U V W; apply/vs2mxP; rewrite !vs2mxD addsmxA submx_refl. Qed.

Lemma addv_idPl {U V}: reflect (U + V = U)%VS (V <= U)%VS.
Proof. by rewrite /subV (sameP addsmx_idPl eqmxP) -vs2mxD; apply: vs2mxP. Qed.

Lemma addv_idPr {U V} : reflect (U + V = V)%VS (U <= V)%VS.
Proof. by rewrite addvC; apply: addv_idPl. Qed.

Lemma addvv : idempotent addV.
Proof. by move=> U; apply/addv_idPl. Qed.

Lemma add0v : left_id 0%VS addV.
Proof. by move=> U; apply/addv_idPr/sub0v. Qed.

Lemma addv0 : right_id 0%VS addV.
Proof. by move=> U; apply/addv_idPl/sub0v. Qed.

Lemma sumfv : left_zero fullv addV.
Proof. by move=> U; apply/addv_idPl/subvf. Qed.

Lemma addvf : right_zero fullv addV.
Proof. by move=> U; apply/addv_idPr/subvf. Qed.

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

Lemma memv_add u v U V : u \in U -> v \in V -> u + v \in (U + V)%VS.
Proof. by rewrite !memvK genmxE linearD; apply: addmx_sub_adds. Qed.

Lemma memv_addP {w U V} :
  reflect (exists2 u, u \in U & exists2 v, v \in V & w = u + v)
          (w \in U + V)%VS.
Proof.
apply: (iffP idP) => [|[u Uu [v Vv ->]]]; last exact: memv_add.
rewrite memvK genmxE => /sub_addsmxP[r /(canRL v2rK)->].
rewrite linearD /=; set u := r2v _; set v := r2v _.
by exists u; last exists v; rewrite // mem_r2v submxMl.
Qed.

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

Lemma sumv_sup i0 P U Vs :
  P i0 -> (U <= Vs i0)%VS -> (U <= \sum_(i | P i) Vs i)%VS.
Proof. by move=> Pi0 /subv_trans-> //; rewrite (bigD1 i0) ?addvSl. Qed.
Arguments sumv_sup i0 [P U Vs].

Lemma subv_sumP {P Us V} :
  reflect (forall i, P i -> Us i <= V)%VS (\sum_(i | P i) Us i <= V)%VS.
Proof.
apply: (iffP idP) => [sUV i Pi | sUV].
  by apply: subv_trans sUV; apply: sumv_sup Pi _.
by elim/big_rec: _ => [|i W Pi sWV]; rewrite ?sub0v // subv_add sUV.
Qed.

Lemma memv_sumr P vs (Us : I -> {vspace vT}) :
    (forall i, P i -> vs i \in Us i) ->
  \sum_(i | P i) vs i \in (\sum_(i | P i) Us i)%VS.
Proof. by move=> Uv; apply/rpred_sum=> i Pi; apply/(sumv_sup i Pi)/Uv. Qed.

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.
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.

End BigSum.


Lemma subv_cap U V W : (U <= V :&: W)%VS = (U <= V)%VS && (U <= W)%VS.
Proof. by rewrite /subV vs2mxI sub_capmx. Qed.

Lemma capvS U1 U2 V1 V2 : (U1 <= U2 -> V1 <= V2 -> U1 :&: V1 <= U2 :&: V2)%VS.
Proof. by rewrite /subV !vs2mxI; apply: capmxS. Qed.

Lemma capvSl U V : (U :&: V <= U)%VS.
Proof. by rewrite /subV vs2mxI capmxSl. Qed.

Lemma capvSr U V : (U :&: V <= V)%VS.
Proof. by rewrite /subV vs2mxI capmxSr. Qed.

Lemma capvC : commutative capV.
Proof. by move=> U V; apply/vs2mxP; rewrite !vs2mxI capmxC submx_refl. Qed.

Lemma capvA : associative capV.
Proof. by move=> U V W; apply/vs2mxP; rewrite !vs2mxI capmxA submx_refl. Qed.

Lemma capv_idPl {U V} : reflect (U :&: V = U)%VS (U <= V)%VS.
Proof. by rewrite /subV(sameP capmx_idPl eqmxP) -vs2mxI; apply: vs2mxP. Qed.

Lemma capv_idPr {U V} : reflect (U :&: V = V)%VS (V <= U)%VS.
Proof. by rewrite capvC; apply: capv_idPl. Qed.

Lemma capvv : idempotent capV.
Proof. by move=> U; apply/capv_idPl. Qed.

Lemma cap0v : left_zero 0%VS capV.
Proof. by move=> U; apply/capv_idPl/sub0v. Qed.

Lemma capv0 : right_zero 0%VS capV.
Proof. by move=> U; apply/capv_idPr/sub0v. Qed.

Lemma capfv : left_id fullv capV.
Proof. by move=> U; apply/capv_idPr/subvf. Qed.

Lemma capvf : right_id fullv capV.
Proof. by move=> U; apply/capv_idPl/subvf. Qed.

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

Lemma memv_cap w U V : (w \in U :&: V)%VS = (w \in U) && (w \in V).
Proof. by rewrite !memvE subv_cap. Qed.

Lemma memv_capP {w U V} : reflect (w \in U /\ w \in V) (w \in U :&: V)%VS.
Proof. by rewrite memv_cap; apply: andP. Qed.

Lemma vspace_modl U V W : (U <= W -> U + (V :&: W) = (U + V) :&: W)%VS.
Proof.
by move=> sUV; apply/vs2mxP; rewrite !(vs2mxD, vs2mxI); apply/eqmxP/matrix_modl.
Qed.

Lemma vspace_modr U V W : (W <= U -> (U :&: V) + W = U :&: (V + W))%VS.
Proof. by rewrite -!(addvC W) !(capvC U); apply: vspace_modl. Qed.

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

Lemma bigcapv_inf i0 P Us V :
  P i0 -> (Us i0 <= V -> \bigcap_(i | P i) Us i <= V)%VS.
Proof. by move=> Pi0; apply: subv_trans; rewrite (bigD1 i0) ?capvSl. Qed.

Lemma subv_bigcapP {P U Vs} :
  reflect (forall i, P i -> U <= Vs i)%VS (U <= \bigcap_(i | P i) Vs i)%VS.
Proof.
apply: (iffP idP) => [sUV i Pi | sUV].
  by rewrite (subv_trans sUV) ?(bigcapv_inf Pi).
by elim/big_rec: _ => [|i W Pi]; rewrite ?subvf // subv_cap sUV.
Qed.

End BigCap.

Lemma addv_complf U : (U + U^C)%VS = fullv.
Proof.
apply/vs2mxP; rewrite vs2mxD -gen_vs2mx -genmx_adds !genmxE submx1 sub1mx.
exact: addsmx_compl_full.
Qed.

Lemma capv_compl U : (U :&: U^C = 0)%VS.
Proof.
apply/val_inj; rewrite [val]/= vs2mx0 vs2mxI -gen_vs2mx -genmx_cap.
by rewrite capmx_compl genmx0.
Qed.

Lemma diffvSl U V : (U :\: V <= U)%VS.
Proof. by rewrite /subV genmxE diffmxSl. Qed.

Lemma capv_diff U V : ((U :\: V) :&: V = 0)%VS.
Proof.
apply/val_inj; rewrite [val]/= vs2mx0 vs2mxI -(gen_vs2mx V) -genmx_cap.
by rewrite capmx_diff genmx0.
Qed.

Lemma addv_diff_cap U V : (U :\: V + U :&: V)%VS = U.
Proof.
apply/vs2mxP; rewrite vs2mxD -genmx_adds !genmxE.
exact/eqmxP/addsmx_diff_cap_eq.
Qed.

Lemma addv_diff U V : (U :\: V + V = U + V)%VS.
Proof. by rewrite -{2}(addv_diff_cap U V) -addvA (addv_idPr (capvSr U V)). Qed.

Lemma dimv0 : \dim (0%VS : {vspace vT}) = 0%N.
Proof. by rewrite /dimv vs2mx0 mxrank0. Qed.

Lemma dimv_eq0 U : (\dim U == 0%N) = (U == 0%VS).
Proof. by rewrite /dimv /= mxrank_eq0 {2}/eq_op /= linear0 genmx0. Qed.

Lemma dimvf : \dim {:vT} = Vector.dim vT.
Proof. by rewrite /dimv vs2mxF mxrank1. Qed.

Lemma dim_vline v : \dim <[v]> = (v != 0).
Proof. by rewrite /dimv mxrank_gen rank_rV (can2_eq v2rK r2vK) linear0. Qed.

Lemma dimvS U V : (U <= V)%VS -> \dim U <= \dim V.
Proof. exact: mxrankS. Qed.

Lemma dimv_leqif_sup U V : (U <= V)%VS -> \dim U <= \dim V ?= iff (V <= U)%VS.
Proof. exact: mxrank_leqif_sup. Qed.

Lemma dimv_leqif_eq U V : (U <= V)%VS -> \dim U <= \dim V ?= iff (U == V).
Proof. by rewrite eqEsubv; apply: mxrank_leqif_eq. Qed.

Lemma eqEdim U V : (U == V) = (U <= V)%VS && (\dim V <= \dim U).
Proof. by apply/idP/andP=> [/eqP | [/dimv_leqif_eq/geq_leqif]] ->. Qed.

Lemma dimv_compl U : \dim U^C = (\dim {:vT} - \dim U)%N.
Proof. by rewrite dimvf /dimv mxrank_gen mxrank_compl. Qed.

Lemma dimv_cap_compl U V : (\dim (U :&: V) + \dim (U :\: V))%N = \dim U.
Proof. by rewrite /dimv !mxrank_gen mxrank_cap_compl. Qed.

Lemma dimv_sum_cap U V : (\dim (U + V) + \dim (U :&: V) = \dim U + \dim V)%N.
Proof. by rewrite /dimv !mxrank_gen mxrank_sum_cap. Qed.

Lemma dimv_disjoint_sum U V :
  (U :&: V = 0)%VS -> \dim (U + V) = (\dim U + \dim V)%N.
Proof. by move=> dxUV; rewrite -dimv_sum_cap dxUV dimv0 addn0. Qed.

Lemma dimv_add_leqif U V :
  \dim (U + V) <= \dim U + \dim V ?= iff (U :&: V <= 0)%VS.
Proof.
by rewrite /dimv /subV !mxrank_gen vs2mx0 genmxE; apply: mxrank_adds_leqif.
Qed.

Lemma diffv_eq0 U V : (U :\: V == 0)%VS = (U <= V)%VS.
Proof.
rewrite -dimv_eq0 -(eqn_add2l (\dim (U :&: V))) addn0 dimv_cap_compl eq_sym.
by rewrite (dimv_leqif_eq (capvSl _ _)) (sameP capv_idPl eqP).
Qed.

Lemma dimv_leq_sum I r (P : pred I) (Us : I -> {vspace vT}) :
  \dim (\sum_(i <- r | P i) Us i) <= \sum_(i <- r | P i) \dim (Us i).
Proof.
elim/big_rec2: _ => [|i d vs _ le_vs_d]; first by rewrite dim_vline eqxx.
by apply: (leq_trans (dimv_add_leqif _ _)); rewrite leq_add2l.
Qed.

Section SumExpr.

Structure addv_expr := Sumv {
  addv_val :> wrapped {vspace vT};
  addv_dim : wrapped nat;
  _ : mxsum_spec (vs2mx (unwrap addv_val)) (unwrap addv_dim)
}.

Definition vs2mx_sum_expr_subproof (S : addv_expr) :
  mxsum_spec (vs2mx (unwrap S)) (unwrap (addv_dim S)).
Proof. by case: S. Qed.
Canonical vs2mx_sum_expr S := ProperMxsumExpr (vs2mx_sum_expr_subproof S).

Canonical trivial_addv U := @Sumv (Wrap U) (Wrap (\dim U)) (TrivialMxsum _).

Structure proper_addv_expr := ProperSumvExpr {
  proper_addv_val :> {vspace vT};
  proper_addv_dim :> nat;
  _ : mxsum_spec (vs2mx proper_addv_val) proper_addv_dim
}.

Definition proper_addvP (S : proper_addv_expr) :=
  let: ProperSumvExpr _ _ termS := S return mxsum_spec (vs2mx S) S in termS.

Canonical proper_addv (S : proper_addv_expr) :=
  @Sumv (wrap (S : {vspace vT})) (wrap (S : nat)) (proper_addvP S).

Section Binary.
Variables S1 S2 : addv_expr.
Fact binary_addv_subproof :
  mxsum_spec (vs2mx (unwrap S1 + unwrap S2))
             (unwrap (addv_dim S1) + unwrap (addv_dim S2)).
Proof. by rewrite vs2mxD; apply: proper_mxsumP. Qed.
Canonical binary_addv_expr := ProperSumvExpr binary_addv_subproof.
End Binary.

Section Nary.
Variables (I : Type) (r : seq I) (P : pred I) (S_ : I -> addv_expr).
Fact nary_addv_subproof :
  mxsum_spec (vs2mx (\sum_(i <- r | P i) unwrap (S_ i)))
             (\sum_(i <- r | P i) unwrap (addv_dim (S_ i))).
Proof. by rewrite vs2mx_sum; apply: proper_mxsumP. Qed.
Canonical nary_addv_expr := ProperSumvExpr nary_addv_subproof.
End Nary.

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

End SumExpr.

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

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

Lemma directvP {S : proper_addv_expr} : reflect (\dim S = S :> nat) (directv S).
Proof. exact: eqnP. Qed.

Lemma directv_trivial U : directv (unwrap (@trivial_addv U)).
Proof. exact: eqxx. Qed.

Lemma dimv_sum_leqif (S : addv_expr) :
  \dim (unwrap S) <= unwrap (addv_dim S) ?= iff directv (unwrap S).
Proof.
rewrite directvE; case: S => [[U] [d] /= defUd]; split=> //=.
rewrite /dimv; elim: {1}_ {U}_ d / defUd => // m1 m2 A1 A2 r1 r2 _ leA1 _ leA2.
by apply: leq_trans (leq_add leA1 leA2); rewrite mxrank_adds_leqif.
Qed.

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

Section BinaryDirect.

Lemma directv_addE (S1 S2 : addv_expr) :
  directv (unwrap S1 + unwrap S2)
    = [&& directv (unwrap S1), directv (unwrap S2)
        & unwrap S1 :&: unwrap S2 == 0]%VS.
Proof.
by rewrite /directv_def /dimv vs2mxD -mxdirectE mxdirect_addsE -vs2mxI -vs2mx0.
Qed.

Lemma directv_addP {U V} : reflect (U :&: V = 0)%VS (directv (U + V)).
Proof. by rewrite directv_addE !directv_trivial; apply: eqP. Qed.

Lemma directv_add_unique {U V} :
   reflect (forall u1 u2 v1 v2, u1 \in U -> u2 \in U -> v1 \in V -> v2 \in V ->
             (u1 + v1 == u2 + v2) = ((u1, v1) == (u2, v2)))
           (directv (U + V)).
Proof.
apply: (iffP directv_addP) => [dxUV u1 u2 v1 v2 Uu1 Uu2 Vv1 Vv2 | dxUV].
  apply/idP/idP=> [| /eqP[-> ->] //]; rewrite -subr_eq0 opprD addrACA addr_eq0.
  move/eqP=> eq_uv; rewrite xpair_eqE -subr_eq0 eq_uv oppr_eq0 subr_eq0 andbb.
  by rewrite -subr_eq0 -memv0 -dxUV memv_cap -memvN -eq_uv !memvB.
apply/eqP; rewrite -subv0; apply/subvP=> v /memv_capP[U1v U2v].
by rewrite memv0 -[v == 0]andbb {1}eq_sym -xpair_eqE -dxUV ?mem0v // addrC.
Qed.

End BinaryDirect.

Section NaryDirect.

Context {I : finType} {P : pred I}.

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.
rewrite directvE /= /dimv vs2mx_sum -mxdirectE; apply: (equivP mxdirect_sumsP).
by do [split=> dxU i /dxU; rewrite -vs2mx_sum -vs2mxI -vs2mx0] => [/val_inj|->].
Qed.

Lemma directv_sumE {Ss : I -> addv_expr} (xunwrap := unwrap) :
  reflect [/\ forall i, P i -> directv (unwrap (Ss i))
            & directv (\sum_(i | P i) xunwrap (Ss i))]
          (directv (\sum_(i | P i) unwrap (Ss i))).
Proof.
by rewrite !directvE /= /dimv 2!{1}vs2mx_sum -!mxdirectE; apply: mxdirect_sumsE.
Qed.

Lemma directv_sum_independent {Us : I -> {vspace vT}} :
   reflect (forall us,
               (forall i, P i -> us i \in Us i) -> \sum_(i | P i) us i = 0 ->
             (forall i, P i -> us i = 0))
           (directv (\sum_(i | P i) Us i)).
Proof.
apply: (iffP directv_sumP) => [dxU us Uu u_0 i Pi | dxU i Pi].
  apply/eqP; rewrite -memv0 -(dxU i Pi) memv_cap Uu //= -memvN -sub0r -{1}u_0.
  by rewrite (bigD1 i) //= addrC addKr memv_sumr // => j /andP[/Uu].
apply/eqP; rewrite -subv0; apply/subvP=> v.
rewrite memv_cap memv0 => /andP[Uiv /memv_sumP[us Uu Dv]].
have: \sum_(j | P j) [eta us with i |-> - v] j = 0.
  rewrite (bigD1 i) //= eqxx {1}Dv addrC -sumrB big1 // => j /andP[_ i'j].
  by rewrite (negPf i'j) subrr.
move/dxU/(_ i Pi); rewrite /= eqxx -oppr_eq0 => -> // j Pj.
by have [-> | i'j] := altP eqP; rewrite ?memvN // Uu ?Pj.
Qed.

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.
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.

End NaryDirect.

Lemma memv_span X v : v \in X -> v \in <<X>>%VS.
Proof.
by case/seq_tnthP=> i {v}->; rewrite unlock memvK genmxE (eq_row_sub i) // rowK.
Qed.

Lemma memv_span1 v : v \in <<[:: v]>>%VS.
Proof. by rewrite memv_span ?mem_head. Qed.

Lemma dim_span X : \dim <<X>> <= size X.
Proof. by rewrite unlock /dimv genmxE rank_leq_row. Qed.

Lemma span_subvP {X U} : reflect {subset X <= U} (<<X>> <= U)%VS.
Proof.
rewrite /subV [@span _ _]unlock genmxE.
apply: (iffP row_subP) => /= [sXU | sXU i].
  by move=> _ /seq_tnthP[i ->]; have:= sXU i; rewrite rowK memvK.
by rewrite rowK -memvK sXU ?mem_tnth.
Qed.

Lemma sub_span X Y : {subset X <= Y} -> (<<X>> <= <<Y>>)%VS.
Proof. by move=> sXY; apply/span_subvP=> v /sXY/memv_span. Qed.

Lemma eq_span X Y : X =i Y -> (<<X>> = <<Y>>)%VS.
Proof.
by move=> eqXY; apply: subv_anti; rewrite !sub_span // => u; rewrite eqXY.
Qed.

Lemma span_def X : span X = (\sum_(u <- X) <[u]>)%VS.
Proof.
apply/subv_anti/andP; split.
  by apply/span_subvP=> v Xv; rewrite (big_rem v) // memvE addvSl.
by rewrite big_tnth; apply/subv_sumP=> i _; rewrite -memvE memv_span ?mem_tnth.
Qed.

Lemma span_nil : (<<Nil vT>> = 0)%VS.
Proof. by rewrite span_def big_nil. Qed.

Lemma span_seq1 v : (<<[:: v]>> = <[v]>)%VS.
Proof. by rewrite span_def big_seq1. Qed.

Lemma span_cons v X : (<<v :: X>> = <[v]> + <<X>>)%VS.
Proof. by rewrite !span_def big_cons. Qed.

Lemma span_cat X Y : (<<X ++ Y>> = <<X>> + <<Y>>)%VS.
Proof. by rewrite !span_def big_cat. Qed.


Definition coord_expanded_def n (X : n.-tuple vT) i v :=
  (v2r v *m pinvmx (b2mx X)) 0 i.
Definition coord := locked_with span_key coord_expanded_def.
Canonical coord_unlockable := [unlockable fun coord].

Fact coord_is_scalar n (X : n.-tuple vT) i : scalar (coord X i).
Proof. by move=> k u v; rewrite unlock linearP mulmxDl -scalemxAl !mxE. Qed.
Canonical coord_addidive n Xn i := Additive (@coord_is_scalar n Xn i).
Canonical coord_linear n Xn i := AddLinear (@coord_is_scalar n Xn i).

Lemma coord_span n (X : n.-tuple vT) v :
  v \in span X -> v = \sum_i coord X i v *: X`_i.
Proof.
rewrite memvK span_b2mx genmxE => Xv.
by rewrite unlock_with mul_b2mx mulmxKpV ?v2rK.
Qed.

Lemma coord0 i v : coord [tuple 0] i v = 0.
Proof.
rewrite unlock /pinvmx rank_rV; case: negP => [[] | _].
  by apply/eqP/rowP=> j; rewrite !mxE (tnth_nth 0) /= linear0 mxE.
by rewrite pid_mx_0 !(mulmx0, mul0mx) mxE.
Qed.


Lemma nil_free : free (Nil vT).
Proof. by rewrite /free span_nil dimv0. Qed.

Lemma seq1_free v : free [:: v] = (v != 0).
Proof. by rewrite /free span_seq1 dim_vline; case: (~~ _). Qed.

Lemma perm_free X Y : perm_eq X Y -> free X = free Y.
Proof.
by move=> eqX; rewrite /free (perm_eq_size eqX) (eq_span (perm_eq_mem eqX)).
Qed.

Lemma free_directv X : free X = (0 \notin X) && directv (\sum_(v <- X) <[v]>).
Proof.
have leXi i (v := tnth (in_tuple X) i): true -> \dim <[v]> <= 1 ?= iff (v != 0).
  by rewrite -seq1_free -span_seq1 => _; apply/leqif_eq/dim_span.
have [_ /=] := leqif_trans (dimv_sum_leqif _) (leqif_sum leXi).
rewrite sum1_card card_ord !directvE /= /free andbC span_def !(big_tnth _ _ X).
by congr (_ = _ && _); rewrite -has_pred1 -all_predC -big_all big_tnth big_andE.
Qed.

Lemma free_not0 v X : free X -> v \in X -> v != 0.
Proof. by rewrite free_directv andbC => /andP[_ /memPn]; apply. Qed.

Lemma freeP n (X : n.-tuple vT) :
  reflect (forall k, \sum_(i < n) k i *: X`_i = 0 -> (forall i, k i = 0))
          (free X).
Proof.
rewrite free_b2mx; apply: (iffP idP) => [t_free k kt0 i | t_free].
  suffices /rowP/(_ i): \row_i k i = 0 by rewrite !mxE.
  by apply/(row_free_inj t_free)/r2v_inj; rewrite mul0mx -lin_b2mx kt0 linear0.
rewrite -kermx_eq0; apply/rowV0P=> rk /sub_kermxP kt0.
by apply/rowP=> i; rewrite mxE {}t_free // mul_b2mx kt0 linear0.
Qed.

Lemma coord_free n (X : n.-tuple vT) (i j : 'I_n) :
  free X -> coord X j (X`_i) = (i == j)%:R.
Proof.
rewrite unlock free_b2mx => /row_freeP[Ct CtK]; rewrite -row_b2mx.
by rewrite -row_mul -[pinvmx _]mulmx1 -CtK 2!mulmxA mulmxKpV // CtK !mxE.
Qed.

Lemma coord_sum_free n (X : n.-tuple vT) k j :
  free X -> coord X j (\sum_(i < n) k i *: X`_i) = k j.
Proof.
move=> Xfree; rewrite linear_sum (bigD1 j) ?linearZ //= coord_free // eqxx.
rewrite mulr1 big1 ?addr0 // => i /negPf j'i.
by rewrite linearZ /= coord_free // j'i mulr0.
Qed.

Lemma cat_free X Y :
  free (X ++ Y) = [&& free X, free Y & directv (<<X>> + <<Y>>)].
Proof.
rewrite !free_directv mem_cat directvE /= !big_cat -directvE directv_addE /=.
rewrite negb_or -!andbA; do !bool_congr; rewrite -!span_def.
by rewrite (sameP eqP directv_addP).
Qed.

Lemma catl_free Y X : free (X ++ Y) -> free X.
Proof. by rewrite cat_free => /and3P[]. Qed.

Lemma catr_free X Y : free (X ++ Y) -> free Y.
Proof. by rewrite cat_free => /and3P[]. Qed.

Lemma filter_free p X : free X -> free (filter p X).
Proof.
rewrite -(perm_free (etrans (perm_filterC p X _) (perm_eq_refl X))).
exact: catl_free.
Qed.

Lemma free_cons v X : free (v :: X) = (v \notin <<X>>)%VS && free X.
Proof.
rewrite (cat_free [:: v]) seq1_free directvEgeq /= span_seq1 dim_vline.
case: eqP => [-> | _] /=; first by rewrite mem0v.
rewrite andbC ltnNge (geq_leqif (dimv_leqif_sup _)) ?addvSr //.
by rewrite subv_add subvv andbT -memvE.
Qed.

Lemma freeE n (X : n.-tuple vT) :
  free X = [forall i : 'I_n, X`_i \notin <<drop i.+1 X>>%VS].
Proof.
case: X => X /= /eqP <-{n}; rewrite -(big_andE xpredT) /=.
elim: X => [|v X IH_X] /=; first by rewrite nil_free big_ord0.
by rewrite free_cons IH_X big_ord_recl drop0.
Qed.

Lemma freeNE n (X : n.-tuple vT) :
  ~~ free X = [exists i : 'I_n, X`_i \in <<drop i.+1 X>>%VS].
Proof. by rewrite freeE -negb_exists negbK. Qed.

Lemma free_uniq X : free X -> uniq X.
Proof.
elim: X => //= v b IH_X; rewrite free_cons => /andP[X'v /IH_X->].
by rewrite (contra _ X'v) // => /memv_span.
Qed.

Lemma free_span X v (sumX := fun k => \sum_(x <- X) k x *: x) :
    free X -> v \in <<X>>%VS ->
  {k | v = sumX k & forall k1, v = sumX k1 -> {in X, k1 =1 k}}.
Proof.
rewrite -{2}[X]in_tupleE => freeX /coord_span def_v.
pose k x := oapp (fun i => coord (in_tuple X) i v) 0 (insub (index x X)).
exists k => [|k1 {def_v}def_v _ /(nthP 0)[i ltiX <-]].
  rewrite /sumX (big_nth 0) big_mkord def_v; apply: eq_bigr => i _.
  by rewrite /k index_uniq ?free_uniq // valK.
rewrite /k /= index_uniq ?free_uniq // insubT //= def_v.
by rewrite /sumX (big_nth 0) big_mkord coord_sum_free.
Qed.

Lemma linear_of_free (rT : lmodType K) X (fX : seq rT) :
  {f : {linear vT -> rT} | free X -> size fX = size X -> map f X = fX}.
Proof.
pose f u := \sum_i coord (in_tuple X) i u *: fX`_i.
have lin_f: linear f.
  move=> k u v; rewrite scaler_sumr -big_split; apply: eq_bigr => i _.
  by rewrite /= scalerA -scalerDl linearP.
exists (Linear lin_f) => freeX eq_szX.
apply/esym/(@eq_from_nth _ 0); rewrite ?size_map eq_szX // => i ltiX.
rewrite (nth_map 0) //= /f (bigD1 (Ordinal ltiX)) //=.
rewrite big1 => [|j /negbTE neqji]; rewrite (coord_free (Ordinal _)) //.
  by rewrite eqxx scale1r addr0.
by rewrite eq_sym neqji scale0r.
Qed.


Lemma span_basis U X : basis_of U X -> <<X>>%VS = U.
Proof. by case/andP=> /eqP. Qed.

Lemma basis_free U X : basis_of U X -> free X.
Proof. by case/andP. Qed.

Lemma coord_basis U n (X : n.-tuple vT) v :
  basis_of U X -> v \in U -> v = \sum_i coord X i v *: X`_i.
Proof. by move/span_basis <-; apply: coord_span. Qed.

Lemma nil_basis : basis_of 0 (Nil vT).
Proof. by rewrite /basis_of span_nil eqxx nil_free. Qed.

Lemma seq1_basis v : v != 0 -> basis_of <[v]> [:: v].
Proof. by move=> nz_v; rewrite /basis_of span_seq1 // eqxx seq1_free. Qed.

Lemma basis_not0 x U X : basis_of U X -> x \in X -> x != 0.
Proof. by move/basis_free/free_not0; apply. Qed.

Lemma basis_mem x U X : basis_of U X -> x \in X -> x \in U.
Proof. by move/span_basis=> <- /memv_span. Qed.

Lemma cat_basis U V X Y :
  directv (U + V) -> basis_of U X -> basis_of V Y -> basis_of (U + V) (X ++ Y).
Proof.
move=> dxUV /andP[/eqP defU freeX] /andP[/eqP defV freeY].
by rewrite /basis_of span_cat cat_free defU defV // eqxx freeX freeY.
Qed.

Lemma size_basis U n (X : n.-tuple vT) : basis_of U X -> \dim U = n.
Proof. by case/andP=> /eqP <- /eqnP->; apply: size_tuple. Qed.

Lemma basisEdim X U : basis_of U X = (U <= <<X>>)%VS && (size X <= \dim U).
Proof.
apply/andP/idP=> [[defU /eqnP <-]| ]; first by rewrite -eqEdim eq_sym.
case/andP=> sUX leXU; have leXX := dim_span X.
rewrite /free eq_sym eqEdim sUX eqn_leq !(leq_trans leXX) //.
by rewrite (leq_trans leXU) ?dimvS.
Qed.

Lemma basisEfree X U :
  basis_of U X = [&& free X, (<<X>> <= U)%VS & \dim U <= size X].
Proof.
by rewrite andbC; apply: andb_id2r => freeX; rewrite eqEdim (eqnP freeX).
Qed.

Lemma perm_basis X Y U : perm_eq X Y -> basis_of U X = basis_of U Y.
Proof.
move=> eqXY; congr ((_ == _) && _); last exact: perm_free.
by apply/eq_span; apply: perm_eq_mem.
Qed.

Lemma vbasisP U : basis_of U (vbasis U).
Proof.
rewrite /basis_of free_b2mx span_b2mx (sameP eqP (vs2mxP _ _)) !genmxE.
have ->: b2mx (vbasis U) = row_base (vs2mx U).
  by apply/row_matrixP=> i; rewrite unlock rowK tnth_mktuple r2vK.
by rewrite row_base_free !eq_row_base submx_refl.
Qed.

Lemma vbasis_mem v U : v \in (vbasis U) -> v \in U.
Proof. exact: (basis_mem (vbasisP _)). Qed.

Lemma coord_vbasis v U :
  v \in U -> v = \sum_(i < \dim U) coord (vbasis U) i v *: (vbasis U)`_i.
Proof. exact: coord_basis (vbasisP U). Qed.

Section BigSumBasis.

Variables (I : finType) (P : pred I) (Xs : I -> seq vT).

Lemma span_bigcat :
  (<<\big[cat/[::]]_(i | P i) Xs i>> = \sum_(i | P i) <<Xs i>>)%VS.
Proof. by rewrite (big_morph _ span_cat span_nil). Qed.

Lemma bigcat_free :
    directv (\sum_(i | P i) <<Xs i>>) ->
  (forall i, P i -> free (Xs i)) -> free (\big[cat/[::]]_(i | P i) Xs i).
Proof.
rewrite /free directvE /= span_bigcat => /directvP-> /= freeXs.
rewrite (big_morph _ (@size_cat _) (erefl _)) /=.
by apply/eqP/eq_bigr=> i /freeXs/eqP.
Qed.

Lemma bigcat_basis Us (U := (\sum_(i | P i) Us i)%VS) :
    directv U -> (forall i, P i -> basis_of (Us i) (Xs i)) ->
  basis_of U (\big[cat/[::]]_(i | P i) Xs i).
Proof.
move=> dxU XsUs; rewrite /basis_of span_bigcat.
have defUs i: P i -> span (Xs i) = Us i by case/XsUs/andP=> /eqP.
rewrite (eq_bigr _ defUs) eqxx bigcat_free // => [|_ /XsUs/andP[]//].
apply/directvP; rewrite /= (eq_bigr _ defUs) (directvP dxU) /=.
by apply/eq_bigr=> i /defUs->.
Qed.

End BigSumBasis.

End VectorTheory.

Hint Resolve subvv.
Arguments subvP [K vT U V].
Arguments addv_idPl [K vT U V].
Arguments addv_idPr [K vT U V].
Arguments memv_addP [K vT w U V ].
Arguments sumv_sup [K vT I] i0 [P U Vs].
Arguments memv_sumP [K vT I P Us v].
Arguments subv_sumP [K vT I P Us V].
Arguments capv_idPl [K vT U V].
Arguments capv_idPr [K vT U V].
Arguments memv_capP [K vT w U V].
Arguments bigcapv_inf [K vT I] i0 [P Us V].
Arguments subv_bigcapP [K vT I P U Vs].
Arguments directvP [K vT S].
Arguments directv_addP [K vT U V].
Arguments directv_add_unique [K vT U V].
Arguments directv_sumP [K vT I P Us].
Arguments directv_sumE [K vT I P Ss].
Arguments directv_sum_independent [K vT I P Us].
Arguments directv_sum_unique [K vT I P Us].
Arguments span_subvP [K vT X U].
Arguments freeP [K vT n X].

Prenex Implicits coord.
Notation directv S := (directv_def (Phantom _ S%VS)).

Section LfunDefs.

Variable R : ringType.
Implicit Types aT vT rT : vectType R.

Fact lfun_key : unit. Proof. by []. Qed.
Definition fun_of_lfun_def aT rT (f : 'Hom(aT, rT)) :=
  r2v \o mulmxr (f2mx f) \o v2r.
Definition fun_of_lfun := locked_with lfun_key fun_of_lfun_def.
Canonical fun_of_lfun_unlockable := [unlockable fun fun_of_lfun].
Definition linfun_def aT rT (f : aT -> rT) :=
  Vector.Hom (lin1_mx (v2r \o f \o r2v)).
Definition linfun := locked_with lfun_key linfun_def.
Canonical linfun_unlockable := [unlockable fun linfun].

Definition id_lfun vT := @linfun vT vT idfun.
Definition comp_lfun aT vT rT (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) :=
  linfun (fun_of_lfun f \o fun_of_lfun g).

End LfunDefs.

Coercion fun_of_lfun : Vector.hom >-> Funclass.
Notation "\1" := (@id_lfun _ _) : lfun_scope.
Notation "f \o g" := (comp_lfun f g) : lfun_scope.

Section LfunVspaceDefs.

Variable K : fieldType.
Implicit Types aT rT : vectType K.

Definition inv_lfun aT rT (f : 'Hom(aT, rT)) := Vector.Hom (pinvmx (f2mx f)).
Definition lker aT rT (f : 'Hom(aT, rT)) := mx2vs (kermx (f2mx f)).
Fact lfun_img_key : unit. Proof. by []. Qed.
Definition lfun_img_def aT rT f (U : {vspace aT}) : {vspace rT} :=
  mx2vs (vs2mx U *m f2mx f).
Definition lfun_img := locked_with lfun_img_key lfun_img_def.
Canonical lfun_img_unlockable := [unlockable fun lfun_img].
Definition lfun_preim aT rT (f : 'Hom(aT, rT)) W :=
  (lfun_img (inv_lfun f) (W :&: lfun_img f fullv) + lker f)%VS.

End LfunVspaceDefs.

Prenex Implicits linfun lfun_img lker lfun_preim.
Notation "f ^-1" := (inv_lfun f) : lfun_scope.
Notation "f @: U" := (lfun_img f%VF%R U) (at level 24) : vspace_scope.
Notation "f @^-1: W" := (lfun_preim f%VF%R W) (at level 24) : vspace_scope.
Notation limg f := (lfun_img f fullv).

Section LfunZmodType.

Variables (R : ringType) (aT rT : vectType R).
Implicit Types f g h : 'Hom(aT, rT).

Canonical lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:].
Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin.
Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:].
Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin.

Fact lfun_is_linear f : linear f.
Proof. by rewrite unlock; apply: linearP. Qed.
Canonical lfun_additive f := Additive (lfun_is_linear f).
Canonical lfun_linear f := AddLinear (lfun_is_linear f).

Lemma lfunE (ff : {linear aT -> rT}) : linfun ff =1 ff.
Proof. by move=> v; rewrite 2!unlock /= mul_rV_lin1 /= !v2rK. Qed.

Lemma fun_of_lfunK : cancel (@fun_of_lfun R aT rT) linfun.
Proof.
move=> f; apply/val_inj/row_matrixP=> i.
by rewrite 2!unlock /= !rowE mul_rV_lin1 /= !r2vK.
Qed.

Lemma lfunP f g : f =1 g <-> f = g.
Proof.
split=> [eq_fg | -> //]; rewrite -[f]fun_of_lfunK -[g]fun_of_lfunK unlock.
by apply/val_inj/row_matrixP=> i; rewrite !rowE !mul_rV_lin1 /= eq_fg.
Qed.

Definition zero_lfun : 'Hom(aT, rT) := linfun \0.
Definition add_lfun f g := linfun (f \+ g).
Definition opp_lfun f := linfun (-%R \o f).

Fact lfun_addA : associative add_lfun.
Proof. by move=> f g h; apply/lfunP=> v; rewrite !lfunE /= !lfunE addrA. Qed.

Fact lfun_addC : commutative add_lfun.
Proof. by move=> f g; apply/lfunP=> v; rewrite !lfunE /= addrC. Qed.

Fact lfun_add0 : left_id zero_lfun add_lfun.
Proof. by move=> f; apply/lfunP=> v; rewrite lfunE /= lfunE add0r. Qed.

Lemma lfun_addN : left_inverse zero_lfun opp_lfun add_lfun.
Proof. by move=> f; apply/lfunP=> v; rewrite !lfunE /= lfunE addNr. Qed.

Definition lfun_zmodMixin := ZmodMixin lfun_addA lfun_addC lfun_add0 lfun_addN.
Canonical lfun_zmodType := Eval hnf in ZmodType 'Hom(aT, rT) lfun_zmodMixin.

Lemma zero_lfunE x : (0 : 'Hom(aT, rT)) x = 0. Proof. exact: lfunE. Qed.
Lemma add_lfunE f g x : (f + g) x = f x + g x. Proof. exact: lfunE. Qed.
Lemma opp_lfunE f x : (- f) x = - f x. Proof. exact: lfunE. Qed.
Lemma sum_lfunE I (r : seq I) (P : pred I) (fs : I -> 'Hom(aT, rT)) x :
  (\sum_(i <- r | P i) fs i) x = \sum_(i <- r | P i) fs i x.
Proof. by elim/big_rec2: _ => [|i _ f _ <-]; rewrite lfunE. Qed.

End LfunZmodType.

Section LfunVectType.

Variables (R : comRingType) (aT rT : vectType R).
Implicit Types f : 'Hom(aT, rT).

Definition scale_lfun k f := linfun (k \*: f).
Local Infix "*:l" := scale_lfun (at level 40).

Fact lfun_scaleA k1 k2 f : k1 *:l (k2 *:l f) = (k1 * k2) *:l f.
Proof. by apply/lfunP=> v; rewrite !lfunE /= lfunE scalerA. Qed.

Fact lfun_scale1 f : 1 *:l f = f.
Proof. by apply/lfunP=> v; rewrite lfunE /= scale1r. Qed.

Fact lfun_scaleDr k f1 f2 : k *:l (f1 + f2) = k *:l f1 + k *:l f2.
Proof. by apply/lfunP=> v; rewrite !lfunE /= !lfunE scalerDr. Qed.

Fact lfun_scaleDl f k1 k2 : (k1 + k2) *:l f = k1 *:l f + k2 *:l f.
Proof. by apply/lfunP=> v; rewrite !lfunE /= !lfunE scalerDl. Qed.

Definition lfun_lmodMixin :=
  LmodMixin lfun_scaleA lfun_scale1 lfun_scaleDr lfun_scaleDl.
Canonical lfun_lmodType := Eval hnf in LmodType R 'Hom(aT, rT) lfun_lmodMixin.

Lemma scale_lfunE k f x : (k *: f) x = k *: f x. Proof. exact: lfunE. Qed.

Fact lfun_vect_iso : Vector.axiom (Vector.dim aT * Vector.dim rT) 'Hom(aT, rT).
Proof.
exists (mxvec \o f2mx) => [a f g|].
  rewrite /= -linearP /= -[A in _ = mxvec A]/(f2mx (Vector.Hom _)).
  congr (mxvec (f2mx _)); apply/lfunP=> v; do 2!rewrite lfunE /=.
  by rewrite unlock /= -linearP mulmxDr scalemxAr.
apply: Bijective (Vector.Hom \o vec_mx) _ _ => [[A]|A] /=; last exact: vec_mxK.
by rewrite mxvecK.
Qed.

Definition lfun_vectMixin := VectMixin lfun_vect_iso.
Canonical lfun_vectType := VectType R 'Hom(aT, rT) lfun_vectMixin.

End LfunVectType.

Section CompLfun.

Variables (R : ringType) (wT aT vT rT : vectType R).
Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)) (h : 'Hom(wT, aT)).

Lemma id_lfunE u: \1%VF u = u :> aT. Proof. exact: lfunE. Qed.
Lemma comp_lfunE f g u : (f \o g)%VF u = f (g u). Proof. exact: lfunE. Qed.

Lemma comp_lfunA f g h : (f \o (g \o h) = (f \o g) \o h)%VF.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=. Qed.

Lemma comp_lfun1l f : (\1 \o f)%VF = f.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=. Qed.

Lemma comp_lfun1r f : (f \o \1)%VF = f.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=. Qed.

Lemma comp_lfun0l g : (0 \o g)%VF = 0 :> 'Hom(aT, rT).
Proof. by apply/lfunP=> u; do !rewrite lfunE /=. Qed.

Lemma comp_lfun0r f : (f \o 0)%VF = 0 :> 'Hom(aT, rT).
Proof. by apply/lfunP=> u; do !rewrite lfunE /=; rewrite linear0. Qed.

Lemma comp_lfunDl f1 f2 g : ((f1 + f2) \o g = (f1 \o g) + (f2 \o g))%VF.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=. Qed.

Lemma comp_lfunDr f g1 g2 : (f \o (g1 + g2) = (f \o g1) + (f \o g2))%VF.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=; rewrite linearD. Qed.

Lemma comp_lfunNl f g : ((- f) \o g = - (f \o g))%VF.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=. Qed.

Lemma comp_lfunNr f g : (f \o (- g) = - (f \o g))%VF.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=; rewrite linearN. Qed.

End CompLfun.

Definition lfun_simp :=
  (comp_lfunE, scale_lfunE, opp_lfunE, add_lfunE, sum_lfunE, lfunE).

Section ScaleCompLfun.

Variables (R : comRingType) (aT vT rT : vectType R).
Implicit Types (f : 'Hom(vT, rT)) (g : 'Hom(aT, vT)).

Lemma comp_lfunZl k f g : (k *: (f \o g) = (k *: f) \o g)%VF.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=. Qed.

Lemma comp_lfunZr k f g : (k *: (f \o g) = f \o (k *: g))%VF.
Proof. by apply/lfunP=> u; do !rewrite lfunE /=; rewrite linearZ. Qed.

End ScaleCompLfun.

Section LinearImage.

Variables (K : fieldType) (aT rT : vectType K).
Implicit Types (f g : 'Hom(aT, rT)) (U V : {vspace aT}) (W : {vspace rT}).

Lemma limgS f U V : (U <= V)%VS -> (f @: U <= f @: V)%VS.
Proof. by rewrite unlock /subsetv !genmxE; apply: submxMr. Qed.

Lemma limg_line f v : (f @: <[v]> = <[f v]>)%VS.
Proof.
apply/eqP; rewrite 2!unlock eqEsubv /subsetv /= r2vK !genmxE.
by rewrite !(eqmxMr _ (genmxE _)) submx_refl.
Qed.

Lemma limg0 f : (f @: 0 = 0)%VS. Proof. by rewrite limg_line linear0. Qed.

Lemma memv_img f v U : v \in U -> f v \in (f @: U)%VS.
Proof. by move=> Uv; rewrite memvE -limg_line limgS. Qed.

Lemma memv_imgP f w U :
  reflect (exists2 u, u \in U & w = f u) (w \in f @: U)%VS.
Proof.
apply: (iffP idP) => [|[u Uu ->]]; last exact: memv_img.
rewrite 2!unlock memvE /subsetv !genmxE => /submxP[ku Drw].
exists (r2v (ku *m vs2mx U)); last by rewrite /= r2vK -mulmxA -Drw v2rK.
by rewrite memvE /subsetv !genmxE r2vK submxMl.
Qed.

Lemma lim0g U : (0 @: U = 0 :> {vspace rT})%VS.
Proof.
apply/eqP; rewrite -subv0; apply/subvP=> _ /memv_imgP[u _ ->].
by rewrite lfunE rpred0.
Qed.

Lemma eq_in_limg V f g : {in V, f =1 g} -> (f @: V = g @: V)%VS.
Proof.
move=> eq_fg; apply/vspaceP=> y.
by apply/memv_imgP/memv_imgP=> [][x Vx ->]; exists x; rewrite ?eq_fg.
Qed.

Lemma limg_add f : {morph lfun_img f : U V / U + V}%VS.
Proof.
move=> U V; apply/eqP; rewrite unlock eqEsubv /subsetv /= -genmx_adds.
by rewrite !genmxE !(eqmxMr _ (genmxE _)) !addsmxMr submx_refl.
Qed.

Lemma limg_sum f I r (P : pred I) Us :
  (f @: (\sum_(i <- r | P i) Us i) = \sum_(i <- r | P i) f @: Us i)%VS.
Proof. exact: (big_morph _ (limg_add f) (limg0 f)). Qed.

Lemma limg_cap f U V : (f @: (U :&: V) <= f @: U :&: f @: V)%VS.
Proof. by rewrite subv_cap !limgS ?capvSl ?capvSr. Qed.

Lemma limg_bigcap f I r (P : pred I) Us :
  (f @: (\bigcap_(i <- r | P i) Us i) <= \bigcap_(i <- r | P i) f @: Us i)%VS.
Proof.
elim/big_rec2: _ => [|i V U _ sUV]; first exact: subvf.
by rewrite (subv_trans (limg_cap f _ U)) ?capvS.
Qed.

Lemma limg_span f X : (f @: <<X>> = <<map f X>>)%VS.
Proof.
by rewrite !span_def big_map limg_sum; apply: eq_bigr => x _; rewrite limg_line.
Qed.

Lemma lfunPn f g : reflect (exists u, f u != g u) (f != g).
Proof.
apply: (iffP idP) => [f'g|[x]]; last by apply: contraNneq => /lfunP->.
suffices /subvPn[_ /memv_imgP[u _ ->]]: ~~ (limg (f - g) <= 0)%VS.
  by rewrite lfunE /= lfunE /= memv0 subr_eq0; exists u.
apply: contra f'g => /subvP fg0; apply/eqP/lfunP=> u; apply/eqP.
by rewrite -subr_eq0 -opp_lfunE -add_lfunE -memv0 fg0 ?memv_img ?memvf.
Qed.

Lemma inv_lfun_def f : (f \o f^-1 \o f)%VF = f.
Proof.
apply/lfunP=> u; do !rewrite lfunE /=; rewrite unlock /= !r2vK.
by rewrite mulmxKpV ?submxMl.
Qed.

Lemma limg_lfunVK f : {in limg f, cancel f^-1%VF f}.
Proof. by move=> _ /memv_imgP[u _ ->]; rewrite -!comp_lfunE inv_lfun_def. Qed.

Lemma lkerE f U : (U <= lker f)%VS = (f @: U == 0)%VS.
Proof.
rewrite unlock -dimv_eq0 /dimv /subsetv !genmxE mxrank_eq0.
by rewrite (sameP sub_kermxP eqP).
Qed.

Lemma memv_ker f v : (v \in lker f) = (f v == 0).
Proof. by rewrite -memv0 !memvE subv0 lkerE limg_line. Qed.

Lemma eqlfunP f g v : reflect (f v = g v) (v \in lker (f - g)).
Proof. by rewrite memv_ker !lfun_simp subr_eq0; apply: eqP. Qed.

Lemma eqlfun_inP V f g : reflect {in V, f =1 g} (V <= lker (f - g))%VS.
Proof. by apply: (iffP subvP) => E x /E/eqlfunP. Qed.

Lemma limg_ker_compl f U : (f @: (U :\: lker f) = f @: U)%VS.
Proof.
rewrite -{2}(addv_diff_cap U (lker f)) limg_add; apply/esym/addv_idPl.
by rewrite (subv_trans _ (sub0v _)) // subv0 -lkerE capvSr.
Qed.

Lemma limg_ker_dim f U : (\dim (U :&: lker f) + \dim (f @: U) = \dim U)%N.
Proof.
rewrite unlock /dimv /= genmx_cap genmx_id -genmx_cap !genmxE.
by rewrite addnC mxrank_mul_ker.
Qed.

Lemma limg_dim_eq f U : (U :&: lker f = 0)%VS -> \dim (f @: U) = \dim U.
Proof. by rewrite -(limg_ker_dim f U) => ->; rewrite dimv0. Qed.

Lemma limg_basis_of f U X :
  (U :&: lker f = 0)%VS -> basis_of U X -> basis_of (f @: U) (map f X).
Proof.
move=> injUf /andP[/eqP defU /eqnP freeX].
by rewrite /basis_of /free size_map -limg_span -freeX defU limg_dim_eq ?eqxx.
Qed.

Lemma lker0P f : reflect (injective f) (lker f == 0%VS).
Proof.
rewrite -subv0; apply: (iffP subvP) => [injf u v eq_fuv | injf u].
  apply/eqP; rewrite -subr_eq0 -memv0 injf //.
  by rewrite memv_ker linearB /= eq_fuv subrr.
by rewrite memv_ker memv0 -(inj_eq injf) linear0.
Qed.

Lemma limg_ker0 f U V : lker f == 0%VS -> (f @: U <= f @: V)%VS = (U <= V)%VS.
Proof.
move/lker0P=> injf; apply/idP/idP=> [/subvP sfUV | ]; last exact: limgS.
by apply/subvP=> u Uu; have /memv_imgP[v Vv /injf->] := sfUV _ (memv_img f Uu).
Qed.

Lemma eq_limg_ker0 f U V : lker f == 0%VS -> (f @: U == f @: V)%VS = (U == V).
Proof. by move=> injf; rewrite !eqEsubv !limg_ker0. Qed.

Lemma lker0_lfunK f : lker f == 0%VS -> cancel f f^-1%VF.
Proof.
by move/lker0P=> injf u; apply: injf; rewrite limg_lfunVK ?memv_img ?memvf.
Qed.

Lemma lker0_compVf f : lker f == 0%VS -> (f^-1 \o f = \1)%VF.
Proof. by move/lker0_lfunK=> fK; apply/lfunP=> u; rewrite !lfunE /= fK. Qed.

End LinearImage.

Arguments memv_imgP [K aT rT f w U].
Arguments lfunPn [K aT rT f g].
Arguments lker0P [K aT rT f].
Arguments eqlfunP [K aT rT f g v].
Arguments eqlfun_inP [K aT rT V f g].

Section FixedSpace.

Variables (K : fieldType) (vT : vectType K).
Implicit Types (f : 'End(vT)) (U : {vspace vT}).

Definition fixedSpace f : {vspace vT} := lker (f - \1%VF).

Lemma fixedSpaceP f a : reflect (f a = a) (a \in fixedSpace f).
Proof.
by rewrite memv_ker add_lfunE opp_lfunE id_lfunE subr_eq0; apply: eqP.
Qed.

Lemma fixedSpacesP f U : reflect {in U, f =1 id} (U <= fixedSpace f)%VS.
Proof. by apply: (iffP subvP) => cUf x /cUf/fixedSpaceP. Qed.

Lemma fixedSpace_limg f U : (U <= fixedSpace f -> f @: U = U)%VS.
Proof.
move/fixedSpacesP=> cUf; apply/vspaceP=> x.
by apply/memv_imgP/idP=> [[{x} x Ux ->] | Ux]; last exists x; rewrite ?cUf.
Qed.

Lemma fixedSpace_id : fixedSpace \1 = {:vT}%VS.
Proof.
by apply/vspaceP=> x; rewrite memvf; apply/fixedSpaceP; rewrite lfunE.
Qed.

End FixedSpace.

Arguments fixedSpaceP [K vT f a].
Arguments fixedSpacesP [K vT f U].

Section LinAut.

Variables (K : fieldType) (vT : vectType K) (f : 'End(vT)).
Hypothesis kerf0 : lker f == 0%VS.

Lemma lker0_limgf : limg f = fullv.
Proof.
by apply/eqP; rewrite eqEdim subvf limg_dim_eq //= (eqP kerf0) capv0.
Qed.

Lemma lker0_lfunVK : cancel f^-1%VF f.
Proof. by move=> u; rewrite limg_lfunVK // lker0_limgf memvf. Qed.

Lemma lker0_compfV : (f \o f^-1 = \1)%VF.
Proof. by apply/lfunP=> u; rewrite !lfunE /= lker0_lfunVK. Qed.

Lemma lker0_compVKf aT g : (f \o (f^-1 \o g))%VF = g :> 'Hom(aT, vT).
Proof. by rewrite comp_lfunA lker0_compfV comp_lfun1l. Qed.

Lemma lker0_compKf aT g : (f^-1 \o (f \o g))%VF = g :> 'Hom(aT, vT).
Proof. by rewrite comp_lfunA lker0_compVf ?comp_lfun1l. Qed.

Lemma lker0_compfK rT h : ((h \o f) \o f^-1)%VF = h :> 'Hom(vT, rT).
Proof. by rewrite -comp_lfunA lker0_compfV comp_lfun1r. Qed.

Lemma lker0_compfVK rT h : ((h \o f^-1) \o f)%VF = h :> 'Hom(vT, rT).
Proof. by rewrite -comp_lfunA lker0_compVf ?comp_lfun1r. Qed.

End LinAut.

Section LinearImageComp.

Variables (K : fieldType) (aT vT rT : vectType K).
Implicit Types (f : 'Hom(aT, vT)) (g : 'Hom(vT, rT)) (U : {vspace aT}).

Lemma lim1g U : (\1 @: U)%VS = U.
Proof.
have /andP[/eqP <- _] := vbasisP U; rewrite limg_span map_id_in // => u _.
by rewrite lfunE.
Qed.

Lemma limg_comp f g U : ((g \o f) @: U = g @: (f @: U))%VS.
Proof.
have /andP[/eqP <- _] := vbasisP U; rewrite !limg_span; congr (span _).
by rewrite -map_comp; apply/eq_map => u; rewrite lfunE.
Qed.

End LinearImageComp.

Section LinearPreimage.

Variables (K : fieldType) (aT rT : vectType K).
Implicit Types (f : 'Hom(aT, rT)) (U : {vspace aT}) (V W : {vspace rT}).

Lemma lpreim_cap_limg f W : (f @^-1: (W :&: limg f))%VS = (f @^-1: W)%VS.
Proof. by rewrite /lfun_preim -capvA capvv. Qed.

Lemma lpreim0 f : (f @^-1: 0)%VS = lker f.
Proof. by rewrite /lfun_preim cap0v limg0 add0v. Qed.

Lemma lpreimS f V W : (V <= W)%VS-> (f @^-1: V <= f @^-1: W)%VS.
Proof. by move=> sVW; rewrite addvS // limgS // capvS. Qed.

Lemma lpreimK f W : (W <= limg f)%VS -> (f @: (f @^-1: W))%VS = W.
Proof.
move=> sWf; rewrite limg_add (capv_idPl sWf) // -limg_comp.
have /eqP->: (f @: lker f == 0)%VS by rewrite -lkerE.
have /andP[/eqP defW _] := vbasisP W; rewrite addv0 -defW limg_span.
rewrite map_id_in // => x Xx; rewrite lfunE /= limg_lfunVK //.
by apply: span_subvP Xx; rewrite defW.
Qed.

Lemma memv_preim f u W : (f u \in W) = (u \in f @^-1: W)%VS.
Proof.
apply/idP/idP=> [Wfu | /(memv_img f)]; last first.
  by rewrite -lpreim_cap_limg lpreimK ?capvSr // => /memv_capP[].
rewrite -[u](addNKr (f^-1%VF (f u))) memv_add ?memv_img //.
  by rewrite memv_cap Wfu memv_img ?memvf.
by rewrite memv_ker addrC linearB /= subr_eq0 limg_lfunVK ?memv_img ?memvf.
Qed.

End LinearPreimage.

Section LfunAlgebra.

Variables (R : comRingType) (vT : vectType R).
Hypothesis vT_proper : Vector.dim vT > 0.

Fact lfun1_neq0 : \1%VF != 0 :> 'End(vT).
Proof.
apply/eqP=> /lfunP/(_ (r2v (const_mx 1))); rewrite !lfunE /= => /(canRL r2vK).
by move=> /rowP/(_ (Ordinal vT_proper))/eqP; rewrite linear0 !mxE oner_eq0.
Qed.

Prenex Implicits comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr.

Definition lfun_comp_ringMixin :=
  RingMixin comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr
            lfun1_neq0.
Definition lfun_comp_ringType := RingType 'End(vT) lfun_comp_ringMixin.

Definition lfun_ringMixin : GRing.Ring.mixin_of (lfun_zmodType vT vT) :=
  GRing.converse_ringMixin lfun_comp_ringType.
Definition lfun_ringType := Eval hnf in RingType 'End(vT) lfun_ringMixin.
Definition lfun_lalgType := Eval hnf in [lalgType R of 'End(vT)
  for LalgType R lfun_ringType (fun k x y => comp_lfunZr k y x)].
Definition lfun_algType := Eval hnf in [algType R of 'End(vT)
  for AlgType R _ (fun k (x y : lfun_lalgType) => comp_lfunZl k y x)].

End LfunAlgebra.

Section Projection.

Variables (K : fieldType) (vT : vectType K).
Implicit Types U V : {vspace vT}.

Definition daddv_pi U V := Vector.Hom (proj_mx (vs2mx U) (vs2mx V)).
Definition projv U := daddv_pi U U^C.
Definition addv_pi1 U V := daddv_pi (U :\: V) V.
Definition addv_pi2 U V := daddv_pi V (U :\: V).

Lemma memv_pi U V w : (daddv_pi U V) w \in U.
Proof. by rewrite unlock memvE /subsetv genmxE /= r2vK proj_mx_sub. Qed.

Lemma memv_proj U w : projv U w \in U. Proof. exact: memv_pi. Qed.

Lemma memv_pi1 U V w : (addv_pi1 U V) w \in U.
Proof. by rewrite (subvP (diffvSl U V)) ?memv_pi. Qed.

Lemma memv_pi2 U V w : (addv_pi2 U V) w \in V. Proof. exact: memv_pi. Qed.

Lemma daddv_pi_id U V u : (U :&: V = 0)%VS -> u \in U -> daddv_pi U V u = u.
Proof.
move/eqP; rewrite -dimv_eq0 memvE /subsetv /dimv !genmxE mxrank_eq0 => /eqP.
by move=> dxUV Uu; rewrite unlock /= proj_mx_id ?v2rK.
Qed.

Lemma daddv_pi_proj U V w (pi := daddv_pi U V) :
  (U :&: V = 0)%VS -> pi (pi w) = pi w.
Proof. by move/daddv_pi_id=> -> //; apply: memv_pi. Qed.

Lemma daddv_pi_add U V w :
  (U :&: V = 0)%VS -> (w \in U + V)%VS -> daddv_pi U V w + daddv_pi V U w = w.
Proof.
move/eqP; rewrite -dimv_eq0 memvE /subsetv /dimv !genmxE mxrank_eq0 => /eqP.
by move=> dxUW UVw; rewrite unlock /= -linearD /= add_proj_mx ?v2rK.
Qed.

Lemma projv_id U u : u \in U -> projv U u = u.
Proof. exact: daddv_pi_id (capv_compl _). Qed.

Lemma projv_proj U w : projv U (projv U w) = projv U w.
Proof. exact: daddv_pi_proj (capv_compl _). Qed.

Lemma memv_projC U w : w - projv U w \in (U^C)%VS.
Proof.
rewrite -{1}[w](daddv_pi_add (capv_compl U)) ?addv_complf ?memvf //.
by rewrite addrC addKr memv_pi.
Qed.

Lemma limg_proj U : limg (projv U) = U.
Proof.
apply/vspaceP=> u; apply/memv_imgP/idP=> [[u1 _ ->] | ]; first exact: memv_proj.
by exists (projv U u); rewrite ?projv_id ?memv_img ?memvf.
Qed.

Lemma lker_proj U : lker (projv U) = (U^C)%VS.
Proof.
apply/eqP; rewrite eqEdim andbC; apply/andP; split.
  by rewrite dimv_compl -(limg_ker_dim (projv U) fullv) limg_proj addnK capfv.
by apply/subvP=> v; rewrite memv_ker -{2}[v]subr0 => /eqP <-; apply: memv_projC.
Qed.

Lemma addv_pi1_proj U V w (pi1 := addv_pi1 U V) : pi1 (pi1 w) = pi1 w.
Proof. by rewrite daddv_pi_proj // capv_diff. Qed.

Lemma addv_pi2_id U V v : v \in V -> addv_pi2 U V v = v.
Proof. by apply: daddv_pi_id; rewrite capvC capv_diff. Qed.

Lemma addv_pi2_proj U V w (pi2 := addv_pi2 U V) : pi2 (pi2 w) = pi2 w.
Proof. by rewrite addv_pi2_id ?memv_pi2. Qed.

Lemma addv_pi1_pi2 U V w :
  w \in (U + V)%VS -> addv_pi1 U V w + addv_pi2 U V w = w.
Proof. by rewrite -addv_diff; apply: daddv_pi_add; apply: capv_diff. Qed.

Section Sumv_Pi.

Variables (I : eqType) (r0 : seq I) (P : pred I) (Vs : I -> {vspace vT}).

Let sumv_pi_rec i :=
  fix loop r := if r is j :: r1 then
    let V1 := (\sum_(k <- r1) Vs k)%VS in
    if j == i then addv_pi1 (Vs j) V1 else (loop r1 \o addv_pi2 (Vs j) V1)%VF
  else 0.

Notation sumV := (\sum_(i <- r0 | P i) Vs i)%VS.
Definition sumv_pi_for V of V = sumV := fun i => sumv_pi_rec i (filter P r0).

Variables (V : {vspace vT}) (defV : V = sumV).

Lemma memv_sum_pi i v : sumv_pi_for defV i v \in Vs i.
Proof.
rewrite /sumv_pi_for.
elim: (filter P r0) v => [|j r IHr] v /=; first by rewrite lfunE mem0v.
by case: eqP => [->|_]; rewrite ?lfunE ?memv_pi1 /=.
Qed.

Lemma sumv_pi_uniq_sum v :
    uniq (filter P r0) -> v \in V ->
  \sum_(i <- r0 | P i) sumv_pi_for defV i v = v.
Proof.
rewrite /sumv_pi_for defV -!(big_filter r0 P).
elim: (filter P r0) v => [|i r IHr] v /= => [_ | /andP[r'i /IHr{IHr}IHr]].
  by rewrite !big_nil memv0 => /eqP.
rewrite !big_cons eqxx => /addv_pi1_pi2; congr (_ + _ = v).
rewrite -[_ v]IHr ?memv_pi2 //; apply: eq_big_seq => j /=.
by case: eqP => [<- /idPn | _]; rewrite ?lfunE.
Qed.

End Sumv_Pi.

End Projection.

Prenex Implicits daddv_pi projv addv_pi1 addv_pi2.
Notation sumv_pi V := (sumv_pi_for (erefl V)).

Section SumvPi.

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

Lemma sumv_pi_sum (I : finType) (P : pred I) Vs v (V : {vspace vT})
                  (defV : V = (\sum_(i | P i) Vs i)%VS) :
  v \in V -> \sum_(i | P i) sumv_pi_for defV i v = v :> vT.
Proof. by apply: sumv_pi_uniq_sum; apply: enum_uniq. Qed.

Lemma sumv_pi_nat_sum m n (P : pred nat) Vs v (V : {vspace vT})
                      (defV : V = (\sum_(m <= i < n | P i) Vs i)%VS) :
  v \in V -> \sum_(m <= i < n | P i) sumv_pi_for defV i v = v :> vT.
Proof. by apply: sumv_pi_uniq_sum; apply/filter_uniq/iota_uniq. Qed.

End SumvPi.

Section SubVector.

Variable (K : fieldType) (vT : vectType K) (U : {vspace vT}).

Inductive subvs_of : predArgType := Subvs u & u \in U.

Definition vsval w := let: Subvs u _ := w in u.
Canonical subvs_subType := Eval hnf in [subType for vsval].
Definition subvs_eqMixin := Eval hnf in [eqMixin of subvs_of by <:].
Canonical subvs_eqType := Eval hnf in EqType subvs_of subvs_eqMixin.
Definition subvs_choiceMixin := [choiceMixin of subvs_of by <:].
Canonical subvs_choiceType := ChoiceType subvs_of subvs_choiceMixin.
Definition subvs_zmodMixin := [zmodMixin of subvs_of by <:].
Canonical subvs_zmodType := ZmodType subvs_of subvs_zmodMixin.
Definition subvs_lmodMixin := [lmodMixin of subvs_of by <:].
Canonical subvs_lmodType := LmodType K subvs_of subvs_lmodMixin.

Lemma subvsP w : vsval w \in U. Proof. exact: valP. Qed.
Lemma subvs_inj : injective vsval. Proof. exact: val_inj. Qed.
Lemma congr_subvs u v : u = v -> vsval u = vsval v. Proof. exact: congr1. Qed.

Lemma vsval_is_linear : linear vsval. Proof. by []. Qed.
Canonical vsval_additive := Additive vsval_is_linear.
Canonical vsval_linear := AddLinear vsval_is_linear.

Fact vsproj_key : unit. Proof. by []. Qed.
Definition vsproj_def u := Subvs (memv_proj U u).
Definition vsproj := locked_with vsproj_key vsproj_def.
Canonical vsproj_unlockable := [unlockable fun vsproj].

Lemma vsprojK : {in U, cancel vsproj vsval}.
Proof. by rewrite unlock; apply: projv_id. Qed.
Lemma vsvalK : cancel vsval vsproj.
Proof. by move=> w; apply/val_inj/vsprojK/subvsP. Qed.

Lemma vsproj_is_linear : linear vsproj.
Proof. by move=> k w1 w2; apply: val_inj; rewrite unlock /= linearP. Qed.
Canonical vsproj_additive := Additive vsproj_is_linear.
Canonical vsproj_linear := AddLinear vsproj_is_linear.

Fact subvs_vect_iso : Vector.axiom (\dim U) subvs_of.
Proof.
exists (fun w => \row_i coord (vbasis U) i (vsval w)).
  by move=> k w1 w2; apply/rowP=> i; rewrite !mxE linearP.
exists (fun rw : 'rV_(\dim U) => vsproj (\sum_i rw 0 i *: (vbasis U)`_i)).
  move=> w /=; congr (vsproj _ = w): (vsvalK w).
  by rewrite {1}(coord_vbasis (subvsP w)); apply: eq_bigr => i _; rewrite mxE.
move=> rw; apply/rowP=> i; rewrite mxE vsprojK.
  by rewrite coord_sum_free ?(basis_free (vbasisP U)).
by apply: rpred_sum => j _; rewrite rpredZ ?vbasis_mem ?memt_nth.
Qed.

Definition subvs_vectMixin := VectMixin subvs_vect_iso.
Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin.

End SubVector.
Prenex Implicits vsval vsproj vsvalK.
Arguments subvs_inj {K vT U} [x1 x2].
Arguments vsprojK {K vT U} [x].

Section MatrixVectType.

Variables (R : ringType) (m n : nat).

Fact matrix_vect_iso : Vector.axiom (m * n) 'M[R]_(m, n).
Proof.
exists mxvec => /=; first exact: linearP.
by exists vec_mx; [apply: mxvecK | apply: vec_mxK].
Qed.
Definition matrix_vectMixin := VectMixin matrix_vect_iso.
Canonical matrix_vectType := VectType R 'M[R]_(m, n) matrix_vectMixin.

End MatrixVectType.

Section RegularVectType.

Variable R : ringType.

Fact regular_vect_iso : Vector.axiom 1 R^o.
Proof.
exists (fun a => a%:M) => [a b c|]; first by rewrite rmorphD scale_scalar_mx.
by exists (fun A : 'M_1 => A 0 0) => [a | A]; rewrite ?mxE // -mx11_scalar.
Qed.
Definition regular_vectMixin := VectMixin regular_vect_iso.
Canonical regular_vectType := VectType R R^o regular_vectMixin.

End RegularVectType.

Section ProdVector.

Variables (R : ringType) (vT1 vT2 : vectType R).

Fact pair_vect_iso : Vector.axiom (Vector.dim vT1 + Vector.dim vT2) (vT1 * vT2).
Proof.
pose p2r (u : vT1 * vT2) := row_mx (v2r u.1) (v2r u.2).
pose r2p w := (r2v (lsubmx w) : vT1, r2v (rsubmx w) : vT2).
have r2pK : cancel r2p p2r by move=> w; rewrite /p2r !r2vK hsubmxK.
have p2rK : cancel p2r r2p by case=> u v; rewrite /r2p row_mxKl row_mxKr !v2rK.
have r2p_lin: linear r2p by move=> a u v; congr (_ , _); rewrite /= !linearP.
by exists p2r; [apply: (@can2_linear _ _ _ (Linear r2p_lin)) | exists r2p].
Qed.
Definition pair_vectMixin := VectMixin pair_vect_iso.
Canonical pair_vectType := VectType R (vT1 * vT2) pair_vectMixin.

End ProdVector.

Section FunVectType.

Variable (I : finType) (R : ringType) (vT : vectType R).

Fact ffun_vect_iso : Vector.axiom (#|I| * Vector.dim vT) {ffun I -> vT}.
Proof.
pose fr (f : {ffun I -> vT}) := mxvec (\matrix_(i < #|I|) v2r (f (enum_val i))).
exists fr => /= [k f g|].
  rewrite /fr -linearP; congr (mxvec _); apply/matrixP=> i j.
  by rewrite !mxE /= !ffunE linearP !mxE.
exists (fun r => [ffun i => r2v (row (enum_rank i) (vec_mx r)) : vT]) => [g|r].
  by apply/ffunP=> i; rewrite ffunE mxvecK rowK v2rK enum_rankK.
by apply/(canLR vec_mxK)/matrixP=> i j; rewrite mxE ffunE r2vK enum_valK mxE.
Qed.

Definition ffun_vectMixin := VectMixin ffun_vect_iso.
Canonical ffun_vectType := VectType R {ffun I -> vT} ffun_vectMixin.

End FunVectType.

Canonical exp_vectType (K : fieldType) (vT : vectType K) n :=
  [vectType K of vT ^ n].

Section Solver.

Variable (K : fieldType) (vT : vectType K).
Variables (n : nat) (lhs : n.-tuple 'End(vT)) (rhs : n.-tuple vT).

Let lhsf u := finfun ((tnth lhs)^~ u).
Definition vsolve_eq U := finfun (tnth rhs) \in (linfun lhsf @: U)%VS.

Lemma vsolve_eqP (U : {vspace vT}) :
  reflect (exists2 u, u \in U & forall i, tnth lhs i u = tnth rhs i)
          (vsolve_eq U).
Proof.
have lhsZ: linear lhsf by move=> a u v; apply/ffunP=> i; rewrite !ffunE linearP.
apply: (iffP memv_imgP) => [] [u Uu sol_u]; exists u => //.
  by move=> i; rewrite -[tnth rhs i]ffunE sol_u (lfunE (Linear lhsZ)) ffunE.
by apply/ffunP=> i; rewrite (lfunE (Linear lhsZ)) !ffunE sol_u.
Qed.

End Solver.