Theory Linear_combinations

theory Linear_combinations
imports Linear_dependence Indexed_Set
begin

section{*Linear combinations*}

context vector_space
begin

text{*To define the notion of linear dependence and independence we already introduced the definition of linear
  combination. Nevertheless, here we present some properties of linear combinations. We could have used them
  to simplify the proofs of some theorems in the previous section, but we have decided to keep the order of 
  the sections in Halmos.*}

(*Next definition is dispensable:
definition linear_combination_of :: "'b=>('b=>'a)=>'b set=> bool"
  where "linear_combination_of x f X = (linear_combination f X = x)"*)

text{*A @{text linear_combination} is closed, when considering a set $X \subseteq carrier$ $V$ and a proper coefficients function $f$:*}
lemma linear_combination_closed: 
  assumes good_set: "good_set X" 
  and f: "f ∈ coefficients_function (carrier V) " 
  shows "linear_combination f X ∈ carrier V"
proof (unfold linear_combination_def, rule finsum_closed)
  show "finite X" using good_set unfolding good_set_def by auto
  show "(λy. f y · y) ∈ X -> carrier V"
  proof (unfold Pi_def, auto)
    fix y
    assume y_in_X: "y ∈ X"
    hence y_in_V: "y ∈ carrier V" using good_set unfolding good_set_def by fast
    show "f y · y ∈ carrier V" using fx_x_in_V[OF y_in_V f] .
  qed
qed

text{*A @{text linear_combination} over the empty set is equal to @{term "\<zero>\<^bsub>V\<^esub>"}*}
lemma linear_combination_of_zero: 
  shows "linear_combination f {} = x <-> x = \<zero>\<^bsub>V\<^esub>"
proof
  assume l_combination_x: "linear_combination f {} = x"
  have l_combination_zero: "linear_combination f {}=\<zero>\<^bsub>V\<^esub>" 
    unfolding linear_combination_def
    using finsum_empty by auto
  show "x = \<zero>\<^bsub>V\<^esub>" 
    using l_combination_x and l_combination_zero by auto
next
  assume x_zero: "x = \<zero>\<^bsub>V\<^esub>"
  have l_combination_x: "linear_combination f {} = \<zero>\<^bsub>V\<^esub>" 
    unfolding linear_combination_def 
    using finsum_empty by auto
  show "linear_combination f {}=x" 
    using l_combination_x and x_zero by simp
qed


text{*From previous lemma we can obtain a corollary which 
  will be useful as a simplification rule.*}
corollary linear_combination_empty_set [simp]: 
  shows "linear_combination f {} = \<zero>\<^bsub>V\<^esub>"
  using linear_combination_of_zero by simp

text{*The computation of the linear combination of a unipuntual set is direct: *}
lemma linear_combination_singleton: 
  assumes cf_f: "f ∈ coefficients_function (carrier V)" 
  and x_in_V: "x ∈ carrier V" 
  shows "linear_combination f {x} = f x · x"
proof -
  have "linear_combination f (insert x {}) 
    = (f x) · x ⊕\<^bsub>V\<^esub> linear_combination f {}"
  proof (unfold linear_combination_def, rule finsum_insert)
    show "finite {}" by simp
    show "x∉ {}" by simp
    show "(λy. f y · y) ∈ {} -> carrier V" by simp
    show "f x · x ∈ carrier V"
    proof (rule mult_closed)
      show "x ∈ carrier V" using x_in_V .
      show "f x ∈ carrier K" using cf_f 
        unfolding coefficients_function_def using x_in_V by auto
    qed
  qed
  also have "… = (f x) · x ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>" 
    using linear_combination_empty_set by auto
  also have "… = (f x) · x"
  proof (rule V.r_zero)
    show "f x · x ∈ carrier V"
    proof (rule mult_closed)
      show "x ∈ carrier V" using x_in_V .
      show "f x ∈ carrier K" 
        using cf_f 
        unfolding coefficients_function_def using x_in_V by auto
    qed
  qed
  finally show ?thesis by auto
qed

text{*A @{text linear_combination} of @{term "insert x X"} is equal to @{term "f x · x ⊕\<^bsub>V\<^esub> linear_combination f X"}*}
lemma linear_combination_insert: 
  assumes good_set_X: "good_set X" 
  and x_in_V: "x ∈ carrier V" 
  and x_not_in_X: "x ∉ X" 
  and cf_f: "f ∈ coefficients_function (carrier V)" 
  shows "linear_combination f (insert x X) 
  = f x · x ⊕\<^bsub>V\<^esub> linear_combination f X"
proof (unfold linear_combination_def, rule finsum_insert)
  show "finite X" using good_set_X 
    unfolding good_set_def by simp
  show "x ∉ X" using x_not_in_X .
  show "(λy. f y · y) ∈ X -> carrier V"
  proof (unfold Pi_def,auto) 
    show "!!x. x ∈ X ==> f x · x ∈ carrier V" 
    proof (rule fx_x_in_V) 
      fix y
      assume y_in_X: "y ∈ X"
      show "y ∈ carrier V"
        using good_set_X 
        unfolding good_set_def using y_in_X by auto
      show "f ∈ coefficients_function (carrier V)" using cf_f .
    qed 
  qed
  show "f x · x ∈ carrier V" using fx_x_in_V[OF x_in_V cf_f] .
qed

text{*If each term of the linear combination is zero, then the sum is zero.*}
lemma linear_combination_zero: 
  assumes good_set_X: "good_set X"
  and cf_f: "f ∈ coefficients_function (carrier V)"
  and all_zero: "!!x. x ∈ X ==> f (x) · x = \<zero>\<^bsub>V\<^esub>"
  shows "linear_combination f X = \<zero>\<^bsub>V\<^esub>"
proof -
  have "linear_combination f X = (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y)" 
    unfolding linear_combination_def ..
  also have "...=(\<Oplus>\<^bsub>V\<^esub>y∈X. \<zero>\<^bsub>V\<^esub>)"
  proof (rule finsum_cong',auto)
    fix x
    assume x_in_X: "x∈X"
    show "f x · x = \<zero>\<^bsub>V\<^esub>"
      using all_zero[OF x_in_X] .
  qed
  also have "...=\<zero>\<^bsub>V\<^esub>" using finsum_zero good_set_X 
    unfolding good_set_def by blast
  finally show ?thesis .
qed


text{*This is an auxiliary lemma which we will use later to prove that 
  @{term "a · (linear_combination f X) = linear_combination (%i. a ⊗ f(i)) X"}.
  We prove it doing induction over the finite set @{term X}. Firstly, we have to
  prove the property in case that the set is empty. After that, we
  suppose that the result is true for a set @{term X} and then we have to
  prove it for a set @{term "(insert x X)"} where @{term "x ∉ X"}.*}
lemma finsum_aux:
  "[|finite X; X ⊆ carrier V; a∈ carrier K; f ∈ X-> carrier K|] 
  ==> a · (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y)=(\<Oplus>\<^bsub>V\<^esub>y∈X. a· (f y · y))"
proof (induct set: finite)
  case empty then show ?case 
    using scalar_mult_zeroV_is_zeroV by auto
next
  case (insert x X) then show ?case 
  proof -
    have sum_closed: "(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) ∈ carrier V" 
    proof (rule finsum_closed) 
      show "finite X" using insert.hyps (1) .
      show "(λy. f y · y) ∈ X -> carrier V" 
        using insert.prems (1) and insert.prems (3) and mult_closed 
        by auto
    qed
    have fx_x_in_V: "f x · x∈ carrier V" 
      using insert.prems (1) and insert.prems (3) and mult_closed 
      by auto
    have "(\<Oplus>\<^bsub>V\<^esub>y∈insert x X. f y · y)=f(x)·x ⊕\<^bsub>V\<^esub>(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y)" 
    proof (rule finsum_insert)
      show "finite X" using insert.hyps (1) .
      show "x∉ X" using insert.hyps (2) .
      show "f x · x ∈ carrier V" using fx_x_in_V .
      show "(λy. f y · y) ∈ X -> carrier V" 
        using insert.prems (1) and insert.prems (3) and mult_closed 
        by auto
    qed
    hence "a·(\<Oplus>\<^bsub>V\<^esub>y∈insert x X. f y · y)=a·f(x)·x ⊕\<^bsub>V\<^esub> a·(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y)"
      using add_mult_distrib1[OF fx_x_in_V 
        sum_closed insert.prems(2)] by auto
    also have "…=a·f(x)·x ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. a· f y · y)" 
    proof -
      have X_subset_V: "X ⊆ carrier V"using insert.prems(1) by auto
      have f1: "f∈ X->carrier K" using insert.prems(3) by auto
      show ?thesis using insert.hyps(3)[OF X_subset_V insert.prems(2) f1] by auto
    qed
    also have "…=(\<Oplus>\<^bsub>V\<^esub>y∈insert x X. a · f y · y)"
    proof (rule finsum_insert[symmetric])
      show "finite X" using insert.hyps(1) .
      show "x ∉ X" using insert.hyps(2) .
      show "(λy. a · f y · y) ∈ X -> carrier V"
      proof (unfold Pi_def, auto)
        fix y
        assume y_in_X: "y∈ X"
        show "a· f y · y ∈ carrier V"
        proof (rule mult_closed)
          show "f(y)·y ∈ carrier V" using y_in_X and insert.prems(1) and insert.prems(3) and mult_closed by auto
          show "a∈ carrier K" using insert.prems(2) .
        qed
      qed
      show" a · f x · x ∈ carrier V"
      proof (rule mult_closed)
        show  "f x · x ∈ carrier V" using insert.prems (1) and insert.prems(3) and mult_closed by auto
        show "a ∈ carrier K" using insert.prems(2) .
      qed
    qed
    finally show ?thesis by auto
  qed
qed

text{*To multiply a linear combination by a scalar $a$ is the same that multiplying each term of the linear
  combination by $a$.*}
lemma linear_combination_rdistrib: 
  "[|good_set X; f ∈ coefficients_function (carrier V); 
  a ∈ carrier K|] ==> a · (linear_combination f X) 
  = linear_combination (%i. a ⊗ f(i)) X"
