Theory Jordan_Normal_Form.DL_Rank

(* 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 US 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 "sS" "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 "sU" 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)" "US" "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 " (xset (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 "ij" "(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 (b1carrier R)"
assumes "x2 = lincomb a2 b2" "a2 (b2carrier R)"
assumes "x = x1 Mx2"
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 (b2carrier 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 (b1carrier R) (λb. 𝟬R)  b2 - b1  carrier R]
          lincomb_union2[OF finite (b2  (b1-b2)) b2  (b1-b2)  carrier M b2  (b1 - b2) = {} a2 (b2carrier 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 (b1b2)"
  proof (rule subsetI)
    fix x assume "x  subspace_sum W1 W2"
    obtain x1 x2 where  "x1  W1" "x2  W2" "x = x1 Vx2"
      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 (b1carrier 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 (b2carrier 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 (b1carrier K)  x2 = lincomb a2 b2 a2 (b2carrier K) x = x1 Vx2] 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 "b1b2  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)) (b1b2)"
  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)) (b1b2)"
      using module.span_li_not_depend(1)[OF b1b2  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)) (b1b2)"
      using b1b2  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 "xsubspace_sum W1 W2" by auto
      then obtain x1 x2 where "x = x1 Vx2" "x1W1" "x2W2"
        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 "x1span b1"  "x2span 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 "x1span (b1  b2)" "x2span (b1  b2)" by (meson le_sup_iff subsetD span_is_monotone subsetI)+
      then show "x  span (b1  b2)" unfolding x = x1 Vx2
        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