Library vector

Finite dimensional vector spaces

vectType K == type for findim vector space structure. vectMixin K == builds the mixins containing the definition of a vector space over K. VectType T M == packs the mixin M to build a vector space of type vecType K. The field K will be infered from the mixin M. The underlying type T should have a lmodType canonical structure. {vspace V} == a vector space over V (V :+: W)%VS == the product of two vecTypes (V ^ n)%VS == the iterated product of a vecType 'Hom(V,W) == homomorphisms from V to W 'End(V) == endomorphisms of V Functions: v%:VS == a vector space of dimension 1 composed of v 0%:VS == the singleton vector space fullv == the complete vector space (V1 + V2)%VS == union of two vector spaces (V1 :&: V2)%VS == intersection of two vector spaces (V^C)%VS == complement of a vector space (V1 :\: V2)%VS == V1 :&: ((V1 :&: V2)^C) \dim V == dimension of a vector space coord l v == coordinates of v in the vector space generated by the sequence l vpick vs == pick an element of vs (0 iff vs is 0%:VS) span l == the linear span generated by the sequence l vbasis vs == a basis of vs \1 == the unit linear function (f \o g)%VS == the composite of two linear functions (f \^-1)%VS == the inverse linear function (f @: vs)%VS == the image of vs by the linear function f (f @^-1: vs)%VS == the pre-image of vs by the linear function f lker f == the kernel of the linear function f limg f == the image of the linear function f (addv_pi1 V1 V2) == projection of (V1 + V2)%VS onto V1 along V2 (addv_pi2 V1 V2) == projection of (V1 + V2)%VS onto V2 along V1 (sumv_pi V_ P i) == projection of (\sum_(j | P j) V_ j)%VS onto V_ i along (\sum_(j | j != i && P j) V_ j) Predicates: v \in vs == v belongs to vs (vs1 <= vs2)%VS == vs1 is a subspace of vs2 free l == l is a list of free vectors is_span vs l == l generates vs is_basis vs l == l is a basis of vs directv vexpr == the vector spaces in the expression vexpr are in direct sum

Open Local Scope ring_scope.

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

Delimit Scope vspace_scope with VS.

Import GRing.Theory.

 Finite dimension vector space 
Module VectorType.

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

 v2rv projection should not be used directly outside of this file
Structure mixin_of (V : lmodType R) : Type := Mixin {
               dim : nat;
  v2rv_isomorphism : V-> 'rV[R]_dim;
                 _ : linear v2rv_isomorphism;
                 _ : bijective v2rv_isomorphism
}.

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

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

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

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

End ClassDef.

Module Exports.

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

End VectorType.
Import VectorType.Exports.

Section VectorTypeTheory.

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

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

 From vector to row matrix:    v2rv 
 From row matrix to vector:    rv2v 
Definition v2rv_isomorphism :=
 (@VectorType.v2rv_isomorphism _ _
    (@VectorType.mixin _ _ (VectorType.class V))).
Local Notation v2rv := v2rv_isomorphism.

Lemma v2rv_linear_proof : linear v2rv.
Canonical Structure v2rv_linear := Linear v2rv_linear_proof.

Lemma v2rv_bij : bijective v2rv.

Lemma v2rv_inj : injective v2rv.

Fact rv2v_proof : forall (rv :'rV[R]_vdim), exists v, rv == v2rv v.

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

Lemma rv2vK : cancel rv2v_isomorphism v2rv.

Lemma v2rvK : cancel v2rv rv2v.

Lemma rv2v_bij : bijective rv2v.

Lemma rv2v_inj : injective rv2v.

Lemma rv2v_linear_proof : linear rv2v.
Canonical Structure rv2v_linear := Linear rv2v_linear_proof.

Variables m n : nat.

Lemma mxvec_bij : bijective (@mxvec R m n).

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

End VectorTypeTheory.

Canonical Structure matrixVectType.

 --- Sub Space --- 
 fin vector space definition : a fin vector space is represented 
 by its canonical matrix. 

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


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

Lemma v2rv_isom : exists f', [/\ cancel v2rv f', cancel f' v2rv & linear f'].

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

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

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

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

Implicit Type vs : {vspace V}.

Lemma vspace_ax: forall vs, <<vs2mx vs>>%MS == vs2mx vs.

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

Lemma vs2mxK : cancel vs2mx (@mx2vs n).

