Theory DL_Rank

theory DL_Rank
imports VS_Connect DL_Missing_List
(* Author: Alexander Bentkamp, Universit├Ąt des Saarlandes
*)
section ‹Matrix Rank›

theory DL_Rank
imports VS_Connect DL_Missing_List
 Determinant
 Missing_VectorSpace
begin

lemma (in vectorspace) full_dim_span:
assumes "S ⊆ carrier V"
and "finite S"
and "vectorspace.dim K (span_vs S) = card S"
shows "lin_indpt S"
proof -
  have "vectorspace K (span_vs S)"
    using field.field_axioms vectorspace_def submodule_is_module[OF span_is_submodule[OF assms(1)]] by metis
  have "S ⊆ carrier (span_vs S)"  by (simp add: assms(1) in_own_span)
  have "LinearCombinations.module.span K (vs (span S)) S = carrier (vs (span S))"
    using module.span_li_not_depend[OF _ span_is_submodule[OF assms(1)]]
    by (simp add: assms(1) in_own_span)
  have "vectorspace.basis K (vs (span S)) S"
    using vectorspace.dim_gen_is_basis[OF ‹vectorspace K (span_vs S)› ‹finite S› ‹S ⊆ carrier (span_vs S)›
     ‹LinearCombinations.module.span K (vs (span S)) S = carrier (vs (span S))›]  ‹vectorspace.dim K (span_vs S) = card S›
    by simp
  then have "LinearCombinations.module.lin_indpt K (vs (span S)) S"
    using vectorspace.basis_def[OF ‹vectorspace K (span_vs S)›] by blast
  then show ?thesis using module.span_li_not_depend[OF _ span_is_submodule[OF assms(1)]]
    by (simp add: assms(1) in_own_span)
qed

lemma (in vectorspace) dim_span:
assumes "S ⊆ carrier V"
and "finite S"
and "maximal U (λT. T ⊆ S ∧ lin_indpt T)"
shows "vectorspace.dim K (span_vs S) = card U"
proof -
  have "lin_indpt U" "U ⊆ S" by (metis assms(3) maximal_def)+
  then have "U ⊆ span S" using in_own_span[OF assms(1)] by blast
  then have lin_indpt: "LinearCombinations.module.lin_indpt K (span_vs S) U"
    using module.span_li_not_depend(2)[OF ‹U ⊆ span S›] ‹lin_indpt U› assms(1) span_is_submodule by blast
  have "span U = span S"
  proof (rule ccontr)
    assume "span U ≠ span S"
    have "span U ⊆ span S" using span_is_monotone ‹U⊆S› by metis
    then have "¬ S ⊆ span U" by (meson ‹U ⊆ S› ‹span U ≠ span S› assms(1) span_is_submodule
      span_is_subset subset_antisym subset_trans)
    then obtain s where "s∈S" "s ∉ span U" by blast
    then have "lin_indpt (U∪{s})" using lindep_span
      by (meson ‹U ⊆ S› ‹lin_indpt U› assms(1) lin_dep_iff_in_span rev_subsetD span_mem subset_trans)
    have "s∉U" using ‹U ⊆ S› ‹s ∉ span U› assms(1) span_mem by auto
    then have "(U∪{s}) ⊆ S ∧ lin_indpt (U∪{s})" using ‹U ⊆ S› ‹lin_indpt (U ∪ {s})› ‹s ∈ S› by auto
    then have "¬maximal U (λT. T ⊆ S ∧ lin_indpt T)"
      unfolding maximal_def using Un_subset_iff ‹s ∉ U› insert_subset  order_refl by auto
    then show False using assms by metis
  qed
  then have span:"LinearCombinations.module.span K (vs (span S)) U = span S"
    using module.span_li_not_depend[OF ‹U ⊆ span S›]
    by (simp add: LinearCombinations.module.span_is_submodule assms(1) module_axioms)
  have "vectorspace K (vs (span S))"
    using field.field_axioms vectorspace_def submodule_is_module[OF span_is_submodule[OF assms(1)]] by metis
  then have "vectorspace.basis K (vs (span S)) U" using vectorspace.basis_def[OF ‹vectorspace K (vs (span S))›]
    by (simp add: span ‹U ⊆ span S› lin_indpt)
  then show ?thesis
    using ‹U ⊆ S› ‹vectorspace K (vs (span S))› assms(2) infinite_super vectorspace.dim_basis by blast
qed

definition (in vec_space) rank ::"'a mat ⇒ nat"
where "rank A = vectorspace.dim class_ring (span_vs (set (cols A)))"

lemma (in vec_space) rank_card_indpt:
assumes "A ∈ carrier_mat n nc"
assumes "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
shows "rank A = card S"
proof -
  have "set (cols A) ⊆ carrier_vec n" using cols_dim assms(1) by blast
  have "finite (set (cols A))" by blast
  show ?thesis using dim_span[OF ‹set (cols A) ⊆ carrier_vec n› ‹finite (set (cols A))› assms(2)]
    unfolding rank_def by blast
qed

lemma maximal_exists_superset:
  assumes "finite S"
  assumes maxc: "⋀A. P A ⟹ A ⊆ S" and "P B"
  shows "∃A. finite A ∧ maximal A P ∧ B ⊆ A"
