# Theory VS_Connect

```(*
Author:      René Thiemann
*)
(* with contributions from Alexander Bentkamp, Universität des Saarlandes *)

section ‹Matrices as Vector Spaces›

text ‹This theory connects the Matrix theory with the VectorSpace theory of
Holden Lee. As a consequence notions like span, basis, linear dependence, etc.
are available for vectors and matrices of the Matrix-theory.›

theory VS_Connect
imports
Matrix
Missing_VectorSpace
Determinant
begin

hide_const (open) Multiset.mult
hide_const (open) Polynomial.smult
hide_const (open) Modules.module
hide_const (open) subspace
hide_fact (open) subspace_def

named_theorems class_ring_simps

abbreviation class_ring :: "'a :: {times,plus,one,zero} ring" where
"class_ring ≡ ⦇ carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+) ⦈"

interpretation class_semiring: semiring "class_ring :: 'a :: semiring_1 ring"
rewrites [class_ring_simps]: "carrier class_ring = UNIV"
and [class_ring_simps]: "mult class_ring = (*)"
and [class_ring_simps]: "add class_ring = (+)"
and [class_ring_simps]: "one class_ring = 1"
and [class_ring_simps]: "zero class_ring = 0"
and [class_ring_simps]: "pow (class_ring :: 'a ring) = (^)"
and [class_ring_simps]: "finsum (class_ring :: 'a ring) = sum"
proof -
let ?r = "class_ring :: 'a ring"
show "semiring ?r"
by (unfold_locales, auto simp: field_simps)
then interpret semiring ?r .
{
fix x y
have "x [^]⇘?r⇙ y = x ^ y"
by (induct y, auto simp: power_commutes)
}
thus "([^]⇘?r⇙) = (^)" by (intro ext)
{
fix f and A :: "'b set"
have "finsum ?r f A = sum f A"
by (induct A rule: infinite_finite_induct, auto)
}
thus "finsum ?r = sum" by (intro ext)
qed auto

interpretation class_ring: ring "class_ring :: 'a :: ring_1 ring"
rewrites "carrier class_ring = UNIV"
and "mult class_ring = (*)"
and "one class_ring = 1"
and "zero class_ring = 0"
and [class_ring_simps]: "a_inv (class_ring :: 'a ring) = uminus"
and [class_ring_simps]: "a_minus (class_ring :: 'a ring) = minus"
and "pow (class_ring :: 'a ring) = (^)"
and "finsum (class_ring :: 'a ring) = sum"
proof -
let ?r = "class_ring :: 'a ring"
interpret semiring ?r ..
show "finsum ?r = sum" "pow ?r = (^)" by (simp_all add: class_ring_simps)
{
fix x :: 'a
have "∃y. x + y = 0" by (rule exI[of _ "-x"], auto)
} note [simp] = this
show "ring ?r"
by (unfold_locales, auto simp: field_simps Units_def)
then interpret ring ?r .
{
fix x :: 'a
have "⊖⇘?r⇙ x = - x" unfolding a_inv_def m_inv_def
by (rule the1_equality, rule ex1I[of _ "- x"], auto simp: minus_unique)
} note ainv = this
thus inv: "a_inv ?r = uminus" by (intro ext)
{
fix x y :: 'a
have "x ⊖⇘?r⇙ y = x - y"
apply (subst a_minus_def)
using inv by auto
}
thus "(λx y. x ⊖⇘?r⇙ y) = minus" by (intro ext)
qed (auto simp: class_ring_simps)

interpretation class_cring: cring "class_ring :: 'a :: comm_ring_1 ring"
rewrites "carrier class_ring = UNIV"
and "mult class_ring = (*)"
and "one class_ring = 1"
and "zero class_ring = 0"
and "a_inv (class_ring :: 'a ring) = uminus"
and "a_minus (class_ring :: 'a ring) = minus"
and "pow (class_ring :: 'a ring) = (^)"
and "finsum (class_ring :: 'a ring) = sum"
and [class_ring_simps]: "finprod class_ring = prod"
proof -
let ?r = "class_ring :: 'a ring"
interpret ring ?r ..
show "cring ?r"
by (unfold_locales, auto)
then interpret cring ?r .
show "a_inv (class_ring :: 'a ring) = uminus"
and "a_minus (class_ring :: 'a ring) = minus"
and "pow (class_ring :: 'a ring) = (^)"
and "finsum (class_ring :: 'a ring) = sum" by (simp_all add: class_ring_simps)
{
fix f and A :: "'b set"
have "finprod ?r f A = prod f A"
by (induct A rule: infinite_finite_induct, auto)
}
thus "finprod ?r = prod" by (intro ext)
qed (auto simp: class_ring_simps)

definition div0 :: "'a :: {one,plus,times,zero}" where
"div0 ≡ m_inv (class_ring :: 'a ring) 0"

lemma class_field: "field (class_ring :: 'a :: field ring)" (is "field ?r")
proof -
interpret cring ?r ..
{
fix x :: 'a
have "x ≠ 0 ⟹ ∃xa. xa * x = 1 ∧ x * xa = 1"
by (intro exI[of _ "inverse x"], auto)
} note [simp] = this
show "field ?r"
by (unfold_locales, auto simp: Units_def)
qed

interpretation class_field: field "class_ring :: 'a :: field ring"
rewrites "carrier class_ring = UNIV"
and "mult class_ring = (*)"
and "one class_ring = 1"
and "zero class_ring = 0"
and "a_inv class_ring = uminus"
and "a_minus class_ring = minus"
and "pow class_ring = (^)"
and "finsum class_ring = sum"
and "finprod class_ring = prod"
and [class_ring_simps]: "m_inv (class_ring :: 'a ring) x =
(if x = 0 then div0 else inverse x)"
(* problem that m_inv ?r 0 = inverse 0 is not guaranteed  *)
proof -
let ?r = "class_ring :: 'a ring"
show "field ?r" using class_field.
then interpret field ?r.
show "a_inv ?r = uminus"
and "a_minus ?r = minus"
and "pow ?r = (^)"
and "finsum ?r = sum"
and "finprod ?r = prod" by (fact class_ring_simps)+
show "inv⇘?r⇙ x = (if x = 0 then div0 else inverse x)"
proof (cases "x = 0")
case True
thus ?thesis unfolding div0_def by simp
next
case False
thus ?thesis unfolding m_inv_def
by (intro the1_equality ex1I[of _ "inverse x"], auto simp: inverse_unique)
qed
qed (auto simp: class_ring_simps)

lemmas matrix_vs_simps = module_mat_simps class_ring_simps

definition class_field :: "'a :: field ring"
where [class_ring_simps]: "class_field ≡ class_ring"

locale matrix_ring =
fixes n :: nat
and field_type :: "'a :: field itself"
begin
abbreviation R where "R ≡ ring_mat TYPE('a) n n"
sublocale ring R
rewrites "carrier R = carrier_mat n n"
and "mult R = (*)"
and "one R = 1⇩m n"
and "zero R = 0⇩m n n"
using ring_mat by (auto simp: ring_mat_simps)

end

lemma matrix_vs: "vectorspace (class_ring :: 'a :: field ring) (module_mat TYPE('a) nr nc)"
proof -
interpret abelian_group "module_mat TYPE('a) nr nc"
by (rule abelian_group_mat)
show ?thesis unfolding class_field_def
by (unfold_locales, unfold matrix_vs_simps,
qed

locale vec_module =
fixes f_ty::"'a::comm_ring_1 itself"
and n::"nat"
begin

abbreviation V where "V ≡ module_vec TYPE('a) n"

sublocale Module.module "class_ring :: 'a ring" V
rewrites "carrier V = carrier_vec n"
and "zero V = 0⇩v n"
and "module.smult V = (⋅⇩v)"
and "carrier class_ring = UNIV"
and "monoid.mult class_ring = (*)"
and "one class_ring = 1"
and "zero class_ring = 0"
and "a_inv (class_ring :: 'a ring) = uminus"
and "a_minus (class_ring :: 'a ring) = (-)"
and "pow (class_ring :: 'a ring) = (^)"
and "finsum (class_ring :: 'a ring) = sum"
and "finprod (class_ring :: 'a ring) = prod"
and "⋀X. X ⊆ UNIV = True" (* These rewrite rules will clean lemmas *)
and "⋀x. x ∈ UNIV = True"
and "⋀a A. a ∈ A → UNIV ≡ True"
and "⋀P. P ∧ True ≡ P"
and "⋀P. (True ⟹ P) ≡ Trueprop P"
apply unfold_locales
apply (auto simp: module_vec_simps class_ring_simps Units_def add_smult_distrib_vec
done

end

locale matrix_vs =
fixes nr :: nat
and nc :: nat
and field_type :: "'a :: field itself"
begin

abbreviation V where "V ≡ module_mat TYPE('a) nr nc"
sublocale
vectorspace class_ring V
rewrites "carrier V = carrier_mat nr nc"
and "mult V = (*)"
and "one V = 1⇩m nr"
and "zero V = 0⇩m nr nc"
and "smult V = (⋅⇩m)"
and "carrier class_ring = UNIV"
and "mult class_ring = (*)"
and "one class_ring = 1"
and "zero class_ring = 0"
and "a_inv (class_ring :: 'a ring) = uminus"
and "a_minus (class_ring :: 'a ring) = minus"
and "pow (class_ring :: 'a ring) = (^)"
and "finsum (class_ring :: 'a ring) = sum"
and "finprod (class_ring :: 'a ring) = prod"
and "m_inv (class_ring :: 'a ring) x =
(if x = 0 then div0 else inverse x)"
by (rule matrix_vs, auto simp: matrix_vs_simps class_field_def)
end

lemma vec_module: "module (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)"
proof -
interpret abelian_group "module_vec TYPE('a) n"
apply (unfold_locales)
unfolding module_vec_def Units_def
show ?thesis
unfolding class_field_def
apply (unfold_locales)
unfolding class_ring_simps
unfolding module_vec_simps
qed

lemma vec_vs: "vectorspace (class_ring :: 'a :: field ring) (module_vec TYPE('a) n)"
unfolding vectorspace_def
using vec_module class_field
by (auto simp: class_field_def)

locale vec_space =
fixes f_ty::"'a::field itself"
and n::"nat"
begin

sublocale vec_module f_ty n.

sublocale vectorspace class_ring V
rewrites cV[simp]: "carrier V = carrier_vec n"
and [simp]: "add V = (+)"
and [simp]: "zero V = 0⇩v n"
and [simp]: "smult V = (⋅⇩v)"
and "carrier class_ring = UNIV"
and "mult class_ring = (*)"
and "one class_ring = 1"
and "zero class_ring = 0"
and "a_inv (class_ring :: 'a ring) = uminus"
and "a_minus (class_ring :: 'a ring) = minus"
and "pow (class_ring :: 'a ring) = (^)"
and "finsum (class_ring :: 'a ring) = sum"
and "finprod (class_ring :: 'a ring) = prod"
and "m_inv (class_ring :: 'a ring) x = (if x = 0 then div0 else inverse x)"
using vec_vs
unfolding class_field_def
by (auto simp: module_vec_simps class_ring_simps)

lemma finsum_vec[simp]: "finsum_vec TYPE('a) n = finsum V"
by (force simp: finsum_vec_def monoid_vec_def finsum_def finprod_def)

lemma finsum_scalar_prod_sum:
assumes f: "f : U → carrier_vec n"
and w: "w: carrier_vec n"
shows "finsum V f U ∙ w = sum (λu. f u ∙ w) U"
using w f
proof (induct U rule: infinite_finite_induct)
case (insert u U)
hence f: "f : U → carrier_vec n" "f u : carrier_vec n"  by auto
show ?case
unfolding finsum_insert[OF insert(1) insert(2) f]
apply (subst add_scalar_prod_distrib) using insert by auto
qed auto

lemma vec_neg[simp]: assumes "x : carrier_vec n" shows "⊖⇘V⇙ x = - x"
unfolding a_inv_def m_inv_def apply simp
apply (rule the_equality, intro conjI)
using assms apply auto
using M.minus_unique uminus_carrier_vec uminus_r_inv_vec by blast

lemma finsum_dim:
"finite A ⟹ f ∈ A → carrier_vec n ⟹ dim_vec (finsum V f A) = n"
proof(induct set:finite)
case (insert a A)
hence dfa: "dim_vec (f a) = n" by auto
have f: "f ∈ A → carrier_vec n" using insert by auto
hence fa: "f a ∈ carrier_vec n" using insert by auto
show ?case
unfolding finsum_insert[OF insert(1) insert(2) f fa]
using insert by auto
qed simp

lemma lincomb_dim:
assumes fin: "finite X"
and X: "X ⊆ carrier_vec n"
shows "dim_vec (lincomb a X) = n"
proof -
let ?f = "λv. a v ⋅⇩v v"
have f: "?f ∈ X → carrier_vec n" apply rule using X by auto
show ?thesis
unfolding lincomb_def
using finsum_dim[OF fin f].
qed

lemma finsum_index:
assumes i: "i < n"
and f: "f ∈ X → carrier_vec n"
and X: "X ⊆ carrier_vec n"
shows "finsum V f X \$ i = sum (λx. f x \$ i) X"
using X f
proof (induct X rule: infinite_finite_induct)
case empty
then show ?case using i by simp next
case (insert x X)
then have Xf: "finite X"
and xX: "x ∉ X"
and x: "x ∈ carrier_vec n"
and X: "X ⊆ carrier_vec n"
and fx: "f x ∈ carrier_vec n"
and f: "f ∈ X → carrier_vec n" by auto
have i2: "i < dim_vec (finsum V f X)"
using i finsum_closed[OF f] by auto
have ix: "i < dim_vec x" using x i by auto
show ?case
unfolding finsum_insert[OF Xf xX f fx]
unfolding sum.insert[OF Xf xX]
using insert lincomb_def
by auto
qed (insert i, auto)

lemma lincomb_index:
assumes i: "i < n"
and X: "X ⊆ carrier_vec n"
shows "lincomb a X \$ i = sum (λx. a x * x \$ i) X"
proof -
let ?f = "λx. a x ⋅⇩v x"
have f: "?f : X → carrier_vec n" using X by auto
have point: "⋀v. v ∈ X ⟹ (a v ⋅⇩v v) \$ i = a v * v \$ i" using i X by auto
show ?thesis
unfolding lincomb_def
unfolding finsum_index[OF i f X]
using point X by simp
qed

lemma append_insert: "set (xs @ [x]) = insert x (set xs)" by simp

lemma lincomb_units:
assumes i: "i < n"
shows "lincomb a (set (unit_vecs n)) \$ i = a (unit_vec n i)"
unfolding lincomb_index[OF i unit_vecs_carrier]
unfolding unit_vecs_first
proof -
let ?f = "λm i. ∑x∈set (unit_vecs_first n m). a x * x \$ i"
have zero:"⋀m j. m ≤ j ⟹ j < n ⟹ ?f m j = 0"
proof -
fix m
show "⋀j. m ≤ j ⟹ j < n ⟹ ?f m j = 0"
proof (induction m)
case (Suc m)
hence mj:"m≤j" and mj':"m≠j" and jn:"j<n" and mn:"m<n" by auto
hence mem: "unit_vec n m ∉ set (unit_vecs_first n m)"
apply(subst unit_vecs_first_distinct) by auto
show ?case
unfolding unit_vecs_first.simps
unfolding append_insert
unfolding sum.insert[OF finite_set mem]
unfolding index_unit_vec(1)[OF mn jn]
unfolding Suc(1)[OF mj jn] using mj' by simp
qed simp
qed
{ fix m
have "i < m ⟹ m ≤ n ⟹ ?f m i = a (unit_vec n i)"
proof (induction m arbitrary: i)
case (Suc m)
hence iSm: "i < Suc m" and i:"i<n" and mn: "m<n" by auto
hence mem: "unit_vec n m ∉ set (unit_vecs_first n m)"
apply(subst unit_vecs_first_distinct) by auto
show ?case
unfolding unit_vecs_first.simps
unfolding append_insert
unfolding sum.insert[OF finite_set mem]
unfolding index_unit_vec(1)[OF mn i]
using zero Suc by (cases "i = m",auto)
qed auto
}
thus "?f n i = a (unit_vec n i)" using assms by auto
qed

lemma lincomb_coordinates:
assumes v: "v : carrier_vec n"
defines "a ≡ (λu. v \$ (THE i. u = unit_vec n i))"
shows "lincomb a (set (unit_vecs n)) = v"
proof -
have a: "a ∈ set (unit_vecs n) → UNIV" by auto
have fvu: "⋀i. i < n ⟹ v \$ i = a (unit_vec n i)"
unfolding a_def using unit_vec_eq by auto
show ?thesis
apply rule
unfolding lincomb_dim[OF finite_set unit_vecs_carrier]
using v lincomb_units fvu
by auto
qed

lemma span_unit_vecs_is_carrier: "span (set (unit_vecs n)) = carrier_vec n" (is "?L = ?R")
proof (rule;rule)
fix v assume vsU: "v ∈ ?L" show "v ∈ ?R"
proof -
obtain a
where v: "v = lincomb a (set (unit_vecs n))"
using vsU
unfolding finite_span[OF finite_set unit_vecs_carrier] by auto
thus ?thesis using lincomb_closed[OF unit_vecs_carrier] by auto
qed
next fix v::"'a vec" assume v: "v ∈ ?R" show "v ∈ ?L"
unfolding span_def
using lincomb_coordinates[OF v,symmetric] by auto
qed

lemma fin_dim[simp]: "fin_dim"
unfolding fin_dim_def
apply (intro eqTrueI exI conjI) using span_unit_vecs_is_carrier unit_vecs_carrier by auto

lemma unit_vecs_basis: "basis (set (unit_vecs n))" unfolding basis_def span_unit_vecs_is_carrier
proof (intro conjI)
show "¬ lin_dep (set (unit_vecs n))"
proof
assume "lin_dep (set (unit_vecs n))"
from this[unfolded lin_dep_def] obtain A a v where
fin: "finite A" and A: "A ⊆ set (unit_vecs n)"
and lc: "lincomb a A = 0⇩v n" and v: "v ∈ A" and av: "a v ≠ 0"
by auto
from v A obtain i where i: "i < n" and vu: "v = unit_vec n i" unfolding unit_vecs_def by auto
define b where "b = (λ x. if x ∈ A then a x else 0)"
have id: "A ∪ (set (unit_vecs n) - A) = set (unit_vecs n)" using A by auto
from lincomb_index[OF i unit_vecs_carrier]
have "lincomb b (set (unit_vecs n)) \$ i = (∑x∈ (A ∪ (set (unit_vecs n) - A)). b x * x \$ i)"
unfolding id .
also have "… = (∑x∈ A. b x * x \$ i) + (∑x∈ set (unit_vecs n) - A. b x * x \$ i)"
by (rule sum.union_disjoint, insert fin, auto)
also have "(∑x∈ A. b x * x \$ i) = (∑x∈ A. a x * x \$ i)"
by (rule sum.cong, auto simp: b_def)
also have "… = lincomb a A \$ i"
by (subst lincomb_index[OF i], insert A unit_vecs_carrier, auto)
also have "… = 0" unfolding lc using i by simp
also have "(∑x∈ set (unit_vecs n) - A. b x * x \$ i) = 0"
by (rule sum.neutral, auto simp: b_def)
finally have "lincomb b (set (unit_vecs n)) \$ i = 0" by simp
from lincomb_units[OF i, of b, unfolded this]
have "b v = 0" unfolding vu by simp
with v av show False unfolding b_def by simp
qed
qed (insert unit_vecs_carrier, auto)

lemma unit_vecs_length[simp]: "length (unit_vecs n) = n"
unfolding unit_vecs_def by auto

lemma unit_vecs_distinct: "distinct (unit_vecs n)"
unfolding distinct_conv_nth unit_vecs_length
proof (intro allI impI)
fix i j
assume *: "i < n" "j < n" "i ≠ j"
show "unit_vecs n ! i ≠ unit_vecs n ! j"
proof
assume "unit_vecs n ! i = unit_vecs n ! j"
from arg_cong[OF this, of "λ v. v \$ i"]
show False using * unfolding unit_vecs_def by auto
qed
qed

lemma dim_is_n: "dim = n"
unfolding dim_basis[OF finite_set unit_vecs_basis]
unfolding distinct_card[OF unit_vecs_distinct]
by simp

end

locale mat_space =
vec_space f_ty nc for f_ty::"'a::field itself" and nc::"nat" +
fixes nr :: "nat"
begin
abbreviation M where "M ≡ ring_mat TYPE('a) nc nr"
end

context vec_space
begin
lemma fin_dim_span:
assumes "finite A" "A ⊆ carrier V"
shows "vectorspace.fin_dim class_ring (vs (span A))"
proof -
have "vectorspace class_ring (span_vs A)"
using assms span_is_subspace subspace_def subspace_is_vs by simp
have "A ⊆ span A" using assms in_own_span by simp
have "submodule class_ring (span A) V" using assms span_is_submodule by simp
have "LinearCombinations.module.span class_ring (vs (span A)) A = carrier (vs (span A))"
using  span_li_not_depend(1)[OF ‹A ⊆ span A› ‹submodule class_ring (span A) V›] by auto
then show ?thesis unfolding vectorspace.fin_dim_def[OF ‹vectorspace class_ring (span_vs A)›]
using List.finite_set ‹A ⊆ span A› ‹vectorspace class_ring (vs (span A))›
vec_vs vectorspace.carrier_vs_is_self[OF ‹vectorspace class_ring (span_vs A)›] using assms(1) by auto
qed

lemma fin_dim_span_cols:
assumes "A ∈ carrier_mat n nc"
shows "vectorspace.fin_dim class_ring (vs (span (set (cols A))))"
using fin_dim_span cols_dim List.finite_set assms carrier_matD(1) module_vec_simps(3) by force
end

context vec_module
begin

lemma lincomb_list_as_mat_mult:
assumes "∀w ∈ set ws. dim_vec w = n"
shows "lincomb_list c ws = mat_of_cols n ws *⇩v vec (length ws) c" (is "?l ws c = ?r ws c")
proof (insert assms, induct ws arbitrary: c)
case Nil
then show ?case by (auto simp: mult_mat_vec_def scalar_prod_def)
next
case (Cons w ws)
{ fix i assume i: "i < n"
have "?l (w#ws) c = c 0 ⋅⇩v w + mat_of_cols n ws *⇩v vec (length ws) (c ∘ Suc)"
also have "… \$ i = ?r (w#ws) c \$ i"
using Cons i index_smult_vec
by (simp add: mat_of_cols_Cons_index_0 mat_of_cols_Cons_index_Suc o_def vec_Suc mult_mat_vec_def row_def length_Cons)
finally have "?l (w#ws) c \$ i = …".
}
with Cons show ?case by (intro eq_vecI, auto)
qed

assumes A: "A ⊆ carrier_vec n"
and BA: "B ⊆ A" and fin_A: "finite A"
and f: "f ∈ A → UNIV" shows "lincomb f A = lincomb f (A-B) + lincomb f B"
proof -
have "A - B ∪ B = A" using BA by auto
hence "lincomb f A = lincomb f (A - B ∪ B)"  by simp
also have "... = lincomb f (A-B) + lincomb f B"
by (rule lincomb_union, insert assms, auto intro: finite_subset)
finally show ?thesis .
qed

lemma dim_sumlist:
assumes "∀x∈set xs. dim_vec x = n"
shows "dim_vec (M.sumlist xs) = n" using assms by (induct xs, auto)

lemma sumlist_nth:
assumes "∀x∈set xs. dim_vec x = n" and "i<n"
shows "(M.sumlist xs) \$ i= sum (λj. (xs ! j) \$ i) {0..<length xs}"
using assms
proof (induct xs rule: rev_induct)
case (snoc a xs)
have [simp]: "x ∈ carrier_vec n" if x: "x∈set xs" for x
using snoc.prems x unfolding carrier_vec_def by auto
have [simp]: "a ∈ carrier_vec n"
using snoc.prems unfolding carrier_vec_def by auto
have hyp: "M.sumlist xs \$ i = (∑j = 0..<length xs. xs ! j \$ i)"
by (rule snoc.hyps, auto simp add: snoc.prems)
have "M.sumlist (xs @ [a]) = M.sumlist xs + M.sumlist [a]"
by (rule M.sumlist_append, auto simp add: snoc.prems)
also have "... = M.sumlist xs + a" by auto
also have "... \$ i = (M.sumlist xs \$ i) + (a \$ i)"
also have "... =  (∑j = 0..<length xs. xs ! j \$ i) + (a \$ i)" unfolding hyp by simp
also have "... = (∑j = 0..<length (xs @ [a]). (xs @ [a]) ! j \$ i)"
by (auto, rule sum.cong, auto simp add: nth_append)
finally show ?case .
qed auto

lemma lincomb_as_lincomb_list_distinct:
assumes s: "set ws ⊆ carrier_vec n" and d: "distinct ws"
shows "lincomb f (set ws) = lincomb_list (λi. f (ws ! i)) ws"
proof (insert assms, induct ws)
case Nil
then show ?case by auto
next
case (Cons a ws)
have [simp]: "⋀v. v ∈ set ws ⟹ v ∈ carrier_vec n" using Cons.prems(1) by auto
then have ws: "set ws ⊆ carrier_vec n" by auto
have hyp: "lincomb f (set (ws)) = lincomb_list (λi. f (ws ! i)) ws"
proof (intro Cons.hyps ws)
show "distinct ws" using Cons.prems(2) by auto
qed
have "(map (λi. f (ws ! i) ⋅⇩v ws ! i) [0..<length ws]) = (map (λv. f v ⋅⇩v v) ws)"
by (intro nth_equalityI, auto)
with ws have sumlist_rw: "sumlist (map (λi. f (ws ! i) ⋅⇩v ws ! i) [0..<length ws])
= sumlist (map (λv. f v ⋅⇩v v) ws)"
by (subst (1 2) sumlist_as_summset, auto)
have "lincomb f (set (a # ws)) = (⨁⇘V⇙v∈set (a # ws). f v ⋅⇩v v)" unfolding lincomb_def ..
also have "... = (⨁⇘V⇙v∈ insert a (set ws). f v ⋅⇩v v)" by simp
also have "... = (f a ⋅⇩v a) + (⨁⇘V⇙v∈ (set ws). f v ⋅⇩v v)"
by (rule finsum_insert, insert Cons.prems, auto)
also have "... = f a ⋅⇩v a + lincomb_list (λi. f (ws ! i)) ws" using hyp lincomb_def by auto
also have "... = f a ⋅⇩v a + sumlist (map (λv. f v ⋅⇩v v) ws)"
unfolding lincomb_list_def sumlist_rw by auto
also have "... = sumlist (map (λv. f v ⋅⇩v v) (a # ws))"
proof -
let ?a = "(map (λv. f v ⋅⇩v v) [a])"
have a: "a ∈ carrier_vec n" using Cons.prems(1) by auto
have "f a ⋅⇩v a = sumlist (map (λv. f v ⋅⇩v v) [a])" using Cons.prems(1) by auto
hence "f a ⋅⇩v a + sumlist (map (λv. f v ⋅⇩v v) ws)
= sumlist ?a + sumlist (map (λv. f v ⋅⇩v v) ws)" by simp
also have "... = sumlist (?a @ (map (λv. f v ⋅⇩v v) ws))"
by (rule sumlist_append[symmetric], auto simp add: a)
finally show ?thesis by auto
qed
also have "... = sumlist (map (λi. f ((a # ws) ! i) ⋅⇩v (a # ws) ! i) [0..<length (a # ws)])"
proof -
have u: "(map (λi. f ((a # ws) ! i) ⋅⇩v (a # ws) ! i) [0..<length (a # ws)])
= (map (λv. f v ⋅⇩v v) (a # ws))"
by (smt (verit, del_insts) length_map map_equality_iff map_nth nth_map)
show ?thesis unfolding u ..
qed
also have "... = lincomb_list (λi. f ((a # ws) ! i)) (a # ws)"
unfolding lincomb_list_def ..
finally show ?case .
qed

end

locale idom_vec = vec_module f_ty for f_ty :: "'a :: idom itself"
begin

lemma lin_dep_cols_imp_det_0':
fixes ws
defines "A ≡ mat_of_cols n ws"
assumes dimv_ws: "∀w∈set ws. dim_vec w = n"
assumes A: "A ∈ carrier_mat n n" and ld_cols: "lin_dep (set (cols A))"
shows  "det A = 0"
proof (cases "distinct ws")
case False
obtain i j where ij: "i≠j" and c: "col A i = col A j" and i: "i<n" and j: "j<n"
using False A unfolding A_def
by (metis dimv_ws distinct_conv_nth carrier_matD(2)
col_mat_of_cols mat_of_cols_carrier(3) nth_mem carrier_vecI)
show ?thesis by (rule det_identical_columns[OF A ij i j c])
next
case True
have d1[simp]: "⋀x. x ∈ set ws ⟹ x ∈ carrier_vec n" using dimv_ws by auto
obtain A' f' v where f'_in: "f' ∈ A' → UNIV"
and lc_f': "lincomb f' A' = 0⇩v n" and f'_v: "f' v ≠ 0"
and v_A': "v ∈ A'" and A'_in_rows: "A' ⊆ set (cols A)"
using ld_cols unfolding lin_dep_def by auto
define f where "f ≡ λx. if x ∉ A' then 0 else f' x"
have f_in: "f ∈ (set (cols A)) → UNIV" using f'_in by auto
have A'_in_carrier: "A' ⊆ carrier_vec n"
by (metis (no_types) A'_in_rows A_def cols_dim carrier_matD(1) mat_of_cols_carrier(1) subset_trans)
have lc_f: "lincomb f (set (cols A)) = 0⇩v n"
proof -
have l1: "lincomb f (set (cols A) - A') = 0⇩v n"
by (rule lincomb_zero, auto simp add: f_def, insert A cols_dim, blast)
have l2: "lincomb f A' = 0⇩v n " using lc_f' unfolding f_def using A'_in_carrier by auto
have "lincomb f (set (cols A)) = lincomb f (set (cols A) - A') + lincomb f A'"
show "set (cols A) ⊆ carrier_vec n"
using A cols_dim by blast
show "A' ⊆ set (cols A)"
using A'_in_rows by blast
qed auto
also have "... =  0⇩v n" using l1 l2 by auto
finally show ?thesis .
qed
have v_in: "v ∈ (set (cols A))" using v_A' A'_in_rows by auto
have fv: "f v ≠ 0" using f'_v v_A' unfolding f_def by auto
let ?c = "(λi. f (ws ! i))"
have "lincomb f (set ws) = lincomb_list ?c ws"
by (rule lincomb_as_lincomb_list_distinct[OF _ True], auto)
have "∃v.  v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ A *⇩v v = 0⇩v n"
proof (rule exI[of _ " vec (length ws) ?c"], rule conjI)
show "vec (length ws) ?c ∈ carrier_vec n" using A A_def by auto
have vec_not0: "vec (length ws) ?c ≠ 0⇩v n"
proof -
obtain i where ws_i: "(ws ! i) = v" and i: "i<length ws" using v_in unfolding A_def
by (metis d1 cols_mat_of_cols in_set_conv_nth subset_eq)
have "vec (length ws) ?c \$ i = ?c i" by (rule index_vec[OF i])
also have "... = f v" using ws_i by simp
also have "... ≠ 0" using fv by simp
finally show ?thesis
using A A_def i by fastforce
qed
have "A *⇩v vec (length ws) ?c = mat_of_cols n ws *⇩v vec (length ws) ?c" unfolding A_def ..
also have "... = lincomb_list ?c ws" by (rule lincomb_list_as_mat_mult[symmetric, OF dimv_ws])
also have "... = lincomb f (set ws)"
by (rule lincomb_as_lincomb_list_distinct[symmetric, OF _ True], auto)
also have "... =  0⇩v n"
using lc_f unfolding A_def using A by (simp add: subset_code(1))
finally show "vec (length ws) (λi. f (ws ! i)) ≠ 0⇩v n ∧ A *⇩v vec (length ws) (λi. f (ws ! i)) = 0⇩v n"
using vec_not0 by fast
qed
thus ?thesis unfolding det_0_iff_vec_prod_zero[OF A] .
qed

lemma lin_dep_cols_imp_det_0:
assumes A: "A ∈ carrier_mat n n" and ld: "lin_dep (set (cols A))"
shows "det A = 0"
proof -
have col_rw: "(cols (mat_of_cols n (cols A))) = cols A"
using A by auto
have m: "mat_of_cols n (cols A) = A" using A by auto
show ?thesis
by (rule A lin_dep_cols_imp_det_0'[of "cols A", unfolded col_rw, unfolded m, OF _ A ld])
(metis A cols_dim carrier_matD(1) subsetCE carrier_vecD)
qed

corollary lin_dep_rows_imp_det_0:
assumes A: "A ∈ carrier_mat n n" and ld: "lin_dep (set (rows A))"
shows "det A = 0"
by (subst det_transpose[OF A, symmetric], rule lin_dep_cols_imp_det_0, auto simp add: ld A)

lemma det_not_0_imp_lin_indpt_rows:
assumes A: "A ∈ carrier_mat n n" and det: "det A ≠ 0"
shows "lin_indpt (set (rows A))"
using lin_dep_rows_imp_det_0[OF A] det by auto

lemma upper_triangular_imp_lin_indpt_rows:
assumes A: "A ∈ carrier_mat n n"
and tri: "upper_triangular A"
and diag: "0 ∉ set (diag_mat A)"
shows "lin_indpt (set (rows A))"
using det_not_0_imp_lin_indpt_rows upper_triangular_imp_det_eq_0_iff assms
by auto

(* Connection from set-based to list-based *)

lemma lincomb_as_lincomb_list:
fixes ws f
assumes s: "set ws ⊆ carrier_vec n"
shows "lincomb f (set ws) = lincomb_list (λi. if ∃j<i. ws!i = ws!j then 0 else f (ws ! i)) ws"
using assms
proof (induct ws rule: rev_induct)
case (snoc a ws)
let ?f = "λi. if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)"
let ?g = "λi. (if ∃j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) ⋅⇩v (ws @ [a]) ! i"
let ?g2= "(λi. (if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)) ⋅⇩v ws ! i)"
have [simp]: "⋀v. v ∈ set ws ⟹ v ∈ carrier_vec n" using snoc.prems(1) by auto
then have ws: "set ws ⊆ carrier_vec n" by auto
have hyp: "lincomb f (set ws) = lincomb_list ?f ws"
by (intro snoc.hyps ws)
show ?case
proof (cases "a∈set ws")
case True
have g_length: "?g (length ws) = 0⇩v n" using True
by (auto, metis in_set_conv_nth nth_append)
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
by auto
also have "... = (map ?g [0..<length ws]) @ [0⇩v n]" using g_length by simp
finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [0⇩v n]" .
have "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
also have "... =  M.sumlist (map ?g [0..<length ws]) + 0⇩v n "
by (metis M.r_zero calculation hyp lincomb_closed lincomb_list_def ws)
also have "... = M.sumlist (map ?g [0..<length ws] @ [0⇩v n])"
by (rule M.sumlist_snoc[symmetric], auto simp add: nth_append)
finally have summlist_rw: "M.sumlist (map ?g2 [0..<length ws])
= M.sumlist (map ?g [0..<length ws] @ [0⇩v n])" .
have "lincomb f (set (ws @ [a])) = lincomb f (set ws)" using True unfolding lincomb_def
thus ?thesis
unfolding hyp lincomb_list_def map_rw summlist_rw
by auto
next
case False
have g_length: "?g (length ws) = f a ⋅⇩v a" using False by (auto simp add: nth_append)
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
by auto
also have "... = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" using g_length by simp
finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" .
have summlist_rw: "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
have "lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))" by auto
also have "... = (⨁⇘V⇙v∈set (a # ws). f v ⋅⇩v v)" unfolding lincomb_def ..
also have "... = (⨁⇘V⇙v∈ insert a (set ws). f v ⋅⇩v v)" by simp
also have "... = (f a ⋅⇩v a) + (⨁⇘V⇙v∈ (set ws). f v ⋅⇩v v)"
proof (rule finsum_insert)
show "finite (set ws)" by auto
show "a ∉ set ws" using False by auto
show "(λv. f v ⋅⇩v v) ∈ set ws → carrier_vec n"
using snoc.prems(1) by auto
show "f a ⋅⇩v a ∈ carrier_vec n" using snoc.prems by auto
qed
also have "... = (f a ⋅⇩v a) + lincomb f (set ws)" unfolding lincomb_def ..
also have "... = (f a ⋅⇩v a) + lincomb_list ?f ws" using hyp by auto
also have "... =  lincomb_list ?f ws  + (f a ⋅⇩v a)"
using M.add.m_comm lincomb_list_carrier snoc.prems by auto
also have "... = lincomb_list (λi. if ∃j<i. (ws @ [a]) ! i
= (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) (ws @ [a])"
proof (unfold lincomb_list_def map_rw summlist_rw, rule M.sumlist_snoc[symmetric])
show "set (map ?g [0..<length ws]) ⊆ carrier_vec n" using snoc.prems
show "f a ⋅⇩v a ∈ carrier_vec n"
using snoc.prems by auto
qed
finally show ?thesis .
qed
qed auto

lemma span_list_as_span:
assumes "set vs ⊆ carrier_vec n"
shows "span_list vs = span (set vs)"
using assms
proof (auto simp: span_list_def span_def)
fix f show "∃a A. lincomb_list f vs = lincomb a A ∧ finite A ∧ A ⊆ set vs"
using assms lincomb_list_as_lincomb by auto
next
fix f::"'a vec ⇒'a" and A assume fA: "finite A" and A: "A ⊆ set vs"
have [simp]: "x ∈ carrier_vec n" if x: "x ∈ A" for x using A x assms by auto
have [simp]:  "v ∈ carrier_vec n" if v: "v ∈ set vs" for v using assms v by auto
have set_vs_Un: "((set vs) - A) ∪ A = set vs" using A by auto
let ?f = "(λx. if x∈(set vs) - A then 0 else f x)"
have f0: "(⨁⇘V⇙v∈(set vs) - A. ?f v ⋅⇩v v) = 0⇩v n" by (rule M.finsum_all0, auto)
have "lincomb f A = lincomb ?f A"
by (auto simp add: lincomb_def intro!: finsum_cong2)
also have "... = (⨁⇘V⇙v∈(set vs) - A. ?f v ⋅⇩v v) + (⨁⇘V⇙v∈A. ?f v ⋅⇩v v)"
unfolding f0 lincomb_def by auto
also have "... = lincomb ?f (((set vs) - A) ∪ A)"
unfolding lincomb_def
by (rule M.finsum_Un_disjoint[symmetric], auto simp add: fA)
also have "... = lincomb ?f (set vs)" using set_vs_Un by auto
finally have "lincomb f A = lincomb ?f (set vs)" .
with lincomb_as_lincomb_list[OF assms]
show "∃c. lincomb f A = lincomb_list c vs" by auto
qed

lemma in_spanI[intro]:
assumes "v = lincomb a A" "finite A" "A ⊆ W"
shows "v ∈ span W"
unfolding span_def using assms by auto
lemma in_spanE:
assumes "v ∈ span W"
shows "∃ a A. v = lincomb a A ∧ finite A ∧ A ⊆ W"
using assms unfolding span_def by auto

declare in_own_span[intro]

lemma smult_in_span:
assumes "W ⊆ carrier_vec n" and insp: "x ∈ span W"
shows "c ⋅⇩v x ∈ span W"
proof -
from in_spanE[OF insp] obtain a A where a: "x = lincomb a A" "finite A" "A ⊆ W" by blast
have "c ⋅⇩v x = lincomb (λ x. c * a x) A" using a(1) unfolding lincomb_def a
apply(subst finsum_smult) using assms a by (auto simp:smult_smult_assoc)
thus "c ⋅⇩v x ∈ span W" using a(2,3) by auto
qed

lemma span_subsetI: assumes ws: "ws ⊆ carrier_vec n"
"us ⊆ span ws"
shows "span us ⊆ span ws"
by (simp add: assms(1) span_is_submodule span_is_subset subsetI ws)

end

context vec_space begin
sublocale idom_vec.

lemma sumlist_in_span: assumes W: "W ⊆ carrier_vec n"
shows "(⋀x. x ∈ set xs ⟹ x ∈ span W) ⟹ sumlist xs ∈ span W"
proof (induct xs)
case Nil
thus ?case using W by force
next
case (Cons x xs)
from span_is_subset2[OF W] Cons(2) have xs: "x ∈ carrier_vec n" "set xs ⊆ carrier_vec n" by auto
from span_add1[OF W Cons(2)[of x] Cons(1)[OF Cons(2)]]
have "x + sumlist xs ∈ span W" by auto
also have "x + sumlist xs = sumlist ([x] @ xs)"
by (subst sumlist_append, insert xs, auto)
finally show ?case by simp
qed

lemma span_span[simp]:
assumes "W ⊆ carrier_vec n"
shows "span (span W) = span W"
proof(standard,standard,goal_cases)
case (1 x) with in_spanE obtain a A where a: "x = lincomb a A" "finite A" "A ⊆ span W" by blast
from a(3) assms have AC:"A ⊆ carrier_vec n" by auto
show ?case unfolding a(1)[unfolded lincomb_def]
proof(insert a(3),atomize (full),rule finite_induct[OF a(2)],goal_cases)
case 1
then show ?case using span_zero by auto
next
case (2 x F)
{ assume F:"insert x F ⊆ span W"
hence "a x ⋅⇩v x ∈ span W" by (intro smult_in_span[OF assms],auto)
hence "a x ⋅⇩v x + (⨁⇘V⇙v∈F. a v ⋅⇩v v) ∈ span W"
using span_add1 F 2 assms by auto
hence "(⨁⇘V⇙v∈insert x F. a v ⋅⇩v v) ∈ span W"
apply(subst M.finsum_insert[OF 2(1,2)]) using F assms by auto
}
then show ?case by auto
qed
next
case 2
show ?case using assms by(intro in_own_span, auto)
qed

lemma upper_triangular_imp_basis:
assumes A: "A ∈ carrier_mat n n"
and tri: "upper_triangular A"
and diag: "0 ∉ set (diag_mat A)"
shows "basis (set (rows A))"
using upper_triangular_imp_distinct[OF assms]
using upper_triangular_imp_lin_indpt_rows[OF assms] A
by (auto intro: dim_li_is_basis simp: distinct_card dim_is_n set_rows_carrier)

lemma fin_dim_span_rows:
assumes A: "A ∈ carrier_mat nr n"
shows "vectorspace.fin_dim class_ring (vs (span (set (rows A))))"
proof (rule fin_dim_span)
show "set (rows A) ⊆ carrier V" using A rows_carrier[of A] unfolding carrier_mat_def by auto
show "finite (set (rows A))" by auto
qed

definition "row_space B = span (set (rows B))"
definition "col_space B = span (set (cols B))"

lemma row_space_eq_col_space_transpose:
shows "row_space A = col_space A⇧T"
unfolding col_space_def row_space_def cols_transpose ..

lemma col_space_eq_row_space_transpose:
shows "col_space A = row_space A⇧T"
unfolding col_space_def row_space_def Matrix.rows_transpose ..

lemma col_space_eq:
assumes A: "A ∈ carrier_mat n nc"
shows "col_space A = {y∈carrier_vec (dim_row A). ∃x∈carrier_vec (dim_col A). A *⇩v x = y}"
proof -
let ?ws = "cols A"
have set_cols_in: "set (cols A) ⊆ carrier_vec n" using A unfolding cols_def by auto
have "lincomb f S ∈ carrier_vec (dim_row A)" if "finite S" and S: "S ⊆ set (cols A)" for f S
using lincomb_closed A
by (metis (full_types) S carrier_matD(1) cols_dim lincomb_closed subsetCE subsetI)
moreover have "∃x∈carrier_vec (dim_col A). A *⇩v x = lincomb f S"
if fin_S: "finite S" and S: "S ⊆ set (cols A)" for f S
proof -
let ?g = "(λv. if v ∈ S then f v else 0)"
let ?g' = "(λi. if ∃j<i. ?ws ! i = ?ws ! j then 0 else ?g (?ws ! i))"
let ?Z = "set ?ws - S"
have union: "set ?ws = S ∪ ?Z" using S by auto
have inter: "S ∩ ?Z = {}" by auto
have "lincomb f S = lincomb ?g S" by (rule lincomb_cong, insert set_cols_in A S, auto)
also have "... = lincomb ?g (S ∪ ?Z)"
by (rule lincomb_clean[symmetric],insert set_cols_in A S fin_S, auto)
also have "... = lincomb ?g (set ?ws)" using union by auto
also have "... = lincomb_list ?g' ?ws"
by (rule lincomb_as_lincomb_list[OF set_cols_in])
also have "... = mat_of_cols n ?ws *⇩v vec (length ?ws) ?g'"
by (rule lincomb_list_as_mat_mult, insert set_cols_in A, auto)
also have "... = A *⇩v (vec (length ?ws) ?g')" using mat_of_cols_cols A by auto
finally show ?thesis by auto
qed
moreover have "∃f S. A *⇩v x = lincomb f S ∧ finite S ∧ S ⊆ set (cols A)"
if Ax: "A *⇩v x ∈ carrier_vec (dim_row A)" and x: "x ∈ carrier_vec (dim_col A)" for x
proof -
let ?c = "λi. x \$ i"
have x_vec: "vec (length ?ws) ?c = x" using x by auto
have "A *⇩v x = mat_of_cols n ?ws *⇩v vec (length ?ws) ?c" using mat_of_cols_cols A x_vec by auto
also have "... = lincomb_list ?c ?ws"
by (rule lincomb_list_as_mat_mult[symmetric], insert set_cols_in A, auto)
also have "... = lincomb (mk_coeff ?ws ?c) (set ?ws)"
by (rule lincomb_list_as_lincomb, insert set_cols_in A, auto)
finally show ?thesis by auto
qed
ultimately show ?thesis unfolding col_space_def span_def by auto
qed

lemma vector_space_row_space:
assumes A: "A ∈ carrier_mat nr n"
shows "vectorspace class_ring (vs (row_space A))"
proof -
have fin: "finite (set (rows A))" by auto
have s: "set (rows A) ⊆ carrier V" using A unfolding rows_def by auto
have "span_vs (set (rows A)) = vs (span (set (rows A)))" by auto
moreover have "vectorspace class_ring (span_vs (set (rows A)))"
using fin s span_is_subspace subspace_def subspace_is_vs by simp
ultimately show ?thesis unfolding row_space_def by auto
qed

lemma row_space_eq:
assumes A: "A ∈ carrier_mat nr n"
shows "row_space A = {w∈carrier_vec (dim_col A). ∃y∈carrier_vec (dim_row A). A⇧T *⇩v y = w}"
using A col_space_eq unfolding row_space_eq_col_space_transpose by auto

lemma row_space_is_preserved:
assumes inv_P: "invertible_mat P" and P: "P ∈ carrier_mat m m" and A: "A ∈ carrier_mat m n"
shows "row_space (P*A) = row_space A"
proof -
have At: "A⇧T ∈ carrier_mat n m" using A by auto
have Pt: "P⇧T ∈ carrier_mat m m" using P by auto
have PA: "P*A ∈ carrier_mat m n" using P A by auto
have "w ∈ row_space A" if w: "w ∈ row_space (P*A)" for w
proof -
have w_carrier: "w ∈ carrier_vec (dim_col (P*A))"
using w mult_carrier_mat[OF P A] row_space_eq by auto
from that and this obtain y where y: "y ∈ carrier_vec (dim_row (P * A))"
and w_By: "w = (P*A)⇧T *⇩v y" unfolding row_space_eq[OF PA] by blast
have ym: "y ∈ carrier_vec m" using y Pt by auto
have "w=((P*A)⇧T) *⇩v y" using w_By .
also have "... = (A⇧T * P⇧T) *⇩v y" using transpose_mult[OF P A] by auto
also have "... = A⇧T *⇩v (P⇧T *⇩v y)" by (rule assoc_mult_mat_vec[OF At Pt], insert Pt y, auto)
finally show "w ∈ row_space A" unfolding row_space_eq[OF A] using At Pt ym by auto
qed
moreover have "w ∈ row_space (P*A)" if w: "w ∈ row_space A" for w
proof -
have w_carrier: "w ∈ carrier_vec (dim_col A)" using w A unfolding row_space_eq[OF A] by auto
obtain P' where PP': "inverts_mat P P'" and P'P: "inverts_mat P' P"
using inv_P P unfolding invertible_mat_def by blast
have P': "P' ∈ carrier_mat m m" using PP' P'P P unfolding inverts_mat_def
by (metis carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_one_mat(3))
from that obtain y where y: "y ∈ carrier_vec (dim_row A)" and
w_Ay: "w = A⇧T *⇩v y" unfolding row_space_eq[OF A] by blast
have Py: "(P'⇧T *⇩v y) ∈ carrier_vec m" using P' y A by auto
have "w = A⇧T *⇩v y" using w_Ay .
also have "... = ((P' * P)*A)⇧T *⇩v y"
using P'P left_mult_one_mat A P' unfolding inverts_mat_def by auto
also have "... = ((P' * (P*A))⇧T) *⇩v y" using assoc_mult_mat_vec P' P A by auto
also have "... = ((P*A)⇧T * P'⇧T) *⇩v y" using transpose_mult P A P' mult_carrier_mat by metis
also have "... = (P*A)⇧T *⇩v (P'⇧T *⇩v y)" using A P' PA y by auto
finally show "w ∈ row_space (P*A)"
unfolding row_space_eq[OF PA]
using Py w_carrier A P by fastforce
qed
ultimately show ?thesis by auto
qed

end

context vec_module begin

lemma R_sumlist[simp]: "R.sumlist = sum_list"
proof (intro ext)
fix xs
show "R.sumlist xs = sum_list xs" by (induct xs, auto)
qed

lemma sumlist_dim: assumes "⋀ x. x ∈ set xs ⟹ x ∈ carrier_vec n"
shows "dim_vec (sumlist xs) = n"
using sumlist_carrier assms
by fastforce

lemma sumlist_vec_index: assumes "⋀ x. x ∈ set xs ⟹ x ∈ carrier_vec n"
and "i < n"
shows "sumlist xs \$ i = sum_list (map (λ x. x \$ i) xs)"
unfolding M.sumlist_def using assms(1) proof(induct xs)
case (Cons a xs)
hence cond:"⋀ x. x ∈ set xs ⟹ x ∈ carrier_vec n" by auto
from Cons(1)[OF cond] have IH:"foldr (+) xs (0⇩v n) \$ i = (∑x←xs. x \$ i)" by auto
have "(a + foldr (+) xs (0⇩v n)) \$ i = a \$ i + (∑x←xs. x \$ i)"
using sumlist_dim[OF cond,unfolded M.sumlist_def] assms by auto
then show ?case by auto next
case Nil thus ?case using assms by auto
qed

lemma scalar_prod_left_sum_distrib:
assumes vs: "⋀ v. v ∈ set vvs ⟹ v ∈ carrier_vec n" and w: "w ∈ carrier_vec n"
shows "sumlist vvs ∙ w = sum_list (map (λ v. v ∙ w) vvs)"
using vs
proof (induct vvs)
case (Cons v vs)
from Cons have v: "v ∈ carrier_vec n" and vs: "sumlist vs ∈ carrier_vec n"
by (auto intro!: sumlist_carrier)
have "sumlist (v # vs) ∙ w = sumlist ([v] @ vs) ∙ w " by auto
also have "… = (v + sumlist vs) ∙ w"
by (subst sumlist_append, insert Cons v vs, auto)
also have "… = v ∙ w + (sumlist vs ∙ w)"
by (rule add_scalar_prod_distrib[OF v vs w])
finally show ?case using Cons by auto
qed (insert w, auto)

lemma scalar_prod_right_sum_distrib:
assumes vs: "⋀ v. v ∈ set vvs ⟹ v ∈ carrier_vec n" and w: "w ∈ carrier_vec n"
shows "w ∙ sumlist vvs = sum_list (map (λ v. w ∙ v) vvs)"
by (subst comm_scalar_prod[OF w sumlist_carrier], insert vs w, force,
subst scalar_prod_left_sum_distrib[OF vs w], force,
rule arg_cong[of _ _ sum_list], rule nth_equalityI,
auto simp: set_conv_nth intro!: comm_scalar_prod)

lemma lincomb_list_add_vec_2: assumes us: "set us ⊆ carrier_vec n"
and x: "x = lincomb_list lc (us [i := us ! i + c ⋅⇩v us ! j])"
and i: "j < length us" "i < length us" "i ≠ j"
shows "x = lincomb_list (lc (j := lc j + lc i * c)) us" (is "_ = ?x")
proof -
let ?xx = "lc j + lc i * c"
let ?i = "us ! i"
let ?j = "us ! j"
let ?v = "?i + c ⋅⇩v ?j"
let ?ws = "us [i := us ! i + c ⋅⇩v us ! j]"
from us have usk: "k < length us ⟹ us ! k ∈ carrier_vec n" for k by auto
from usk i have ij: "?i ∈ carrier_vec n" "?j ∈ carrier_vec n" by auto
hence v: "c ⋅⇩v ?j ∈ carrier_vec n" "?v ∈ carrier_vec n" by auto
with us have ws: "set ?ws ⊆ carrier_vec n" unfolding set_conv_nth using i
by (auto, rename_tac k, case_tac "k = i", auto)
from us have us': "∀w∈set us. dim_vec w = n" by auto
from ws have ws': "∀w∈set ?ws. dim_vec w = n" by auto
have mset: "mset_set {0..<length us} = {#i#} + {#j#} + (mset_set ({0..<length us} - {i,j}))"
by (rule multiset_eqI, insert i, auto, rename_tac x, case_tac "x ∈ {0 ..< length us}", auto)
define M2 where "M2 = M.summset
{#lc ia ⋅⇩v ?ws ! ia. ia ∈# mset_set ({0..<length us} - {i, j})#}"
define M1 where "M1 = M.summset {#(if i = j then ?xx else lc i) ⋅⇩v us ! i. i ∈# mset_set ({0..<length us} - {i, j})#}"
have M1: "M1 ∈ carrier_vec n" unfolding M1_def using usk by fastforce
have M2: "M1 = M2" unfolding M2_def M1_def
by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto)
have x1: "x = lc j ⋅⇩v ?j + (lc i ⋅⇩v ?i + lc i ⋅⇩v (c ⋅⇩v ?j) + M1)"
unfolding x lincomb_list_def M2 M2_def
apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk,
have x2: "?x = ?xx ⋅⇩v ?j + (lc i ⋅⇩v ?i + M1)"
unfolding x lincomb_list_def M1_def
apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk,
show ?thesis unfolding x1 x2 using M1 ij
by (intro eq_vecI, auto simp: field_simps)
qed

lemma lincomb_list_add_vec_1: assumes us: "set us ⊆ carrier_vec n"
and x: "x = lincomb_list lc us"
and i: "j < length us" "i < length us" "i ≠ j"
shows "x = lincomb_list (lc (j := lc j - lc i * c)) (us [i := us ! i + c ⋅⇩v us ! j])" (is "_ = ?x")
proof -
let ?i = "us ! i"
let ?j = "us ! j"
let ?v = "?i + c ⋅⇩v ?j"
let ?ws = "us [i := us ! i + c ⋅⇩v us ! j]"
from us have usk: "k < length us ⟹ us ! k ∈ carrier_vec n" for k by auto
from usk i have ij: "?i ∈ carrier_vec n" "?j ∈ carrier_vec n" by auto
hence v: "c ⋅⇩v ?j ∈ carrier_vec n" "?v ∈ carrier_vec n" by auto
with us have ws: "set ?ws ⊆ carrier_vec n" unfolding set_conv_nth using i
by (auto, rename_tac k, case_tac "k = i", auto)
from us have us': "∀w∈set us. dim_vec w = n" by auto
from ws have ws': "∀w∈set ?ws. dim_vec w = n" by auto
have mset: "mset_set {0..<length us} = {#i#} + {#j#} + (mset_set ({0..<length us} - {i,j}))"
by (rule multiset_eqI, insert i, auto, rename_tac x, case_tac "x ∈ {0 ..< length us}", auto)
define M2 where "M2 = M.summset
{#(if ia = j then lc j - lc i * c else lc ia) ⋅⇩v ?ws ! ia
. ia ∈# mset_set ({0..<length us} - {i, j})#}"
define M1 where "M1 = M.summset {#lc i ⋅⇩v us ! i. i ∈# mset_set ({0..<length us} - {i, j})#}"
have M1: "M1 ∈ carrier_vec n" unfolding M1_def using usk by fastforce
have M2: "M1 = M2" unfolding M2_def M1_def
by (rule arg_cong[of _ _ M.summset], rule multiset.map_cong0, insert i usk, auto)
have x1: "x = lc j ⋅⇩v ?j + (lc i ⋅⇩v ?i + M1)"
unfolding x lincomb_list_def M1_def
apply (subst sumlist_as_summset, (insert us ws i v ij, auto simp: set_conv_nth)[1], insert i ij v us ws usk,