Lemma mx2vsK : forall m (M : 'M_(m,n)), (vs2mx (mx2vs M) :=: M)%MS.

Lemma vseq2mxeq : forall vs1 vs2, (vs1 == vs2) = (vs2mx vs1 == vs2mx vs2)%MS.

Lemma mxeq2vseq: forall m1 m2 M1 M2,
   (M1 == M2)%MS = (@mx2vs m1 M1 == @mx2vs m2 M2).

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

Lemma subv_refl : reflexive subsetv.
Hint Resolve subv_refl.

Lemma subv_trans : transitive subsetv.

Lemma subv_anti : antisymmetric subsetv.

 Standard injection of a vector as a vector space (a line) 
Definition injv (v: V) : {vspace V} := mx2vs (v2rv v).

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

 This injection allows us to define a notion of membership 
Canonical Structure vpredType := mkPredType (fun vs v => (v%:VS <= vs)%VS).

Lemma vs2mx0 : vs2mx 0%:VS = 0.

Lemma mx2vs0: forall m, mx2vs (0 : 'M_(m,n)) = 0%:VS.

Lemma injvP : forall v1 v2, reflect (exists k, v1 = k *: v2) (v1 \in v2%:VS).

Lemma mem0v : forall vs, 0 \in vs.

Lemma memv_inj : forall v, v \in v%:VS.

Lemma memvD : forall vs v1 v2, v1 \in vs -> v2 \in vs -> v1 + v2 \in vs.

Lemma memvMn : forall vs v m, v \in vs -> v *+ m \in vs.

Lemma memvZl : forall vs k v, v \in vs -> k *: v \in vs.

Lemma memvZ : forall vs k v, (k *: v \in vs) = (k == 0) || (v \in vs).

Lemma memvNr : forall vs v, v \in vs -> -v \in vs.

Lemma memvNl : forall vs v, -v \in vs -> v \in vs.

Lemma memv_sub : forall vs v1 v2, v1 \in vs -> v2 \in vs -> v1 - v2 \in vs.

Lemma memvDl : forall vs v1 v2, v1 \in vs -> (v1 + v2 \in vs) = (v2 \in vs).

Lemma memvDr : forall vs v1 v2, v1 \in vs -> (v2 + v1 \in vs) = (v2 \in vs).

Lemma memvN : forall vs v, (-v \in vs) = (v \in vs).

Lemma memv_subl : forall vs v1 v2, v1 \in vs -> (v1 - v2 \in vs) = (v2 \in vs).

Lemma memv_subr : forall vs v1 v2, v1 \in vs -> (v2 - v1 \in vs) = (v2 \in vs).

Lemma memv_suml : forall (I : finType) (P : pred I) (vs_ : I -> V) vs,
  (forall i, P i -> vs_ i \in vs) -> \sum_(i | P i) vs_ i \in vs.

 The ith row of the canonical matrice as a vector 
Lemma rv2v_iE : forall i vs,
      <<row i (vs2mx vs)>>%MS = vs2mx (rv2v (row i (vs2mx vs)))%:VS.

Lemma subvP : forall vs1 vs2,
  reflect (forall v, v \in vs1 -> v \in vs2) (vs1 <= vs2)%VS.

Lemma vspaceP : forall vs1 vs2, reflect (vs1 =i vs2) (vs1 == vs2)%VS.

 Empty space 

Lemma sub0v : forall vs, (0%:VS <= vs)%VS.

Lemma subv0 : forall vs, (vs <= 0%:VS)%VS = (vs == 0%:VS).

Lemma memv0 : forall v, v \in 0%:VS = (v == 0).

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

Lemma vs2mxf : (vs2mx fullv :=: 1%:M)%MS.

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

Lemma subvf : forall vs, (vs <= fullv)%VS.

Lemma memvf : forall v, v \in fullv.

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

Lemma memv_pick : forall vs, vpick vs \in vs.

Lemma vpick0 : forall vs, (vpick vs == 0) = (vs == 0%:VS).

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

Lemma mx2vsD : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 + M2)%MS = (mx2vs M1 + mx2vs M2)%VS.

Lemma vs2mx_morph : {morph vs2mx : u v / (u + v)%VS >-> (u + v)%MS}.

Lemma vs2mx_sum : forall (I : finType) (P : pred I) (vs_ : I -> {vspace V}),
   (vs2mx (\sum_(i | P i) vs_ i))%VS = (\sum_(i | P i) (vs2mx (vs_ i)))%MS.

Lemma mx2vsDr : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 + vs2mx (mx2vs M2))%MS = mx2vs (M1 + M2)%MS.

Lemma mx2vsDl : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (vs2mx (mx2vs M1) + M2)%MS = mx2vs (M1 + M2)%MS.

Lemma subv_add : forall vs1 vs2 vs3,
  (vs1 + vs2 <= vs3)%VS = (vs1 <= vs3)%VS && (vs2 <= vs3)%VS.

Lemma addvSl : forall vs1 vs2, (vs1 <= vs1 + vs2)%VS.

Lemma addvSr : forall vs1 vs2, (vs2 <= vs1 + vs2)%VS.

Lemma addvKl : forall vs1 vs2, (vs1 <= vs2)%VS = (vs1 + vs2 == vs2)%VS.

Lemma addvKr: forall vs1 vs2, (vs2 <= vs1)%VS = (vs1 + vs2 == vs1)%VS.

Lemma addvC : commutative addv.

Lemma addvA : associative addv.

Lemma addvS : forall vs1 vs2 vs3 vs4,
  (vs1 <= vs2 -> vs3 <= vs4 -> vs1 + vs3 <= vs2 + vs4)%VS.

Lemma addvv : idempotent addv.

Lemma sum0v : left_id 0%:VS addv.

Lemma addv0 : right_id 0%:VS addv.

Lemma sumfv : left_zero fullv addv.

Lemma addvf : right_zero fullv addv.

Lemma memv_add : forall v1 v2 vs1 vs2,
  v1 \in vs1 -> v2 \in vs2 -> v1 + v2 \in (vs1 + vs2)%VS.