proof -
  have "finite (S-B)" using assms(1) assms(3) infinite_super maxc by blast
  then show ?thesis using ‹P B›
  proof (induction "S-B" arbitrary:B rule: finite_psubset_induct)
    case (psubset B)
    then show ?case
    proof (cases "maximal B P")
      case True
      then show ?thesis using order_refl psubset.hyps by (metis assms(1) maxc psubset.prems rev_finite_subset)
    next
      case False
      then obtain B' where "B ⊂ B'" "P B'" using maximal_def psubset.prems by (metis dual_order.order_iff_strict)
      then have "B' ⊆ S" "B ⊆ S" using maxc ‹P B› by auto
      then have "S - B' ⊂ S - B" using ‹B ⊂ B'› by blast
      then show ?thesis using psubset(2)[OF ‹S - B' ⊂ S - B› ‹P B'›] using ‹B ⊂ B'› by fast
    qed
  qed
qed

lemma (in vec_space) rank_ge_card_indpt:
assumes "A ∈ carrier_mat n nc"
assumes "U ⊆ set (cols A)"
assumes "lin_indpt U"
shows "rank A ≥ card U"
proof -
  obtain S where "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)" "U⊆S" "finite S"
    using maximal_exists_superset[of "set (cols A)" "(λT. T ⊆ set (cols A) ∧ lin_indpt T)" U]
    using List.finite_set assms(2) assms(3) maximal_exists_superset by blast
  then show ?thesis
    unfolding rank_card_indpt[OF ‹A ∈ carrier_mat n nc› ‹maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)›]
    using card_mono by blast
qed

lemma (in vec_space) lin_indpt_full_rank:
assumes "A ∈ carrier_mat n nc"
assumes "distinct (cols A)"
assumes "lin_indpt (set (cols A))"
shows "rank A = nc"
proof -
  have "maximal (set (cols A)) (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
    by (simp add: assms(3) maximal_def subset_antisym)
  then have "rank A = card (set (cols A))" using assms(1) vec_space.rank_card_indpt by blast
  then show ?thesis using assms(1) assms(2) distinct_card by fastforce
qed

lemma (in vec_space) rank_le_nc:
assumes "A ∈ carrier_mat n nc"
shows "rank A ≤ nc"
proof -
  obtain S where "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
    using maximal_exists[of "(λT. T ⊆ set (cols A) ∧ lin_indpt T)" "card (set (cols A))" "{}"]
    by (meson List.finite_set card_mono empty_iff empty_subsetI finite_lin_indpt2 rev_finite_subset)
  then have "card S ≤ card (set (cols A))" by (simp add: card_mono maximal_def)
  then have "card S ≤ nc"
    using assms(1) cols_length card_length carrier_matD(2) by (metis dual_order.trans)
  then show ?thesis
    using rank_card_indpt[OF ‹A ∈ carrier_mat n nc› ‹maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)›]
    by simp
qed

lemma (in vec_space) full_rank_lin_indpt:
assumes "A ∈ carrier_mat n nc"
assumes "rank A = nc"
assumes "distinct (cols A)"
shows "lin_indpt (set (cols A))"
proof -
  have 1:"set (cols A) ⊆ carrier_vec n" using assms(1) cols_dim by blast
  have 2:"finite (set (cols A))" by simp
  have "card (set (cols A)) = nc"
    using assms(1) assms(3) distinct_card by fastforce
  have 3:"vectorspace.dim class_ring (span_vs (set (cols A))) = card (set (cols A))"
    using ‹rank A = nc›[unfolded rank_def]
    using assms(1) assms(3) distinct_card by fastforce
  show ?thesis using full_dim_span[OF 1 2 3] .
qed


lemma (in vec_space) mat_mult_eq_lincomb:
assumes "A ∈ carrier_mat n nc"
assumes "distinct (cols A)"
shows "A *v (vec nc (λi. a (col A i))) = lincomb a (set (cols A))"
proof (rule eq_vecI)
  have "finite (set (cols A))" using assms(1) by simp
  then show "dim_vec (A *v (vec nc (λi. a (col A i)))) = dim_vec (lincomb a (set (cols A)))"
    using assms cols_dim vec_space.lincomb_dim by (metis dim_mult_mat_vec carrier_matD(1))
  fix i assume "i < dim_vec (lincomb a (set (cols A)))"
  then have "i < n" using ‹dim_vec (A *v (vec nc (λi. a (col A i)))) = dim_vec (lincomb a (set (cols A)))› assms by auto
  have "set (cols A) ⊆ carrier_vec n" using cols_dim ‹A ∈ carrier_mat n nc› carrier_matD(1) by blast
  have "bij_betw (nth (cols A)) {..<length (cols A)} (set (cols A))"
    unfolding bij_betw_def by (rule conjI, simp add: inj_on_nth ‹distinct (cols A)›;
    metis subset_antisym in_set_conv_nth lessThan_iff rev_image_eqI subsetI
    image_subsetI lessThan_iff nth_mem)
  then have " (∑x∈set (cols A). a x * x $ i) =
    (∑j∈{..<length (cols A)}. a (cols A ! j) * (cols A ! j) $ i)"
    using bij_betw_imp_surj_on bij_betw_imp_inj_on by (metis (no_types, lifting) sum.reindex_cong)
  also have "... = (∑j∈{..<length (cols A)}. a (col A j) * (cols A ! j) $ i)"
    using assms(1) assms(2) find_first_unique[OF ‹distinct (cols A)›] ‹i < n› by auto
  also have "... = (∑j∈{..<length (cols A)}. (cols A ! j) $ i * a (col A j))" by (metis mult_commute_abs)
  also have "... = (∑j∈{..<length (cols A)}. row A i $ j * a (col A j))" using ‹i < n› assms(1) assms(2) by auto
  finally show "(A *v (vec nc (λi. a (col A i)))) $ i = lincomb a (set (cols A)) $ i"
    unfolding lincomb_index[OF ‹i < n› ‹set (cols A) ⊆ carrier_vec n›]
    unfolding mult_mat_vec_def scalar_prod_def
    using ‹i < n› assms(1) atLeast0LessThan lessThan_def carrier_matD(1) index_vec sum.cong by auto