proof -
  assume good_set: "good_set X" 
    and coefficients_function_f: 
    "f ∈ coefficients_function (carrier V)" 
    and a_in_K:"a ∈ carrier K"
  have X_subset_V: "X⊆ carrier V" 
    using good_set unfolding good_set_def by auto
  have finite_X: "finite X" 
    using good_set unfolding good_set_def by auto
  have f: "f ∈ X->carrier K"
  proof (unfold Pi_def, auto)
    fix x
    assume x_in_X: "x ∈ X"
    show "f x∈ carrier K" 
      using x_in_X and X_subset_V and coefficients_function_f 
      unfolding coefficients_function_def  by auto
  qed  
  show "a · linear_combination f X 
    = linear_combination (λi. a ⊗ f i) X"
  proof (unfold linear_combination_def)
    have "(\<Oplus>\<^bsub>V\<^esub>y∈X. (a ⊗ f y) · y)=(\<Oplus>\<^bsub>V\<^esub>y∈X. a · f y · y)" 
    proof (rule finsum_cong')
      show "X=X" ..
      show "(λy. a · f y · y) ∈ X -> carrier V"
      proof (unfold Pi_def, auto)
        fix y
        assume y_in_X: "y∈ X"
        show "a · f y · y ∈ carrier V"
        proof (rule mult_closed)
          show "f y · y ∈ carrier V" using y_in_X and X_subset_V and f and mult_closed by auto
          show "a∈ carrier K" using a_in_K .
        qed
      qed
      show "!!i. i ∈ X ==> (a ⊗ f i) · i = a · f i · i" 
      proof (rule impE, auto)
        fix i
        assume i_in_X: "i∈ X"
        show "(a ⊗ f i) · i = a · f i · i"
        proof (rule mult_assoc)
          show "i∈ carrier V" using i_in_X and X_subset_V by auto
          show "a∈ carrier K" using a_in_K .
          show "f i ∈ carrier K" using i_in_X and f by auto
        qed
      qed
    qed
    also have "…=a·(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y)" 
      using finsum_aux [OF finite_X X_subset_V a_in_K f, symmetric] .
    finally show "a · (\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈X. (a ⊗ f y) · y)"
      by auto
  qed
qed

text{*Now some useful lemmas which will be helpful to prove other ones.*}
lemma coefficients_function_g_f_null: 
  assumes cf_f: "f ∈ coefficients_function (carrier V)" 
  shows "(λx. if x ∈ Y then f(x) else \<zero>\<^bsub>K\<^esub>) 
  ∈ coefficients_function (carrier V)" using cf_f
  unfolding coefficients_function_def by auto

text{*This lemma is a generalization of the idea through we have proved 
  @{text "linear_dependent_subset_implies_linear_dependent_set:"}
  @{thm linear_dependent_subset_implies_linear_dependent_set[no_vars]}. 
  Using it we could reduce its proof, but in 
  Halmos the section of linear dependence goes before the one about linear combinations. The proof is based on dividing
  the linear combination into two sums, from which one of them is equal to $0_V$. This lemma takes up about 130 code lines.*}
lemma eq_lc_when_out_of_set_is_zero: 
  assumes good_set_A: "good_set A" and good_set_Y: "good_set Y" 
  and cf_f: "f∈ coefficients_function (carrier V)" 
  shows "linear_combination (λx. if x ∈ Y then f(x) else \<zero>\<^bsub>K\<^esub>) 
  (Y∪A) = linear_combination f Y"
proof -
  let ?g="(λx. if x ∈ Y then f(x) else \<zero>\<^bsub>K\<^esub>)"
  have descomposicion_conjuntos:"Y∪A=Y∪(A-Y)" by auto 
  have disjuntos: "Y Int (A-Y)={}" 
    by simp
  have finite_A: "finite A" 
    using good_set_A
    unfolding good_set_def by simp
  have finite_Y: "finite Y"
    using good_set_Y
    unfolding good_set_def by auto
  have finite_A_minus_Y: "finite (A-Y)" 
    using finite_A  by simp
  have g1:"?g ∈ Y -> carrier K" 
    using coefficients_function_g_f_null[OF cf_f, of Y]
    unfolding coefficients_function_def 
    using good_set_Y
    unfolding good_set_def
    by auto
  have g2:"?g ∈ (A-Y) -> carrier K" 
    using coefficients_function_g_f_null[OF cf_f, of "(A-Y)"]
    unfolding coefficients_function_def 
    by auto
  let ?h="(λx. ?g(x)·x)"
  have h1: "?h ∈ Y -> carrier V"
  proof
    fix x
    assume x_in_Y: "x∈Y"
    have x_in_V: "x∈ carrier V"
    proof
      have Y_subset_V: "Y⊆ carrier V"
        using good_set_Y
        unfolding good_set_def
        by auto
      show ?thesis using Y_subset_V and x_in_Y by auto
    qed (auto)
    have gx_in_K: "?g(x)∈ carrier K"
      using g1
      using x_in_Y 
      unfolding Pi_def by auto
    have gx_x_in_V: "?g(x)·x ∈ carrier V"
      using mult_closed [OF x_in_V gx_in_K] by auto 
    show "(if x ∈ Y then f x else \<zero>) · x ∈ carrier V" 
      using gx_x_in_V by auto
  qed
  have h2: "?h ∈ (A-Y) -> carrier V"
  proof
    fix x
    assume x_in_A_minus_Y: "x∈ (A-Y)"
    have x_in_V: "x∈ carrier V"
    proof
      have A_minus_Y_subset_V: "(A-Y)⊆carrier V"
        using good_set_Y and good_set_A
        unfolding good_set_def
        by auto
      show ?thesis
        using A_minus_Y_subset_V
        using x_in_A_minus_Y by auto
    qed (auto)
    have gx_in_K: "?g(x)∈ carrier K"
      using x_in_A_minus_Y 
      by auto
    have gx_x_in_V: "?g(x)·x ∈ carrier V" 
      using mult_closed [OF x_in_V gx_in_K] by auto 
    show "(if x ∈ Y then f x else \<zero>) · x ∈ carrier V" 
      using gx_x_in_V by auto
  qed
  have descomposicion: "linear_combination ?g (Y∪(A-Y))=linear_combination ?g Y ⊕\<^bsub>V\<^esub> linear_combination ?g (A-Y)" 
    unfolding linear_combination_def 
    using finsum_Un_disjoint [OF finite_Y finite_A_minus_Y disjuntos h1 h2]
    by auto
  have sum_g_Y_equal_sum_f_Y: "linear_combination ?g Y=linear_combination f Y"
  proof (unfold linear_combination_def)
    have iguales: "Y=Y" ..
    show "(\<Oplus>\<^bsub>V\<^esub>y∈Y. (if y ∈ Y then f y else \<zero>) · y) = (\<Oplus>\<^bsub>V\<^esub>y∈Y. f y · y)"
      using finsum_cong [OF iguales] using h1 by auto
  qed
  have sum_g_A_minus_Y:"linear_combination ?g (A-Y)=\<zero> \<^bsub>V\<^esub>"
  proof -
    have X_subset_V: "A ⊆ carrier V" 
      using good_set_A
      unfolding good_set_def by auto
    hence A_minus_Y_subset_V:"(A-Y) ⊆ carrier V"  by auto
    have not_in_Y: "x ∈ (A-Y)==> x ∉ Y" by auto
    have "linear_combination ?g (A-Y)=(\<Oplus>\<^bsub>V\<^esub>y∈A - Y.  \<zero> · y)" 
    proof (unfold linear_combination_def)
      have igualesA_minus_Y: "A-Y=A-Y"..
      show "(\<Oplus>\<^bsub>V\<^esub>y∈A - Y. (if y ∈ Y then f y else \<zero>) · y) = finsum V (op · \<zero>) (A - Y)"
        using finsum_cong [OF igualesA_minus_Y eqTrueI [OF h2]] by auto
    qed
    also have "…=(\<Oplus>\<^bsub>V\<^esub>y∈A - Y. \<zero>\<^bsub>V\<^esub>)"    
    proof (rule finsum_cong')
      show "A - Y = A - Y" ..
      show "(λy. \<zero>\<^bsub>V\<^esub>) ∈ A - Y -> carrier V" by simp
      show "!!i. i ∈ A - Y ==> \<zero> · i = \<zero>\<^bsub>V\<^esub>"
        using zeroK_mult_V_is_zeroV
        using A_minus_Y_subset_V by auto
    qed  
    also have "…=\<zero> \<^bsub>V\<^esub>"
      using finsum_zero [OF finite_A_minus_Y] .
    finally show ?thesis by auto
  qed
  have aux: "linear_combination ?g (Y∪(A-Y))=linear_combination ?g (Y∪A)"  
    using descomposicion_conjuntos by auto
  show ?thesis
    using descomposicion
    using aux
    using sum_g_Y_equal_sum_f_Y 
    using sum_g_A_minus_Y
    using V.r_zero[OF linear_combination_closed[OF good_set_Y cf_f]]
    by auto
qed

text{*Another auxiliary lemma. It will be very useful to prove properties in future sections.
  If we have an equality of the form @{term "\<zero>\<^bsub>V\<^esub> = g(x)·x ⊕\<^bsub>V\<^esub> linear_combination g X"}, then
  we can work out the value of x (there exists a coefficients function $f$ such that $x=linear\_combination$ $f$ $X$. This
  coefficients function is explicitly defined by dividing each of the values $g(y)$ by $g(x)$).*}
lemma work_out_the_value_of_x: 
  assumes good_set: "good_set X" 
  and coefficients_function_g: 
  "g ∈ coefficients_function (carrier V)" 
  and x_in_V: "x ∈ carrier V" 
  and gx_not_zero: "g x ≠ \<zero>\<^bsub>K\<^esub>"
  and lc_descomposicion: "\<zero>\<^bsub>V\<^esub> = g(x)·x ⊕\<^bsub>V\<^esub> linear_combination g X"
  shows "∃f. f ∈ coefficients_function (carrier V) 
  ∧ linear_combination f X = x"
proof -
  have gx_in_K: "g(x) ∈ carrier K" 
    using coefficients_function_g using x_in_V 
    unfolding coefficients_function_def by auto
  hence gx_in_Units: "g(x)∈ Units K" 
    using gx_not_zero using field_Units by auto
  hence inv_gx_in_K: "inv g(x) ∈ carrier K" 
    using Units_inv_closed by auto
  hence minv_gx_in_K: "\<ominus> (inv g(x)) ∈ carrier K" 
    using a_inv_closed by auto
  have "(\<ominus>\<^bsub>K\<^esub> (inv g x))· \<zero>\<^bsub>V\<^esub>= \<ominus>\<^bsub>K\<^esub> (inv g x) · (g(x)·x ⊕\<^bsub>V\<^esub> linear_combination g X)" 
    using lc_descomposicion by auto
  hence "\<zero>\<^bsub>V\<^esub>= \<ominus>\<^bsub>K\<^esub> (inv g x)·g(x)·x ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>K\<^esub> (inv g x)· (linear_combination g X)"
    using scalar_mult_zeroV_is_zeroV[OF minv_gx_in_K]
    using add_mult_distrib1[OF mult_closed[OF x_in_V gx_in_K] 
      linear_combination_closed[OF good_set coefficients_function_g] minv_gx_in_K] by auto
  also have "…=(\<ominus>\<^bsub>K\<^esub> (inv g x)⊗ g(x))·x ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>K\<^esub> (inv g x)· (linear_combination g X)"
    using mult_assoc[OF x_in_V minv_gx_in_K gx_in_K] by auto    
  also have "…=(\<ominus>\<^bsub>K\<^esub> ((inv g x)⊗ g(x)))·x ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>K\<^esub> (inv g x)· (linear_combination g X)"
    using l_minus[OF inv_gx_in_K gx_in_K] by auto    
  also have "…=\<ominus>\<^bsub>V\<^esub>x ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>K\<^esub> (inv g x)· (linear_combination g X)" 
    using Units_l_inv[OF gx_in_Units] using negate_eq[OF x_in_V] by auto    
  also have "…=\<ominus>\<^bsub>V\<^esub>x ⊕\<^bsub>V\<^esub> linear_combination (%i. (\<ominus>\<^bsub>K\<^esub> (inv g x)) ⊗ g(i)) X"
    using linear_combination_rdistrib [OF good_set coefficients_function_g minv_gx_in_K] by auto    
  finally have igualdad: "\<zero>\<^bsub>V\<^esub>=\<ominus>\<^bsub>V\<^esub>x ⊕\<^bsub>V\<^esub> linear_combination (%i. (\<ominus>\<^bsub>K\<^esub> (inv g x)) ⊗ g(i)) X" .    
  let ?f="(λy.(\<ominus>\<^bsub>K\<^esub> (inv g x))⊗ g(y))"
  have coefficients_function_f: "?f ∈ coefficients_function (carrier V)"
  proof (unfold coefficients_function_def, unfold Pi_def, auto)
    fix y
    assume y_in_V: "y∈ carrier V"
    show "\<ominus> (inv g x) ⊗ g y ∈ carrier K" 
      using minv_gx_in_K y_in_V coefficients_function_g unfolding coefficients_function_def by auto
    next 
      fix xa 
      assume xa_notin_V: "xa ∉ carrier V"
      have "\<ominus> (inv g x) ⊗ g xa = \<ominus> (inv g x) ⊗ \<zero>" 
        using xa_notin_V coefficients_function_g unfolding coefficients_function_def by simp
      also have "...= \<zero>" using K.r_null[OF minv_gx_in_K] .
      finally  show "\<ominus> (inv g x) ⊗ g xa = \<zero>" .
  qed    
  hence "x ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>= x ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> x ⊕\<^bsub>V\<^esub> linear_combination ?f X" 
    using igualdad 
    using V.a_assoc [OF x_in_V a_inv_closed[OF x_in_V] linear_combination_closed[OF good_set _], symmetric]
    by auto
  hence "x = linear_combination ?f X" 
    using V.r_zero [OF x_in_V] 
    using a_minus_def[OF x_in_V x_in_V,symmetric] r_neg [OF x_in_V]
    using V.l_zero [OF linear_combination_closed[OF good_set coefficients_function_f]] 
    by auto   
  thus ?thesis using coefficients_function_f by fastsimp
qed

text{*Now we are going to prove a property presented in Halmos, 
  section 6: if $\{x_i\}_{i \in \mathbb{N}}$ is linearly independent,
then a necessary an sufficient condition that $x$ be a linear 
  combination of $\{x_i\}_{i \in \mathbb{N}}$ is that the enlarged set, obtained by adjoining $x$
to $\{x_i\}_{i \in \mathbb{N}}$, be linearly dependent.*}

text{*Here the first implication. The proof is based on definig a linear combination of the set $insert$ $x$ $X$ equal
  to $0_V$. As long as we know that $linear\_combination$ $f$ $X=x$ we define a coefficients function for $insert$ $x$ $X$
  where the coefficients of $y \in X$ are $f(y)$ and the coefficient of $x$ is $-1$. 
  A detail that is omitted in Halmos is that not every coefficient is zero since the coefficient of $x$ is
  $-1$. The complete proof requires 102 lines of Isabelle code.*}
lemma lc1:
  assumes linear_independent_X: "linear_independent X" 
  and x_in_V:"x ∈ carrier V" and x_not_in_X:"x ∉ X"
  shows "(∃f. f∈ coefficients_function (carrier V) ∧ linear_combination f X = x) ==> linear_dependent (insert x X)"
proof -
  assume "(∃f. f∈ coefficients_function (carrier V) ∧ linear_combination f X = x)"
  from this obtain f 
    where coefficients_function_f: "f∈ coefficients_function (carrier V)" 
    and linear_combination_x: "linear_combination f X = x" by auto
  show "linear_dependent (insert x X)"
  proof (unfold linear_dependent_def)
    have good_set: "good_set X" using l_ind_good_set [OF linear_independent_X] .
    have finite_X_union_x: "finite (insert x X)" 
      using good_set unfolding good_set_def by auto
    have X_union_x_in_V: "(insert x X) ⊆ carrier V"
    proof -
      have X_subset_V: "X⊆ carrier V" using good_set unfolding good_set_def by auto
      from this show ?thesis using x_in_V by auto
    qed
    have good_set_X_union_x: "good_set (insert x X)" 
      unfolding good_set_def using finite_X_union_x X_union_x_in_V by auto
    (*let ?g="(λx. if x ∈ X then f(x) else \<ominus>\<^bsub>K\<^esub> \<one> \<^bsub>K\<^esub>)"*)
    let ?g="(λy. if y = x then \<ominus>\<^bsub>K\<^esub> \<one> \<^bsub>K\<^esub> else f(y))"
    have g: "?g ∈ (insert x X)-> carrier K"
      using X_union_x_in_V 
      using coefficients_function_f 
      unfolding coefficients_function_def by auto
    have coefficients_function_g: "?g∈ coefficients_function (carrier V)"
      proof (unfold coefficients_function_def, auto)
        fix x
        assume "x ∈ carrier V"
        thus "f x ∈ carrier K" using fx_in_K[OF _ coefficients_function_f] by simp
        next
        assume x_notin_carrier_V: "x ∉ carrier V"
        thus "\<ominus> \<one> = \<zero>" using x_in_V by contradiction
        next
        fix xa
        assume xa_not_x: "xa ≠ x" and xa_notin_V: "xa ∉ carrier V"
        thus "f xa = \<zero>" using coefficients_function_f unfolding coefficients_function_def by blast
      qed
    have sum_zero: "linear_combination ?g (insert x X)=\<zero>\<^bsub>V\<^esub>"
    proof -
      have "linear_combination ?g (insert x X)=?g x · x ⊕\<^bsub>V  \<^esub>linear_combination ?g X"
        proof (rule linear_combination_insert)
           show "good_set X" using good_set .
           show "x ∈ carrier V" using x_in_V .
           show "x ∉ X" using x_not_in_X .
           show "?g ∈ coefficients_function (carrier V)" using coefficients_function_g .
          qed        
      also have "…=\<ominus> \<one> · x ⊕\<^bsub>V  \<^esub> linear_combination ?g X" using x_not_in_X by auto
      also have "…=\<ominus>\<^bsub>V\<^esub>x ⊕\<^bsub>V  \<^esub>x"
      proof -
        have "linear_combination ?g X=linear_combination f X" unfolding linear_combination_def 
        proof (rule finsum_cong', auto)
          assume x_in_X: "x ∈ X"
          thus "\<ominus> \<one> · x = f x · x" using x_not_in_X by contradiction
        next
          fix y
          assume y_in_X: "y ∈ X"
          hence y_in_V: "y ∈ carrier V" using good_set unfolding good_set_def by fast
          show "f y · y ∈ carrier V" using fx_x_in_V[OF y_in_V coefficients_function_f] .
        qed
        thus ?thesis 
          using negate_eq
          using linear_combination_x 
          using x_in_V unfolding linear_combination_def by auto
      qed
      also have "…=\<zero>\<^bsub>V\<^esub>" using V.l_neg[OF x_in_V] .
      finally show ?thesis by simp
    qed
    have not_all_zero: " ¬ (∀x::'b∈insert x X. ?g x = \<zero>)"
    proof -
      have minus_one_not_zero: "\<ominus>\<one> ≠ \<zero>"
        --"We know that 1 is not 0, but not that - 1 is not 0. We have to prove it."
        proof (rule notI)
          assume minus_one_eq_zero: "\<ominus> \<one> = \<zero>"
          hence " \<ominus> \<one> ⊕ \<one> = \<zero> ⊕ \<one> " by simp
          hence "\<zero>=\<one>" using K.l_neg using K.one_closed using l_zero by simp
          thus False using K.one_not_zero by simp
        qed
      thus ?thesis
        using x_not_in_X by auto
    qed
    have "?g ∈ coefficients_function (carrier V)  
      ∧ linear_combination ?g (insert x X) = \<zero>\<^bsub>V\<^esub> ∧ ¬ (∀x::'b∈insert x X. ?g x = \<zero>)"
      using coefficients_function_g and sum_zero and not_all_zero by auto
    hence "∃f::'b => 'a.
      f ∈ coefficients_function (carrier V) ∧ linear_combination f (insert x X) = \<zero>\<^bsub>V\<^esub> 
      ∧ ¬ (∀x::'b∈insert x X. f x = \<zero>)"
      apply (rule exI [of _ "?g"]) .
    thus 
      "good_set (insert x X) ∧ 
      (∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f (insert x X) = \<zero>\<^bsub>V\<^esub> 
      ∧ ¬ (∀x∈insert x X. f x = \<zero>))"
      using good_set_X_union_x by simp
  qed
qed

text{*And now we present the second implication. The proof is based on obtaining a linear combination of $insert$ $x$ $X$
  in which not all scalars are zero (we can do it since $X$ is linearly dependent). Hence we prove that the scalar of $x$
  is not zero (if it is, hence $X$ would be dependent and independent so a contradiction). Then, we can express $x$ as a 
  linear combination of the elements of $X$.*}
lemma lc2:
  assumes linear_independent_X: "linear_independent X"
  and x_in_V: "x ∈ carrier V" 
  and x_not_in_X: "x ∉ X"
  shows "linear_dependent (insert x X) 
  ==> (∃ f. f∈ coefficients_function (carrier V) 
  ∧ linear_combination f X = x)"
proof -
  assume linear_dependent_X_union_x: "linear_dependent (insert x X)"
  show "(∃ f. f∈ coefficients_function (carrier V) ∧ linear_combination f X = x)"
  proof -
    have good_set: "good_set X" using l_ind_good_set[OF linear_independent_X] .
    have X_subset_V: "X⊆ carrier V" using good_set unfolding good_set_def by auto
    have finite_X: "finite X" using good_set unfolding good_set_def by auto
    from linear_dependent_X_union_x obtain g 
      where coefficients_function_g: "g ∈ coefficients_function (carrier V)" 
      and sum_zero_g_X_union_x: "linear_combination g (insert x X) = \<zero>\<^bsub>V\<^esub>" 
      and not_all_zero_g_X_union_x: "¬ (∀x∈insert x X. g x = \<zero>)"
      unfolding linear_dependent_def unfolding coefficients_function_def unfolding linear_combination_def  by auto
    have lc_descomposicion: "linear_combination g (insert x X) = g(x)·x ⊕\<^bsub>V\<^esub> linear_combination g X"
    proof (unfold linear_combination_def, rule finsum_insert)
      show "finite X" using finite_X .
      show "x∉ X" using x_not_in_X .
      show "(λy. g y · y) ∈ X -> carrier V"
        using coefficients_function_g unfolding coefficients_function_def using X_subset_V using mult_closed by auto
      show "g x · x ∈ carrier V"  
        using coefficients_function_g unfolding coefficients_function_def using x_in_V using mult_closed by auto
    qed  
    have gx_not_zero: "g x ≠ \<zero>\<^bsub>K\<^esub>"
    proof (rule notI)
      assume gx_zero: "g x = \<zero>\<^bsub>K\<^esub>"           
      have sum_zero_g_X: "linear_combination g X=\<zero>\<^bsub>V\<^esub>"
      proof -
        have gx_x_zero: "g(x)· x=\<zero>\<^bsub>V\<^esub>" using gx_zero using zeroK_mult_V_is_zeroV [OF x_in_V] by auto
        have "\<zero>\<^bsub>V\<^esub>= \<zero>\<^bsub>V\<^esub>⊕\<^bsub>V\<^esub> linear_combination g X"
          using lc_descomposicion using gx_x_zero using sum_zero_g_X_union_x by auto
        also have "…=linear_combination g X"
        proof (rule V.l_zero)
          show "linear_combination g X ∈ carrier V"
          proof (unfold linear_combination_def, rule finsum_closed)
            show "finite X" using good_set unfolding good_set_def by auto
            show "(λy. g y · y) ∈ X -> carrier V"
              using coefficients_function_g unfolding coefficients_function_def 
              using X_subset_V using mult_closed by auto
          qed
        qed
        finally show ?thesis by simp
      qed
      have not_all_zero_g_X: "¬ (∀x∈X. g x = \<zero>)"  using not_all_zero_g_X_union_x and gx_zero by auto
      have "g ∈ coefficients_function (carrier V) ∧ good_set X ∧ linear_combination g X = \<zero>\<^bsub>V\<^esub>" 
        using coefficients_function_g and good_set and sum_zero_g_X by simp
      thus False using linear_independent_X and not_all_zero_g_X unfolding linear_independent_def by auto
    qed
    have "∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f X = x" 
    proof (rule work_out_the_value_of_x)
      show  "good_set X" using good_set .
      show "g ∈ coefficients_function (carrier V)" using coefficients_function_g .
      show "x ∈ carrier V" using x_in_V .
      show "g x ≠ \<zero>" using gx_not_zero .
      show "\<zero>\<^bsub>V\<^esub> = g x · x ⊕\<^bsub>V\<^esub> linear_combination g X" using lc_descomposicion using sum_zero_g_X_union_x by auto
    qed
    thus ?thesis by fast
  qed
qed

text{*Finally, the theorem proving the equivalence of both definitions.*}
lemma lc1_eq_lc2:
  assumes linear_independent_X: "linear_independent X"
  and x_in_V:"x ∈ carrier V" and x_not_in_X:"x ∉ X"
  shows "linear_dependent (insert x X) <-> 
  (∃ f. f∈ coefficients_function (carrier V) 
  ∧ linear_combination f X = x) "
  using assms lc1 lc2 by blast

text{*This lemma doesn't appears in Halmos (but it seems to be a similar result to the theorem 
  \ref{t:combinacion_anteriores}). The proof is based on obtaining a linear combination of the elements of $X \cup Y$ equal
  to $0_V$ where not all scalars are equal to $0_{\mathbb{K}}$. Hence we can express an element $y \in (X \cup Y)$ such that
  its scalar is not zero as a linear combination of the rest elements of $X \cup Y$. This is a long proof of 180 lines.*}
lemma exists_x_linear_combination:
  assumes li_X: "linear_independent X"
  and ld_XY: "linear_dependent (X ∪ Y)"
  shows "∃y∈Y. ∃g. g ∈ coefficients_function (carrier V) 
  ∧ y = linear_combination g (X ∪ (Y - {y}))"
proof -
  from ld_XY obtain f where coefficients_function_f: "f ∈ coefficients_function (carrier V)" 
    and sum_zero_XY: "linear_combination f (X∪Y)=\<zero>\<^bsub>V\<^esub>" 
    and not_all_zero: "¬ (∀x ∈ X∪Y. f x = \<zero>\<^bsub>K\<^esub>)" 
    and good_set_XY: "good_set (X∪Y)"
    unfolding linear_dependent_def by auto
  have "X∪Y=X∪(Y-X)" by simp  
  hence "linear_combination f (X∪Y)= linear_combination f (X∪(Y-X))" by simp
  also have "…=linear_combination f X ⊕\<^bsub>V\<^esub> linear_combination f (Y-X)"
  proof (unfold linear_combination_def, rule finsum_Un_disjoint)
    show "finite X" using good_set_XY unfolding good_set_def by auto
    show "finite (Y - X)" using good_set_XY unfolding good_set_def by auto
    show "X ∩ (Y - X) = {}" by simp
    show "(λy. f y · y) ∈ X -> carrier V"
    proof (unfold Pi_def, auto)
      fix x
      assume x_in_X: "x ∈ X"
      hence x_in_V: "x ∈ carrier V" using good_set_XY unfolding good_set_def by fast
      show "f x · x ∈ carrier V" using fx_x_in_V[OF x_in_V coefficients_function_f] .
      qed
    show "(λy. f y · y) ∈ Y - X -> carrier V"
    proof -
      have "Y-X ⊆ carrier V" using good_set_XY unfolding good_set_def by auto
      thus ?thesis using coefficients_function_f unfolding coefficients_function_def using mult_closed by auto
    qed
  qed
  finally have descomposicion: "linear_combination f X ⊕\<^bsub>V\<^esub> linear_combination f (Y - X)=\<zero>\<^bsub>V\<^esub>" using sum_zero_XY by simp 
  have "¬(∀x ∈ (Y-X). f x = \<zero>\<^bsub>K\<^esub>)"
  proof (rule notI)
    assume all_zero_YX: "(∀x ∈ (Y-X). f x = \<zero>\<^bsub>K\<^esub>)"
    have good_set_X:"good_set X" using good_set_XY unfolding good_set_def by auto 
    have "linear_combination f (Y-X)=\<zero>\<^bsub>V\<^esub>"
    proof -
      have YX_in_V: "Y-X ⊆ carrier V" using good_set_XY unfolding good_set_def by auto
      have finite_YX:"finite (Y-X)" using good_set_XY unfolding good_set_def by auto    
      have good_set_X:"good_set X" using good_set_XY unfolding good_set_def by auto       
      have "(\<Oplus>\<^bsub>V\<^esub>y∈Y - X. f y · y)=(\<Oplus>\<^bsub>V\<^esub>y∈Y - X. \<zero>\<^bsub>V\<^esub>)"
      proof (rule finsum_cong')
        show "Y - X = Y - X" by simp
        show "(λy. \<zero>\<^bsub>V\<^esub>) ∈ Y - X -> carrier V" by simp
        show "!!i. i ∈ Y - X ==> f i · i = \<zero>\<^bsub>V\<^esub>" using YX_in_V using all_zero_YX using zeroK_mult_V_is_zeroV by auto
      qed
      also have "…=\<zero>\<^bsub>V\<^esub>" using finsum_zero[OF finite_YX] .
      finally show ?thesis unfolding linear_combination_def by simp
    qed
    hence "linear_combination f X=\<zero>\<^bsub>V\<^esub>" 
      using descomposicion and good_set_X
        and V.r_zero[OF linear_combination_closed[OF good_set_X coefficients_function_f]] by auto
    hence "(∀x∈X. f x = \<zero>)"
      using coefficients_function_f and good_set_X and li_X unfolding linear_independent_def by auto
    hence "(∀x∈X∪(Y-X). f x = \<zero>)" using all_zero_YX by auto
    hence "(∀x∈X∪Y. f x = \<zero>)" by auto
    thus False using not_all_zero by contradiction
  qed
  then obtain y where y_in_Y: "y ∈ Y" and y_notin_X: "y ∉ X" and fy_not_zero: "f(y)≠\<zero>\<^bsub>K\<^esub>" by auto
  hence igualdad_conjuntos: "insert y ((Y-X)-{y})=Y-X"  by auto
  have "linear_combination f (insert y ((Y-X)-{y}))=f(y)·y ⊕\<^bsub>V\<^esub> linear_combination f ((Y-X)-{y})"
  proof (unfold linear_combination_def, rule finsum_insert)
    show "finite (Y - X - {y})" using good_set_XY unfolding good_set_def by auto
    show "y ∉ Y - X - {y}" by simp
    show "(λx. f x · x) ∈ Y - X - {y} -> carrier V"
    proof -
      have "(Y - X - {y}) ⊆ carrier V" using good_set_XY unfolding good_set_def by auto
      thus ?thesis
        using coefficients_function_f unfolding coefficients_function_def 
        using mult_closed by auto
    qed
    show "f y · y ∈ carrier V"
    proof (rule mult_closed)
      show "y ∈ carrier V" using y_in_Y and good_set_XY unfolding good_set_def by auto
      show "f(y) ∈ carrier K" 
        using coefficients_function_f unfolding coefficients_function_def 
        using good_set_XY unfolding good_set_def using y_in_Y by auto
    qed
  qed
  hence eq_lc_when_out_of_set_is_zero: "linear_combination f (Y-X)=f(y)·y ⊕\<^bsub>V\<^esub> linear_combination f ((Y-X)-{y})"
    using igualdad_conjuntos by auto
  have good_set_X: "good_set X" using good_set_XY unfolding good_set_def by simp
  have cb_YXy: "good_set (Y-X-{y})"using good_set_XY unfolding good_set_def by auto
  have cb_XYy: "good_set (X∪(Y-{y}))" using good_set_XY unfolding good_set_def by auto
  have fy_in_K:"f(y) ∈ carrier K"
    using coefficients_function_f unfolding coefficients_function_def 
    using y_in_Y good_set_XY unfolding good_set_def by auto
  hence mfy_in_K: "\<ominus>\<^bsub>K\<^esub> f(y) ∈ carrier K" using K.a_inv_closed by auto
  have "\<ominus>\<^bsub>K\<^esub> f(y) ≠ \<zero>\<^bsub>K\<^esub>"
  proof (rule notI)
    assume "\<ominus> f y = \<zero>"
    hence "\<ominus>(\<ominus> f(y)) =\<ominus>\<zero>" by auto
    hence "f(y)=\<zero>" using fy_in_K and K.minus_minus and K.minus_zero by auto
    thus False using fy_not_zero by contradiction
  qed
  hence mfy_in_Units_K: "\<ominus>\<^bsub>K\<^esub> f(y) ∈ Units K" using mfy_in_K and K.field_Units by auto
  hence inv_mfy_in_K: "inv(\<ominus>\<^bsub>K\<^esub> f(y)) ∈ carrier K" by auto
  have fy_y_in_V: "f(y)·y ∈ carrier V"
  proof (rule mult_closed)
    show "y∈ carrier V" using y_in_Y good_set_XY unfolding good_set_def by auto
    show "f(y) ∈ carrier K" using fy_in_K .
  qed
  have "linear_combination f (Y-X)=linear_combination f ((Y-X)-{y}) ⊕\<^bsub>V\<^esub> f(y)·y"
    using eq_lc_when_out_of_set_is_zero V.a_comm
    [OF linear_combination_closed[OF cb_YXy coefficients_function_f] fy_y_in_V] by auto
  hence "linear_combination f X ⊕\<^bsub>V\<^esub> (linear_combination f ((Y-X)-{y}) ⊕\<^bsub>V\<^esub> f(y)·y)=\<zero>\<^bsub>V\<^esub>"
    using descomposicion by auto
  hence descomposicion2: "linear_combination f X ⊕\<^bsub>V\<^esub> linear_combination f ((Y-X)-{y}) ⊕\<^bsub>V\<^esub> f(y)·y=\<zero>\<^bsub>V\<^esub>"
    using  V.a_assoc
    [OF linear_combination_closed[OF good_set_X coefficients_function_f] linear_combination_closed
      [OF cb_YXy coefficients_function_f] fy_y_in_V] by auto
  hence "linear_combination f X ⊕\<^bsub>V\<^esub> linear_combination f ((Y-X)-{y}) ⊕\<^bsub>V\<^esub> f(y)·y ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (f(y)·y)=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (f(y)·y)" by simp
  have igualdad_conjuntos2: "X∪((Y-X)-{y}) = X∪(Y-{y})" using y_in_Y y_notin_X by auto
  have "linear_combination f (X∪((Y-X)-{y})) = linear_combination f X ⊕\<^bsub>V\<^esub> linear_combination f ((Y-X)-{y})"
  proof (unfold linear_combination_def, rule finsum_Un_disjoint)
    show "finite X" using good_set_X unfolding good_set_def by auto
    show "finite (Y - X - {y})" using good_set_XY unfolding good_set_def by auto
    show " X ∩ (Y - X - {y}) = {}" using y_in_Y y_notin_X by auto
    show "(λx. f x · x) ∈ X -> carrier V"
      using good_set_X unfolding good_set_def 
      using coefficients_function_f unfolding coefficients_function_def using mult_closed by auto
    show "(λx. f x · x) ∈ Y - X - {y} -> carrier V"               
    proof -
      have "(Y - X - {y}) ⊆ carrier V" using good_set_XY unfolding good_set_def by auto
      thus ?thesis
        using coefficients_function_f unfolding coefficients_function_def 
        using mult_closed by auto
    qed
  qed
  hence "linear_combination f (X∪(Y-{y})) = linear_combination f X ⊕\<^bsub>V\<^esub> linear_combination f ((Y-X)-{y})"
    using igualdad_conjuntos2 by auto
  hence "linear_combination f (X∪(Y-{y})) ⊕\<^bsub>V\<^esub> f(y)·y ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (f(y)·y)=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (f(y)·y)" using descomposicion2 by auto
  hence "linear_combination f (X∪(Y-{y})) ⊕\<^bsub>V\<^esub> (f(y)·y ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (f(y)·y))=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (f(y)·y)" 
    using V.a_assoc[OF linear_combination_closed [OF cb_XYy coefficients_function_f] fy_y_in_V V.a_inv_closed[OF fy_y_in_V]]
    by auto
  hence "linear_combination f (X∪(Y-{y})) ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> (f(y)·y)" using V.r_neg[OF fy_y_in_V] by auto
  hence "linear_combination f (X∪(Y-{y}))= \<ominus>\<^bsub>V\<^esub>(f(y)·y)" 
    using V.r_zero[OF linear_combination_closed [OF cb_XYy coefficients_function_f]]
    using V.l_zero[OF V.a_inv_closed[OF fy_y_in_V]]
    by auto
  hence "linear_combination f (X∪(Y-{y}))= (\<ominus>\<^bsub>K\<^esub>f(y)·y)" using good_set_XY unfolding good_set_def using y_in_Y
    using negate_eq2[OF _ fy_in_K] by auto
  hence "inv(\<ominus>\<^bsub>K\<^esub>f(y)) · linear_combination f (X∪(Y-{y}))= inv(\<ominus>\<^bsub>K\<^esub>f(y))·(\<ominus>\<^bsub>K\<^esub>f(y)·y)" by simp
  hence "inv(\<ominus>\<^bsub>K\<^esub>f(y)) · linear_combination f (X∪(Y-{y}))= ((inv(\<ominus>\<^bsub>K\<^esub>f(y))) ⊗\<^bsub>K\<^esub>(\<ominus>\<^bsub>K\<^esub>f(y)))· y"
    using y_in_Y using good_set_XY unfolding good_set_def using mult_assoc[OF _ inv_mfy_in_K mfy_in_K,symmetric]
    by auto
  hence "inv(\<ominus>\<^bsub>K\<^esub>f(y)) · linear_combination f (X∪(Y-{y}))= \<one>\<^bsub>K\<^esub>· y" using K.Units_l_inv[OF mfy_in_Units_K] by auto
  hence "inv(\<ominus>\<^bsub>K\<^esub>f(y)) · linear_combination f (X∪(Y-{y}))= y"
    using y_in_Y using good_set_XY unfolding good_set_def using mult_1 by auto
  hence descomposicion3: "linear_combination (%i. inv(\<ominus>\<^bsub>K\<^esub>f(y))⊗ f(i)) (X∪(Y-{y}))= y"
    using linear_combination_rdistrib[OF cb_XYy coefficients_function_f inv_mfy_in_K] by auto
  let ?g="(%i. inv(\<ominus>\<^bsub>K\<^esub>f(y))⊗ f(i))"
  have coefficients_function_g: "?g ∈ coefficients_function (carrier V)"
  proof (unfold coefficients_function_def, unfold Pi_def, auto)
    fix x
    assume x_in_V: "x ∈ carrier V"
    hence fx_in_K: "f x ∈ carrier K" using coefficients_function_f unfolding coefficients_function_def by auto
    show "inv (\<ominus> f y) ⊗ f x ∈ carrier K" using K.m_closed [OF inv_mfy_in_K fx_in_K] .
    next
    fix x
    assume x_notin_V: "x ∉ carrier V"
    have "inv (\<ominus> f y) ⊗ f x = inv (\<ominus> f y) ⊗ \<zero>" 
      using x_notin_V coefficients_function_f unfolding coefficients_function_def by simp
    also have "...= \<zero>" using K.r_null[OF inv_mfy_in_K] .
    finally show "inv (\<ominus> f y) ⊗ f x = \<zero>" .
  qed
  have "linear_combination ?g (X∪(Y-{y}))= y" using descomposicion3 by auto
  hence "?g ∈ coefficients_function (carrier V) ∧ y=linear_combination ?g (X∪(Y-{y}))"
    using coefficients_function_g by auto
  hence "∃g. g ∈ coefficients_function (carrier V) ∧ y=linear_combination g (X∪(Y-{y}))"
    apply (rule exI[of _ ?g]) .
  thus ?thesis using y_in_Y by auto
qed

text{*A corollary of the previous lemma claims that if we have a linearly dependent set, then there exists one element
which can be expressed as a linear combination of the other elements of the set.*}
corollary exists_x_linear_combination2:
  assumes ld_Y: "linear_dependent Y"
  shows "∃y∈Y. ∃g. g ∈ coefficients_function (carrier V) 
  ∧ y = linear_combination g (Y - {y})"
proof -
  have ld_empty_Y: "linear_dependent({} ∪ Y)" using ld_Y by simp
  have "∃y∈Y. ∃g. g ∈ coefficients_function (carrier V) 
    ∧ y = linear_combination g ({} ∪ (Y - {y}))" 
    using exists_x_linear_combination
    [OF empty_set_is_linearly_independent ld_empty_Y] .
  thus ?thesis by simp
qed

text{*Every singleton set is linearly independent. This lemma could be in previous section, however we have
  to make use of some properties of linear combinations. We can repeat the proof without these properties,
  but it would be longer. We will use that @{text "a · x = \<zero> ==> a = \<zero>"} because @{term "x ≠ \<zero>"}.*}

lemma unipuntual_is_li:
  assumes x_in_V: "x ∈ carrier V" and x_not_zero: "x ≠ \<zero>\<^bsub>V\<^esub>"
  shows "linear_independent {x}"
proof (cases "linear_independent {x}")
  case True show ?thesis using True .
next
  case False show ?thesis
  proof -
    have cb: "good_set {x}" 
      using x_in_V unfolding good_set_def by simp
    have "linear_dependent {x}" 
      using False 
      using not_independent_implies_dependent[OF cb False] 
      by auto
    from this obtain f 
      where cf_f: "f ∈ coefficients_function (carrier V)" 
      and lc: "linear_combination f {x} = \<zero>\<^bsub>V\<^esub>" 
      and not_all_zero: " ¬ (∀x∈{x}. f x = \<zero>)" 
      unfolding linear_dependent_def by auto
    have fx_not_zero: "f x ≠ \<zero>" using not_all_zero by auto
    have "(f x) · x = \<zero>\<^bsub>V\<^esub>" thm finsum_insert
    proof -
      --"We could have used @{thm linear_combination_singleton[no_vars]} directly or next calculation:"
      have "linear_combination f (insert x {}) 
        = (f x) · x ⊕\<^bsub>V\<^esub> linear_combination f {}" 
        using linear_combination_insert[OF _ x_in_V _ cf_f] 
        by auto
      also have "… = (f x) · x ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>" 
        using linear_combination_of_zero by auto
      also have "… = (f x) · x"
      using V.r_zero[OF fx_x_in_V[OF x_in_V cf_f]] .
      finally show ?thesis using lc by auto
    qed
    hence "f x = \<zero>\<^bsub>K\<^esub>" 
      using mult_zero_uniq and x_in_V and x_not_zero and cf_f 
      unfolding coefficients_function_def  by auto 
    thus ?thesis using fx_not_zero by contradiction
  qed
qed

(*PRIMER INTENTO*)

  (*PRIMER INTENTO, FALLO PORQUE LA f NO ES CONMUTATIVA A IZQUIERDA*)
  (*
  definition f
  where "f x A = (if linear_independent (insert x A) then (insert x A) else A)"
  *)
  (*definition remove
  where "remove = fold f"
  *)
  (*term remove*)

  (*lemma "remove A {} = A"
  by(simp add: remove_def)
  *)

(*EL SIGUIENTE LEMA ES FALSO. CONTRAEJEMPLO CORREO*)
(*lemma
  assumes fin_B: "finite B" and b_not: "b ~: B"
  shows "remove A (insert b B) = (if linear_independent (insert b A) then remove (insert b A) B else remove A B)"
proof -
  interpret fun_left_comm f
  proof (unfold_locales)
    fix x :: "'b" and y :: "'b" and Z :: "'b set"
    show "f x (f y Z) = f y (f x Z)"
    proof (cases "linear_independent (insert y Z)")
      case False note ld_yZ = False
      show ?thesis
      proof (cases "linear_independent (insert x Z)")
        case False note ld_xZ = False
        show ?thesis using ld_yZ ld_xZ unfolding f_def by simp
      next
        case True note li_xZ = True
        show ?thesis using ld_yZ li_xZ unfolding f_def apply auto
        proof (rule FalseE)
          assume nli_yZ: "¬ linear_independent (insert y Z)" and li_yxZ: "linear_independent (insert y (insert x Z))"
          have ld_yZ: "linear_dependent (insert y Z)" 
          proof (rule not_independent_implies_dependent)
            show "good_set (insert y Z)" using l_ind_good_set[OF li_yxZ] unfolding good_set_def by auto
            show "¬ linear_independent (insert y Z)" using nli_yZ .
          qed
          have good_set_yxZ: "good_set (insert y (insert x Z))"
            using l_ind_good_set[OF li_yxZ] unfolding good_set_def by auto
          hence ld_yxZ: "linear_dependent (insert y (insert x Z))"
            using linear_dependent_subset_implies_linear_dependent_set[OF _ good_set_yxZ ld_yZ] by auto
          hence nli_yxZ: "¬ linear_independent (insert y (insert x Z))" 
            using dependent_implies_not_independent[OF ld_yxZ] by auto
          thus False using li_yxZ by contradiction
        qed
      qed
    next
      case True note li_yZ = True
      show ?thesis
      proof (cases "linear_independent (insert x Z)")
        case False note ld_xZ = False
        show ?thesis using li_yZ ld_xZ unfolding f_def apply auto 

        proof (rule FalseE)
          assume nli_xZ: "¬ linear_independent (insert x Z)" and li_xyZ: "linear_independent (insert x (insert y Z))"
          have ld_xZ: "linear_dependent (insert x Z)" 
          proof (rule not_independent_implies_dependent)
            show "good_set (insert x Z)" using l_ind_good_set[OF li_xyZ] unfolding good_set_def by auto
            show "¬ linear_independent (insert x Z)" using nli_xZ .
          qed
          have good_set_yxZ: "good_set (insert x (insert y Z))"
            using l_ind_good_set[OF li_xyZ] unfolding good_set_def by auto
          hence ld_yxZ: "linear_dependent (insert x (insert y Z))"
            using linear_dependent_subset_implies_linear_dependent_set[OF _ good_set_yxZ ld_xZ] by auto
          hence nli_yxZ: "¬ linear_independent (insert x (insert y Z))" 
            using dependent_implies_not_independent[OF ld_yxZ] by auto
          thus False using li_xyZ by contradiction
        qed
      next
        case True note li_xZ = True
        show ?thesis
          using li_yZ li_xZ
          unfolding f_def [of x Z]
          unfolding f_def [of y Z] apply simp
          unfolding f_def [of x "insert y Z"]
          unfolding f_def [of y "insert x Z"]
          unfolding insert_commute
          apply simp apply rule apply auto

  *)
  (*
lemma
  assumes fin_B: "finite B" and b_not_in_B: "b ∉ B"
  shows "remove A (insert b B) = f b (remove A B)"
proof -
  interpret fun_left_comm f sorry
  show ?thesis 
    unfolding remove_def
    using fold_insert_remove [OF assms (1), of A b]
    using b_not_in_B by simp
qed

  *)

  (*FIN DEL PRIMER INTENTO*)


  (*SEGUNDO INTENTO, PRIMERA IDEA DE JULIO*)

  (*
  definition f
  where "f x A = (if linear_independent (insert x A) then (insert x A) else A)"
  
  definition g
  where "g X = {x ∈ carrier V. (∃f. (f ∈ coefficients_function ∧ linear_combination f X = x))}"

  definition h
  where "h x A = g (f x A)"
  
  definition remove
  where "remove = fold h"
  *)

(*
lemma
  assumes fin_B: "finite B" and b_not_in_B: "b ∉ B"
  shows "remove A (insert b B) =
  (if linear_independent (insert b A) then remove (insert b A) B else remove A B)"
proof -
  interpret fun_left_comm f sorry
  show ?thesis 
    unfolding remove_def
    unfolding fold_insert2[OF assms]
    unfolding f_def by auto
    by(simp add: remove_def h_def fold_insert2[OF assms])
qed*)

(*definition basis_2
  where "basis_2 X = (linear_independent_ext X ∧ g X = V)"*)
(*
lemma "remove A {} = A"
  by(simp add: remove_def)
*)
(*lemma
  assumes fin_B: "finite B"
  shows "fold h (g A) B = fold h A B"
  using fin_B proof (induct B set: finite)
  case empty
  show ?case apply simp unfolding g_def*)
(*
lemma
  assumes fin_B: "finite B" and b_not_in_B: "b ∉ B"
  shows "remove A (insert b B) = h b (remove A B)"
proof -
  interpret fun_left_comm h sorry
  show ?thesis 
    unfolding remove_def
    using fold_insert_remove [OF assms (1), of A b]
    using b_not_in_B by simp
qed

lemma
  assumes fin_B: "finite B" and b_not_in_B: "b ∉ B"
  shows "remove A (insert b B) =
  (if linear_independent (insert b A) then remove (g (insert b A)) B else remove (g A) B)"
proof-
  interpret fun_left_comm h sorry
  show ?thesis
    unfolding remove_def
    unfolding fold_insert2[OF assms]
    unfolding h_def
    unfolding f_def by simp
qed
*)
(*El siguiente lema es el que expresa que la capacidad expresiva de remove se mantiene intacta tras cada iteración.*)
(*
lemma
  assumes fin_B: "finite B"
  shows "g (remove A B) = g (A ∪ B)"
  using fin_B proof (induct set: finite)
  case empty
  show ?case
    sorry
next
  case insert
  show ?case
    sorry
qed
*)
(*El siguiente lema expresa que la colección formada preseva la condición de independencia lineal*)
(*
lemma
  assumes "linear_independent A"
  and fin_B: "finite B"
  shows "linear_independent (remove A B)"
  using fin_B proof (induct set: finite)
  case empty
  show ?case
    sorry
next
  case insert
  show ?case
    sorry
qed
*)
(*Error*)

(*lemma 
  assumes "linear_independent A"
  and "finite_dimensional V"
  shows "∃B. basis B ∧ (B = A ∪ A')"
proof -
apply auto
    unfolding g_id
    unfolding f_def by simp
  proof (cases "linear_independent (insert b A)")
    case True
    show "fold h (g (if linear_independent (insert b A) then insert b A else A)) B =
    (if linear_independent (insert b A) then fold h (insert b A) B else fold h A B)"
      using True apply simp
      using fin_B proof (induct B: rule finite)
    apply auto
    by(simp add: remove_def h_def fold_insert2[OF assms])
qed
*)


(*FIN DEL SEGUNDO INTENTO*)



(*ULTIMO INTENTO, SEGUNDA IDEA DE JULIO*)
(*
definition g
  where "g X = {x ∈ carrier V. (∃f. (f ∈ coefficients_function ∧ linear_combination f X = x))}"

definition f
  where "f A B = (if (g A = g B) then \<zero>\<^bsub>V\<^esub> else (SOME b. b ∈ B ∧ 
  (linear_independent (A ∪ {b}))))"

term f

*)
(*
lemma "f A {} = a"
  sorry

function (tailrec) F
  where "F A B = (if f A B = \<zero>\<^bsub>V\<^esub> then A else F (A ∪ {f A B}) B)"
  by auto

lemma
  assumes "linear_independent A"
  and fin_B: "finite B" and B_ne: "B ≠ {}"
  shows "∃X. F A B = A ∪ X"
  using fin_B and B_ne 
proof (induct set: finite)
  case empty then show ?case by auto
next
  case (insert b B) then show ?case 
    proof (unfold F.simps[of A "insert b B"])
      show "∃X. (if f A (insert b B) = \<zero>\<^bsub>V\<^esub> then A else F (A ∪ {f A (insert b B)}) (insert b B)) = A ∪ X"
        proof (cases "f A (insert b B) = \<zero>\<^bsub>V\<^esub>")
          case True show ?thesis using True by auto
          next
          case False show ?thesis
          sorry
        qed
     qed
qed

*)              
            
(*

lemma 
  assumes "linear_independent A"
  and fin_B: "finite B" and B_ne: "B ≠ {}"
  and basis: "basis B"
  shows "basis (F A B)"
   using fin_B and B_ne proof (induct set: finite)
   case empty show ?case 
     proof (rule FalseE)
       show False using empty (1) by simp
     qed
     next
     case (insert b B) then show ?case sorry -- "No tiene porqué cumplirse F A B = F A (insert b B)"
qed*)
  
(*Con B el conjunto vacío no se puede definir nada*)
(*
lemma "F A {} = {}"
  unfolding F.simps [of A "{}"]
  unfolding f_def
  unfolding F_def sorry
*)
(*
lemma
  assumes fd_V: "finite_dimensional V"
  and li_Y: "linear_independet Y"
  shows "basis Y | (∃X. basis (Y ∪ X))"
proof (cases "basis Y")
  case True thus ?thesis by fast
next
  case False
  show ?thesis
  proof -
    from fd_V obtain B where "basis B" -- "unfolding finite_dimensional_def" sorry
    show ?thesis
      proof (rule disjI2, rule exI [of _ "F Y B"])
        
      .
      F Y B
    
*)


(*FIN DEL TERCER INTENTO*)

(*LO PROBAMOS USANDO LOS INDEXINGS*)


text{*Now we are ready to prove the theorem 1 in section 6 in Halmos. 
  It will be useful (really indispensable) in future proofs and it is
  basic in our developement. The theorem claims that in a linear dependent set exists an element which is a linear 
  combination of the preceding ones.*}

text{*NOTE: As we are assuming that @{term "\<zero>\<^bsub>V\<^esub>"} is not in the set, the element which is a 
  linear combination of the preceding ones will be between the
  second and the last position of the set ($1$ and $card(A)-1$ with the notation 
  used in our implementation of indexed sets). The element in the first position (position $0$) can't be 
  a linear combination of the preceding ones because it would be a linear combination of the empty set, 
  hence this element would be @{term "\<zero>\<^bsub>V\<^esub>"} and it is not in the set.*}

text{*We make the proof using induction (we don't follow the proof of the book). At first, it seemed easier this way.*}
lemma
  linear_dependent_set_contains_linear_combination:
  assumes ld_X: "linear_dependent X"
  and not_zero: "\<zero>\<^bsub>V \<^esub>∉ X"
  shows "∃y ∈ X. ∃g. ∃k::nat. ∃f ∈ {i. i<(card X)} -> X. f`{i. i<(card X)} = X ∧ g ∈ coefficients_function (carrier V)  
  ∧ (1::nat) ≤ k ∧ k < (card X) ∧ f k = y ∧ y = linear_combination g (f`{i::nat. i<k})"
proof -
  have good_set_X: "good_set X" using l_dep_good_set[OF ld_X] .
  hence finite_X: "finite X" unfolding good_set_def by simp
  thus ?thesis using ld_X and not_zero
  proof (induct set: finite)
    case empty 
    show ?case 
      -- "Contradiction: we can prove that the empty set is linearly
      dependent."
      using empty_set_is_linearly_independent
        and dependent_implies_not_independent [OF empty.prems (1)] by contradiction
  next
    case (insert x X)
    show ?case
    proof -
        --"Some previous facts which will be useful in the proof:" 
      have finite_xX: "finite (insert x X)"
        using insert.hyps(1) by auto
      have cb_X: "good_set X"
        using l_dep_good_set[OF insert.prems(1)]
        unfolding good_set_def by auto
      show ?thesis 
        --"Now we separate the proof in cases, depending on the set @{term X} is linearly dependent."
      proof (cases "linear_dependent X")
        case True
        have zero_not_in_X: "\<zero>\<^bsub>V\<^esub> ∉ X" using insert.prems(2) by simp
        --"We obtain the 'candidates' for the goal, using the induction hypothesis."
        obtain y f g k
          where y_in_X: "y ∈ X" 
          and cf_g: "g ∈ coefficients_function (carrier V)" and one_le_k:" 1 ≤ k" and k_le_card_X:" k < card  X"
          and fk_y: "f k = y" and y_lc:" y = linear_combination g (f ` {i. i < k})" and ordenfX: "f `{i. i < card X} = X"
          using insert.hyps(3)[OF True zero_not_in_X] by auto
        have f_buena:"f ∈ {i. i < (card X)} -> X" using ordenfX by auto
        have y_in_xX:"y ∈ (insert x X)" using y_in_X by simp
        obtain h where h: "h ∈ {i. i < (card (insert x X))} -> (insert x X)" 
          and ordenxX:"h`{i. i < (card (insert x X))} = (insert x X)" 
          and h_cardX_x: "h (card X) = x" and h_is_f_in_X: "∀i. i<card(X) --> h(i)=f(i)"
          using indexation_x_union_X[OF insert.hyps(1) insert.hyps(2) f_buena ordenfX] by auto          
        show ?thesis
          --"We introduce the candidates: we have to proof that satisfy the requirements:"
        proof (rule bexI [of _ y], rule exI [of _ g], rule exI [of _ k], rule bexI [of _ h], rule conjI6)
          show "y ∈ insert x X" using y_in_X by fast
          show "h ∈ {i. i < card (insert x X)} -> insert x X" using ordenxX by fast
          show "h ` {i. i < card (insert x X)} = insert x X" using ordenxX .
          show "g ∈ coefficients_function (carrier V)" using cf_g .
          show "1 ≤ k" using one_le_k .
          show "k < card (insert x X)" using k_le_card_X 
            by (metis card_insert_disjoint insert.hyps(1) insert.hyps(2) less_Suc_eq)
          show "h k = y" using fk_y and h_is_f_in_X and k_le_card_X by simp
          show "y = linear_combination g (h ` {i. i < k})" 
            using y_lc and h_is_f_in_X and k_le_card_X
            unfolding image_def by auto
        qed
      next
        case False 
        --"We try to do it similarly: we define the candidates for the existencial terms (in this case we can not 
          obtain it from the induction hypothesis)  and finally we will face the thesis"
        have li_X: "linear_independent X" using not_dependent_implies_independent[OF cb_X False] .
        obtain y and g 
          where y_x: "y=x" and cf_g: "g ∈ coefficients_function (carrier V)" 
          and x_lc_X: "x = linear_combination g X" 
          using insert.prems(1)
          using exists_x_linear_combination[OF li_X, of "{x}"] by auto
        obtain f where ordenfX: "X = f ` {i. i<(card X)}"
          using finite_imp_nat_seg_image_inj_on_Pi_card[of "X"]
          using insert.hyps (1) by auto
        hence f_buena: "f ∈ {i. i < (card X)} -> X" by auto
        obtain h where h: "h ∈ {i. i < (card (insert x X))} -> (insert x X)" 
          and ordenxX:"h`{i. i < (card (insert x X))} = (insert x X)" 
          and h_cardX_x: "h (card X) = x" and h_is_f_in_X: "∀i. i<card(X) --> h(i)=f(i)"
          using indexation_x_union_X[OF insert.hyps(1) insert.hyps(2) f_buena ordenfX [symmetric]] by auto
        show ?thesis
        proof (cases "1 ≤ card X")
          case True 
          show ?thesis
          proof (rule bexI [of _ x], rule exI [of _ g], rule exI [of _ "card X"], rule bexI [of _ h], rule conjI6)
            show "h ` {i. i < card (insert x X)} = insert x X"
              using ordenxX .
            show "g ∈ coefficients_function (carrier V)"
              using cf_g .
            show "1 ≤ (card X)"  using True .
            show "card X < card (insert x X)"
              by (metis card_insert_disjoint insert.hyps(1) insert.hyps(2) lessI)
            show "h (card X) = x" using h_cardX_x .
            show "x = linear_combination g (h ` {i. i < (card X)})"
              using h_is_f_in_X ordenfX x_lc_X unfolding image_def by auto
            show "h ∈ {i. i < card (insert x X)} -> insert x X" using h .
            show "x ∈ insert x X" by fast
          qed
        next
          case False 
          show ?thesis
          proof (rule FalseE)
            have "1>(card X)" using False by simp
            hence X_empty: "X = {}" using card_eq_0_iff and insert.hyps(1) by simp
            have ld_x: "linear_dependent {x}" using insert.prems(1) unfolding X_empty .
            have li_x: "linear_independent {x}"
            proof (rule unipuntual_is_li)
              show "x ∈ carrier V"
                using l_dep_good_set [OF ld_x]
                unfolding good_set_def by simp
              show "x ≠ \<zero>\<^bsub>V\<^esub>" using insert.prems(2) by auto
            qed
            show False 
              using independent_implies_not_dependent [OF li_x] and ld_x
              by contradiction
          qed
        qed
      qed
    qed
  qed
qed

(*lemma
  assumes step: "!!A. (!!B. card B < card A ==> P B) ==> P A"
  shows "P A"
  apply (rule measure_induct_rule [of card P A])
  using step .*)


lemma
  card_less_induct_good_set:
  assumes c: "good_set A"
  and step: "!!A. [| (!!B. [| card B < card A; good_set B |] ==> P B); 
  good_set A |] ==> P A"
  shows "P A"
proof -
  have f: "finite A" using good_set_finite [OF c] .
  have "!!B. [|card B ≤ card A; good_set B|] ==> P B"
    using f c proof (induct)
    case empty
    show ?case
      apply (rule step)
      using empty.prems by auto
  next
    case (insert x F)
    show ?case
      apply (rule step)
      using insert.prems
      using insert.hyps
      unfolding good_set_def by auto
  qed
  thus ?thesis using c by auto
qed

text{*Really, the result that we need to prove corresponds closer to the next theorem than
  we have proved in the previous theorem @{text linear_dependent_set_contains_linear_combination}. 
  We have to assume that the indexation is
  known beforehand. This will be necessary in the future, because we will remove dependent elements in regard a
  gived indexation of one set (so the removed element will be unique). We will apply this theorem iteratively to a set
  in future proofs, so if we didn't fix the order beforehand we won't have unicity of the result (because the indexing could
  change in each step).*}

text{*We will use the induction rule for indexed sets that we introduced before (@{text indexed_set_induct2}).
This is a laborious and large theorem, of about 400 code lines.*}
theorem
  linear_dependent_set_sorted_contains_linear_combination:
  assumes ld_A: "linear_dependent A"
  and not_zero: "\<zero>\<^bsub>V \<^esub>∉ A"
  and i: "indexing (A, f)" 
  shows "∃y∈A. ∃g. ∃k::nat. 
  g ∈ coefficients_function (carrier V)
  ∧ (1::nat) ≤ k ∧ k < (card A) 
  ∧ f k = y ∧ y = linear_combination g (f`{i::nat. i<k})"
  using i and ld_A and not_zero
proof (induct A f rule: indexed_set_induct2)
  show "indexing (A, f)" by fact
  case (empty f)
  show "∃y∈{}. ∃g k. g ∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧ k < card {} ∧ f k = y 
    ∧ y = linear_combination g (f ` {i. i < k})"
    using "empty.prems" (2) and independent_implies_not_dependent[OF empty_set_is_linearly_independent] by contradiction
next
  case (insert a A f n)
  show ?case
  proof -
    have good_set_aA: "good_set (insert a A)" using l_dep_good_set [OF prems(12)] .
    hence good_set_A: "good_set A" unfolding good_set_def by simp
    have indexing_Af: "indexing (A,f)"
      using indexing_indexing_ext prems (8) prems (9) prems (10) prems (5)
      by auto 
    have not_zero_A: "\<zero>\<^bsub>V\<^esub> ∉ A" using prems(13) by simp
    have finite_A: "finite A" using prems(7) by auto
    show ?thesis
    proof (cases "linear_dependent A")
      case True show ?thesis
      proof -
        have ex: "∃y∈A. ∃g k. g ∈ coefficients_function (carrier V) ∧
          1 ≤ k ∧
          k < card A ∧
          f k = y ∧ y = linear_combination g (f ` {i. i < k})"
          using prems(6)[OF indexing_Af  indexing_Af True not_zero_A] .
        from this obtain y g k where cf_g: "g ∈ coefficients_function (carrier V)"
          and one_le_k: "1≤k" and k_le_cardA: "k < (card A)" 
          and fk_y: "f k = y" 
          and y_lc_g_f: "y = linear_combination g (f ` {i. i < k})"
          and y_in_A: "y∈A" by auto
        have one_le_k_plus_one: "1≤(k+1)" using one_le_k by simp
        have k_plus_one_le_card_insert_a_A: "(k+1)<card(insert a A)"
          using k_le_cardA and card_insert_if[OF finite_A, of "a"] using prems(5) by auto
        let ?h="(λx. if x ∈ (f`{i. i < k}) then g(x) else \<zero>\<^bsub>K\<^esub>)"                         
        have cb_imf: "good_set (f`{i. i < k})" 
          using indexing_Af unfolding indexing_def 
          unfolding bij_betw_def unfolding iset_to_index_def unfolding iset_to_set_def 
          using k_le_cardA one_le_k using good_set_A unfolding good_set_def
          by auto                
        hence cf_h: "?h ∈ coefficients_function (carrier V)" using coefficients_function_g_f_null[OF cf_g] by auto
        have cb_a: "good_set {a}" using good_set_aA unfolding good_set_def  by auto       
        show ?thesis
        proof (cases "1≤k")
          case False show ?thesis
          proof (rule FalseE)
            have "k=0" using False by simp
            hence "f ` {i. i < k} = {}" by auto
            hence "linear_combination g (f ` {i. i < k})=\<zero>\<^bsub>V\<^esub>" by auto
            hence "\<zero>\<^bsub>V\<^esub>=y" using y_lc_g_f by simp
            thus False using y_in_A and not_zero_A by auto
          qed
        next
          case True
          note one_le_k = True
          show ?thesis
          proof (cases "k<n")
            case True show ?thesis
            proof -
              have "(indexing_ext (A, f) a n) k = f k" 
                using True
                unfolding indexing_ext_def by auto
              hence 1:"indexing_ext (A, f) a n k = y" using fk_y by simp
              have "indexing_ext (A, f) a n ` {i. i < k} = f` {i. i < k}"
                using True unfolding indexing_ext_def by auto
              hence "linear_combination g (indexing_ext (A, f) a n ` {i. i < k})= linear_combination g (f ` {i. i < k})" 
                using arg_cong2 by auto
              hence 2: "y=linear_combination g (indexing_ext (A, f) a n ` {i. i < k})" using y_lc_g_f by auto
              have "k < card (insert a A)" 
                using prems(5) and k_le_cardA and card_insert_if and finite_A by auto
              thus ?thesis using 1 2 one_le_k y_in_A cf_g by force
            qed
          next
            case False note k_ge_n = False show ?thesis
            proof (cases "k=n")
              case True show ?thesis  
              proof -
                have 1:"indexing_ext (A, f) a n ` {i. i < k} = f` {i. i < k}"
                  using True unfolding indexing_ext_def by auto
                hence "linear_combination g (indexing_ext (A, f) a n ` {i. i < k})= linear_combination g (f ` {i. i < k})" 
                  using arg_cong2 by auto
                hence "y=linear_combination g (indexing_ext (A, f) a n ` {i. i < k})" using y_lc_g_f by auto
                have igualdad_conjuntos: "{i. i < (k+1)}={i. i < k}∪{i. i = k}" by auto
                hence "indexing_ext (A, f) a n ` {i. i < (k+1)}=indexing_ext (A, f) a n ` ({i. i < k}∪{i. i = k})" by auto
                also have "...=indexing_ext (A, f) a n ` {i. i < k} ∪ indexing_ext (A, f) a n ` {i. i = k}" by auto
                also have "...= f` {i. i < k} ∪ {a}" using 1 and True unfolding indexing_ext_def by auto
                finally have 2:"indexing_ext (A, f) a n ` {i. i < (k+1)}=f` {i. i < k} ∪ {a}" .                
                hence y_lc_h: "y=linear_combination ?h (indexing_ext (A, f) a n ` {i. i < (k+1)})"
                proof -
                  have "linear_combination ?h (indexing_ext (A, f) a n ` {i. i < (k+1)})
                    =linear_combination ?h (f` {i. i < k} ∪ {a})" 
                    using arg_cong2 using 2 by auto
                  also have "...=linear_combination g (f` {i. i < k})" 
                    using eq_lc_when_out_of_set_is_zero[OF cb_a cb_imf cf_g] by auto
                  also have "...=y" using y_lc_g_f by simp
                  finally show ?thesis by simp
                qed                
                have "(indexing_ext (A, f) a n) (k+1) = f k"
                  using True
                  unfolding indexing_ext_def by auto
                hence 3:"(indexing_ext (A, f) a n) (k+1) = y" using fk_y by simp
                show ?thesis using cf_h one_le_k_plus_one k_plus_one_le_card_insert_a_A 3 y_lc_h y_in_A by force 
                  -(*"We can do it with force method, but not using auto. We can also do (we have to write scape character):
                  proof (rule bexI [of _ y], rule exI [of _ \"?h\"], rule exI [of _ \"k+1\"])"*)
              qed
            next
              case False show ?thesis
              proof -
                have k_g_n: "k>n" using False and k_ge_n by simp
                hence "(indexing_ext (A, f) a n) (k+1) = f k"
                  unfolding indexing_ext_def by auto
                hence indexing_ext_y: "(indexing_ext (A, f) a n) (k+1) = y" using fk_y by simp 
                have 1:"indexing_ext (A, f) a n ` {i. i < n} = f` {i. i < n}"
                  unfolding indexing_ext_def by auto
                have 2:"indexing_ext (A, f) a n ` {i. n < i ∧ i<(k+1)} = f` {i. n ≤ i ∧ i<k}"
                  using k_g_n unfolding indexing_ext_def unfolding iset_to_index_def 
                  unfolding image_def 
                proof auto
                  show "!!xa. [|n < xa; xa < Suc k|] ==> ∃x≥n. x < k ∧ f (xa - Suc 0) = f x"
                  proof -
                    fix xa
                    assume n_l_xa: "n<xa" and xa_l_suc_k: "xa<(Suc k)"
                    let ?x= "xa-(Suc 0)"
                    have 1:"f(xa - Suc 0)=f (?x)" by simp
                    have 2:"?x≥n" using n_l_xa by auto
                    have 3:"?x < k"using xa_l_suc_k
                      by (metis One_nat_def diff_less gr0I gr_implies_not0 
                        k_g_n less_imp_diff_less linorder_neqE_nat not_less_eq zero_less_Suc)
                    show "∃x≥n. x < k ∧ f (xa - Suc 0) = f x" using 1 and 2 and 3 by auto
                  qed
                  show "!!xa. [|n ≤ xa; xa < k|] ==> ∃x>n. x < Suc k ∧ f xa = f (x - Suc 0)"
                  proof -
                    fix xa
                    assume n_le_xa: "n≤xa" and xa_l_k: "xa<k"
                    let ?x= "xa+(Suc 0)"
                    have 1:"f(xa)=f (?x - Suc 0)" by simp
                    have 2:"?x>n" using n_le_xa by auto
                    have 3:"?x < Suc k"using xa_l_k by auto
                    show "∃x>n. x < Suc k ∧ f xa = f (x - Suc 0)" using 1 and 2 and 3 by auto
                  qed
                qed                
                have "{i. i < (k+1)}={i. i < n}∪{i. i = n}∪{i. n<i ∧ i<(k+1)}" using k_g_n by auto
                hence "indexing_ext (A, f) a n ` {i. i < (k+1)}=indexing_ext (A, f) a n ` ({i. i < n}
                  ∪{i. i = n}∪{i. n<i ∧ i<(k+1)})" by auto
                also have "...=indexing_ext (A, f) a n ` {i. i < n} ∪ indexing_ext (A, f) a n ` {i. i = n}
                  ∪ indexing_ext (A, f) a n ` {i. n<i ∧ i<(k+1)}" by auto
                also have "...= f` {i. i < n} ∪ {a} ∪ f`{i. n≤i ∧ i<k}" using 1 2 k_g_n unfolding indexing_ext_def by auto
                also have "...=f` {i. i < k} ∪ {a}"
                proof -
                  have "{i. i < k}={i. i < n}∪{i. n≤i ∧ i<k}" using k_g_n by auto
                  hence "f`{i. i < k}=f`{i. i < n}∪f`{i. n≤i ∧ i<k}" by auto
                  thus ?thesis by auto
                qed
                finally have 3: "indexing_ext (A, f) a n ` {i. i < (k+1)}=f` {i. i < k} ∪ {a}" .                
                have y_lc_h: "y=linear_combination ?h (indexing_ext (A, f) a n ` {i. i < (k+1)})"
                proof -
                  have "linear_combination ?h (indexing_ext (A, f) a n ` {i. i < (k+1)})
                    =linear_combination ?h (f` {i. i < k} ∪ {a})" 
                    using arg_cong2 using 3 by auto
                  also have "...=linear_combination g (f` {i. i < k})" 
                    using eq_lc_when_out_of_set_is_zero[OF cb_a cb_imf cf_g] by auto
                  also have "...=y" using y_lc_g_f by simp
                  finally show ?thesis by simp
                qed             
                show ?thesis
                  using cf_h one_le_k_plus_one k_plus_one_le_card_insert_a_A indexing_ext_y 3 y_lc_h y_in_A by force
              qed
            qed 
          qed 
        qed 
      qed
    next
      case False show ?thesis
      proof -
        have li_A: "linear_independent A" using False and independent_if_only_if_not_dependent and good_set_A by simp
        from prems(12) obtain h
          where cf_h: "h ∈ coefficients_function (carrier V)" 
          and sum_zero: "linear_combination h (insert a A)=\<zero>\<^bsub>V\<^esub>"
          and not_all_zero: "¬ (∀x∈insert a A. h x =\<zero>\<^bsub>K\<^esub>)"
          unfolding linear_dependent_def by auto        
        have 1:"indexing_ext (A,f) a n ` {..<(card(insert a A))} = (insert a A)" using prems(8)
          unfolding indexing_def unfolding bij_betw_def 
          unfolding iset_to_index_def by auto        
        let ?A="{k∈{..<card (insert a A)}. h ((indexing_ext (A,f) a n) k) ≠ \<zero>\<^bsub>K\<^esub>}"
        have finite_A: "finite ?A" by auto
        have A_not_empty: "?A≠{}" using not_all_zero using 1 by force        
        def m == "Max ?A"
        have m_in_A: "m∈ ?A" using Max.closed[OF finite_A A_not_empty] unfolding m_def by force        
        have "∀x∈{..<card (insert a A)}. (x<card(insert a A))" by auto
        hence m_le_card_aA: "m<(card(insert a A))"  using Max_less_iff [OF finite_A A_not_empty] unfolding m_def by auto
        have "¬ (∃x∈?A. m < x)" using Max_less_iff [OF finite_A A_not_empty] unfolding m_def by auto        
        hence h_indexing_m_card_zero: "∀x∈{m<..<(card(insert a A))}. h ((indexing_ext (A,f) a n) x) = \<zero>\<^bsub>K\<^esub>" by auto
        have indexing_m_in_aA: "indexing_ext (A,f) a n m ∈ (insert a A)" using 1 using m_le_card_aA by auto        
        have descomposicion_conjunto:"{..<(card(insert a A))}= {..m} ∪ {m<..<(card(insert a A))}"                         
          using m_le_card_aA unfolding m_def by auto
        have "indexing_ext (A,f) a n `{..<(card(insert a A))}
          = indexing_ext (A,f) a n ` ({..m}∪{m<..<(card(insert a A))})"
          unfolding  descomposicion_conjunto  ..
        also have"...= indexing_ext (A,f) a n ` {..m} ∪ indexing_ext (A,f) a n `{m<..<(card(insert a A))}" by auto
        finally have descomposicion_indexing_ext: "indexing_ext (A, f) a n ` {..<card (insert a A)} = 
          indexing_ext (A, f) a n ` {..m} ∪ indexing_ext (A, f) a n ` {m<..<card (insert a A)}" .                
        have descomposicion_conjunto2: "{..m}=insert m {..<m}" by auto
        hence descomposicion_indexing_ext2:"indexing_ext (A, f) a n ` {..m}
          =(insert (indexing_ext (A, f) a n m) (indexing_ext (A, f) a n ` {..<m}))"
          by auto        
        have cb_l_m: "good_set (indexing_ext (A, f) a n ` {..m})"
        proof -
          have "indexing_ext (A, f) a n ` {..m}
            ⊆ indexing_ext (A, f) a n ` {..<card (insert a A)}" using m_le_card_aA by auto
          hence "indexing_ext (A, f) a n ` {..m}⊆ (insert a A)" using 1 by simp
          thus ?thesis using good_set_aA unfolding good_set_def by auto
        qed
        have i_m_in_V: "indexing_ext (A, f) a n m ∈ carrier V" using cb_l_m unfolding good_set_def by auto                
        have "\<zero>\<^bsub>V\<^esub>=linear_combination h (indexing_ext (A,f) a n ` {..<(card(insert a A))})" using sum_zero 1 by auto
        also have "...=linear_combination h (indexing_ext (A, f) a n ` {..m} 
          ∪ indexing_ext (A, f) a n ` {m<..<card (insert a A)})"
          using descomposicion_indexing_ext by auto        
        also have "...= linear_combination h (indexing_ext (A, f) a n ` {..m}) 
          ⊕\<^bsub>V\<^esub> linear_combination h (indexing_ext (A, f) a n ` {m<..<card (insert a A)})"
        proof (unfold linear_combination_def, rule finsum_Un_disjoint,force)
          show "finite (indexing_ext (A, f) a n ` {m<..<card (insert a A)})" using m_le_card_aA by auto
          show "indexing_ext (A, f) a n ` {..m} ∩ indexing_ext (A, f) a n ` {m<..<card (insert a A)} = {}" 
          proof -
            have disjuntos: "{..m} ∩ {m<..<(card(insert a A))}={}"  by auto
            have " indexing_ext (A,f) a n ` {..m}∩indexing_ext (A,f) a n `{m<..<(card(insert a A))}=
              indexing_ext (A,f) a n ` ({..m}∩{m<..<(card(insert a A))})"
            proof(rule inj_on_image_Int[symmetric])
              show "inj_on (indexing_ext (A,f) a n) {..<card(insert a A)}"
                using prems(8) 
                unfolding indexing_def unfolding iset_to_set_def iset_to_index_def 
                unfolding bij_betw_def by simp
              show "{..m} ⊆ {..<card (insert a A)}" using m_le_card_aA by auto
              show "{m<..<card (insert a A)} ⊆ {..<card (insert a A)}" using m_le_card_aA by auto
            qed
            also have "...={}" using disjuntos by simp
            finally show ?thesis .
          qed
          show "(λy. h y · y) ∈ indexing_ext (A, f) a n ` {..m} -> carrier V"  
          proof (auto,rule mult_closed)
            fix x
            assume x_le_m: "x≤m"
            show "indexing_ext (A, f) a n x ∈ carrier V" 
              using 1 and good_set_aA 
              unfolding good_set_def unfolding indexing_ext_def unfolding iset_to_index_def 
              using x_le_m and m_le_card_aA by auto
            thus "h (indexing_ext (A, f) a n x) ∈ carrier K" using cf_h unfolding coefficients_function_def by auto
          qed
          show "(λy. h y · y) ∈ indexing_ext (A, f) a n ` {m<..<card (insert a A)} -> carrier V"
          proof (auto,rule mult_closed)
            fix x
            assume m_le_x: "m<x"
              and x_le_card_aA: "x<card(insert a A)"
            show "indexing_ext (A, f) a n x ∈ carrier V" 
              using 1 and good_set_aA 
              unfolding good_set_def unfolding indexing_ext_def unfolding iset_to_index_def 
              using m_le_x and x_le_card_aA by auto                                   
            thus "h (indexing_ext (A, f) a n x) ∈ carrier K" using cf_h unfolding coefficients_function_def by auto
          qed
        qed        
        also have "...= linear_combination h (indexing_ext (A, f) a n ` {..m}) ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>"
        proof -                    
          have "linear_combination h (indexing_ext (A, f) a n ` {m<..<card (insert a A)})=\<zero>\<^bsub>V\<^esub>"
          proof (unfold linear_combination_def) 
            have hy_zero: "!!y. [|y∈indexing_ext (A, f) a n ` {m<..<card (insert a A)}|] ==> h y = \<zero>\<^bsub>K\<^esub>" 
              using h_indexing_m_card_zero by auto
            have "(\<Oplus>\<^bsub>V\<^esub>y∈indexing_ext (A, f) a n ` {m<..<card (insert a A)}. h y · y) = 
              (\<Oplus>\<^bsub>V\<^esub>y∈indexing_ext (A, f) a n ` {m<..<card (insert a A)}. \<zero>\<^bsub>V\<^esub>) "
            proof (rule finsum_cong')
              show "indexing_ext (A, f) a n ` {m<..<card (insert a A)} 
                = indexing_ext (A, f) a n ` {m<..<card (insert a A)}" ..
              show "(λy. \<zero>\<^bsub>V\<^esub>) ∈ indexing_ext (A, f) a n ` {m<..<card (insert a A)} -> carrier V" by auto
              show "!!i. i ∈ indexing_ext (A, f) a n ` {m<..<card (insert a A)} ==> h i · i = \<zero>\<^bsub>V\<^esub>"
              proof -
                fix i
                assume i_in_indexing: "i ∈ indexing_ext (A, f) a n ` {m<..<card (insert a A)}"
                show "h i · i = \<zero>\<^bsub>V\<^esub>"
                proof -
                  have hi_zero:"h(i)=\<zero>\<^bsub>K\<^esub>" using hy_zero[OF i_in_indexing] .
                  have i_in_V: "i∈ carrier V" using 1
                  proof -
                    have "indexing_ext (A, f) a n ` {m<..<card (insert a A)}
                      ⊆ indexing_ext (A, f) a n ` {..<card (insert a A)}" using m_le_card_aA by auto
                    hence "indexing_ext (A, f) a n ` {m<..<card (insert a A)} ⊆ (insert a A)" using 1 by simp
                    thus ?thesis using i_in_indexing and good_set_aA unfolding good_set_def by auto
                  qed
                  show ?thesis using zeroK_mult_V_is_zeroV and hi_zero and i_in_V by auto
                qed
              qed
            qed
            also have "...=\<zero>\<^bsub>V\<^esub>" 
            proof (rule finsum_zero)
              show "finite (indexing_ext (A, f) a n ` {m<..<card (insert a A)})"
              proof -
                have "indexing_ext (A, f) a n ` {m<..<card (insert a A)}
                  ⊆ indexing_ext (A, f) a n ` {..<card (insert a A)}" using m_le_card_aA by auto
                hence "indexing_ext (A, f) a n ` {m<..<card (insert a A)}⊆ (insert a A)" using 1 by simp
                thus ?thesis using good_set_aA unfolding good_set_def by auto
              qed 
            qed
            finally show "(\<Oplus>\<^bsub>V\<^esub>y∈indexing_ext (A, f) a n ` {m<..<card (insert a A)}. h y · y) = \<zero>\<^bsub>V\<^esub>" .
          qed
          thus ?thesis by auto
        qed
        also have "...=linear_combination h (indexing_ext (A, f) a n ` {..m})"
        proof (rule V.r_zero, rule linear_combination_closed)
          show  "good_set (indexing_ext (A, f) a n ` {..m})" using cb_l_m .          
          show "h ∈ coefficients_function (carrier V)" using cf_h .
        qed        
        also have  "...=h (indexing_ext (A, f) a n m) · (indexing_ext (A, f) a n m) 
          ⊕\<^bsub>V\<^esub> linear_combination h (indexing_ext (A, f) a n ` {..<m})"
        proof -
          have "linear_combination h (indexing_ext (A, f) a n ` {..m})
            = linear_combination h ((insert (indexing_ext (A, f) a n m) (indexing_ext (A, f) a n ` {..<m})))"
            using arg_cong2 and descomposicion_indexing_ext2 by auto
          also have "...
            = h (indexing_ext (A, f) a n m) · indexing_ext (A, f) a n m 
            ⊕\<^bsub>V\<^esub> linear_combination h (indexing_ext (A, f) a n ` {..<m})"
          proof (rule linear_combination_insert)
            show "good_set (indexing_ext (A, f) a n ` {..<m})" using cb_l_m unfolding good_set_def by auto
            show "indexing_ext (A, f) a n m ∈ carrier V" using i_m_in_V .
            show "indexing_ext (A, f) a n m ∉ indexing_ext (A, f) a n ` {..<m}" 
            proof -
              have inj_on_m: "inj_on (indexing_ext (A, f) a n)  {..m}"
                proof (rule subset_inj_on)
                  show "inj_on (indexing_ext (A, f) a n) {..<card(insert a A)}" 
                    using prems(8) unfolding indexing_def unfolding bij_betw_def by auto
                  show "{..m}⊆{..<card(insert a A)}" using m_le_card_aA by auto
                  qed
              hence auxiliar:"{indexing_ext (A, f) a n m} ⊆ indexing_ext (A, f) a n ` {m} " by auto
              have d1:"{..m}={..<m}∪{m}" by auto
              have "{..<m}∩{m}={}" by auto
              hence disjuntos: "(indexing_ext (A, f) a n) ` {..<m} ∩ (indexing_ext (A, f) a n)` {m}={}" 
                using inj_on_m and d1 by auto
              show ?thesis
                proof (cases "indexing_ext (A, f) a n m ∉ indexing_ext (A, f) a n ` {..<m}")
                  case True thus ?thesis .
                  next
                  case False show ?thesis
                    proof (rule FalseE)
                      have "indexing_ext (A, f) a n m ∈ indexing_ext (A, f) a n ` {..<m}" using False by auto
                      thus False using auxiliar and disjuntos by auto
                      qed
            qed 
          qed 
            show "h ∈ coefficients_function (carrier V)" using cf_h .
          qed
          finally show ?thesis by auto
        qed
        finally have descomposicion_lc: "\<zero>\<^bsub>V\<^esub>=h (indexing_ext (A, f) a n m) · indexing_ext (A, f) a n m 
          ⊕\<^bsub>V\<^esub> linear_combination h (indexing_ext (A, f) a n ` {..<m})" .        
        have "∃w. w ∈ coefficients_function (carrier V) 
          ∧ linear_combination w (indexing_ext (A, f) a n ` {..<m}) = indexing_ext (A, f) a n m"
        proof (rule work_out_the_value_of_x)
          show "good_set (indexing_ext (A, f) a n ` {..<m})" using cb_l_m unfolding good_set_def by auto
          show "h ∈ coefficients_function (carrier V)" using cf_h .
          show "indexing_ext (A, f) a n m ∈ carrier V" using cb_l_m unfolding good_set_def by auto
          show "h (indexing_ext (A, f) a n m) ≠ \<zero>" using m_in_A by simp
          show "\<zero>\<^bsub>V\<^esub> = h (indexing_ext (A, f) a n m) · indexing_ext (A, f) a n m 
            ⊕\<^bsub>V\<^esub> linear_combination h (indexing_ext (A, f) a n ` {..<m})" using descomposicion_lc .
        qed        
        from this obtain w where cf_w: "w ∈ coefficients_function (carrier V)" and
          lc_w: "linear_combination w (indexing_ext (A, f) a n ` {..<m}) = indexing_ext (A, f) a n m" by auto
        have one_le_m: "1≤m"
        proof (cases "1≤m")
          case True thus ?thesis .
        next
          case False show ?thesis
          proof (rule FalseE)
            have m_zero: "m=0" using False by auto
            hence not_zero:"indexing_ext (A, f) a n m ≠ \<zero>\<^bsub>V\<^esub>" using m_in_A
              by (metis "1" "insert"(9) imageI lessThan_iff m_le_card_aA)
            have zero: "linear_combination w (indexing_ext (A, f) a n ` {..< m})=\<zero>\<^bsub>V\<^esub>" using m_zero by auto
            show False using lc_w and zero and not_zero by auto
          qed
        qed        
            (*"Isabelle can not prove it with: show ?thesis using cf_w one_le_m m_le_card_aA lc_w indexing_m_in_aA by force.
            I will descompose it more."*)
        let ?y="indexing_ext (A, f) a n m"
        have "{i. i < m}={..<m}" by auto
        hence "?y = linear_combination w (indexing_ext (A, f) a n ` {i. i < m})" using lc_w by auto
        thus ?thesis using cf_w and one_le_m and m_le_card_aA and indexing_m_in_aA by force
      qed
    qed 
  qed
  next
  show "finite A"using l_dep_good_set [OF ld_A] unfolding good_set_def by simp
qed

text{*The proof can be also done without induction and then the proof of the theorem is shorter: ``only'' 200 code lines.
  The proof is a generalization of one of the cases in the induction above.*}

theorem
  linear_dependent_set_sorted_contains_linear_combination2:
  assumes ld_A: "linear_dependent A"
  and not_zero: "\<zero>\<^bsub>V \<^esub>∉ A"
  and i: "indexing (A, f)" 
  shows "∃y∈A. ∃g. ∃k::nat. 
  g ∈ coefficients_function (carrier V)
  ∧ (1::nat) ≤ k ∧ k < (card A) 
  ∧ f k = y ∧ y = linear_combination g (f`{i::nat. i<k})"
proof -
  have good_set_A: "good_set A" using l_dep_good_set[OF ld_A] .
  from ld_A obtain h
    where cf_h: "h ∈ coefficients_function (carrier V)" 
    and sum_zero: "linear_combination h A=\<zero>\<^bsub>V\<^esub>"
    and not_all_zero: "¬ (∀x∈A. h x =\<zero>\<^bsub>K\<^esub>)"
    unfolding linear_dependent_def by auto  
  have 1: "f ` {..<(card A)} = A" using i
    unfolding indexing_def unfolding bij_betw_def 
    unfolding iset_to_index_def by auto  
  let ?A="{k∈{..<card A}. h (f k) ≠ \<zero>\<^bsub>K\<^esub>}"
  have finite_A: "finite ?A" by auto
  have A_not_empty: "?A≠{}" using not_all_zero using 1 by force  
  def m ≡ "Max ?A"  
  have m_in_A: "m ∈ ?A" using Max.closed[OF finite_A A_not_empty] unfolding m_def by force  
  have "∀x∈{..<card A}. (x<card A)" by auto
  hence m_le_card_aA: "m<(card A)"  using Max_less_iff [OF finite_A A_not_empty] unfolding m_def by auto
  have "¬ (∃x∈?A. m < x)" using Max_less_iff [OF finite_A A_not_empty] unfolding m_def by auto  
  hence h_indexing_m_card_zero: "∀x∈{m<..<(card A)}. h (f x) = \<zero>\<^bsub>K\<^esub>" by auto 
  have indexing_m_in_aA: "f m ∈ A" using 1 using m_le_card_aA by auto  
  have descomposicion_conjunto:"{..<(card A)} = {..m} ∪ {m<..<(card A)}"                         
    using m_le_card_aA unfolding m_def by auto
  have "f `{..<(card A)}
    = f ` ({..m}∪{m<..<(card A)})"
    unfolding  descomposicion_conjunto  ..
  also have"...= f ` {..m} ∪ f `{m<..<(card(A))}" by auto
  finally have descomposicion_indexing_ext: "f ` {..<card A} = 
    f ` {..m} ∪ f ` {m<..<card A}" .    
  have descomposicion_conjunto2: "{..m}=insert m {..<m}" by auto
  hence descomposicion_indexing_ext2: "f ` {..m} = (insert (f m) (f ` {..<m}))"
    by auto  
  have cb_l_m: "good_set (f ` {..m})"
  proof -
    have "f ` {..m} ⊆ f ` {..<card (A)}" using m_le_card_aA by auto
    hence "f ` {..m} ⊆ A" using 1 by simp
    thus ?thesis using good_set_A unfolding good_set_def by auto
  qed
  have i_m_in_V: "f m ∈ carrier V" using cb_l_m unfolding good_set_def by auto    
  have "\<zero>\<^bsub>V\<^esub>=linear_combination h (f ` {..<card A})" using sum_zero 1 by auto
  also have "...=linear_combination h (f ` {..m} ∪ f ` {m<..<card A})"
    using descomposicion_indexing_ext by auto  
  also have "...= linear_combination h (f ` {..m}) 
    ⊕\<^bsub>V\<^esub> linear_combination h (f ` {m<..<card A})"
  proof (unfold linear_combination_def, rule finsum_Un_disjoint,force)
    show "finite (f ` {m<..<card A})" using m_le_card_aA by auto
    show "f ` {..m} ∩ f ` {m<..<card A} = {}" 
    proof -
      have disjuntos: "{..m} ∩ {m<..<(card(A))}={}"  by auto
      have "f ` {..m}∩f `{m<..<(card(A))}=
        f ` ({..m}∩{m<..<(card(A))})"
      proof(rule inj_on_image_Int[symmetric])
        show "inj_on f {..<card(A)}"
          using i 
          unfolding indexing_def unfolding iset_to_set_def iset_to_index_def 
          unfolding bij_betw_def by simp
        show "{..m} ⊆ {..<card A}" using m_le_card_aA by auto
        show "{m<..<card (A)} ⊆ {..<card (A)}" using m_le_card_aA by auto
      qed
      also have "...={}" using disjuntos by simp
      finally show ?thesis .
    qed
    show "(λy. h y · y) ∈ f ` {..m} -> carrier V"  
    proof (auto,rule mult_closed)
      fix x
      assume x_le_m: "x≤m"
      show "f x ∈ carrier V" 
        using 1 and good_set_A 
        unfolding good_set_def unfolding indexing_ext_def unfolding iset_to_index_def 
        using x_le_m and m_le_card_aA by auto
      thus "h (f x) ∈ carrier K" using cf_h unfolding coefficients_function_def by auto
    qed
    show "(λy. h y · y) ∈ f ` {m<..<card (A)} -> carrier V"
    proof (auto,rule mult_closed)
      fix x
      assume m_le_x: "m<x"
        and x_le_card_aA: "x<card(A)"
      show "f x ∈ carrier V" 
        using 1 and good_set_A 
        unfolding good_set_def unfolding indexing_ext_def unfolding iset_to_index_def 
        using m_le_x and x_le_card_aA by auto                                   
      thus "h (f x) ∈ carrier K" using cf_h unfolding coefficients_function_def by auto
    qed
  qed  
  also have "...= linear_combination h (f ` {..m}) ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub>"
  proof -                    
    have "linear_combination h (f ` {m<..<card (A)})=\<zero>\<^bsub>V\<^esub>"
    proof (unfold linear_combination_def) 
      have hy_zero: "!!y. [|y∈f ` {m<..<card (A)}|] ==> h y = \<zero>\<^bsub>K\<^esub>" 
        using h_indexing_m_card_zero by auto
      have "(\<Oplus>\<^bsub>V\<^esub>y∈f ` {m<..<card (A)}. h y · y) = 
        (\<Oplus>\<^bsub>V\<^esub>y∈f ` {m<..<card (A)}. \<zero>\<^bsub>V\<^esub>) "
      proof (rule finsum_cong')
        show "f ` {m<..<card (A)} 
          = f ` {m<..<card (A)}" ..
        show "(λy. \<zero>\<^bsub>V\<^esub>) ∈ f ` {m<..<card (A)} -> carrier V" by auto
        show "!!i. i ∈ f ` {m<..<card (A)} ==> h i · i = \<zero>\<^bsub>V\<^esub>"
        proof -
          fix i
          assume i_in_indexing: "i ∈ f ` {m<..<card (A)}"
          show "h i · i = \<zero>\<^bsub>V\<^esub>"
          proof -
            have hi_zero:"h(i)=\<zero>\<^bsub>K\<^esub>" using hy_zero[OF i_in_indexing] .
            have i_in_V: "i∈ carrier V" using 1
            proof -
              have "f ` {m<..<card (A)}
                ⊆ f ` {..<card (A)}" using m_le_card_aA by auto
              hence "f ` {m<..<card A}⊆ A" using 1 by simp
              thus ?thesis using i_in_indexing and good_set_A unfolding good_set_def by auto
            qed
            show ?thesis using zeroK_mult_V_is_zeroV and hi_zero and i_in_V by auto
          qed
        qed
      qed
      also have "...=\<zero>\<^bsub>V\<^esub>" 
      proof (rule finsum_zero)
        show "finite (f ` {m<..<card (A)})"
        proof -
          have "f ` {m<..<card (A)}
            ⊆ f ` {..<card (A)}" using m_le_card_aA by auto
          hence "f ` {m<..<card (A)}⊆ A" using 1 by simp
          thus ?thesis using good_set_A unfolding good_set_def by auto
        qed 
      qed
      finally show "(\<Oplus>\<^bsub>V\<^esub>y∈f ` {m<..<card (A)}. h y · y) = \<zero>\<^bsub>V\<^esub>" .
    qed
    thus ?thesis by auto
  qed
  also have "...=linear_combination h (f` {..m})"
  proof (rule V.r_zero, rule linear_combination_closed)
    show  "good_set (f ` {..m})" using cb_l_m .    
    show "h ∈ coefficients_function (carrier V)" using cf_h .
  qed  
  also have  "...=h (f m) · (f m) 
    ⊕\<^bsub>V\<^esub> linear_combination h (f ` {..<m})"
  proof -
    have "linear_combination h (f ` {..m})
      = linear_combination h ((insert (f m) (f ` {..<m})))"
      using arg_cong2 and descomposicion_indexing_ext2 by auto
    also have "...
      =h (f m) · f m ⊕\<^bsub>V\<^esub> linear_combination h (f` {..<m})"
    proof (rule linear_combination_insert)
      show "good_set (f ` {..<m})" using cb_l_m unfolding good_set_def by auto
      show "f m ∈ carrier V" using i_m_in_V .
      show "f m ∉ f ` {..<m}" 
      proof -
        have inj_on_m: "inj_on f  {..m}"
        proof (rule subset_inj_on)
          show "inj_on f {..<card(A)}" 
            using i unfolding indexing_def unfolding bij_betw_def by auto
          show "{..m}⊆{..<card(A)}" using m_le_card_aA by auto
        qed
        hence auxiliar:"{f m} ⊆ f ` {m} " by auto
        have d1:"{..m}={..<m}∪{m}" by auto
        have "{..<m}∩{m}={}" by auto
        hence disjuntos: "f` {..<m} ∩ f` {m}={}" using inj_on_m and d1 by auto
        show ?thesis
        proof (cases "f m ∉ f ` {..<m}")
          case True thus ?thesis .
        next
          case False show ?thesis
          proof (rule FalseE)
            have "f m ∈ f ` {..<m}" using False by auto
            thus False using auxiliar and disjuntos by auto
          qed
        qed 
      qed 
      show "h ∈ coefficients_function (carrier V)" using cf_h .
    qed
    finally show ?thesis by auto
  qed
  finally have descomposicion_lc: "\<zero>\<^bsub>V\<^esub>=h (f m) · f m 
    ⊕\<^bsub>V\<^esub> linear_combination h (f ` {..<m})" .  
  have "∃w. w ∈ coefficients_function  (carrier V)
    ∧ linear_combination w (f ` {..<m}) = f m"
  proof (rule work_out_the_value_of_x)
    show "good_set (f ` {..<m})" using cb_l_m unfolding good_set_def by auto
    show "h ∈ coefficients_function (carrier V)" using cf_h .
    show "f m ∈ carrier V" using cb_l_m unfolding good_set_def by auto
    show "h (f m) ≠ \<zero>" using m_in_A by simp
    show "\<zero>\<^bsub>V\<^esub> = h (f m) · f m 
      ⊕\<^bsub>V\<^esub> linear_combination h (f ` {..<m})" using descomposicion_lc .
  qed  
  from this obtain w where cf_w: "w ∈ coefficients_function (carrier V)" and
    lc_w: "linear_combination w (f ` {..<m}) = f m" by auto
  have one_le_m: "1≤m"
  proof (cases "1≤m")
    case True thus ?thesis .
  next
    case False show ?thesis
    proof (rule FalseE)
      have m_zero: "m=0" using False by auto
      hence not_zero:"f m ≠ \<zero>\<^bsub>V\<^esub>" using m_in_A 
        by (metis indexing_m_in_aA not_zero)      
      have zero: "linear_combination w (f ` {..< m})=\<zero>\<^bsub>V\<^esub>" using m_zero by auto
      show False using lc_w and zero and not_zero by auto
    qed
  qed  
  let ?y="f m"
  have "{i. i < m}={..<m}" by auto
  hence "?y = linear_combination w (f ` {i. i < m})" using lc_w by auto
  thus ?thesis using cf_w and one_le_m and m_le_card_aA and indexing_m_in_aA by force
qed

end
end