Lemma memv_addP : forall v vs1 vs2,
  reflect (exists v1, exists v2, [/\ v1 \in vs1, v2 \in vs2 & v = v1 + v2])
           (v \in (vs1 + vs2)%VS).
Implicit Arguments memv_addP [v vs1 vs2].

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

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

Lemma sumv_sup : forall i0 P vs (vs_ : I -> {vspace V}),
  P i0 -> (vs <= vs_ i0)%VS ->
   (vs <= \sum_(i | P i) vs_ i)%VS.

Implicit Arguments sumv_sup [P vs vs_].

Lemma subv_sumP : forall P (vs_ : I -> {vspace V}) vs,
  reflect (forall i, P i -> vs_ i <= vs)%VS
          (\sum_(i | P i) vs_ i <= vs)%VS.

Lemma memv_sumP : forall P (vs_ : I -> {vspace V}) v,
  reflect (exists v_ : I -> V,
            (forall i, P i -> v_ i \in vs_ i) /\
             v = \sum_(i | P i) v_ i)
          (v \in (\sum_(i | P i) vs_ i)%VS).

Lemma memv_sumr : forall P (vs_ : I -> V) (Vs_ : I -> {vspace V}),
  (forall i, P i -> vs_ i \in Vs_ i) ->
  \sum_(i | P i) vs_ i \in (\sum_(i | P i) Vs_ i)%VS.

End BigSum.

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

Lemma capv_mx2vs : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 :&: M2)%MS = (mx2vs M1 :&: mx2vs M2)%VS.

Lemma capv_vs2mx : forall vs1 vs2,
 (vs2mx (vs1 :&: vs2)%VS :=: vs2mx vs1 :&: vs2mx vs2)%MS.

Lemma capv_mx2vsr : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (M1 :&: vs2mx (mx2vs M2))%MS = mx2vs (M1 :&: M2)%MS.

Lemma capv_mx2vsl : forall m1 m2 (M1 : 'M_(m1,n)) (M2 : 'M_(m2,n)),
 mx2vs (vs2mx (mx2vs M1) :&: M2)%MS = mx2vs (M1 :&: M2)%MS.

Lemma subv_cap : forall vs1 vs2 vs3,
  (vs1 <= vs2 :&: vs3)%VS = (vs1 <= vs2)%VS && (vs1 <= vs3)%VS.

Lemma capvSl : forall vs1 vs2, (vs1 :&: vs2 <= vs1)%VS.

Lemma capvSr : forall vs1 vs2, (vs1 :&: vs2 <= vs2)%VS.

Lemma capvKl : forall vs1 vs2, (vs1 <= vs2)%VS = (vs1 :&: vs2 == vs1)%VS.

Lemma capvKr : forall vs1 vs2, ((vs2 <= vs1) = (vs1 :&: vs2 == vs2))%VS.

Lemma capvv : idempotent capv.

Lemma capvC : commutative capv.

Lemma capvA : associative capv.

Lemma capvS : forall vs1 vs2 vs3 vs4,
  (vs1 <= vs2 -> vs3 <= vs4 -> vs1 :&: vs3 <= vs2 :&: vs4)%VS.

Lemma cap0v : left_zero 0%:VS capv.

Lemma capv0 : right_zero 0%:VS capv.

Lemma capfv : left_id fullv capv.

Lemma capvf : right_id fullv capv.

Lemma memv_cap : forall v vs1 vs2,
  (v \in (vs1 :&: vs2)%VS) = (v \in vs1) && (v \in vs2).

Lemma vspace_modl : forall vs1 vs2 vs3,
  (vs1 <= vs3 -> vs1 + (vs2 :&: vs3) = (vs1 + vs2) :&: vs3)%VS.

Lemma vspace_modr : forall vs1 vs2 vs3,
  (vs3 <= vs1 -> (vs1 :&: vs2) + vs3 = vs1 :&: (vs2 + vs3))%VS.

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

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

Lemma bigcapv_inf : forall i0 P (vs_ : I -> {vspace V}) vs,
  P i0 -> (vs_ i0 <= vs -> \bigcap_(i | P i) vs_ i <= vs)%VS.

Lemma subv_bigcapP : forall P vs (vs_ : I -> {vspace V}),
  reflect (forall i, P i -> vs <= vs_ i)%VS
          (vs <= \bigcap_(i | P i) vs_ i)%VS.

End BigCap.

 Complement 
Definition complv vs := mx2vs ((vs2mx vs) ^C)%MS.
Local Notation "A ^C" := (complv A) : vspace_scope.

Lemma addv_complf : forall vs, (vs + vs^C = fullv)%VS.

Lemma capv_compl : forall vs, (vs :&: vs^C)%VS = 0%:VS.

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

Lemma diffvSl : forall vs1 vs2, (vs1 :\: vs2 <= vs1)%VS.

Lemma capv_diff : forall vs1 vs2, ((vs1 :\: vs2) :&: vs2 = 0%:VS )%VS.

Lemma addv_diff_cap_eq : forall vs1 vs2, (vs1 :\: vs2 + vs1 :&: vs2 = vs1)%VS.

 Notion of dimension 
Definition dimv vs := \rank (vs2mx vs).
Local Notation "\dim A" := (dimv A) : nat_scope.

Lemma dimv0 : \dim (0 %:VS) = 0%N.