qed

lemma (in vec_space) lincomb_eq_mat_mult:
assumes "A ∈ carrier_mat n nc"
assumes "v ∈ carrier_vec nc"
assumes "distinct (cols A)"
shows "lincomb (λa. v $ find_first a (cols A)) (set (cols A)) = (A *v v)"
proof -
  have "⋀i. i < nc ⟹ find_first (col A i) (cols A) = i"
    using assms(1) assms(3) find_first_unique by fastforce
  then have "vec nc (λi. v $ find_first (col A i) (cols A)) = v"
    using assms(2) by auto
  then show ?thesis
    using mat_mult_eq_lincomb[where a = "(λa. v $ find_first a (cols A))", OF assms(1) assms(3)] by auto
qed

lemma (in vec_space) lin_depI:
assumes "A ∈ carrier_mat n nc"
assumes "v ∈ carrier_vec nc" "v ≠ 0v nc" "A *v v = 0v n"
assumes "distinct (cols A)"
shows "lin_dep (set (cols A))"
proof -
  have 1: "finite (set (cols A))" by simp
  have 2: "set (cols A) ⊆ set (cols A)" by auto
  have 3: "(λa. v $ find_first a (cols A)) ∈ set (cols A) → UNIV" by simp
  obtain i where "v $ i ≠ 0" "i < nc"
    using ‹v ≠ 0v nc›
    by (metis assms(2) dim_vec carrier_vecD vec_eq_iff zero_vec_def index_zero_vec(1))
  then have "i < dim_col A" using assms(1) by blast
  have 4:"col A i ∈ set (cols A)"
    using cols_nth[OF ‹i < dim_col A›] ‹i < dim_col A› in_set_conv_nth by fastforce
  have 5:"v $ find_first (col A i) (cols A) ≠ 0"
    using find_first_unique[OF ‹distinct (cols A)›] cols_nth[OF ‹i < dim_col A›] ‹i < nc› ‹v $ i ≠ 0›
    assms(1) by auto
  have 6:"lincomb (λa. v $ find_first a (cols A)) (set (cols A)) = 0v n"
    using assms(1) assms(2) assms(4) assms(5) lincomb_eq_mat_mult by auto
  show ?thesis using lin_dep_crit[OF 1 2 _ 4 5 6] by metis
qed

lemma (in vec_space) lin_depE:
assumes "A ∈ carrier_mat n nc"
assumes "lin_dep (set (cols A))"
assumes "distinct (cols A)"
obtains v where "v ∈ carrier_vec nc" "v ≠ 0v nc" "A *v v = 0v n"
proof -
  have "finite (set (cols A))" by simp
  obtain a w where "a ∈ set (cols A) → UNIV" "lincomb a (set (cols A)) = 0v n" "w ∈ set (cols A)" "a w ≠ 0"
    using finite_lin_dep[OF ‹finite (set (cols A))› ‹lin_dep (set (cols A))›]
    using assms(1) cols_dim carrier_matD(1) by blast
  define v where "v = vec nc (λi. a (col A i))"
  have 1:"v ∈ carrier_vec nc" by (simp add: v_def)
  have 2:"v ≠ 0v nc"
  proof -
    obtain i where "w = col A i" "i < length (cols A)"
      by (metis ‹w ∈ set (cols A)› cols_length cols_nth in_set_conv_nth)
    have "v $ i ≠ 0"
      unfolding v_def
      using ‹a w ≠ 0›[unfolded ‹w = col A i›] index_vec[OF ‹i < length (cols A)›]
      assms(1) cols_length carrier_matD(2) by (metis (no_types) ‹A ∈ carrier_mat n nc›
      ‹⋀f. vec (length (cols A)) f $ i = f i› ‹a (col A i) ≠ 0› cols_length carrier_matD(2))
    then show ?thesis using ‹i < length (cols A)› assms(1) by auto
  qed
  have 3:"A *v v = 0v n" unfolding v_def
    using ‹lincomb a (set (cols A)) = 0v n› mat_mult_eq_lincomb[OF ‹A ∈ carrier_mat n nc› ‹distinct (cols A)›] by auto
  show thesis using 1 2 3 by (simp add: that)
qed

lemma (in vec_space) non_distinct_low_rank:
assumes "A ∈ carrier_mat n n"
and "¬ distinct (cols A)"
shows "rank A < n"
proof -
  obtain S where "maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)"
    using maximal_exists[of "(λT. T ⊆ set (cols A) ∧ lin_indpt T)" "card (set (cols A))" "{}"]
    by (meson List.finite_set card_mono empty_iff empty_subsetI finite_lin_indpt2 rev_finite_subset)
  then have "card S ≤ card (set (cols A))" by (simp add: card_mono maximal_def)
  then have "card S < n"
    using assms(1) cols_length card_length ‹¬ distinct (cols A)› card_distinct carrier_matD(2) nat_less_le
    by (metis dual_order.antisym dual_order.trans)
  then show ?thesis
    using rank_card_indpt[OF ‹A ∈ carrier_mat n n› ‹maximal S (λT. T ⊆ set (cols A) ∧ lin_indpt T)›]
    by simp
qed

text ‹The theorem "det non-zero $\longleftrightarrow$ full rank" is practically proven in det\_0\_iff\_vec\_prod\_zero\_field,
but without an actual definition of the rank.›

