(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop finfun tuple.
From mathcomp Require Import ssralg matrix mxalgebra zmodp.

(******************************************************************************)
(*                    Finite dimensional vector spaces                        *)
(*                                                                            *)
(* NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.   *)
(*                                                                            *)
(*           vectType R == interface structure for finite dimensional (more   *)
(*                         precisely, detachable) vector spaces over R, which *)
(*                         should be at least a ringType                      *)
(*                         The HB class is called Vector.                     *)
(*     Vector.axiom n M <-> type M is linearly isomorphic to 'rV_n            *)
(*                         := {v2r : M -> 'rV_n| linear v2r & bijective v2r}  *)
(*          {vspace vT} == the type of (detachable) subspaces of vT; vT       *)
(*                         should have a vectType structure over a fieldType  *)
(*           subvs_of U == the subtype of elements of V in the subspace U     *)
(*                         This is canonically a vectType.                    *)
(*              vsval u == linear injection of u : subvs_of U into V          *)
(*           vsproj U v == linear projection of v : V in subvs U              *)
(*             rVof e v == row vector in 'rV_(\dim vT) of coordinates of      *)
(*                         v : vT in the basis e                              *)
(*            vecof e v == vector in vT whose coordinates in the basis e are  *)
(*                         given by v : 'rV_(\dim vT)                         *)
(*                         Note that this is the inverse of rVof.             *)
(*          mxof e e' f == \dim uT * \dim vT matrix of the linear function    *)
(*                         f : 'Hom(uT, vT) in the bases e of uT and e' of vT,*)
(*                         acting on row vectors                              *)
(*          hommx e f M == linear function in 'Hom(uT, vT) whose matrix       *)
(*                         in the bases e and f is M : 'M_(\dim uT, \dim vT)  *)
(*                         Note that this is the inverse of mxof.             *)
(*             vsof e M == the subspace of vT generated by the rows of M,     *)
(*                         seen as coordinates in the basis e                 *)
(*             msof e U == matrix whose rows, seen as coordinates in the      *)
(*                         basis e, generate the subspace U of vT             *)
(*                         Note that this is the inverse of vsof.             *)
(*         'Hom(aT, rT) == the type of linear functions (homomorphisms) from  *)
(*                         aT to rT, where aT and rT are vectType structures  *)
(*                         Elements of 'Hom(aT, rT) coerce to Coq functions.  *)
(*             linfun f == a vector linear function in 'Hom(aT, rT) that      *)
(*                         coincides with f : aT -> rT when f is linear       *)
(*             'End(vT) == endomorphisms of vT (:= 'Hom(vT, vT))              *)
(* --> The types subvs_of U, 'Hom(aT, rT), 'End(vT), K^o, 'M[K]_(m, n),       *)
(*     vT * wT, {ffun I -> vT}, vT ^ n all have canonical vectType instances. *)
(*                                                                            *)
(*  Functions:                                                                *)
(*             <[v]>%VS == the vector space generated by v (a line if v != 0) *)
(*                 0%VS == the trivial vector subspace                        *)
(*         fullv, {:vT} == the complete vector subspace (displays as fullv)   *)
(*           (U + V)%VS == the join (sum) of two subspaces U and V            *)
(*         (U :&: V)%VS == intersection of vector subspaces U and V           *)
(*             (U^C)%VS == a complement of the vector subspace U              *)
(*         (U :\: V)%VS == a local complement to U :& V in the subspace U     *)
(*               \dim U == dimension of a vector space U                      *)
(*     span X, <<X>>%VS == the subspace spanned by the vector sequence X      *)
(*          coord X i v == i'th coordinate of v on X, when v \in <<X>>%VS and *)
(*                         where X : n.-tuple vT and i : 'I_n                 *)
(*                         Note that coord X i is a scalar function.          *)
(*              vpick U == a nonzero element of U if U= 0%VS, or 0 if U = 0   *)
(*             vbasis U == a (\dim U).-tuple that is a basis of U             *)
(*                \1%VF == the identity linear function                       *)
(*          (f \o g)%VF == the composite of two linear functions f and g      *)
(*            (f^-1)%VF == a linear function that is a right inverse to the   *)
(*                         linear function f on the codomain of f             *)
(*          (f @: U)%VS == the image of U by the linear function f            *)
(*       (f @^-1: U)%VS == the pre-image of U by the linear function f        *)
(*               lker f == the kernel of the linear function f                *)
(*               limg f == the image of the linear function f                 *)
(*         fixedSpace f == the fixed space of a linear endomorphism f         *)
(*         daddv_pi U V == projection onto U along V if U and V are disjoint; *)
(*                         daddv_pi U V + daddv_pi V U is then a projection   *)
(*                         onto the direct sum (U + V)%VS                     *)
(*              projv U == projection onto U (along U^C, := daddv_pi U U^C)   *)
(*         addv_pi1 U V == projection onto the subspace U :\: V of U along V  *)
(*         addv_pi2 U V == projection onto V along U :\: V; note that         *)
(*                         addv_pi1 U V and addv_pi2 U V are (asymmetrical)   *)
(*                         complementary projections on (U + V)%VS            *)
(*   sumv_pi_for defV i == for defV : V = (V \sum_(j <- r | P j) Vs j)%VS,    *)
(*                         j ranging over an eqType, this is a projection on  *)
(*                         a subspace of Vs i, along a complement in V, such  *)
(*                         that \sum_(j <- r | P j) sumv_pi_for defV j is a   *)
(*                         projection onto V if filter P r is duplicate-free  *)
(*                         (e.g., when V := \sum_(j | P j) Vs j)              *)
(*          sumv_pi V i == notation the above when defV == erefl V, and V is  *)
(*                         convertible to \sum_(j <- r | P j) Vs j)%VS        *)
(*      leigenspace f a == linear eigenspace of the linear function f for     *)
(*                         the (potential) eigenvalue a                       *)
(*                                                                            *)
(*  Predicates:                                                               *)
(*              v \in U == v belongs to U (:= (<[v]> <= U)%VS)                *)
(*          (U <= V)%VS == U is a subspace of V                               *)
(*               free B == B is a sequence of nonzero linearly independent    *)
(*                         vectors                                            *)
(*         basis_of U b == b is a basis of the subspace U                     *)
(*            directv S == S is the expression for a direct sum of subspaces  *)
(*      leigenvalue f a == a is a linear eigenvalue of the linear function f  *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope vspace_scope.
Declare Scope lfun_scope.

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.

(* Finite dimension vector space *)
Definition vector_axiom_def (R : ringType) n (V : lmodType R) :=
  {v2r : V -> 'rV[R]_n | linear v2r & bijective v2r}.
Arguments vector_axiom_def [R] n%N V%type.

HB.mixin Record Lmodule_hasFinDim (R : ringType) (V : Type) of GRing.Lmodule R V :=
  { dim : nat;
    vector_subdef : vector_axiom_def dim V }.

#[mathcomp(axiom="vector_axiom_def"), short(type="vectType")]
HB.structure Definition Vector (R : ringType) :=
  { V of Lmodule_hasFinDim R V & GRing.Lmodule R V }.

#[deprecated(since="mathcomp 2.2.0", note="Use Vector.axiom instead.")]
Notation vector_axiom := Vector.axiom.
Arguments dim {R} s.

(* FIXME: S/space and H/hom were defined behind the module Vector *
 * Perhaps we should change their names to avoid conflicts.       *)
Section OtherDefs.
Local Coercion dim : Vector.type >-> nat.
Inductive space (K : fieldType) (vT : Vector.type K) :=
  Space (mx : 'M[K]_vT) & <<mx>>%MS == mx.
Inductive hom (R : ringType) (vT wT : Vector.type R) :=
  Hom of 'M[R]_(vT, wT).
End OtherDefs.
(* /FIXME *)

Module Import VectorExports.
Bind Scope ring_scope with Vector.sort.

Arguments space [K] vT%type.

Notation "{ 'vspace' vT }" := (space 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 VectorExports.

(* The contents of this module exposes the matrix encodings, and should       *)
(* therefore not be used outside of the vector library implementation.        *)
Module VectorInternalTheory.

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

Fact v2r_subproof : Vector.axiom vT vT. Proof. exact: vector_subdef. 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.

HB.instance Definition _ := GRing.isLinear.Build R vT 'rV_vT _ v2r
  (s2valP v2r_subproof).
HB.instance Definition _ := GRing.isLinear.Build R 'rV_vT vT _ r2v
  (can2_linear v2rK r2vK).
End Iso.

Section Vspace.
Variables (K : fieldType) (vT : vectType K).
Local Coercion dim : Vector.type >-> 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 (U : @space K vT) := 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).

HB.instance Definition _ := [isSub of {vspace vT} for vs2mx].
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.
HB.instance Definition _ : isSub _ _ 'Hom(aT, rT) := [isNew for f2mx].
End Hom.

Arguments mx2vs {K vT m%N} A%MS.
Prenex Implicits v2r r2v v2rK r2vK b2mx vs2mx vs2mxK f2mx.

End VectorInternalTheory.

Export VectorExports.
Import VectorInternalTheory.

Section VspaceDefs.

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

HB.instance Definition _ := [Choice of {vspace vT} by <:].

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

(* Vspace membership is defined as line inclusion. *)
Definition pred_of_vspace (U : space vT) : {pred vT} :=
  fun v => (vs2mx (vline v) <= vs2mx U)%MS.
Canonical vspace_predType := @PredType _ (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].

(* coord and directv are defined in the VectorTheory section. *)

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

End VspaceDefs.

Coercion pred_of_vspace : space >-> pred_sort.
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).

(* begin hide *)

(* Internal theory facts *)
Let vs2mxP U V : reflect (U = V) (vs2mx U == vs2mx V)%MS.
Proof. by rewrite (sameP genmxP eqP) !gen_vs2mx; apply: eqP. Qed.

Let memvK v U : (v \in U) = (v2r v <= vs2mx U)%MS.
Proof. by rewrite -genmxE. Qed.

Let mem_r2v rv U : (r2v rv \in U) = (rv <= vs2mx U)%MS.
Proof. by rewrite memvK r2vK. Qed.

Let vs2mx0 : @vs2mx K vT 0 = 0.
Proof. by rewrite /= linear0 genmx0. Qed.

Let vs2mxD U V : vs2mx (U + V) = (vs2mx U + vs2mx V)%MS.
Proof. by rewrite /= genmx_adds !gen_vs2mx. Qed.

Let vs2mx_sum := big_morph _ vs2mxD vs2mx0.

Let vs2mxI U V : vs2mx (U :&: V) = (vs2mx U :&: vs2mx V)%MS.
Proof. by rewrite /= genmx_cap !gen_vs2mx. Qed.

Let vs2mxF : vs2mx {:vT} = 1%:M.
Proof. by rewrite /= genmx1. Qed.

Let row_b2mx n (X : n.-tuple vT) i : row i (b2mx X) = v2r X`_i.
Proof. by rewrite -tnth_nth rowK. Qed.

Let span_b2mx n (X : n.-tuple vT) : span X = mx2vs (b2mx X).
Proof. by rewrite unlock tvalK; case: _ / (esym _). Qed.

Let mul_b2mx n (X : n.-tuple vT) (rk : 'rV_n) :
  \sum_i rk 0 i *: X`_i = r2v (rk *m b2mx X).
Proof.
rewrite mulmx_sum_row linear_sum; apply: eq_bigr => i _.
by rewrite row_b2mx linearZ /= v2rK.
Qed.

Let lin_b2mx n (X : n.-tuple vT) k :
  \sum_(i < n) k i *: X`_i = r2v (\row_i k i *m b2mx X).
Proof. by rewrite -mul_b2mx; apply: eq_bigr => i _; rewrite mxE. Qed.

Let free_b2mx n (X : n.-tuple vT) : free X = row_free (b2mx X).
Proof. by rewrite /free /dimv span_b2mx genmxE size_tuple. Qed.
(* end hide *)

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 1?linear0 1?sub0mx // => Uu Uv.
by rewrite linearP addmx_sub ?scalemx_sub.
Qed.
HB.instance Definition _ (U : {vspace vT}) :=
  GRing.isSubmodClosed.Build K vT (pred_of_vspace U) (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 : core.

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.

(* Empty space. *)
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.

(* Full space *)

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

(* Picking a non-zero vector in a subspace. *)
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.

(* Sum of subspaces. *)
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_op 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.

HB.instance Definition _ := Monoid.isComLaw.Build {vspace vT} 0%VS addv
  addvA addvC add0v.

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.

(* Intersection *)

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

HB.instance Definition _ := Monoid.isComLaw.Build {vspace vT} fullv capv
  capvA capvC capfv.

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.

(* Complement *)
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.

(* Difference *)
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.

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

Lemma dimv_eq0 U :  (\dim U == 0) = (U == 0%VS).
Proof. by rewrite /dimv /= mxrank_eq0 [in RHS]/eq_op /= linear0 genmx0. Qed.

Lemma dimvf : \dim {:vT} = 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.

(* The vector direct sum theory clones the interface types of the matrix     *)
(* direct sum theory (see mxalgebra for the technical details), but          *)
(* nevetheless reuses much of the matrix theory.                             *)
Structure addv_expr := Sumv {
  addv_val :> wrapped {vspace vT};
  addv_dim : wrapped nat;
  _ : mxsum_spec (vs2mx (unwrap addv_val)) (unwrap addv_dim)
}.

(* Piggyback on mxalgebra theory. *)
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] := eqVneq; 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.

(* Linear span generated by a list of vectors *)
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.

(* Coordinates function; should perhaps be generalized to nat indices. *)

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.
HB.instance Definition _ n Xn i :=
  GRing.isLinear.Build K vT K _ (coord Xn i) (@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.

(* Free generator sequences. *)

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=> eqXY; rewrite /free (perm_size eqXY) (eq_span (perm_mem eqXY)).
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 3!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) 1?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_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 _ /(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.
pose flM := GRing.isLinear.Build _ _ _ _ f lin_f.
pose fL : {linear _ -> _} := HB.pack f flM.
exists fL => 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.

(* Subspace bases *)

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.
exact/eq_span/perm_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.

#[global] Hint Resolve subvv : core.
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)).

(* Linear functions over a vectType *)
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) :=
  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 : 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)) := 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).

HB.instance Definition _ := [Choice of 'Hom(aT, rT) by <:].

Fact lfun_is_linear f : linear f.
Proof. by rewrite unlock; apply: linearP. Qed.
HB.instance Definition _ (f : hom aT rT) :=
  GRing.isLinear.Build R aT rT _ f (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.

HB.instance Definition _ := GRing.isZmodule.Build 'Hom(aT, rT)
  lfun_addA lfun_addC lfun_add0 lfun_addN.

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.

Arguments fun_of_lfunK {R aT rT}.

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.

HB.instance Definition _ :=
  GRing.Zmodule_isLmodule.Build _ 'Hom(aT, rT)
    lfun_scaleA lfun_scale1 lfun_scaleDr lfun_scaleDl.

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

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

HB.instance Definition _ := Lmodule_hasFinDim.Build _ 'Hom(aT, rT)
  lfun_vect_iso.

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 limgD 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 _ (limgD 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 subset_limgP f U (r : seq rT) :
  {subset r <= (f @: U)%VS} <-> (exists2 a, all (mem U) a & r = map f a).
Proof.
split => [|[{}r /allP/= rE ->] _ /mapP[x xr ->]]; last by rewrite memv_img ?rE.
move=> /(_ _ _)/memv_imgP/sig2_eqW-/(all_sig_cond (0 : aT))[f' f'P].
exists (map f' r); first by apply/allP => _ /mapP [x /f'P[? ?] ->].
by symmetry; rewrite -map_comp; apply: map_id_in => x /f'P[].
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)) limgD; 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.

Lemma lker0_img_cap f U V : lker f == 0%VS ->
  (f @: (U :&: V) = f @: U :&: f @: V)%VS.
Proof.
move=> kf0; apply/eqP; rewrite eqEsubv limg_cap/=; apply/subvP => x.
rewrite memv_cap => /andP[/memv_imgP[u uU ->]] /memv_imgP[v vV].
by move=> /(lker0P _ kf0) eq_uv; rewrite memv_img// memv_cap uU eq_uv vV.
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}.
Arguments limg_lfunVK {K aT rT f} [x] f_x.

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

Arguments lpreimK {K aT rT f} [W] fW.

Section LfunAlgebra.
(* This section is a bit of a place holder: the instances we build here can't *)
(* be canonical because we are missing an interface for proper vectTypes,     *)
(* would sit between Vector and Falgebra. For now, we just supply structure   *)
(* definitions here and supply actual instances for F-algebras in a submodule *)
(* of the algebra library (there is currently no actual use of the End(vT)    *)
(* algebra structure). Also note that the unit ring structure is missing.     *)

Variables (R : comRingType) (vT : vectType R).
Hypothesis vT_proper : 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.

(* FIXME: as explained above, the following structures should not be declared *
 * as canonical, so mixins and structures are built separately, and we        *
 * don't use HB.instance Definition _ := ...                                  *
 *  This is ok, but maybe we could introduce an alias                         *)
Definition lfun_comp_ringMixin := GRing.Zmodule_isRing.Build 'End(vT)
  comp_lfunA comp_lfun1l comp_lfun1r comp_lfunDl comp_lfunDr lfun1_neq0.
Definition lfun_comp_ringType : ringType :=
  HB.pack 'End(vT) lfun_comp_ringMixin.

(* In the standard endomorphism ring product is categorical composition. *)
Definition lfun_ringType : ringType := lfun_comp_ringType^c.

Definition lfun_lalgMixin := GRing.Lmodule_isLalgebra.Build R lfun_ringType
  (fun k x y => comp_lfunZr k y x).
Definition lfun_lalgType : lalgType R :=
  HB.pack 'End(vT) lfun_ringType lfun_lalgMixin.

Definition lfun_algMixin := GRing.Lalgebra_isAlgebra.Build R lfun_lalgType
  (fun k x y => comp_lfunZl k y x).
Definition lfun_algType : algType R :=
  HB.pack 'End(vT) lfun_lalgType lfun_algMixin.

End LfunAlgebra.

Section Projection.

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

Definition daddv_pi U V := 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; exact/daddv_pi_add/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]].
  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; have [e _ []] := big_enumP. 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.

(* Turn a {vspace V} into a vectType                                          *)
Variable (K : fieldType) (vT : vectType K) (U : {vspace vT}).

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

Definition vsval w : vT := let: Subvs u _ := w in u.
HB.instance Definition _ := [isSub of subvs_of for vsval].
HB.instance Definition _ := [Choice of subvs_of by <:].
HB.instance Definition _ := [SubChoice_isSubZmodule of subvs_of by <:].
HB.instance Definition _ := [SubZmodule_isSubLmodule of subvs_of by <:].

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.
HB.instance Definition _ := GRing.isLinear.Build K subvs_of vT _ vsval
  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.
HB.instance Definition _ := GRing.isLinear.Build K vT subvs_of _ vsproj
  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.

HB.instance Definition _ := Lmodule_hasFinDim.Build K subvs_of subvs_vect_iso.

Lemma SubvsE x (xU : x \in U) : Subvs xU = vsproj x.
Proof. by apply/val_inj; rewrite /= vsprojK. Qed.

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

Section MatrixVectType.

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

(* The apparently useless => /= in line 1 of the proof performs some evar     *)
(* expansions that the Ltac interpretation of exists is incapable of doing.   *)
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.
HB.instance Definition _ := Lmodule_hasFinDim.Build _ 'M[R]_(m, n) matrix_vect_iso.

Lemma dim_matrix : dim 'M[R]_(m, n) = m * n.
Proof. by []. Qed.

End MatrixVectType.

(* A ring is a one-dimension vector space *)
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.
HB.instance Definition _ := Lmodule_hasFinDim.Build _ R^o regular_vect_iso.

End RegularVectType.

(* External direct product of two vectTypes. *)
Section ProdVector.

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

Fact pair_vect_iso : Vector.axiom (dim vT1 + 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.
pose r2plM := GRing.isLinear.Build _ _ _ _ r2p r2p_lin.
pose r2pL : {linear _ -> _} := HB.pack r2p r2plM.
by exists p2r; [apply: (@can2_linear _ _ _ r2pL) | exists r2p].
Qed.
HB.instance Definition _ := Lmodule_hasFinDim.Build _ (vT1 * vT2)%type
  pair_vect_iso.

End ProdVector.

(* Function from a finType into a ring form a vectype. *)
Section FunVectType.

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

(* Type unification with exist is again a problem in this proof. *)
Fact ffun_vect_iso : Vector.axiom (#|I| * 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 -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.

HB.instance Definition _ := Lmodule_hasFinDim.Build _ {ffun I -> vT}
  ffun_vect_iso.

End FunVectType.

HB.instance Definition _ (K : fieldType) (vT : vectType K) n :=
  Vector.on (vT ^ n)%type.

(* Solving a tuple of linear equations. *)
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.
pose lhslM := GRing.isLinear.Build _ _ _ _ lhsf lhsZ.
pose lhsL : {linear _ -> _} := HB.pack lhsf lhslM.
apply: (iffP memv_imgP) => [] [u Uu sol_u]; exists u => //.
  by move=> i; rewrite -[tnth rhs i]ffunE sol_u (lfunE lhsL) ffunE.
by apply/ffunP=> i; rewrite (lfunE lhsL) !ffunE sol_u.
Qed.

End Solver.

Section lfunP.
Variable (F : fieldType).
Context {uT vT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).

Lemma span_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) :
  {in <<U>>%VS, phi =1 psi} <-> {in U, phi =1 psi}.
Proof.
split=> eq_phi_psi u uU; first by rewrite eq_phi_psi ?memv_span.
rewrite [u](@coord_span _ _ _ (in_tuple U))// !linear_sum/=.
by apply: eq_bigr=> i _; rewrite 2!linearZ/= eq_phi_psi// ?mem_nth.
Qed.

Lemma fullv_lfunP (U : seq uT) (phi psi : 'Hom(uT,vT)) : <<U>>%VS = fullv ->
  phi = psi <-> {in U, phi =1 psi}.
Proof.
by move=> Uf; split=> [->//|/span_lfunP]; rewrite Uf=> /(_ _ (memvf _))-/lfunP.
Qed.
End lfunP.

Module passmx.
Section passmx.
Variable (F : fieldType).

Section vecmx.
Context {vT : vectType F}.
Local Notation n := (\dim {:vT}).

Variables (e : n.-tuple vT).

Definition rVof (v : vT) := \row_i coord e i v.
Lemma rVof_linear : linear rVof.
Proof. by move=> x v1 v2; apply/rowP=> i; rewrite !mxE linearP. Qed.
HB.instance Definition _ := GRing.isLinear.Build F _ _ _ rVof rVof_linear.

Lemma coord_rVof i v : coord e i v = rVof v 0 i.
Proof. by rewrite !mxE. Qed.

Definition vecof (v : 'rV_n) := \sum_i v 0 i *: e`_i.

Lemma vecof_delta i : vecof (delta_mx 0 i) = e`_i.
Proof.
rewrite /vecof (bigD1 i)//= mxE !eqxx scale1r big1 ?addr0// => j neq_ji.
by rewrite mxE (negPf neq_ji) andbF scale0r.
Qed.

Lemma vecof_linear : linear vecof.
Proof.
move=> x v1 v2; rewrite linear_sum -big_split/=.
by apply: eq_bigr => i _/=; rewrite !mxE scalerDl scalerA.
Qed.
HB.instance Definition _ := GRing.isLinear.Build F _ _ _ vecof vecof_linear.

Variable e_basis : basis_of {:vT} e.

Lemma rVofK : cancel rVof vecof.
Proof.
move=> v; rewrite [v in RHS](coord_basis e_basis) ?memvf//.
by apply: eq_bigr => i; rewrite !mxE.
Qed.

Lemma vecofK : cancel vecof rVof.
Proof.
move=> v; apply/rowP=> i; rewrite !(lfunE, mxE).
by rewrite coord_sum_free ?(basis_free e_basis).
Qed.

Lemma rVofE (i : 'I_n) : rVof e`_i = delta_mx 0 i.
Proof.
apply/rowP=> k; rewrite !mxE.
by rewrite eqxx coord_free ?(basis_free e_basis)// eq_sym.
Qed.

Lemma coord_vecof i v : coord e i (vecof v) = v 0 i.
Proof. by rewrite coord_rVof vecofK. Qed.

Lemma rVof_eq0 v : (rVof v == 0) = (v == 0).
Proof. by rewrite -(inj_eq (can_inj vecofK)) rVofK linear0. Qed.

Lemma vecof_eq0 v : (vecof v == 0) = (v == 0).
Proof. by rewrite -(inj_eq (can_inj rVofK)) vecofK linear0. Qed.

End vecmx.

Section hommx.
Context {uT vT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).

Variables (e : m.-tuple uT) (e' : n.-tuple vT).

Definition mxof (h : 'Hom(uT, vT)) := lin1_mx (rVof e' \o h \o vecof e).

Lemma mxof_linear : linear mxof.
Proof.
move=> x h1 h2; apply/matrixP=> i j; do !rewrite ?lfunE/= ?mxE.
by rewrite linearP.
Qed.
HB.instance Definition _ := GRing.isLinear.Build F _ _ _ mxof mxof_linear.

Definition funmx (M : 'M[F]_(m, n)) u := vecof e' (rVof e u *m M).

Lemma funmx_linear M : linear (funmx M).
Proof.
by rewrite /funmx => x u v; rewrite linearP mulmxDl -scalemxAl linearP.
Qed.
HB.instance Definition _ M :=
  GRing.isLinear.Build F _ _ _ (funmx M) (funmx_linear M).

Definition hommx M : 'Hom(uT, vT) := linfun (funmx M).

Lemma hommx_linear : linear hommx.
Proof.
rewrite /hommx; move=> x A B; apply/lfunP=> u; do !rewrite lfunE/=.
by rewrite /funmx mulmxDr -scalemxAr linearP.
Qed.
HB.instance Definition _ M := GRing.isLinear.Build F _ _ _ hommx hommx_linear.

Hypothesis e_basis: basis_of {:uT} e.
Hypothesis f_basis: basis_of {:vT} e'.

Lemma mxofK : cancel mxof hommx.
Proof.
by move=> h; apply/lfunP=> u; rewrite lfunE/= /funmx mul_rV_lin1/= !rVofK.
Qed.

Lemma hommxK : cancel hommx mxof.
Proof.
move=> M; apply/matrixP => i j; rewrite !mxE/= lfunE/=.
by rewrite /funmx vecofK// -rowE coord_vecof// mxE.
Qed.

Lemma mul_mxof phi u : u *m mxof phi = rVof e' (phi (vecof e u)).
Proof. by rewrite mul_rV_lin1/=. Qed.

Lemma hommxE M u : hommx M u = vecof e' (rVof e u *m M).
Proof. by rewrite -[M in RHS]hommxK mul_mxof !rVofK//. Qed.

Lemma rVof_mul M u : rVof e u *m M = rVof e' (hommx M u).
Proof. by rewrite hommxE vecofK. Qed.

Lemma hom_vecof (phi : 'Hom(uT, vT)) u :
  phi (vecof e u) = vecof e' (u *m mxof phi).
Proof. by rewrite mul_mxof rVofK. Qed.

Lemma rVof_app (phi : 'Hom(uT, vT)) u :
  rVof e' (phi u) = rVof e u *m mxof phi.
Proof. by rewrite mul_mxof !rVofK. Qed.

Lemma vecof_mul M u : vecof e' (u *m M) = hommx M (vecof e u).
Proof. by rewrite hommxE vecofK. Qed.

Lemma mxof_eq0 phi : (mxof phi == 0) = (phi == 0).
Proof. by rewrite -(inj_eq (can_inj hommxK)) mxofK linear0. Qed.

Lemma hommx_eq0 M : (hommx M == 0) = (M == 0).
Proof. by rewrite -(inj_eq (can_inj mxofK)) hommxK linear0. Qed.

End hommx.

Section hommx_comp.

Context {uT vT wT : vectType F}.
Local Notation m := (\dim {:uT}).
Local Notation n := (\dim {:vT}).
Local Notation p := (\dim {:wT}).

Variables (e : m.-tuple uT) (f : n.-tuple vT) (g : p.-tuple wT).
Hypothesis e_basis: basis_of {:uT} e.
Hypothesis f_basis: basis_of {:vT} f.
Hypothesis g_basis: basis_of {:wT} g.

Lemma mxof_comp (phi : 'Hom(uT, vT)) (psi : 'Hom(vT, wT)) :
  mxof e g (psi \o phi)%VF = mxof e f phi *m mxof f g psi.
Proof.
apply/matrixP => i k; rewrite !(mxE, comp_lfunE, lfunE) /=.
rewrite [phi _](coord_basis f_basis) ?memvf// 2!linear_sum/=.
by apply: eq_bigr => j _ /=; rewrite !mxE !linearZ/= !vecof_delta.
Qed.

Lemma hommx_mul (A : 'M_(m,n)) (B : 'M_(n, p)) :
  hommx e g (A *m B) = (hommx f g B \o hommx e f A)%VF.
Proof.
by apply: (can_inj (mxofK e_basis g_basis)); rewrite mxof_comp !hommxK.
Qed.

End hommx_comp.

Section vsms.

Context {vT : vectType F}.
Local Notation n := (\dim {:vT}).

Variables (e : n.-tuple vT).

Definition msof (V : {vspace vT}) : 'M_n := mxof e e (projv V).
(* alternative *)
(* (\sum_(v <- vbasis V) <<rVof e v>>)%MS. *)

Definition vsof (M : 'M[F]_n) := limg (hommx e e M).
(* alternative *)
(* <<[seq vecof e (row i M) | i : 'I_n]>>%VS. *)

Lemma mxof1 : free e -> mxof e e \1 = 1%:M.
Proof.
by move=> eF; apply/matrixP=> i j; rewrite !mxE vecof_delta lfunE coord_free.
Qed.

Hypothesis e_basis : basis_of {:vT} e.

Lemma hommx1 : hommx e e 1%:M = \1%VF.
Proof. by rewrite -mxof1 ?(basis_free e_basis)// mxofK. Qed.

Lemma msofK : cancel msof vsof.
Proof. by rewrite /msof /vsof; move=> V; rewrite mxofK// limg_proj. Qed.

Lemma mem_vecof u (V : {vspace vT}) : (vecof e u \in V) = (u <= msof V)%MS.
Proof.
apply/idP/submxP=> [|[v ->{u}]]; last by rewrite -hom_vecof// memv_proj.
rewrite -[V in X in X -> _]msofK => /memv_imgP[v _].
by move=> /(canRL (vecofK _)) ->//; rewrite -rVof_mul//; eexists.
Qed.

Lemma rVof_sub u M : (rVof e u <= M)%MS = (u \in vsof M).
Proof.
apply/submxP/memv_imgP => [[v /(canRL (rVofK _)) ->//]|[v _ ->]]{u}.
  by exists (vecof e v); rewrite ?memvf// -vecof_mul.
by exists (rVof e v); rewrite -rVof_mul.
Qed.

Lemma vsof_sub M V : (vsof M <= V)%VS = (M <= msof V)%MS.
Proof.
apply/subvP/rV_subP => [MsubV _/submxP[u ->]|VsubM _/memv_imgP[u _ ->]].
  by rewrite -mem_vecof MsubV// -rVof_sub vecofK// submxMl.
by rewrite -[V]msofK -rVof_sub VsubM// -rVof_mul// submxMl.
Qed.

Lemma msof_sub V M : (msof V <= M)%MS = (V <= vsof M)%VS.
Proof.
apply/rV_subP/subvP => [VsubM v vV|MsubV _/submxP[u ->]].
  by rewrite -rVof_sub VsubM// -mem_vecof rVofK.
by rewrite mul_mxof rVof_sub MsubV// memv_proj.
Qed.

Lemma vsofK M : (msof (vsof M) == M)%MS.
Proof. by rewrite msof_sub -vsof_sub subvv. Qed.

Lemma sub_msof : {mono msof : V V' / (V <= V')%VS >-> (V <= V')%MS}.
Proof. by move=> V V'; rewrite msof_sub msofK. Qed.

Lemma sub_vsof : {mono vsof : M M' / (M <= M')%MS >-> (M <= M')%VS}.
Proof. by move=> M M'; rewrite vsof_sub (eqmxP (vsofK _)). Qed.

Lemma msof0 : msof 0 = 0.
Proof.
apply/eqP; rewrite -submx0; apply/rV_subP => v.
by rewrite -mem_vecof memv0 vecof_eq0// => /eqP->; rewrite sub0mx.
Qed.

Lemma vsof0 : vsof 0 = 0%VS.
Proof. by apply/vspaceP=> v; rewrite memv0 -rVof_sub submx0 rVof_eq0. Qed.

Lemma msof_eq0 V : (msof V == 0) = (V == 0%VS).
Proof. by rewrite -(inj_eq (can_inj msofK)) msof0. Qed.

Lemma vsof_eq0 M : (vsof M == 0%VS) = (M == 0).
Proof.
rewrite (sameP eqP eqmx0P) -!(eqmxP (vsofK M)) (sameP eqmx0P eqP) -msof0.
by rewrite (inj_eq (can_inj msofK)).
Qed.

End vsms.

Section eigen.

Context {uT : vectType F}.

Definition leigenspace (phi : 'End(uT)) a := lker (phi - a *: \1%VF).
Definition leigenvalue phi a := leigenspace phi a != 0%VS.

Local Notation m := (\dim {:uT}).
Variables (e : m.-tuple uT).
Hypothesis e_basis: basis_of {:uT} e.
Let e_free := basis_free e_basis.

Lemma lker_ker phi : lker phi = vsof e (kermx (mxof e e phi)).
Proof.
apply/vspaceP => v; rewrite memv_ker -rVof_sub// (sameP sub_kermxP eqP).
by rewrite -rVof_app// rVof_eq0.
Qed.

Lemma limgE phi : limg phi = vsof e (mxof e e phi).
Proof.
apply/vspaceP => v; rewrite -rVof_sub//.
apply/memv_imgP/submxP => [[u _ ->]|[u /(canRL (rVofK _)) ->//]].
  by exists (rVof e u); rewrite -rVof_app.
by exists (vecof e u); rewrite ?memvf// -hom_vecof.
Qed.

Lemma leigenspaceE f a : leigenspace f a = vsof e (eigenspace (mxof e e f) a).
Proof. by rewrite [LHS]lker_ker linearB linearZ/= mxof1// scalemx1. Qed.

End eigen.
End passmx.
End passmx.