Lemma dimv_eq0 : forall vs, (\dim vs == 0%N) = (vs == 0%:VS).

Lemma dimvf : \dim fullv = vdim V.

Lemma dim_injv : forall v, \dim (v %:VS) = (v != 0).

Lemma dimvS : forall vs1 vs2, (vs1 <= vs2)%VS -> \dim vs1 <= \dim vs2.

Lemma dimv_leqif_sup : forall vs1 vs2,
 (vs1 <= vs2)%VS -> \dim vs1 <= \dim vs2 ?= iff (vs2 <= vs1)%VS.

Lemma dimv_leqif_eq : forall vs1 vs2,
 (vs1 <= vs2)%VS -> \dim vs1 <= \dim vs2 ?= iff (vs1 == vs2)%VS.

Lemma dimv_compl : forall vs, \dim vs^C = (n - \dim vs)%N.

Lemma dimv_disjoint_sum : forall vs1 vs2,
  (vs1 :&: vs2)%VS = 0%:VS -> \dim (vs1 + vs2)%VS = (\dim vs1 + \dim vs2)%N.

Lemma dimv_cap_compl : forall vs1 vs2,
  (\dim (vs1 :&: vs2) + \dim (vs1 :\: vs2))%N = \dim vs1.

Lemma dimv_sum_cap : forall vs1 vs2,
  (\dim (vs1 + vs2) + \dim (vs1 :&: vs2) = \dim vs1 + \dim vs2)%N.

Lemma dimv_sum_leqif : forall vs1 vs2,
  \dim (vs1 + vs2) <= \dim vs1 + \dim vs2 ?= iff (vs1 :&: vs2 <= 0 %:VS)%VS.

Lemma subv_diffv0 : forall vs1 vs2,
  ((vs1 <= vs2) = (vs1 :\: vs2 == 0%:VS))%VS.

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

Lemma dimv_leq_sum : forall P (vs_ : I -> {vspace V}),
  \dim (\sum_(i | P i) vs_ i)%VS <= (\sum_(i | P i) \dim (vs_ i))%N.

End BigDim.

Section SumExpr.

 Here we just mimick the trick in matrix for vector space. See matrix      
 for a proper documention                                                  

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

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

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

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

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

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

Section Vector.

Variable (v : V).

Fact vector_addv_proof : addv_spec (v%:VS) (v != 0).
Canonical Structure vector_addv_expr := ProperSumvExpr vector_addv_proof.
End Vector.

Section Binary.
Variable (S1 S2 : addv_expr).

Fact binary_addv_proof :
  addv_spec (unwrap S1 + unwrap S2)
             (unwrap (addv_dim S1) + unwrap (addv_dim S2)).
Canonical Structure binary_addv_expr := ProperSumvExpr binary_addv_proof.
End Binary.

Section Nary.

Variables (I : finType) (P : pred I) (S_ : I -> addv_expr).
Fact nary_addv_proof : forall r,
  addv_spec (\sum_(i <- r | P i) unwrap (S_ i))
             (\sum_(i <- r | P i) unwrap (addv_dim (S_ i))).

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

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

End SumExpr.

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

Lemma directvP : forall (S : proper_addv_expr),
  reflect (\dim S = proper_addv_dim S) (directv S).
Implicit Arguments directvP [S].

Lemma directv_trivial : forall vs, directv (unwrap (@trivial_addv vs)).

Lemma dimv_sumw_leqif : forall (S : addv_expr),
  \dim (unwrap S) <= unwrap (addv_dim S) ?= iff directv (unwrap S).

Lemma directvE : forall (S : addv_expr),
  directv (unwrap S) = (\dim (unwrap S) == unwrap (addv_dim S)).

Lemma directvEgeq : forall (S : addv_expr),
  directv (unwrap S) = (\dim (unwrap S) >= unwrap (addv_dim S)).

Section BinaryDirect.

Lemma directv_addE : forall (S1 S2 : addv_expr),
   directv (unwrap S1 + unwrap S2)
    = [&& directv (unwrap S1), directv (unwrap S2)
        & unwrap S1 :&: unwrap S2 == 0%:VS]%VS.

Lemma directv_addP vs1 vs2 :
   reflect (vs1 :&: vs2 = 0%:VS)%VS (directv (vs1 + vs2)).

Lemma directv_add_unique : forall vs1 vs2,
   directv (vs1 + vs2) <->
   (forall u1 v1 u2 v2, u1 \in vs1 -> v1 \in vs1 ->
                        u2 \in vs2 -> v2 \in vs2 ->
                        u1 + u2 == v1 + v2 = ((u1,u2) == (v1,v2))).

End BinaryDirect.

Section NaryDirect.

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


Let directv_sum_recP : forall S_ : I -> addv_expr,
  reflect (forall i, P i -> directv (unwrap (S_ i)) /\ TIsum (unwrap \o S_) i)
          (directv (\sum_(i | P i) (unwrap (S_ i)))).

Lemma directv_sumP : forall vs_ : I -> {vspace V},
  reflect (forall i,
            P i -> vs_ i :&: (\sum_(j | P j && (j != i)) vs_ j) = 0%:VS)%VS
          (directv (\sum_(i | P i) vs_ i)).