lemma (in vec_space) det_zero_low_rank:
assumes "A ∈ carrier_mat n n"
and "det A = 0"
shows "rank A < n"
proof (rule ccontr)
  assume "¬ rank A < n"
  then have "rank A = n" using rank_le_nc assms le_neq_implies_less by blast
  obtain v where "v ∈ carrier_vec n" "v ≠ 0v n" "A *v v = 0v n"
    using det_0_iff_vec_prod_zero_field[OF assms(1)] assms(2) by blast
  then show False
  proof (cases "distinct (cols A)")
    case True
    then have "lin_indpt (set (cols A))" using full_rank_lin_indpt using ‹rank A = n› assms(1) by auto
    then show False using lin_depI[OF assms(1) ‹v ∈ carrier_vec n› ‹v ≠ 0v n› ‹A *v v = 0v n›] True by blast
  next
    case False
    then show False using non_distinct_low_rank ‹rank A = n› ‹¬ rank A < n› assms(1) by blast
  qed
qed

lemma det_identical_cols:
  assumes A: "A ∈ carrier_mat n n"
    and ij: "i ≠ j"
    and i: "i < n" and j: "j < n"
    and r: "col A i = col A j"
  shows "det A = 0"
  using det_identical_rows det_transpose
  by (metis A i ij j carrier_matD(2) transpose_carrier_mat r row_transpose)

lemma (in vec_space) low_rank_det_zero:
assumes "A ∈ carrier_mat n n"
and "det A ≠ 0"
shows "rank A = n"
proof -
  have "distinct (cols A)"
  proof (rule ccontr)
    assume "¬ distinct (cols A)"
    then obtain i j where "i≠j" "(cols A) ! i = (cols A) ! j" "i<length (cols A)" "j<length (cols A)"
      using distinct_conv_nth by blast
    then have "col A i = col A j" "i<n" "j<n" using assms(1) by auto
    then have "det A = 0"  using det_identical_cols using ‹i ≠ j› assms(1) by blast
    then show False using ‹det A ≠ 0› by auto
  qed
  have "⋀v. v ∈ carrier_vec n ⟹ v ≠ 0v n ⟹ A *v v ≠ 0v n"
    using det_0_iff_vec_prod_zero_field[OF assms(1)] assms(2) by auto
  then have "lin_indpt (set (cols A))" using lin_depE[OF assms(1) _ ‹distinct (cols A)›] by auto
  then show ?thesis using lin_indpt_full_rank[OF assms(1) ‹distinct (cols A)›] by metis
qed

lemma (in vec_space) det_rank_iff:
assumes "A ∈ carrier_mat n n"
shows "det A ≠ 0 ⟷ rank A = n"
  using assms det_zero_low_rank low_rank_det_zero by force

section "Subadditivity of rank"

text ‹Subadditivity is the property of rank, that rank (A + B) <= rank A + rank B.›

lemma (in Module.module) lincomb_add:
assumes "finite (b1 ∪ b2)"
assumes "b1 ∪ b2 ⊆ carrier M"
assumes "x1 = lincomb a1 b1" "a1∈ (b1→carrier R)"
assumes "x2 = lincomb a2 b2" "a2∈ (b2→carrier R)"
assumes "x = x1 ⊕M x2"
shows "lincomb (λv. (λv. if v ∈ b1 then a1 v else 𝟬) v ⊕ (λv. if v ∈ b2 then a2 v else 𝟬) v) (b1 ∪ b2) = x"
proof -
  have "finite (b1 ∪ (b2-b1))" "finite (b2 ∪ (b1-b2))"
       "b1 ∪ (b2 - b1) ⊆ carrier M" "b2 ∪ (b1-b2) ⊆ carrier M"
       "b1 ∩ (b2 - b1) = {}" "b2 ∩ (b1 - b2) = {}"
       "(λb. 𝟬R) ∈ b2 - b1 → carrier R" "(λb. 𝟬R) ∈ b1 - b2 → carrier R"
    using ‹finite (b1 ∪ b2)› ‹b1 ∪ b2 ⊆ carrier M› ‹a2∈ (b2→carrier R)› by auto
  have "lincomb (λb. 𝟬R) (b2 - b1) = 𝟬M" "lincomb (λb. 𝟬R) (b1 - b2) = 𝟬M"
    unfolding lincomb_def using M.finsum_all0 assms(2) lmult_0 subset_iff
    by (metis (no_types, lifting) Un_Diff_cancel2 inf_sup_aci(5) le_sup_iff)+
  then have "x1 = lincomb (λv. if v ∈ b1 then a1 v else 𝟬) (b1 ∪ b2)"
            "x2 = lincomb (λv. if v ∈ b2 then a2 v else 𝟬) (b1 ∪ b2)"
    using lincomb_union2[OF ‹finite (b1 ∪ (b2-b1))› ‹b1 ∪ (b2 - b1) ⊆ carrier M› ‹b1 ∩ (b2 - b1) = {}› ‹a1∈ (b1→carrier R)› ‹(λb. 𝟬R) ∈ b2 - b1 → carrier R›]
          lincomb_union2[OF ‹finite (b2 ∪ (b1-b2))› ‹b2 ∪ (b1-b2) ⊆ carrier M› ‹b2 ∩ (b1 - b2) = {}› ‹a2∈ (b2→carrier R)› ‹(λb. 𝟬R) ∈ b1 - b2 → carrier R›]
    using assms(2) assms(3) assms(4)  assms(5)  assms(6) by (simp_all add:Un_commute)
  have "(λv. if v ∈ b1 then a1 v else 𝟬) ∈ (b1 ∪ b2) → carrier R"
       "(λv. if v ∈ b2 then a2 v else 𝟬) ∈ (b1 ∪ b2) → carrier R" using assms(4) assms(6) by auto
  show "lincomb (λv. (λv. if v ∈ b1 then a1 v else 𝟬) v ⊕ (λv. if v ∈ b2 then a2 v else 𝟬) v) (b1 ∪ b2) = x"
    using lincomb_sum[OF ‹finite (b1 ∪ b2)› ‹b1 ∪ b2 ⊆ carrier M›
    ‹(λv. if v ∈ b1 then a1 v else 𝟬) ∈ (b1 ∪ b2) → carrier R› ‹(λv. if v ∈ b2 then a2 v else 𝟬) ∈ (b1 ∪ b2) → carrier R›]
    ‹x1 = lincomb (λv. if v ∈ b1 then a1 v else 𝟬) (b1 ∪ b2)› ‹x2 = lincomb (λv. if v ∈ b2 then a2 v else 𝟬) (b1 ∪ b2)› assms(7) by blast
qed

lemma (in vectorspace) dim_subadditive:
assumes "subspace K W1 V"
and "vectorspace.fin_dim K (vs W1)"
assumes "subspace K W2 V"
and "vectorspace.fin_dim K (vs W2)"
shows "vectorspace.dim K (vs (subspace_sum W1 W2)) ≤ vectorspace.dim K (vs W1) + vectorspace.dim K (vs W2)"
proof -
  have "vectorspace K (vs W1)" "vectorspace K (vs W2)" "submodule K W1 V" "submodule K W2 V"
    by (simp add: ‹subspace K W1 V› ‹subspace K W2 V› subspace_is_vs)+
  obtain b1 b2 where "vectorspace.basis K (vs W1) b1" "vectorspace.basis K (vs W2) b2" "finite b1" "finite b2"
    using vectorspace.finite_basis_exists[OF ‹vectorspace K (vs W1)› ‹vectorspace.fin_dim K (vs W1)›]
    using vectorspace.finite_basis_exists[OF ‹vectorspace K (vs W2)› ‹vectorspace.fin_dim K (vs W2)›]
    by blast
  then have "LinearCombinations.module.gen_set K (vs W1) b1" "LinearCombinations.module.gen_set K (vs W2) b2"
    using ‹vectorspace K (vs W1)› ‹vectorspace K (vs W2)› vectorspace.basis_def by blast+
  then have "span b1 = W1" "span b2 = W2"
    using module.span_li_not_depend(1) ‹submodule K W1 V›  ‹submodule K W2 V›
    ‹vectorspace K (vs W1)› ‹vectorspace.basis K (vs W1) b1› ‹vectorspace K (vs W2)›
    ‹vectorspace.basis K (vs W2) b2› vectorspace.basis_def by force+
  have "W1 ⊆ carrier V" "W2 ⊆ carrier V" using ‹subspace K W1 V› ‹subspace K W2 V› subspace_def submodule_def by metis+
  have "b1 ⊆ carrier V"
    using ‹vectorspace.basis K (vs W1) b1› ‹vectorspace K (vs W1)› vectorspace.basis_def
    ‹W1 ⊆ carrier V› by fastforce
  have "b2 ⊆ carrier V"
    using ‹vectorspace.basis K (vs W2) b2› ‹vectorspace K (vs W2)› vectorspace.basis_def
    ‹W2 ⊆ carrier V› by fastforce
  have "finite (b1 ∪ b2)" "b1 ∪ b2 ⊆ carrier V"
    by (simp_all add: ‹finite b1› ‹finite b2› ‹b2 ⊆ carrier V› ‹b1 ⊆ carrier V›)
  have "subspace_sum W1 W2 ⊆ span (b1∪b2)"
  proof (rule subsetI)
    fix x assume "x ∈ subspace_sum W1 W2"
    obtain x1 x2 where  "x1 ∈ W1" "x2 ∈ W2" "x = x1 ⊕V x2"
      using imageE[OF ‹x ∈ subspace_sum W1 W2›[unfolded submodule_sum_def]]
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD split_def)
    obtain a1 where "x1 = lincomb a1 b1" "a1∈ (b1→carrier K)"
      using ‹span b1 = W1› finite_span[OF ‹finite b1› ‹b1 ⊆ carrier V›] ‹x1 ∈ W1› by auto
    obtain a2 where "x2 = lincomb a2 b2" "a2∈ (b2→carrier K)"
      using ‹span b2 = W2› finite_span[OF ‹finite b2› ‹b2 ⊆ carrier V›] ‹x2 ∈ W2› by auto
    obtain a where "x = lincomb a (b1 ∪ b2)" using lincomb_add[OF ‹finite (b1 ∪ b2)› ‹b1 ∪ b2 ⊆ carrier V›
      ‹x1 = lincomb a1 b1› ‹a1∈ (b1→carrier K)›  ‹x2 = lincomb a2 b2› ‹a2∈ (b2→carrier K)› ‹x = x1 ⊕V x2›] by blast
    then show "x ∈ span (b1 ∪ b2)" using finite_span[OF ‹finite (b1 ∪ b2)› ‹(b1 ∪ b2) ⊆ carrier V›]
      using ‹b1 ⊆ carrier V› ‹b2 ⊆ carrier V› ‹span b1 = W1› ‹span b2 = W2› ‹x ∈ subspace_sum W1 W2› span_union_is_sum by auto
  qed
  have "b1 ⊆ W1" "b2 ⊆ W2"
    using ‹vectorspace K (vs W1)› ‹vectorspace K (vs W2)› ‹vectorspace.basis K (vs W1) b1›
    ‹vectorspace.basis K (vs W2) b2› vectorspace.basis_def local.carrier_vs_is_self by blast+
  then have "b1∪b2 ⊆ subspace_sum W1 W2" using ‹submodule K W1 V› ‹submodule K W2 V› in_sum
    by (metis assms(1) assms(3) dual_order.trans sup_least vectorspace.vsum_comm vectorspace_axioms)
  have "subspace_sum W1 W2 = LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1∪b2)"
  proof (rule subset_antisym)
    have "submodule K (subspace_sum W1 W2) V" by (simp add: ‹submodule K W1 V› ‹submodule K W2 V› sum_is_submodule)
    show "subspace_sum W1 W2 ⊆ LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1∪b2)"
      using module.span_li_not_depend(1)[OF ‹b1∪b2 ⊆ subspace_sum W1 W2› ‹submodule K (subspace_sum W1 W2) V›]
      by (simp add: ‹subspace_sum W1 W2 ⊆ span (b1 ∪ b2)›)
    show "subspace_sum W1 W2 ⊇ LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1∪b2)"
      using ‹b1∪b2 ⊆ subspace_sum W1 W2› by (metis (full_types) LinearCombinations.module.span_is_subset2
      LinearCombinations.module.submodule_is_module ‹submodule K (subspace_sum W1 W2) V› local.carrier_vs_is_self submodule_def)
  qed
  have "vectorspace K (vs (subspace_sum W1 W2))" using assms(1) assms(3) subspace_def sum_is_subspace vectorspace.subspace_is_vs by blast
  then have "vectorspace.dim K (vs (subspace_sum W1 W2)) ≤ card (b1 ∪ b2)"
    using vectorspace.gen_ge_dim[OF ‹vectorspace K (vs (subspace_sum W1 W2))› ‹finite (b1 ∪ b2)›]
    ‹b1 ∪ b2 ⊆ subspace_sum W1 W2›
    ‹subspace_sum W1 W2 = LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2)›
    local.carrier_vs_is_self by blast
  also have "... ≤ card b1 + card b2" by (simp add: card_Un_le)
  also have "... = vectorspace.dim K (vs W1) + vectorspace.dim K (vs W2)"
    by (metis ‹finite b1› ‹finite b2› ‹vectorspace K (vs W1)› ‹vectorspace K (vs W2)›
    ‹vectorspace.basis K (vs W1) b1› ‹vectorspace.basis K (vs W2) b2› vectorspace.dim_basis)
  finally show ?thesis by auto