Lemma directv_sumE : forall (S_ : I -> addv_expr) (xunwrap := unwrap),
  reflect (and (forall i, P i -> directv (unwrap (S_ i)))
               (directv (\sum_(i | P i) (xunwrap (S_ i)))))
          (directv (\sum_(i | P i) (unwrap (S_ i)))).

Lemma directv_sum_unique : forall vs_ : I -> {vspace V},
   directv (\sum_(i | P i) vs_ i) <->
   (forall (u_ v_ : I -> V), (forall i : I, P i -> u_ i \in vs_ i) ->
                             (forall i : I, P i -> v_ i \in vs_ i) ->
                             (\sum_(i | P i) u_ i == \sum_(i | P i) v_ i) =
                             (forallb i : I, P i ==> (u_ i == v_ i))).

End NaryDirect.

 Linear span generated by a list of vectors 
Definition span (l : seq V) := (\sum_(i <- l) i%:VS)%VS.

Lemma span_nil : span [::] = 0%:VS.

Lemma span_seq1: forall v, span [::v] = v%:VS.

Lemma span_cons : forall v l, span (v::l) = (v%:VS + span l)%VS.

Lemma span_cat : forall l1 l2, span (l1 ++ l2) = (span l1 + span l2)%VS.

Lemma memv_span : forall l v, v \in l -> v \in span l.

Lemma span_subset : forall (l1 l2 : seq V),
  {subset l1 <= l2} -> (span l1 <= span l2)%VS.

Lemma span_eq : forall (l1 l2 : seq V), l1 =i l2 -> span l1 = span l2.

Lemma dim_span : forall l, \dim (span l) <= size l.

 The matrix whose line are the vectors of the span 