qed

lemma (in Module.module) nested_submodules:
assumes "submodule R W M"
assumes "submodule R X M"
assumes "X ⊆ W"
shows "submodule R X (md W)"
  unfolding submodule_def
  using ‹X ⊆ W› submodule_is_module[OF ‹submodule R W M›] using ‹submodule R X M›[unfolded submodule_def] by auto

lemma (in vectorspace) nested_subspaces:
assumes "subspace K W V"
assumes "subspace K X V"
assumes "X ⊆ W"
shows "subspace K X (vs W)"
  using assms nested_submodules subspace_def subspace_is_vs by blast

lemma (in vectorspace) subspace_dim:
assumes "subspace K X V" "fin_dim" "vectorspace.fin_dim K (vs X)"
shows "vectorspace.dim K (vs X) ≤ dim"
proof -
  have "vectorspace K (vs X)" using assms(1) subspace_is_vs by auto
  then obtain b where "vectorspace.basis K (vs X) b" using vectorspace.finite_basis_exists
    using assms(3) by blast
  then have "b ⊆ carrier V" "LinearCombinations.module.lin_indpt K (vs X) b"
    using vectorspace.basis_def[OF ‹vectorspace K (vs X)›] ‹subspace K X V›[unfolded subspace_def submodule_def] by auto
  then have "lin_indpt b"
    by (metis LinearCombinations.module.span_li_not_depend(2) ‹vectorspace K (vs X)› ‹vectorspace.basis K (vs X) b›
    assms(1) is_module local.carrier_vs_is_self submodule_def vectorspace.basis_def)
  show ?thesis using li_le_dim(2)[OF ‹fin_dim› ‹b ⊆ carrier V› ‹lin_indpt b›]
    using ‹b ⊆ carrier V› ‹lin_indpt b› ‹vectorspace K (vs X)› ‹vectorspace.basis K (vs X) b› assms(2)
    fin_dim_li_fin vectorspace.dim_basis by fastforce
qed

lemma (in vectorspace) fin_dim_subspace_sum:
assumes "subspace K W1 V"
assumes "subspace K W2 V"
assumes "vectorspace.fin_dim K (vs W1)" "vectorspace.fin_dim K (vs W2)"
shows "vectorspace.fin_dim K (vs (subspace_sum W1 W2))"
proof -
  obtain b1 where "finite b1" "b1 ⊆ W1" "LinearCombinations.module.gen_set K (vs W1) b1"
    using assms vectorspace.fin_dim_def subspace_is_vs by force
  obtain b2 where "finite b2" "b2 ⊆ W2" "LinearCombinations.module.gen_set K (vs W2) b2"
    using assms vectorspace.fin_dim_def subspace_is_vs by force
  have 1:"finite (b1 ∪ b2)" by (simp add: ‹finite b1› ‹finite b2›)
  have 2:"b1 ∪ b2 ⊆ subspace_sum W1 W2"
    by (metis (no_types, lifting) ‹b1 ⊆ W1› ‹b2 ⊆ W2› assms(1) assms(2)
    le_sup_iff subset_Un_eq vectorspace.in_sum_vs vectorspace.vsum_comm vectorspace_axioms)
  have 3:"LinearCombinations.module.gen_set K (vs (subspace_sum W1 W2)) (b1 ∪ b2)"
  proof (rule subset_antisym)
    have 0:"LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2) = span (b1 ∪ b2)"
      using span_li_not_depend(1)[OF ‹b1 ∪ b2 ⊆ subspace_sum W1 W2›] sum_is_subspace[OF assms(1) assms(2)] by auto
    then show "LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2) ⊆ carrier (vs (subspace_sum W1 W2))"
      using ‹b1 ∪ b2 ⊆ subspace_sum W1 W2› span_is_subset sum_is_subspace[OF assms(1) assms(2)] by auto
    show "carrier (vs (subspace_sum W1 W2)) ⊆ LinearCombinations.module.span K (vs (subspace_sum W1 W2)) (b1 ∪ b2)"
     unfolding 0
    proof
      fix x assume assumption:"x ∈ carrier (vs (subspace_sum W1 W2))"
      then have "x∈subspace_sum W1 W2" by auto
      then obtain x1 x2 where "x = x1 ⊕V x2" "x1∈W1" "x2∈W2"
        using imageE[OF ‹x ∈ subspace_sum W1 W2›[unfolded submodule_sum_def]]
        by (metis (no_types, lifting) BNF_Def.Collect_case_prodD split_def)
      have "x1∈span b1"  "x2∈span b2"
        using ‹LinearCombinations.module.span K (vs W1) b1 = carrier (vs W1)› ‹b1 ⊆ W1› ‹x1 ∈ W1›
              ‹LinearCombinations.module.span K (vs W2) b2 = carrier (vs W2)› ‹b2 ⊆ W2› ‹x2 ∈ W2›
        assms(1) assms(2) span_li_not_depend(1) by auto
      then have "x1∈span (b1 ∪ b2)" "x2∈span (b1 ∪ b2)" by (meson le_sup_iff subsetD span_is_monotone subsetI)+
      then show "x ∈ span (b1 ∪ b2)" unfolding ‹x = x1 ⊕V x2›
        by (meson ‹b1 ∪ b2 ⊆ subspace_sum W1 W2› assms(1) assms(2) is_module submodule.subset
        subset_trans sum_is_submodule vectorspace.span_add1 vectorspace_axioms)
    qed
  qed
  show ?thesis using 1 2 3 vectorspace.fin_dim_def
    by (metis assms(1) assms(2) local.carrier_vs_is_self subspace_def sum_is_subspace vectorspace.subspace_is_vs)
qed

lemma (in vec_space) rank_subadditive:
assumes "A ∈ carrier_mat n nc"
assumes "B ∈ carrier_mat n nc"
shows "rank (A + B) ≤ rank A + rank B"
proof -
  define W1 where "W1 = span (set (cols A))"
  define W2 where "W2 = span (set (cols B))"
  have "set (cols (A + B)) ⊆ subspace_sum W1 W2"
  proof
    fix x assume "x ∈ set (cols (A + B))"
    obtain i where "x = col (A + B) i" "i < length (cols (A + B))"
      using ‹x ∈ set (cols (A + B))› nth_find_first cols_nth find_first_le by (metis cols_length)
    then have "x = col A i + col B i" using ‹i < length (cols (A + B))› assms(1) assms(2) by auto
    have "col A i ∈ span (set (cols A))" "col B i ∈ span (set (cols B))"
      using ‹i < length (cols (A + B))› assms(1) assms(2) in_set_conv_nth
      by (metis cols_dim cols_length cols_nth carrier_matD(1) carrier_matD(2) index_add_mat(3) span_mem)+
    then show "x ∈ subspace_sum W1 W2"
      unfolding W1_def W2_def ‹x = col A i + col B i› submodule_sum_def by blast
  qed
  have "subspace class_ring (subspace_sum W1 W2) V"
    by (metis W1_def W2_def assms(1) assms(2) cols_dim carrier_matD(1) span_is_submodule subspace_def sum_is_submodule vec_vs)
  then have "span (set (cols (A + B))) ⊆ subspace_sum W1 W2"
    by (simp add: ‹set (cols (A + B)) ⊆ subspace_sum W1 W2› span_is_subset)
  have "subspace class_ring (span (set (cols (A + B)))) V" by (metis assms(2) cols_dim add_carrier_mat carrier_matD(1) span_is_subspace)
  have subspace:"subspace class_ring (span (set (cols (A + B)))) (vs (subspace_sum W1 W2))"
    using nested_subspaces[OF ‹subspace class_ring (subspace_sum W1 W2) V› ‹subspace class_ring (span (set (cols (A + B)))) V›
    ‹span (set (cols (A + B))) ⊆ subspace_sum W1 W2›] .
  have "vectorspace.fin_dim class_ring (vs W1)" "vectorspace.fin_dim class_ring (vs W2)"
       "subspace class_ring W1 V" "subspace class_ring W2 V"
    using span_is_subspace W1_def W2_def assms(1) assms(2) cols_dim carrier_matD fin_dim_span_cols by auto
  then have fin_dim: "vectorspace.fin_dim class_ring (vs (subspace_sum W1 W2))" using fin_dim_subspace_sum by auto
  have "vectorspace.fin_dim class_ring (span_vs (set (cols (A + B))))" using assms(2) add_carrier_mat vec_space.fin_dim_span_cols by blast
  then have "rank (A + B) ≤ vectorspace.dim class_ring (vs (subspace_sum W1 W2))" unfolding rank_def
    using vectorspace.subspace_dim[OF subspace_is_vs[OF ‹subspace class_ring (subspace_sum W1 W2) V›] subspace fin_dim] by auto
  also have "vectorspace.dim class_ring (vs (subspace_sum W1 W2)) ≤ rank A + rank B" unfolding rank_def
    using W1_def W2_def ‹subspace class_ring W1 V› ‹subspace class_ring W2 V› ‹vectorspace.fin_dim class_ring (vs W1)›
    ‹vectorspace.fin_dim class_ring (vs W2)› subspace_def vectorspace.dim_subadditive by blast
  finally show ?thesis by auto