Definition span_mx l := \matrix_(i < size l) (v2rv l`_i).

Lemma span_mx_row : forall l i, row i (span_mx l) = v2rv l`_i.

Lemma span_vs2mx : forall l, (vs2mx (span l) == span_mx l)%MS.

Lemma span_mulmx : forall (l : seq V) (s : 'I_(size l) -> K),
  \sum_(i < size l) s i *: l`_i =
     rv2v ((\row_(i < size l) (s i)) *m (span_mx l)).

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

Lemma coord_is_linear : forall l, linear (coord l).
Canonical Structure coord_linear l := Linear (coord_is_linear l).

Lemma coord_sumE : forall l I r (P : pred I) (F : I -> V) i,
 coord l (\sum_(j <- r | P j) F j) i = \sum_(j <- r | P j) coord l (F j) i.

Lemma coord_span :
  forall l v, v \in span l -> v = \sum_(i < size l) coord l v i *: l`_i.

Lemma span_subsetl : forall l vs,
  all (fun v => v \in vs) l = (span l <= vs)%VS.

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

Lemma free_span_mx : forall l, free l = row_free (span_mx l).

Lemma free_nil : free [::].

Lemma free_seq1 : forall v, v != 0 -> free [::v].

Lemma free_perm_eq : forall (l1 l2 : seq V),
  perm_eq l1 l2 -> free l1 = free l2.

Lemma free_notin0 : forall v l, free l -> v \in l -> v != 0.

Lemma freeP : forall l,
  reflect
    (forall s, \sum_(i < size l) s i *: l`_i = 0 -> s =1 fun _ => 0)
     (free l).

Lemma free_coord : forall l i,
  free l -> coord l (l`_i) = [ffun j : 'I_(size l) => (i == j)%:R].

Lemma free_coordE : forall l i j, free l -> coord l (l`_i) j = (i == j)%:R.

Lemma free_catl : forall l2 l1, free (l1 ++ l2) -> free l1.

Lemma free_catr : forall l1 l2, free (l1 ++ l2) -> free l2.

Lemma free_filter : forall P (l: seq V),
  free l -> free (filter P l).

Lemma addv_free : forall l1 l2,
  directv (span l1 + span l2) -> free (l1 ++ l2) = free l1 && free l2.

 Notion of is_basis 
Definition is_span vs l := span l == vs.

Lemma is_span_nil : is_span 0%:VS [::].

Lemma is_span_seq1 : forall v, v != 0 -> is_span v%:VS [::v].

Lemma memv_is_span : forall v vs l, is_span vs l -> v \in l -> v \in vs.

Lemma is_span_span : forall vs l v,
  is_span vs l -> v \in vs -> v = \sum_i coord l v i *: l`_i.

Lemma addv_is_span : forall vs1 vs2 l1 l2,
  is_span vs1 l1 -> is_span vs2 l2 -> is_span (vs1 + vs2)%VS (l1 ++ l2).

 Notion of basis 
Definition is_basis vs l := is_span vs l && free l.

Lemma is_basis_span : forall vs l, is_basis vs l -> is_span vs l.

Lemma is_basis_free : forall vs l, is_basis vs l -> free l.

Lemma is_basis_nil : is_basis 0%:VS [::].

Lemma is_basis_seq1 : forall v, v != 0 -> is_basis v%:VS [::v].

Lemma is_basis_notin0 : forall v vs l, is_basis vs l -> v \in l -> v != 0.

Lemma memv_is_basis : forall v vs l, is_basis vs l -> v \in l -> v \in vs.

Lemma addv_is_basis : forall vs1 vs2 l1 l2,
  directv (vs1 + vs2) -> is_basis vs1 l1 -> is_basis vs2 l2 ->
  is_basis (vs1 + vs2)%VS (l1 ++ l2).

Lemma size_is_basis : forall vs l, is_basis vs l -> size l = \dim vs.

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

Lemma vbasis0 : vbasis 0%:VS = [::].

Lemma is_basis_vbasis : forall vs, is_basis vs (vbasis vs).

Lemma memv_basis : forall v vs, v \in (vbasis vs) -> v \in vs.

Lemma coord_basis : forall v vs, v \in vs ->
  v = \sum_(i < size (vbasis vs)) coord (vbasis vs) v i *: (vbasis vs)`_i.

Lemma size_basis : forall vs, size (vbasis vs) = \dim vs.

Section BigSumBasis.

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

Lemma span_bigcat : forall P (l_ : I -> seq V),
  span (\big[cat/[::]]_(i | P i) l_ i) = (\sum_(i | P i) span (l_ i))%VS.

Lemma bigaddv_free : forall P (l_ : I -> seq V),
  (directv (\sum_(i | P i) span (l_ i)))%VS ->
  (forall i, P i -> free (l_ i)) -> free (\big[cat/[::]]_(i | P i) l_ i).

Lemma bigaddv_is_span : forall P l_ (vs_ : I -> {vspace V}),
  (forall i, P i -> is_span (vs_ i) (l_ i)) ->
    is_span (\sum_(i | P i) vs_ i)%VS (\big[cat/[::]]_(i | P i) l_ i).

Lemma bigaddv_is_basis : forall P l_ (vs_ : I -> {vspace V}),
  let vs := (\sum_(i | P i) vs_ i)%VS in
  directv vs ->
  (forall i, P i -> is_basis (vs_ i) (l_ i)) ->
    is_basis vs (\big[cat/[::]]_(i | P i) l_ i).

End BigSumBasis.

End VSpaceDef.

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


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

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

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

 Linear applications over a vectType 
Section LinearApp.

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

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

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

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

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

Coercion fun_of_lapp : linearApp >-> Funclass.

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

Lemma eq_lapp : forall (f g : linearApp), reflect (f =1 g) (f == g).

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

Lemma lapp_addA : associative add_lapp.

Lemma lapp_addC : commutative add_lapp.

Lemma lapp_add0 : left_id zero_lapp add_lapp.

Lemma lapp_addN : left_inverse zero_lapp opp_lapp add_lapp.

Definition lapp_zmodMixin := ZmodMixin lapp_addA lapp_addC lapp_add0 lapp_addN.

Lemma zero_lappE : forall x, (\0 x = 0)%VS.

Lemma add_lappE : forall f g x, (f \+ g)%VS x = f x + g x.

Lemma opp_lappE : forall f x, (opp_lapp f) x = - f x.

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

Lemma sum_lappE : forall I (r : seq I) (P : pred I) (F : I -> linearApp) x,
  (\big[+%R/0]_(i <- r | P i) F i) x = \big[+%R/0]_(i <- r | P i) (F i x).

Lemma lapp_scaleA : forall k1 k2 f, (k1 \*: (k2 \*: f) = (k1 * k2) \*: f)%VS.
Lemma lapp_scale1 : forall f, (1 \*: f = f)%VS.

Lemma lapp_addr : forall k f1 f2,
  (k \*: (f1 \+ f2) = (k \*: f1) \+ (k \*: f2))%VS.

Lemma lapp_addl : forall f k1 k2,
  ((k1 + k2) \*: f = (k1 \*: f) \+ (k2 \*: f))%VS.

Definition lapp_lmodMixin :=
  LmodMixin lapp_scaleA lapp_scale1 lapp_addr lapp_addl.

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

Definition lapp_rep := mxvec \o mx_of_lapp.

Definition lapp_rep_is_linear : linear lapp_rep.
Canonical Structure lapp_rep_linear:= Linear lapp_rep_is_linear.

Lemma lapp_rep_bij : bijective lapp_rep.

 Linear Application as a vector type 
Definition linearMixin := VectMixin lapp_rep_is_linear lapp_rep_bij.
Canonical Structure linearVect (phV : phant V) (phW : phant W) :=
  VectType R linearMixin.

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

Lemma hom_is_linear : forall (f : linearVect phV phW), linear f.
Canonical Structure hom_linear f := Linear (hom_is_linear f).

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

Lemma fun_of_lappK : cancel fun_of_lapp lapp_of_fun.

Lemma lapp_of_funK : forall (f : V -> W), linear f -> lapp_of_fun f =1 f.

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

Section ScaleLapp.

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

Lemma scale_lappE : forall a x, ((a \*: f) x)%VS = a *: f x.

End ScaleLapp.

Section UnitApp.

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

Lemma unit_lappE : forall x, (\1 x = x)%VS.

Lemma unit_nonzero_lapp : (\1 != \0)%VS.

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

Section CompLinearApp.

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

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

Lemma comp_lappE : forall f g, (f \o g)%VS =1 f \o g.

End CompLinearApp.

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

Section InvLinearApp.

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

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

Lemma inv_lapp_def : forall f, (f \o (f \^-1 \o f) = f)%VS.

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

Section LAlgLinearApp.

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

Lemma comp_lappA : forall f g h, (f \o (g \o h) = (f \o g) \o h)%VS.

Lemma comp_lapp_addl : forall f1 f2 g,
  ((f1 \+ f2) \o g = (f1 \o g) \+ (f2 \o g))%VS.

Lemma comp_lapp_addr : forall f g1 g2,
  (f \o (g1 \+ g2) = (f \o g1) \+ (f \o g2))%VS.

Lemma comp_1lapp : forall f, (\1 \o f = f)%VS.

Lemma comp_lapp1 : forall f, (f \o \1)%VS = f.

Lemma scale_lapp_Ar : forall k f g, (k \*: (f \o g) = f \o (k \*: g))%VS.

End LAlgLinearApp.

Section AlgLinearApp.

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

Lemma scale_lapp_Al : forall k f g, (k \*: (f \o g) = (k \*: f) \o g)%VS.

End AlgLinearApp.

Module LApp.

Section LinearAppStruct.

 Endomorphisms over V have an algebra structure as soon as dim V != 0 
Variable (R : comRingType) (V : vectType R).
Hypothesis dim_nz : (vdim V != 0)%N.

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

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

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

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

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

End LinearAppStruct.

End LApp.

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

Section LinearImage.

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

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

Definition limg f := mx2vs (mx_of_lapp f).

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

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

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

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

Lemma lkerE : forall f vs, (f @: vs == 0%:VS)%VS = (vs <= lker f)%VS.

Lemma limgE : forall f, limg f = (f @: (fullv V))%VS.

Lemma limg_monotone : forall f vs1 vs2,
  (vs1 <= vs2)%VS -> (f @: vs1 <= f @: vs2)%VS.

Lemma limg_inj : forall f v, (f @: (v %:VS))%VS = (f v)%:VS.

Lemma lpre_img0 : forall f, (f @^-1: 0%:VS)%VS = lker f.

Lemma lpre_img_full : forall f (vs : {vspace W}),
  (f @^-1: (vs :&: limg f))%VS = (f @^-1: vs)%VS.

Lemma lpre_imgK : forall f (vs : {vspace W}),
  (vs <= limg f)%VS -> (f @: (f @^-1: vs))%VS = vs.

Lemma limg0 : forall f, (f @: (0 %:VS))%VS = 0%:VS.

Lemma lim0g : forall vs, (0 @: vs)%VS = 0%:VS.

Lemma memv_img : forall f v vs, v \in vs -> f v \in (f @: vs)%VS.

Lemma memv_ker : forall f v, (v \in lker f)%VS = (f v == 0).

Lemma limg_add : forall f, {morph (fun_of_limg f) : u v / (u + v)%VS}.

Lemma limg_sum : forall f (I : finType) (P : pred I) (vs_ : I -> {vspace V}),
  (f @: (\sum_(i | P i) vs_ i) = \sum_(i | P i) (f @: (vs_ i)))%VS.

Lemma limg_cap : forall f vs1 vs2,
  (f @: (vs1 :&: vs2) <= f @: vs1 :&: f @: vs2)%VS.

Lemma limg_bigcap :
  forall f (I : finType) (P : pred I) (vs_ : I -> {vspace V}),
  (f @: (\bigcap_(i | P i) vs_ i) <= \bigcap_(i | P i) (f @: (vs_ i)))%VS.

Lemma limg_span : forall f l, (f @: span l)%VS = span (map f l).

Lemma memv_imgP : forall f v vs,
  reflect (exists v1, v1 \in vs /\ v = f v1) (v \in f @: vs)%VS.

Lemma limg_ker_compl : forall f vs, (f @: (vs :\: lker f))%VS = (f @: vs)%VS.

Lemma limg_dim_eq : forall f vs,
  (vs :&: lker f)%VS = 0%:VS -> \dim (f @: vs) = \dim vs.

Lemma limg_is_basis : forall f vs l, (vs :&: lker f)%VS = 0%:VS ->
   (is_basis vs l -> is_basis (f @: vs)%VS (map f l)).

Lemma limg_ker_dim : forall f vs,
  (\dim (vs :&: lker f) + \dim (f @: vs) = \dim vs)%N.

Lemma lker0P : forall f, reflect (injective f) (lker f == 0%:VS).

Lemma limg_ker0 : forall f vs ws,
 lker f == 0%:VS -> (f @: vs <= f @: ws)%VS = (vs <= ws)%VS.

Lemma eq_limg_ker0 : forall f vs ws,
 lker f == 0%:VS -> (f @: vs == f @: ws)%VS = (vs == ws)%VS.

End LinearImage.

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

Section UnitImage.

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

Lemma lim1g : forall vs, ((\1 : 'End(V)) @: vs = vs)%VS.

End UnitImage.

Section CompImage.

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

Lemma limg_comp : forall (f : 'Hom(V,W)) (g : 'Hom(W,Z)) vs,
 ((g \o f) @: vs = g @: (f @: vs))%VS.

End CompImage.

Section LinearPreImage.

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

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

Lemma lpre_imgE : forall f (vs : {vspace W}),
  (f @^-1: vs)%VS = (((f \^-1) @: (vs :&: limg f)%VS) + lker f)%VS.

Lemma lpre_img_monotone : forall f (vs1 vs2 : {vspace W}),
  (vs1 <= vs2)%VS-> (f @^-1: vs1 <= f @^-1: vs2)%VS.

Lemma memv_pre_img : forall f v (vs : {vspace W}), (f v \in vs) = (v \in f @^-1: vs)%VS.

Lemma inv_lker0 : forall f, lker f == 0%:VS -> (f \^-1 \o f = \1)%VS.

End LinearPreImage.

Section Projection.

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

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

Lemma projv_id : forall vs v, v \in vs -> projv vs v = v.

Lemma lker_proj : forall vs, lker (projv vs) = (vs^C)%VS.

Lemma limg_proj : forall vs, limg (projv vs) = vs.

Lemma memv_proj : forall vs v, projv vs v \in vs.

Lemma memv_projC : forall vs v, v - projv vs v \in (vs^C)%VS.

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

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

Lemma memv_pi1 : forall vs1 vs2 v, (addv_pi1 vs1 vs2) v \in vs1.

Lemma memv_pi2 : forall vs1 vs2 v, (addv_pi2 vs1 vs2) v \in vs2.

Lemma addv_pi1_pi2 : forall vs1 vs2 v, v \in (vs1 + vs2)%VS ->
 v = ((addv_pi1 vs1 vs2) + (addv_pi2 vs1 vs2)) v.

Section Sumv_Pi.

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


Let size_loop : forall Vs, size (loop Vs) = size Vs.

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

Lemma memv_sum_pi : forall i v, sumv_pi i v \in V_ i.

Lemma sumv_sum_pi : forall v, v \in (\sum_(i | P i) V_ i)%VS ->
 v = (\sum_(i | P i) sumv_pi i) v.

End Sumv_Pi.

End Projection.

Section SubVectorType.

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

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

Lemma subvectP : forall u, sv_val u \in vs.
Lemma subvect_inj : injective sv_val.
Lemma congr_subv : forall u v, u = v -> sv_val u = sv_val v.

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

Lemma subvect_addA : associative subvect_add.
Lemma subvect_addC : commutative subvect_add.
Lemma subvect_add0 : left_id subvect_zero subvect_add.
Lemma subvect_addN : left_inverse subvect_zero subvect_opp subvect_add.

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

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

Lemma subvect_scaleA : forall k1 k2 u,
  subvect_scale k1 (subvect_scale k2 u) = subvect_scale (k1 * k2) u.
Lemma subvect_scale1 : left_id 1 subvect_scale.
Lemma subvect_scale_addr : forall k, {morph (subvect_scale k) : x y / x + y}.
Lemma subvect_scale_addl : forall u,
  {morph (subvect_scale)^~ u : k1 k2 / k1 + k2}.

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

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

Lemma subvect_is_linear : linear subvect_v2rv.

Canonical Structure subvect_linear := Linear subvect_is_linear.

Lemma subvect_bij : bijective subvect_v2rv.

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

End SubVectorType.

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

 Simple Product of 2 vectType 
Section ProdVector.

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

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

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

Definition p2pv : forall (vw: V * W), prodVector.
Defined.

Definition pv2p : forall (p : prodVector), V * W.
Defined.

Lemma p2pvK : cancel p2pv pv2p.

Lemma pv2pK : cancel pv2p p2pv.

Lemma pvaddE : forall p q : prodVector,
  pv2p (p + q) = ((pv2p p).1+(pv2p q).1,(pv2p p).2+(pv2p q).2).

Lemma pvoppE : forall p : prodVector,
  pv2p (-p) = (-(pv2p p).1,-(pv2p p).2).

Lemma pvscaleE : forall (a: K) (p : prodVector),
  pv2p (a *: p) = (a *: (pv2p p).1, a *: (pv2p p).2).

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

Lemma pvfK : forall (f : 'End(V)) (g : 'End(W)),
   pvf f g =1 (fun x : prodVector => p2pv (f (pv2p x).1 , g (pv2p x).2)).

End ProdVector.

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

 Iterated product 
Section ExpVector.

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

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

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

Lemma l2ev_cons : forall x l, l2ev (x :: l) = p2pv (x, (l2ev l)).

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

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

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

Let behead_tupleE : forall n u (v : n.-tuple V),
  behead_tuple [tuple of u :: v] = v.

Lemma tuple_of_evK : forall n, cancel (@tuple_of_ev n) (@ev_of_tuple n).

Lemma ev_of_tupleK : forall n, cancel (@ev_of_tuple n) (@tuple_of_ev n).

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

Let map_tupleE :
  forall (T1 T2 : Type) (f : T1 -> T2) (x : T1) n (t : n.-tuple T1),
   map_tuple f [tuple of x :: t] = [tuple of f x :: map f t].

Lemma evfK : forall n (ft : n.-tuple (V -> V)),
  (forall i, linear (tnth ft i)) ->
  evf ft =1 (fun p => ev_of_tuple (map_tuple (fun x => x p) ft)).

End ExpVector.

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

 Solving a tuple of linear equations 
Section Solver.

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

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

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

Lemma vsolve_eqP : forall (ms : {vspace V}),
  reflect
      (exists u, u \in ms /\
         forall i : 'I_n, tnth feq i u = tnth veq i)
      (vsolve_eq ms).

End Solver.

Export VectorType.Exports.