qed

lemma (in vec_space) span_zero: "span {zero V} = {zero V}"
  by (metis (no_types, lifting) empty_subsetI in_own_span span_is_submodule span_is_subset
  span_is_subset2 subset_antisym vectorspace.span_empty vectorspace_axioms)

lemma (in vec_space) dim_zero_vs: "vectorspace.dim class_ring (span_vs {}) = 0"
proof -
  have "vectorspace class_ring (span_vs {})" using field.field_axioms span_is_submodule submodule_is_module vectorspace_def by auto
  have "{} ⊆ carrier_vec n ∧ lin_indpt {}"
    by (metis (no_types) empty_subsetI fin_dim finite_basis_exists subset_li_is_li vec_vs vectorspace.basis_def)
  then have "vectorspace.basis class_ring (span_vs {}) {}" using vectorspace.basis_def
    by (simp add: ‹vectorspace class_ring (vs (span {}))› span_is_submodule span_li_not_depend(1) span_li_not_depend(2) vectorspace.basis_def)
  then show ?thesis using ‹vectorspace class_ring (vs (span {}))› vectorspace.dim_basis by fastforce
qed

lemma (in vec_space) rank_0I: "rank (0m n nc) = 0"
proof -
  have "set (cols (0m n nc)) ⊆ {0v n}"
    by (metis col_zero cols_length cols_nth in_set_conv_nth insertCI index_zero_mat(3) subsetI)
  have "set (cols (0m n nc::'a mat)) = {} ∨ set (cols (0m n nc)) = {0v n::'a vec}"
    by (meson ‹set (cols (0m n nc)) ⊆ {0v n}› subset_singletonD)
  then have "span (set (cols (0m n nc))) = {0v n}"
    by (metis (no_types) span_empty span_zero vectorspace.span_empty vectorspace_axioms)
  then show ?thesis unfolding rank_def ‹span (set (cols (0m n nc))) = {0v n}›
    using span_empty dim_zero_vs by simp
qed


lemma (in vec_space) rank_le_1_product_entries:
fixes f g::"nat ⇒ 'a"
assumes "A ∈ carrier_mat n nc"
assumes "⋀r c. r<dim_row A ⟹ c<dim_col A ⟹ A $$ (r,c) = f r * g c"
shows "rank A ≤ 1"
proof -
  have "set (cols A) ⊆ span {vec n f}"
  proof
    fix v assume "v ∈ set (cols A)"
    then obtain c where "c < dim_col A" "v = col A c" by (metis cols_length cols_nth in_set_conv_nth)
    have "g c ⋅v vec n f = v"
    proof (rule eq_vecI)
      show "dim_vec (g c ⋅v Matrix.vec n f) = dim_vec v" using ‹v = col A c› assms(1) by auto
      fix r assume "r < dim_vec v"
      then have "r < dim_vec (Matrix.vec n f)" using ‹dim_vec (g c ⋅v Matrix.vec n f) = dim_vec v› by auto
      then have "r < n" "r < dim_row A"using index_smult_vec(2) ‹A ∈ carrier_mat n nc› by auto
      show "(g c ⋅v Matrix.vec n f) $ r = v $ r"
        unfolding ‹v = col A c› col_def index_smult_vec(1)[OF ‹r < dim_vec (Matrix.vec n f)›]
        index_vec[OF ‹r < n›] index_vec[OF ‹r < dim_row A›] by (simp add: ‹c < dim_col A› ‹r < dim_row A› assms(2))
    qed
    then show "v ∈ span {vec n f}" using submodule.smult_closed[OF span_is_submodule]
      using UNIV_I empty_subsetI insert_subset span_self dim_vec module_vec_simps(4) by auto
  qed
  have "vectorspace class_ring (vs (span {Matrix.vec n f}))" using span_is_subspace[THEN subspace_is_vs, of "{vec n f}"] by auto
  have "submodule class_ring (span {Matrix.vec n f}) V" by (simp add: span_is_submodule)
  have "subspace class_ring(span (set (cols A))) (vs (span {Matrix.vec n f}))"
    using vectorspace.span_is_subspace[OF ‹vectorspace class_ring (vs (span {Matrix.vec n f}))›, of "set (cols A)", unfolded
    span_li_not_depend(1)[OF ‹set (cols A) ⊆ span {vec n f}› ‹submodule class_ring (span {Matrix.vec n f}) V›]]
    ‹set (cols A) ⊆ span {vec n f}› by auto
  have fin_dim:"vectorspace.fin_dim class_ring (vs (span {Matrix.vec n f}))"
       "vectorspace.fin_dim class_ring (vs (span {Matrix.vec n f})⦇carrier := span (set (cols A))⦈)"
    using fin_dim_span fin_dim_span_cols ‹A ∈ carrier_mat n nc› by auto
  have "vectorspace.dim class_ring (vs (span {Matrix.vec n f})) ≤ 1"
    using vectorspace.dim_le1I[OF ‹vectorspace class_ring (vs (span {Matrix.vec n f}))›]
    span_mem span_li_not_depend(1)[OF _ ‹submodule class_ring (span {Matrix.vec n f}) V›] by simp
  then show ?thesis unfolding rank_def using  "vectorspace.subspace_dim"[OF
    ‹vectorspace class_ring (vs (span {Matrix.vec n f}))› ‹subspace class_ring (span (set (cols A))) (vs (span {Matrix.vec n f}))›
    fin_dim(1) fin_dim(2)] by simp
qed

end