Up to index of Isabelle/HOL/HOL-Algebra/Vector_Spaces
theory Basistheory Basis
imports Linear_combinations
begin
section{*Basis*}
context vector_space
begin
text{*A finite spanning set is a finite set of vectors that can generate every vector in the space through
such linear combinations.*}
definition spanning_set :: "'b set => bool"
where "spanning_set X = (good_set X
∧ (∀x. x ∈ carrier V --> (∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f X = x)))"
text{*Even, we can talk about an infinite spanning set. We say that a set (finite or infinite) @{term "X ⊆ carrier V"}
is a spanning set (we will rename this definition as @{text spanning_set_ext}) if for every @{term "x ∈ carrier V"}
it is possible to choose a finite subset of X such that exists a linear combination of its elements equal to x.*}
text{*As we have said before, the sums are all finite: we can not talk about an infinite sum of vectors without
adding some concepts and more structure (the axioms of Vector Space do not allow it).*}
definition spanning_set_ext :: "'b set => bool"
where "spanning_set_ext X = (∀x. x ∈ carrier V -->
(∃A. ∃f. good_set A ∧ A ⊆ X ∧ f ∈ coefficients_function (carrier V) ∧ linear_combination f A = x))"
text{*Let's see the compatibility between the definitions:*}
text{*Now we prove that every @{text spanning_set} is a @{text spanning_set_ext}: *}
lemma spanning_imp_spanning_ext:
assumes sp_X: "spanning_set X"
shows "spanning_set_ext X"
unfolding spanning_set_ext_def
using sp_X
by (auto simp add: mem_def spanning_set_def subset_refl)
text{*Whenever we have a @{text spanning_set_ext} which is finite and @{text "X ⊆ carrier V"} then it is a @{text spanning_set}. *}
lemma gs_spanning_ext_imp_spanning:
assumes sp_X: "spanning_set_ext X"
and gs_X: "good_set X"
shows "spanning_set X"
proof (unfold spanning_set_def, rule conjI)
show "good_set X" using gs_X .
show "∀x. x ∈ carrier V
--> (∃f. f ∈ coefficients_function (carrier V)
∧ linear_combination f X = x)"
proof (auto)
fix x
assume x_in_V: "x ∈ carrier V"
from sp_X obtain A and f where A_in_X: "A ⊆ X"
and gs_A: "good_set A"
and cf_f: "f ∈ coefficients_function (carrier V)"
and lc_fA: "linear_combination f A = x"
unfolding spanning_set_ext_def using x_in_V by blast
def g ≡ "(λx. if x ∈ A then f x else \<zero>)"
have cf_g: "g ∈ coefficients_function (carrier V)"
using cf_f
unfolding coefficients_function_def g_def by force
have "linear_combination g X = x"
proof -
have "x=linear_combination f A" using lc_fA by blast
also have "...=linear_combination g (A∪X)" unfolding g_def
proof (rule eq_lc_when_out_of_set_is_zero[symmetric])
show "good_set X" using gs_X .
show "good_set A" using gs_A .
show "f ∈ coefficients_function (carrier V)" using cf_f .
qed
also have "...=linear_combination g X"
using arg_cong2 [of g g "A∪X" X "linear_combination"]
using A_in_X by fast
finally show ?thesis by fast
qed
thus "∃g. g ∈ coefficients_function (carrier V)
∧ linear_combination g X = x" using cf_g by auto
qed
qed
text{*A basis is an independent spanning set. We define it in general (X could be finite or infinite).*}
definition basis :: "'b set => bool"
where "basis X = (X ⊆ carrier V ∧ linear_independent_ext X ∧ spanning_set_ext X)"
text{*If we have a finite basis, then it is a good set.*}
lemma finite_basis_implies_good_set:
assumes basis_B: "basis B"
and finite_B: "finite B"
shows "good_set B"
using basis_B finite_B unfolding basis_def good_set_def by fast
text{*We introduce the definition of \emph{span} of a determinated set @{term "A::'b set"} like the
set of all elements which can be expressed as a linear combination of the elements of @{term "A::'b set"}.*}
definition span :: "'b set => 'b set"
where "span A = {x. ∃g ∈ coefficients_function (carrier V). x = linear_combination g A}"
text{*First of all, we prove the behavior of @{term "span"} with respect to @{term "{}::'b set"}. *}
lemma
span_empty [simp]:
shows "span {} = {\<zero>\<^bsub>V\<^esub>}"
unfolding span_def
unfolding linear_combination_def
using V.finsum_empty
unfolding coefficients_function_def by auto
text{*One auxiliar result says that @{term "\<zero>\<^bsub>V\<^esub>"} is in the span of every set.*}
lemma
span_contains_zero [simp]:
assumes fin_A: "finite A"
and A_in_V: "A ⊆ carrier V"
shows "\<zero>\<^bsub>V\<^esub> ∈ span A"
proof -
have "\<zero>\<^bsub>V\<^esub> = linear_combination (λx. \<zero>\<^bsub>K\<^esub>) A"
proof (unfold linear_combination_def,
subst finsum_zero [symmetric, OF fin_A], -- "Be careful applying unfold, we enter in a loop."
rule finsum_cong')
show "A = A" by (rule refl)
show "op · \<zero> ∈ A -> carrier V"
unfolding Pi_def
using mult_closed using A_in_V by auto
show "!!i. i ∈ A ==> \<zero>\<^bsub>V\<^esub> = \<zero> · i"
using zeroK_mult_V_is_zeroV using A_in_V by auto
qed
thus ?thesis
unfolding span_def
unfolding coefficients_function_def
unfolding Pi_def using zero_closed by auto
qed
text{*Now we are going to prove that if we remove an element of a set which is a linear combination of the rest of elements
then the span of the set is the same than the span of the set minus the element. This will be a fundamental property to be applied in the future.
First of all, we do two auxiliar proofs.*}
text{*This auxiliary lemma claims that given a coefficients funcion $g$ of $A-\{a\}$ hence there exists another one (denoted by $ga$)
such that @{term "linear_combination g (A-{a})=linear_combination ga A"}. The coefficients function $ga$ will be defined as follows:
@{term "(λx. if x=a then \<zero>\<^bsub>K\<^esub> else g(x))"}. *}
lemma exists_function_Aa_A:
assumes cf_g: "g ∈ coefficients_function (carrier V)"
and good_set_A: "good_set A"
and a_in_A: "a ∈ A"
shows "∃ga ∈ coefficients_function (carrier V).
(\<Oplus>\<^bsub>V\<^esub>y∈A - {a}. g y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈A. ga y · y)"
proof
let ?f="(%x. if x=a then \<zero>\<^bsub>K\<^esub> else g(x))"
show cf_f: "?f ∈ coefficients_function (carrier V)"
using cf_g unfolding coefficients_function_def unfolding Pi_def by auto
show "(\<Oplus>\<^bsub>V\<^esub>y∈A - {a}. g y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈A. ?f y · y)"
proof -
have A_in_V: "A ⊆ carrier V" using good_set_A unfolding good_set_def by simp
hence a_in_V: "a ∈ carrier V" using a_in_A by auto
have good_set_Aa: "good_set (A - {a})"
using good_set_A unfolding good_set_def by auto
have Aa_in_V: "(A - {a}) ⊆ carrier V" using A_in_V by auto
have insert_aA: "(insert a (A - {a}))=A" using a_in_A by auto
have "(\<Oplus>\<^bsub>V\<^esub>y∈(insert a (A-{a})). ?f y · y)= ?f(a)·a ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈A-{a}. ?f y · y)"
proof (rule finsum_insert)
show "finite (A - {a})" using good_set_A unfolding good_set_def by simp
show "a ∉ A - {a}" by simp
show "(λy. (if y = a then \<zero> else g y) · y) ∈ A - {a} -> carrier V"
using A_in_V cf_g unfolding coefficients_function_def
unfolding Pi_def using mult_closed by auto
show "(if a = a then \<zero> else g a) · a ∈ carrier V"
using mult_closed[OF a_in_V K.zero_closed] by auto
qed
also have "...=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈A-{a}. ?f y · y)" using zeroK_mult_V_is_zeroV[OF a_in_V] by auto
also have "...=(\<Oplus>\<^bsub>V\<^esub>y∈A-{a}. ?f y · y)"
using V.l_zero[OF linear_combination_closed [OF good_set_Aa cf_f]]
unfolding linear_combination_def .
also have "...=(\<Oplus>\<^bsub>V\<^esub>y∈A-{a}. g y · y)"
proof (rule finsum_cong')
show "A - {a} = A - {a}" ..
show "(λy. g y · y) ∈ A - {a} -> carrier V"
using Aa_in_V using cf_g
unfolding Pi_def unfolding coefficients_function_def
using mult_closed by auto
show " !!i. i ∈ A - {a} ==> (if i = a then \<zero> else g i) · i = g i · i" by auto
qed
finally show ?thesis using insert_aA by auto
qed
qed
text{*This auxiliary lemma is similar to the previous one.
It claims that given a coefficients function $h$ and another one $g$ such that
@{term "a=linear_combination g (A-{a})"},
there exists a coefficients function $ga$ such that @{term "linear_combination h A=linear_combination ga (A-{a})"}.
This coefficients funcion $ga$ is defined as follows: @{term "(λx. (h a ⊗ g x) ⊕\<^bsub>K\<^esub> h x)"}. In other words,
with these premises every linear combination of elements of $A$ can be expressed as a linear combination of elements
of $A-\{a\}$.*}
lemma exists_function_A_Aa:
assumes cf_h:"h ∈ coefficients_function (carrier V)"
and cf_g: "g ∈ coefficients_function (carrier V)"
and a_lc_g_Aa: "a = linear_combination g (A-{a})"
and good_set_A: "good_set A" and a_in_A: "a∈A"
shows "∃ga ∈ coefficients_function (carrier V).
(\<Oplus>\<^bsub>V\<^esub>y∈A. h y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈A - {a}. ga y · y)"
proof
let ?f= "(%x. (h a ⊗ g x) ⊕\<^bsub>K\<^esub> h x)"
have cb_Aa: "good_set (A - {a})"
using a_in_A and good_set_A unfolding good_set_def by auto
have a_in_V: "a ∈ carrier V"
using a_in_A and good_set_A unfolding good_set_def by auto
have A_in_V: "A⊆ carrier V"
using good_set_A unfolding good_set_def by auto
have igualdad_conjuntos: "insert a (A-{a})=A" using a_in_A by auto
show cf_f: "?f ∈ coefficients_function (carrier V)"
proof (unfold coefficients_function_def, unfold Pi_def, auto)
fix x
assume x_in_V: "x∈ carrier V"
hence "(h a ⊗ g x)∈ carrier K"
using cf_g cf_h a_in_V unfolding coefficients_function_def using K.m_closed by auto
thus "(h a ⊗ g x) ⊕ h x ∈ carrier K"
using K.a_closed [OF _ fx_in_K [OF x_in_V cf_h]] by auto
next
fix x
assume x_notin_V: "x ∉ carrier V"
have "h a ⊗ g x ⊕ h x = h a ⊗ g x ⊕ \<zero>"
using cf_h unfolding coefficients_function_def using x_notin_V by simp
also have "...= h a ⊗ \<zero> ⊕ \<zero>"
using cf_g unfolding coefficients_function_def using x_notin_V by simp
also have "...= \<zero> ⊕ \<zero>" using K.r_null[OF fx_in_K[OF a_in_V cf_h]] by simp
also have "...= \<zero>" by simp
finally show "h a ⊗ g x ⊕ h x = \<zero>" .
qed
show "(\<Oplus>\<^bsub>V\<^esub>y∈A. h y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈A - {a}. ?f y · y)"
proof -
have "linear_combination h (insert a (A-{a})) = h a · a ⊕\<^bsub>V\<^esub> linear_combination h (A-{a})"
-- "We want to apply the theorem @{text linear_combination_insert},
so we have to write insert a (A - {a}) instead of directly @{term A}."
proof (rule linear_combination_insert)
show "good_set (A - {a})" using cb_Aa .
show "a ∈ carrier V" using a_in_V .
show "a ∉ A - {a}" using a_in_A by simp
show "h ∈ coefficients_function (carrier V)" using cf_h .
qed
also have "... = h a · linear_combination g (A-{a}) ⊕\<^bsub>V\<^esub> linear_combination h (A-{a})"
using a_lc_g_Aa by auto
also have "... = linear_combination (%x. h(a) ⊗ g x) (A-{a}) ⊕\<^bsub>V\<^esub> linear_combination h (A-{a})"
using fx_in_K[OF a_in_V cf_h] and linear_combination_rdistrib [OF cb_Aa cf_g _] by auto
also have "... = (\<Oplus>\<^bsub>V\<^esub>y∈A - {a}. (h a ⊗ g y)·y ⊕\<^bsub>V\<^esub> (h y) · y)"
proof (unfold linear_combination_def, rule finsum_addf[symmetric])
show "finite (A - {a})" using cb_Aa unfolding good_set_def by auto
show "(λy. (h a ⊗ g y) · y) ∈ A - {a} -> carrier V"
proof (unfold Pi_def, auto)
fix x
assume x_in_A: "x∈A"
hence x_in_V: "x∈carrier V"
using good_set_A unfolding good_set_def by auto
hence "(h a ⊗ g x)∈ carrier K"
using cf_g cf_h a_in_V unfolding coefficients_function_def
using K.m_closed by auto
thus "(h a ⊗ g x) · x ∈ carrier V"
using mult_closed[OF x_in_V _] by auto
qed
show "(λy. h y · y) ∈ A - {a} -> carrier V"
unfolding Pi_def using A_in_V using fx_x_in_V[OF _ cf_h] by auto
qed
also have "...=linear_combination (%x. (h(a) ⊗ g x) ⊕\<^bsub>K\<^esub> (h x)) (A-{a})"
proof (unfold linear_combination_def, rule finsum_cong')
show "A - {a} = A - {a}" ..
show "(λy. (h a ⊗ g y ⊕ h y) · y) ∈ A - {a} -> carrier V"
proof (unfold Pi_def, auto)
fix x
assume x_in_A: "x∈A"
hence x_in_V: "x∈carrier V"
using good_set_A unfolding good_set_def by auto
hence "(h a ⊗ g x)∈ carrier K"
using cf_g cf_h a_in_V
unfolding coefficients_function_def using K.m_closed by auto
hence "(h a ⊗ g x) ⊕ h x ∈ carrier K"
using K.a_closed[OF _ fx_in_K[OF x_in_V cf_h]] by auto
thus "(h a ⊗ g x ⊕ h x) · x ∈ carrier V" using mult_closed[OF x_in_V _] by simp
qed
show "!!i. i ∈ A - {a} ==> (h a ⊗ g i) · i ⊕\<^bsub>V\<^esub> h i · i = (h a ⊗ g i ⊕ h i) · i"
proof (rule add_mult_distrib2[symmetric])
fix x
assume x_in_A: "x∈A-{a}"
thus x_in_V: "x∈carrier V" using cb_Aa unfolding good_set_def by auto
thus "(h a ⊗ g x)∈ carrier K"
using cf_g cf_h a_in_V unfolding coefficients_function_def using K.m_closed by auto
show "h x ∈ carrier K" using fx_in_K[OF x_in_V cf_h] .
qed
qed
finally show ?thesis unfolding linear_combination_def using igualdad_conjuntos by auto
qed
qed
text{*Now we present the theorem. The proof is done by double content of both span sets and
we make use of the two previous lemmas.*}
theorem
span_minus:
assumes good_set_A: "good_set A"
and a_in_A: "a ∈ A"
and exists_g: "∃g. g∈ coefficients_function (carrier V)
∧ a = linear_combination g (A - {a})"
shows "span A = span (A - {a})"
proof
show "span (A - {a}) ⊆ span A"
unfolding span_def
unfolding linear_combination_def
using assms and exists_function_Aa_A by auto
next
from exists_g obtain g
where cf_g: "g ∈ coefficients_function (carrier V)"
and a_lc: "a = linear_combination g (A-{a})" by auto
show "span A ⊆ span (A - {a})"
proof (unfold span_def, unfold linear_combination_def,auto)
fix f
assume cf_f: "f∈ coefficients_function (carrier V)"
show "∃ga ∈ coefficients_function (carrier V).
(\<Oplus>\<^bsub>V\<^esub>y∈A. f y · y) = (\<Oplus>\<^bsub>V\<^esub>y∈A - {a}. ga y · y)"
using exists_function_A_Aa
[OF cf_f cf_g a_lc good_set_A a_in_A] .
qed
qed
text{*A corollary of this theorem claims that for every linearly dependent set $A$, then @{term "∃a ∈ A. span A = span (A - {a})"}.*}
text{*We also need to use @{thm exists_x_linear_combination2[no_vars]}*}
corollary
span_minus2:
assumes ld_A: "linear_dependent A"
shows "∃a∈A. span A = span (A - {a})"
proof -
have "∃a∈A. ∃g. g ∈ coefficients_function (carrier V) ∧ a = linear_combination g (A - {a})"
using exists_x_linear_combination2[OF ld_A] .
thus ?thesis using span_minus l_dep_good_set[OF ld_A] by auto
qed
text{*If an element $y$ is not in the span of a set $A$, hence that element is not in that set. The proof is completed by \emph{reductio ad absurdum}.
If $a \in A$, then there is a linear combination of the elements of $A$, and thus $a \in$ $span(A)$, which is a contradiction with one of the premises.*}
lemma not_in_span_impl_not_in_set:
assumes y_notin_span: "y ∉ span A"
and cb_A: "good_set A"
and y_in_V: "y ∈ carrier V"
shows "y ∉ A"
proof (cases "y ∉ A")
case True thus ?thesis .
next
case False
show ?thesis
proof -
def g≡"(%x. if x=y then \<one> else \<zero>)"
have cf_g: "g ∈ coefficients_function (carrier V)"
unfolding g_def coefficients_function_def using y_in_V
by simp
have "linear_combination g A = y"
proof -
have igualdad_conjuntos: "A=(insert y (A-{y}))"
using False by fast
hence "linear_combination g A
=linear_combination g (insert y (A-{y}))"
using arg_cong2 by force
also have "...=g(y)·y ⊕\<^bsub>V\<^esub> linear_combination g (A-{y})"
proof (rule linear_combination_insert)
show "good_set (A - {y})" using cb_A
unfolding good_set_def by fast
show "y ∈ carrier V" using False cb_A
unfolding good_set_def by fast
show "y ∉ A - {y}" by simp
show "g ∈ coefficients_function (carrier V)" using cf_g .
qed
also have "...=g(y)·y ⊕\<^bsub>V\<^esub> \<zero>\<^bsub>V\<^esub> "
proof -
have "linear_combination g (A-{y})=\<zero>\<^bsub>V\<^esub>"
proof -
have "(\<Oplus>\<^bsub>V\<^esub>y∈A - {y}. g y · y)=(\<Oplus>\<^bsub>V\<^esub>y∈A - {y}. \<zero>\<^bsub>V\<^esub>)"
apply (rule finsum_cong') apply auto
unfolding g_def apply simp
apply (rule zeroK_mult_V_is_zeroV)
using cb_A unfolding good_set_def by blast
also have "...= \<zero>\<^bsub>V\<^esub>"
using finsum_zero cb_A
unfolding good_set_def by blast
finally show ?thesis unfolding linear_combination_def .
qed
thus ?thesis by simp
qed
also have "...=g(y)·y"
using r_zero and mult_closed and False cb_A
unfolding good_set_def g_def by auto
also have "...=y"
using mult_1 False cb_A
unfolding good_set_def g_def by auto
finally show ?thesis .
qed
thus ?thesis
using cf_g y_notin_span unfolding span_def by fast
qed
qed
text{*If we have an element which is not in the span of an independent set, then the result of inserting this element into
that set is a linearly independent set. The proof is done dividing the goal into cases.
The case where $A\neq \{\}$ again is divided in cases with respect to the
boolean @{term "linear_independent (insert y A)"}. In the case where @{term "linear_independent (insert y A)"}
is false, again we proceed by \emph{reductio
ad absurdum}. It is a long lemma of 129 lines. *}
lemma insert_y_notin_span_li:
assumes y_notin_span: "y ∉ span A"
and y_in_V: "y ∈ carrier V"
and li_A: "linear_independent A"
shows "linear_independent (insert y A)"
proof (cases "A={}")
case True thus ?thesis --"If A is empty it is trivial."
using insertI1 span_empty
unipuntual_is_li y_in_V y_notin_span by auto
next
case False note A_not_empty=False
show ?thesis
proof (cases "linear_independent (insert y A)")
case True thus ?thesis .
next
case False show ?thesis
proof -
have y_not_zero: "y≠\<zero>\<^bsub>V\<^esub>"
using y_notin_span good_set_finite good_set_in_carrier
l_ind_good_set li_A span_contains_zero
by auto
have cb_A: "good_set A" using l_ind_good_set li_A by fast
have finite_A: "finite A" using good_set_finite l_ind_good_set li_A by fast
have ld_Ay: "linear_dependent (A ∪ {y})" using not_independent_implies_dependent False cb_A y_in_V
unfolding good_set_def by auto
have zero_not_in: "\<zero>\<^bsub>V\<^esub> ∉ A ∪ {y}" using zero_not_in_linear_independent_set[OF li_A] y_not_zero by fast
have "∃h. indexing (A ∪ {y}, h) ∧ h ` {..<card A} = A ∧ h ` ({..<card A + card {y}} - {..<card A}) = {y}"
proof (rule indexing_union)
show "A ∩ {y} = {}" using not_in_span_impl_not_in_set[OF y_notin_span cb_A y_in_V] by simp
show "finite A" using finite_A .
show "A ≠ {}" using A_not_empty .
show "finite {y}" by simp
qed
from this obtain h where indexing: "indexing (A ∪ {y}, h)" and surj_h_A: "h ` {..<card A} = A"
and surj_h_y: "h ` ({..<card A + card {y}} - {..<card A}) = {y}" by fastsimp
let ?P = "(λk. ∃b∈A∪{y}. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧
k < card (A∪{y}) ∧ h k = b ∧ b = linear_combination g (h ` {i. i < k}))"
have exK: "(∃k. ?P k)"
using linear_dependent_set_sorted_contains_linear_combination [
OF ld_Ay zero_not_in indexing] by auto
have ex_LEAST: "?P (LEAST k. ?P k)"
using LeastI_ex [OF exK] .
let ?k = "(LEAST k. ?P k)"
have "∃b∈A∪{y}. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ ?k ∧
?k < card (A∪{y}) ∧ h ?k = b ∧ b = linear_combination g (h ` {i. i < ?k})"
using ex_LEAST by simp
then obtain b g
where one_le_k: "1 ≤ ?k" and k_l_card: "?k < card (A∪{y})" and h_k_eq_b: "h ?k = b"
and cf_g: "g ∈ coefficients_function (carrier V)" and
combinacion_anteriores: "b = linear_combination g (h ` {i. i < ?k})"
and b_in_Ay: "b ∈ (A ∪ {y})"
by blast
show ?thesis
proof (cases "b∈{y}")
case True note b_in_y=True
have k_eq_card: "?k=card A"
proof -
--"I will prove that k is less or equal to card A. If k<card A we will obtain a contradiction (because the element will be in A).
So k = card A"
have "card (A∪{y})= card A + 1"
using not_in_span_impl_not_in_set[OF y_notin_span cb_A y_in_V] finite_A card_insert_if by auto
hence k_le_cardA: "?k ≤ card A" using k_l_card by auto
thus ?thesis
proof (cases "?k<card A")
case True
have "h ?k ∈ A" using surj_h_A True by auto
thus ?thesis using not_in_span_impl_not_in_set[OF y_notin_span cb_A y_in_V] h_k_eq_b b_in_y by auto
next
case False thus ?thesis using k_le_cardA by auto
qed
qed
have "linear_combination g A = y"
proof -
have "h ` {i. i < ?k}=A" using surj_h_A k_eq_card by auto
hence "linear_combination g A = linear_combination g (h ` {i. i < ?k})"
using arg_cong2[of g g A "h`{..<card A}"] by presburger
also have "...=b" using combinacion_anteriores by simp
also have "...=y" using True by simp
finally show ?thesis .
qed
thus ?thesis using cf_g y_notin_span unfolding span_def by auto
next
case False
show ?thesis
proof -
have b_in_A: "b∈A" using False b_in_Ay by simp
have k_le_cardA: "?k<card(A)"
using b_in_A and h_k_eq_b and surj_h_A and k_l_card and indexing
unfolding indexing_def and bij_betw_def and inj_on_def
by force
have ld_insert: "linear_dependent (insert b (h`{i. i<?k}))"
proof (rule lc1)
show "linear_independent (h`{i. i<?k})"
proof (rule independent_set_implies_independent_subset)
show "linear_independent A" using li_A .
show "h ` {i. i < ?k} ⊆ A" using surj_h_A k_le_cardA by auto
qed
show "b ∈ carrier V" using b_in_A cb_A unfolding good_set_def
by auto
show "b ∉ h`{i. i<?k}"
using b_in_A and h_k_eq_b and surj_h_A and k_l_card and indexing
unfolding indexing_def and bij_betw_def and inj_on_def
by force
show "∃f. f ∈ coefficients_function (carrier V) ∧
linear_combination f (h `{i. i<?k})=b"
using cf_g and combinacion_anteriores by auto
qed
have "linear_dependent (h`{..<card(A)})"
proof (rule linear_dependent_subset_implies_linear_dependent_set)
show "insert b (h`{i. i<?k})⊆ h ` {..<card A}"
proof -
have igualdad_conjuntos: "{i. i<?k} ∪ {?k}={..?k}" using atMost_def[of "?k"] ivl_disj_un(2) by auto
have "insert b (h`{i. i<?k})=(h`{i. i<?k}) ∪ {b}" by simp
also have "...=h`{i. i<?k} ∪ h` {?k} " using h_k_eq_b by auto
also have "...=h` ({i. i<?k} ∪ {?k})" by auto
also have "...=h`{..?k}" using igualdad_conjuntos by auto
also have "... ⊆ h ` {..<card A}" using k_le_cardA by auto
finally show ?thesis .
qed
show "good_set (h ` {..<card A})"
using surj_h_A cb_A by auto
show "linear_dependent (insert b (h`{i. i<?k}))" using ld_insert .
qed
--"Contradiction: we have linear dependent A and linear independent A"
thus ?thesis using surj_h_A li_A cb_A independent_implies_not_dependent by auto
qed
qed
qed
qed
qed
text{*We can unify the concepts of @{term "spanning_set"}, @{term "span"} and @{term "basis"} and illustrate the relationships
that exist among them.*}
text{*The @{term "span"} of a @{term "spanning_set"} is @{term "carrier V"}.*}
lemma span_basis_implies_spanning_set:
assumes span_A_V: "span A = carrier V"
and good_set_A: "good_set A"
shows "spanning_set A"
unfolding spanning_set_def
using span_A_V good_set_A
unfolding span_def good_set_def by force
text{*The opposite implication:*}
lemma spanning_set_implies_span_basis:
assumes sg_A: "spanning_set A"
shows "span A = carrier V"
using sg_A and linear_combination_closed
unfolding spanning_set_def and span_def
by fast
text{*Now we present the relationship between @{term "spanning_set"} and @{term "span"}: if \mbox{$span\mbox{ }A=carrier\mbox{ }V$} then $A$
is a \emph{spanning set}.*}
lemma span_V_eq_spanning_set:
assumes cb_A: "good_set A"
shows "span A = carrier V <-> spanning_set A"
using span_basis_implies_spanning_set
and spanning_set_implies_span_basis
and cb_A by auto
text{*Now we can introduce in Isabelle a new definition of basis (in the case of finite dimensional vector spaces).
A finite basis will be a set @{text A} which
is @{text "linear_independent"} and satisfies @{term "span A = carrier V"}. We use the previous lemma to check
that it is equivalent to @{thm basis_def[no_vars]}.*}
lemma basis_def':
assumes cb_A: "good_set A"
shows "basis A <-> (linear_independent A ∧ span A = carrier V)"
using assms basis_def fin_ind_ext_impl_ind good_set_def
good_set_in_carrier gs_spanning_ext_imp_spanning
independent_imp_independent_ext
span_V_eq_spanning_set spanning_imp_spanning_ext
spanning_set_implies_span_basis by auto
text{*If we have a finite basis, we can forget extended versions of linear independence and spanning set: *}
lemma finite_basis:
assumes fin_A: "finite A"
shows "basis A <-> (linear_independent A ∧ spanning_set A)"
using assms basis_def basis_def' fin_ind_ext_impl_ind
l_ind_good_set span_V_eq_spanning_set spanning_set_implies_span_basis
by metis
end
subsection{*Finite Dimensional Vector Space*}
text{*For working in a finite vector space we need to fix a finite basis.*}
text{*The definition of finite dimensional vector spaces in Isabelle/HOL is direct. It consists of a vector space in which we
assume that there exists a finite basis. Note that we have not proved yet that every vector space contains a basis.*}
locale finite_dimensional_vector_space = vector_space +
fixes X :: "'c set"
assumes finite_X: "finite X" (*This assumption adds the finitude of the basis*)
and basis_X: "basis X"
context finite_dimensional_vector_space
begin
text{*From this point the fixed basis is denoted by X.*}
text{*We add to simplifier both premisses. *}
lemmas [simp] = finite_X basis_X
text{*It is easy to show that the basis is a good set, is linearly independent and a spanning set.*}
lemma good_set_X:
shows "good_set X"
using basis_X
unfolding basis_def
using finite_X
unfolding good_set_def by simp
lemma linear_independent_X:
shows "linear_independent X"
using basis_X
unfolding basis_def
unfolding linear_independent_ext_def
using finite_X by simp
lemma spanning_set_X:
shows "spanning_set X"
using basis_X good_set_X
unfolding basis_def
using gs_spanning_ext_imp_spanning by fast
text{*We add to simplifier these three lemmas.*}
lemmas [simp] = good_set_X linear_independent_X spanning_set_X
text{*For all @{term "x ∈ carrier V"} exists a linear combination of elements of the basis
(we can write @{term "x ∈ carrier V"} in combination of the elements of a basis).*}
lemma exists_combination:
assumes x_in_V: "x ∈ carrier V"
shows "∃f. (f ∈ coefficients_function (carrier V) ∧ x = linear_combination f X)"
using x_in_V spanning_set_X
unfolding spanning_set_def
by fast
text{*Next lemma shows us that coordinates of a vector are unique
for each basis*}
lemma unique_coordenates:
assumes x_in_V: "x ∈ carrier V"
and cf_f: "f ∈ coefficients_function (carrier V)"
and lc_f: "x = linear_combination f X"
and cf_g: "g ∈ coefficients_function (carrier V)"
and lc_g: "x = linear_combination g X"
shows "∀x ∈ X. g x = f x"
proof -
have "linear_combination f X ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> linear_combination g X
= x ⊕\<^bsub>V\<^esub> \<ominus>\<^bsub>V\<^esub> x"
using lc_f and lc_g by auto
hence "\<zero>\<^bsub>V\<^esub> = linear_combination f X
⊕\<^bsub>V\<^esub> ((\<ominus>\<^bsub>K\<^esub> \<one>\<^bsub>K \<^esub>)· linear_combination g X)"
using V.r_neg [OF x_in_V]
negate_eq[OF linear_combination_closed[OF good_set_X cf_g]]
by auto
also have "…=linear_combination f X
⊕\<^bsub>V\<^esub> linear_combination (%i. (\<ominus>\<^bsub>K\<^esub> \<one>\<^bsub>K \<^esub>)⊗ g(i)) X"
using linear_combination_rdistrib[OF
good_set_X cf_g K.a_inv_closed[OF K.one_closed]] by auto
also have "…=linear_combination (%x. f(x) ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K\<^esub>g(x)) X"
unfolding linear_combination_def
proof -
have "(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. (\<ominus> \<one> ⊗ g y) · y) =
(\<Oplus>\<^bsub>V\<^esub>y∈X. (f y ·y)⊕\<^bsub>V\<^esub> (\<ominus> \<one> ⊗ g y) · y)"
proof (rule finsum_addf[symmetric])
show "finite X" using finite_X .
show "(λy. f y · y) ∈ X -> carrier V"
using mult_closed and cf_f and good_set_X
unfolding good_set_def and coefficients_function_def and Pi_def by auto
show "(λy. (\<ominus> \<one> ⊗ g y) · y) ∈ X -> carrier V"
proof (unfold Pi_def, auto, rule mult_closed)
fix y
assume y_in_X: "y∈X"
hence "y∈carrier V" using good_set_X unfolding good_set_def by auto
thus "y ∈ carrier V" .
thus "\<ominus> \<one> ⊗ g y ∈ carrier K"
using cf_g and y_in_X unfolding coefficients_function_def
using K.m_closed[OF K.a_inv_closed[OF K.one_closed] _] by auto
qed
qed
also have "…=linear_combination (%x. f(x) ⊕\<^bsub>K\<^esub>((\<ominus>\<^bsub>K\<^esub> \<one>\<^bsub>K \<^esub>)⊗ g(x))) X"
proof (unfold linear_combination_def, rule finsum_cong')
show "X=X" ..
show "(λy. (f y ⊕ \<ominus> \<one> ⊗ g y) · y) ∈ X -> carrier V"
proof (unfold Pi_def, auto, rule mult_closed)
fix y
assume y_in_X: "y∈X"
thus y_in_V: "y ∈ carrier V" using good_set_X unfolding good_set_def by auto
show "f y ⊕ \<ominus> \<one> ⊗ g y ∈ carrier K"
using fx_in_K[OF y_in_V cf_f]
using fx_in_K[OF y_in_V cf_g]
using K.m_closed[OF K.a_inv_closed[OF K.one_closed] _] and K.a_closed by blast
qed
show "!!i. i ∈ X ==> f i · i ⊕\<^bsub>V\<^esub> (\<ominus> \<one> ⊗ g i) · i = (f i ⊕ \<ominus> \<one> ⊗ g i) · i"
proof -
fix y
assume y_in_X: "y ∈ X"
hence y_in_V: "y ∈ carrier V" using good_set_X unfolding good_set_def
by auto
thus "f y · y ⊕\<^bsub>V\<^esub> (\<ominus> \<one> ⊗ g y) · y = (f y ⊕ \<ominus> \<one> ⊗ g y) · y"
proof (rule add_mult_distrib2[symmetric])
show "f y ∈ carrier K" using cf_f and y_in_V
unfolding coefficients_function_def by auto
show "\<ominus> \<one> ⊗ g y ∈ carrier K"
using cf_g and y_in_V unfolding coefficients_function_def
using K.m_closed[OF K.a_inv_closed[OF K.one_closed] _] by auto
qed
qed
qed
also have "…=linear_combination (%x. f(x) ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K\<^esub>g(x)) X"
proof (unfold linear_combination_def, rule finsum_cong',auto)
fix y
assume y_in_X: "y∈X"
hence y_in_V: "y∈carrier V" using good_set_X unfolding good_set_def by auto
show "(f y ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K \<^esub>g y) · y ∈ carrier V"
proof (rule mult_closed)
show "y ∈ carrier V" using y_in_V .
show "f y ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K\<^esub> g y ∈ carrier K"
using fx_in_K [OF y_in_V cf_f]
using fx_in_K [OF y_in_V cf_g]
unfolding coefficients_function_def using K.a_inv_closed using K.a_closed by auto
qed
have fy_in_K: "f(y)∈ carrier K"
using cf_f and y_in_V unfolding coefficients_function_def by auto
have gy_in_K: "g(y)∈ carrier K"
using cf_g and y_in_V unfolding coefficients_function_def by auto
show "(f y ⊕ \<ominus> \<one> ⊗ g y) · y = (f y ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K\<^esub> g y) · y"
proof -
have "(f y ⊕ \<ominus> \<one> ⊗ g y) = (f y ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K\<^esub> g y)" using K.l_minus_one[OF gy_in_K] by auto
thus ?thesis by auto
qed
qed
finally show "(\<Oplus>\<^bsub>V\<^esub>y∈X. f y · y) ⊕\<^bsub>V\<^esub> (\<Oplus>\<^bsub>V\<^esub>y∈X. (\<ominus> \<one> ⊗ g y) · y) = (\<Oplus>\<^bsub>V\<^esub>y∈X. (f y ⊕ \<ominus> g y) · y)"
unfolding linear_combination_def by auto
qed
finally have
lc_fg: "\<zero>\<^bsub>V\<^esub>=linear_combination (%x. f(x) ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K\<^esub>g(x)) X"
by simp
have cf_fg: " (%x. (f(x) ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K \<^esub>g(x)))
∈ coefficients_function (carrier V)"
proof (unfold coefficients_function_def, auto)
fix x
assume x_in_V: "x ∈ carrier V"
show "f x ⊕ \<ominus> g x ∈ carrier K"
using fx_in_K[OF x_in_V cf_f] fx_in_K[OF x_in_V cf_g] by fast
next
fix x
assume x_notin_V: "x ∉ carrier V"
show "f x ⊕ \<ominus> g x = \<zero>" using cf_f cf_g unfolding coefficients_function_def using x_notin_V by simp
qed
hence fg_0:"∀x∈X. f(x) ⊕\<^bsub>K\<^esub> \<ominus>\<^bsub>K \<^esub>g(x)=\<zero>\<^bsub>K\<^esub>"
using linear_independent_X and lc_fg[symmetric]
unfolding linear_independent_def by auto
show "∀x ∈ X. g(x)=f(x)"
proof
fix y
assume y_in_X: "y∈X"
hence y_in_V: "y∈carrier V"
using good_set_X unfolding good_set_def
by auto
have fg_y0: "f y ⊕ \<ominus> g y = \<zero>"
using y_in_X and fg_0 by auto
have fy_in_K: "f(y)∈ carrier K"
using cf_f and y_in_V
unfolding coefficients_function_def by auto
have gy_in_K: "g(y)∈ carrier K"
using cf_g and y_in_V
unfolding coefficients_function_def by auto
hence "\<ominus>\<^bsub>K\<^esub>(\<ominus>\<^bsub>K\<^esub> g y)=f y"
using K.minus_equality
[OF fg_y0 K.a_inv_closed[OF gy_in_K] fy_in_K]
by auto
thus "g(y)=f(y)" using K.minus_minus[OF gy_in_K] by auto
qed
qed
text{*We have fixed a finite basis and now we can prove some theorems about the @{term span}. Note that the
concept of finitude of the basis is very important in the proofs.*}
text{*The span of a basis is the total, so it's easy to prove that @{term "carrier V ⊆ span X"}. The other
implication is also easy: we have only to unfold the definition and use @{thm linear_combination_closed}.*}
lemma span_basis_is_V: "span X = carrier V"
proof
show "span X ⊆ carrier V"
unfolding span_def
using linear_combination_closed by auto
show "carrier V ⊆ span X"
unfolding span_def
using spanning_set_X unfolding spanning_set_def by auto
qed
text{*The span of every set joined with a basis is the total. Before proving this theorem, we make two auxiliar lemmas.*}
text{*First one: *}
lemma exists_linear_combination_union_basis:
assumes fin_A: "finite A"
and A_in_V: "A ⊆ carrier V"
and x_in_V: "x ∈ carrier V"
shows "∃g. g ∈ coefficients_function (carrier V) ∧ x = linear_combination g (A ∪ X)"
proof -(*(rule exI[of _ "(%x. if x ∈ X then f(x) else \<zero>\<^bsub>K\<^esub>)"])*)
from spanning_set_X obtain f where cf_f: "f ∈ coefficients_function (carrier V)"
and x_lc_fX: "x=linear_combination f X"
unfolding spanning_set_def using x_in_V by auto
let ?g="(%x. if x ∈ X then f(x) else \<zero>\<^bsub>K\<^esub>)"
have cf_g: "?g∈coefficients_function (carrier V)"
using coefficients_function_g_f_null[OF cf_f] .
have good_set_A: "good_set A"
using fin_A A_in_V unfolding good_set_def by auto
have "linear_combination ?g (A ∪ X)=linear_combination ?g (X ∪ A)"
-- "It is easier apply @{thm arg_cong2} than
@{thm finsum_cong'}, the unique different is in the arguments of the function. "
by (rule arg_cong2 [of ?g ?g _ _ "linear_combination"], auto)
also have "...=linear_combination f X"
using eq_lc_when_out_of_set_is_zero[OF good_set_A good_set_X cf_f] .
also have "... = x" using x_lc_fX [symmetric] .
finally have x_lc_g_AX: "x = linear_combination ?g (A∪X)" by (rule sym)
hence "?g ∈ coefficients_function (carrier V) ∧ x = linear_combination ?g (A ∪ X)"
using cf_g by auto
thus ?thesis by (rule exI[of _ "?g"])
qed
text{*Second one*}
lemma span_union_basis_eq:
assumes fin_A: "finite A"
and A_in_V: "A ⊆ carrier V"
shows "span (A ∪ X) = span X"
using span_basis_is_V
proof (unfold span_def,auto)
fix x
assume x_in_V: "x∈carrier V"
show "∃g∈coefficients_function (carrier V). x = linear_combination g (A ∪ X)"
using exists_linear_combination_union_basis[OF fin_A A_in_V x_in_V] by auto
next
fix g
assume cf_g: "g∈ coefficients_function (carrier V)"
show "linear_combination g (A ∪ X) ∈ carrier V"
proof (rule linear_combination_closed)
show "good_set (A ∪ X)"
using good_set_X and fin_A and A_in_V
unfolding good_set_def by auto
show "g ∈ coefficients_function (carrier V)" using cf_g .
qed
qed
text{*Finally the theorem: the span of every set joined with a basis is the total*}
corollary span_union_basis_is_V:
assumes fin_A: "finite A"
and A_in_V: "A ⊆ carrier V"
shows "span (A ∪ X) = carrier V"
using assms span_union_basis_eq and span_basis_is_V
by auto
subsection{*Theorem 1.*}
text{*From this, we are going to center into the proof that every linearly independent set can be extended to a basis.*}
text{*The function @{text remove_ld} takes an element of type @{typ "'a iset"} and returns other element of that type
in which in the set has been removed the first element that is a combination of the preceding ones, and the
indexation has removed the corresponding index.*}
text{*In the next definition, making use of previous theorem:*}
text{*@{thm linear_dependent_set_contains_linear_combination[no_vars]},
we remove the \emph{least} element that verifies the property that it can be expressed as a linear combination of the
preceding ones. The existence of this element is guaranteed by the fact that the set is linearly dependent.
If we iterate the function @{text remove_ld} we can be sure that it will terminate because sooner or later we will
achieve a linearly independent set.*}
text{*It is important to note that we have to provide a fixed indexation @{term "f::nat => 'c"} for the elements to be
removed are uniquely determined.*}
text{*The function @{text remove_ld} must be only applied to an indexation of a linearly dependent set that
does not contain @{term "\<zero>\<^bsub>V\<^esub>"}, since these are the uniques conditions where we have ensured the existence of the
element to be removed using:*}
text{* @{text linear_dependent_set_contains_linear_combination}:
@{thm linear_dependent_set_contains_linear_combination[no_vars]}.*}
definition remove_ld :: "'c iset => 'c iset"
where "remove_ld A =
(let n = (LEAST k::nat. ∃y∈(fst A). ∃g.
g ∈ coefficients_function (carrier V)
∧ (1::nat) ≤ k ∧ k < (card (fst A))
∧ (snd A) k = y
∧ y = linear_combination g ( (snd A) ` {i::nat. i<k}))
in remove_iset A n)"
text{*Next lemma expresses another notation for @{thm remove_ld_def}.*}
lemma remove_ld_def':
"remove_ld (A, f) = (let n = (LEAST k::nat. ∃y∈A. ∃g.
g ∈ coefficients_function (carrier V) ∧ (1::nat) ≤ k
∧ k < (card A) ∧ f k = y ∧ y = linear_combination g (f`{i::nat. i<k}))
in (A - {f n}, (λk. if k < n then f k else f (Suc k))))"
unfolding remove_ld_def
unfolding Let_def
unfolding remove_iset_def' by simp
text{*Now we can prove some properties of the function @{text remove_ld}:
it preserves the carrier, is monotone and decrease the cardinality.
*}
lemma remove_ld_preserves_carrier:
assumes b: "B ⊆ carrier V"
shows "fst (remove_ld (B, h)) ⊆ carrier V"
using b
unfolding remove_ld_def'
unfolding Let_def by auto
lemma remove_ld_monotone:
assumes b: "B ⊆ carrier V"
shows "fst (remove_ld (B, h)) ⊆ B"
using b
unfolding remove_ld_def'
unfolding Let_def by auto
lemma remove_ld_decr_card:
assumes ld_A: "linear_dependent A"
and not_zero: "\<zero>\<^bsub>V \<^esub>∉ A"
and indexing_A_f: "indexing (A, f)"
shows "card (fst (remove_ld (A, f))) = card A - 1"
proof -
let ?P = "(λk. ∃y∈A. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧
k < card A ∧ f k = y ∧ y = linear_combination g (f ` {i. i < k}))"
have fin_A: "finite A"
using l_dep_good_set [OF ld_A]
unfolding good_set_def by fast
have exK: "(∃k. ?P k)"
using linear_dependent_set_sorted_contains_linear_combination [
OF ld_A not_zero indexing_A_f] by auto
have ex_LEAST: "?P (LEAST k. ?P k)"
using LeastI_ex [OF exK] .
let ?k = "(LEAST k. ?P k)"
have "∃y∈A. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ ?k ∧
?k < card A ∧ f ?k = y ∧ y = linear_combination g (f ` {i. i < ?k})"
using ex_LEAST by simp
then obtain y
where one_le_k: "1 ≤ ?k" and k_l_card: "?k < card A" and f_k_eq_y: "f ?k = y"
by auto
then have rem_eq: "fst (remove_ld (A, f)) = (A - {y})" and y_in_A: "y ∈ A"
using indexing_equiv_img [OF indexing_A_f]
unfolding Pi_def unfolding remove_ld_def' by auto
show ?thesis
unfolding rem_eq
using card_Diff_singleton fin_A y_in_A by auto
qed
corollary remove_ld_decr_card2:
assumes ld_A: "linear_dependent A"
and not_zero: "\<zero>\<^bsub>V \<^esub>∉ A"
and indexing_A_f: "indexing (A, f)"
shows "card (fst (remove_ld (A, f))) < card A"
proof -
have card_A_g_zero: "card A > 0"
proof -
have not_empty: "A≠{}" using dependent_not_empty [OF ld_A] .
have finite_A: "finite A" using l_dep_good_set[OF ld_A] unfolding good_set_def by simp
show ?thesis using card_gt_0_iff[of "A"] and not_empty and finite_A by auto
qed
have "card (fst (remove_ld (A, f))) = card A - 1"
using remove_ld_decr_card[OF ld_A not_zero indexing_A_f] .
also have "...<card A" using card_A_g_zero by auto
finally show ?thesis .
qed
text{*This is an indispensable result: our function @{term remove_ld} preserves the propiety of @{term "span"}.
For this proof is very important the theorem @{text "span_minus:"} @{thm "span_minus"}.*}
lemma remove_ld_preserves_span:
assumes ld_A: "linear_dependent A"
and not_zero: "\<zero>\<^bsub>V \<^esub>∉ A"
and indexing_A_f: "indexing (A, f)"
shows "span (fst (remove_ld (A, f))) = span A"
proof -
let ?P = "(λk. ∃y∈A. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧
k < card A ∧ f k = y ∧ y = linear_combination g (f ` {i. i < k}))"
have fin_A: "finite A"
using l_dep_good_set [OF ld_A]
unfolding good_set_def by fast
have exK: "(∃k. ?P k)"
using linear_dependent_set_sorted_contains_linear_combination [
OF ld_A not_zero indexing_A_f] by auto
have ex_LEAST: "?P (LEAST k. ?P k)"
using LeastI_ex [OF exK] .
let ?k = "(LEAST k. ?P k)"
def k == "?k" -- "I introduce a new constant named @{term k} to make some goals more legible. When we want to unfold it
we will have to use @{term k_def}."
have "∃y ∈ A. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ ?k ∧
?k < card A ∧ f ?k = y ∧ y = linear_combination g (f ` {i. i < ?k})"
using ex_LEAST by simp
then
obtain y g
where one_le_k: "1 ≤ k" and k_l_card: "k < card A" and f_k_eq_y: "f k = y"
and cf_g: "g ∈ coefficients_function (carrier V)"
and y_lc_gf: "y = linear_combination g (f ` {i. i < k})" and y_in_A: "y ∈ A"
unfolding k_def by auto
have rem_eq: "fst (remove_ld (A, f)) = (A - {y})" and y_in_A: "y ∈ A"
using indexing_equiv_img [OF indexing_A_f] and one_le_k and k_l_card and f_k_eq_y
unfolding Pi_def unfolding k_def remove_ld_def' by auto
-- "I have to prove that this @{term y} is a linear combination of @{term \"A-{y}\"}."
have contenido: "f ` {i. i < k} ⊆ A - {y}"
proof -
have bb: "bij_betw f {i. i ≤ k} (f ` {i. i ≤ k})"
proof (rule bij_betw_subset [of f "{..<card A}" A "{i. i ≤ k}"])
show "bij_betw f {..<card A} A"
using indexing_A_f unfolding indexing_def by simp
show "{i. i ≤ k} ⊆ {..<card A}"
using k_l_card unfolding k_def by auto
qed
have "f ` ({i. i < k}) = f ` ({i. i ≤ k} - {k})" by auto
also have "f ` ({i. i ≤ k} - {k}) = f ` {i. i ≤ k} - {f k}"
by (rule bij_betw_image_minus, rule bb, simp)
finally have "f ` ({i. i < k}) = f ` {i. i ≤ k} - {f k}" by fast
thus ?thesis
using indexing_equiv_img [OF indexing_A_f]
unfolding f_k_eq_y
using k_l_card by auto
qed
hence union: "(f`{i. i < k} ∪ (A - {y})) = A - {y}" by auto
have good_set_A: "good_set A"
using l_dep_good_set[OF ld_A] .
hence good_set_Ay: "good_set (A - {y})"
using y_in_A unfolding good_set_def by auto
hence good_set_f: "good_set (f`{i. i < k})"
using contenido unfolding good_set_def by auto
let ?h="(%y. if y ∈ f ` {i. i < k} then g y else \<zero>\<^bsub>K\<^esub>)"
have cf_h: "?h ∈ coefficients_function (carrier V)"
using coefficients_function_g_f_null[OF cf_g] .
have "linear_combination g (f ` {i. i < k}) =
linear_combination ?h (f`{i. i < k} ∪ (A - {y}))"
using eq_lc_when_out_of_set_is_zero[OF good_set_Ay good_set_f cf_g, symmetric] by fast
also have "...=linear_combination ?h (A - {y})"
using arg_cong2 [of ?h ?h "(f`{i. i < ?k} ∪ (A - {y}))" "(A - {y})" "linear_combination"]
using union by presburger
finally have "y = linear_combination ?h (A - {y})" using y_lc_gf by fastsimp
hence exists_h: "∃h. h ∈ coefficients_function (carrier V) ∧ y = linear_combination h (A - {y})"
using cf_h by fast
have "span A = span (A - {y})"
using span_minus[OF good_set_A y_in_A exists_h] .
also have "... = span (fst (remove_ld (A, f)))" using rem_eq by simp
finally show ?thesis by blast
qed
text{*The next function @{text "iterate_remove_ld"} has done that we have to install @{text Isabelle2011}.
In previous versions we have to make use of @{text "function (tailrec)"}, but this element had some bugs.
In particular, we could not use @{text "function (tailrec)"} in the next definition. *}
partial_function (tailrec) iterate_remove_ld :: "'c set => (nat => 'c) => 'c set"
where "iterate_remove_ld A f = (if linear_independent A then A
else iterate_remove_ld (fst (remove_ld (A, f)))
(snd (remove_ld (A, f))))"
declare iterate_remove_ld.simps [simp del]
text{*Its behaviour is the next: from a set and a indexation of it, we apply recursively the operation @{term "remove_ld"}
up to we achieve a linearly independent set. The reiterated elimination of the linearly dependent elements would
have to keep the span.*}
text{*If we call to the function @{term iterate_remove_ld} with a linearly independent set, it will return us that set.*}
lemma iterate_remove_ld_empty [simp]: "iterate_remove_ld {} f = {}"
unfolding iterate_remove_ld.simps [of "{}"] by simp
lemma
iterate_remove_ld_li [simp]:
assumes li_A: "linear_independent A"
shows "iterate_remove_ld A f = A"
using iterate_remove_ld.simps using li_A by simp
text{*Now we are going to prove some lemmas about indexings and @{term remove_iset}. Note that we
can not put this lemmas in the file @{text "Indexed_Set.thy"} because the axioms @{term good_set} and @{term linear_dependent}
are sometimes in the premises.*}
text{*The next lemma express that the result of aplying @{term remove_iset} preserves the good set property.
In our context we need to prove it for @{term remove_ld}...but it does not cease to be a particular case of
@{term remove_iset}.*}
lemma
remove_iset_good_set:
assumes c: "good_set A"
and i: "indexing (A, h)"
shows "good_set (fst (remove_iset (A, h) n))"
using c
unfolding good_set_def
unfolding remove_iset_def by auto
lemma
remove_ld_good_set:
assumes c: "good_set A"
and i: "indexing (A, h)"
shows "good_set (fst (remove_ld (A, h)))"
unfolding remove_ld_def
unfolding Let_def
by (rule remove_iset_good_set) fact+
text{*Next theorem applies @{thm indexing_remove_iset} to the function @{term remove_ld}. We can omit the good set
condition: it is implicit in the fact that the set is linearly dependent. *}
theorem indexing_remove_ld:
assumes l: "linear_dependent A"
and i: "indexing (A, f)"
and n: "\<zero>\<^bsub>V\<^esub> ∉ A"
shows "indexing (remove_ld (A, f))"
unfolding remove_ld_def
unfolding Let_def
proof (rule indexing_remove_iset, unfold fst_conv snd_conv)
show "indexing (A, f)" by fact
show "(LEAST k. ∃y∈A. ∃g. g ∈ coefficients_function (carrier V) ∧
1 ≤ k ∧
k < card A ∧
f k = y ∧
y = linear_combination g (f ` {i. i < k})) < card A"
proof -
let ?P = "(λk. ∃y∈A. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧
k < card A ∧ f k = y ∧ y = linear_combination g (f ` {i. i < k}))"
have fin_A: "finite A"
using l_dep_good_set [OF l]
unfolding good_set_def by fast
have exK: "(∃k. ?P k)"
using linear_dependent_set_sorted_contains_linear_combination [
OF l n i] by auto
have ex_LEAST: "?P (LEAST k. ?P k)"
using LeastI_ex [OF exK] .
let ?k = "(LEAST k. ?P k)"
have "∃y∈A. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ ?k ∧
?k < card A ∧ f ?k = y ∧ y = linear_combination g (f ` {i. i < ?k})"
using ex_LEAST by simp
thus ?thesis by auto
qed
qed
text{*Next lemma shows us that first element of a indexed set is in the carrier. Note that we can not put this lemma
in the file @{text "Indexed Set"} due to the axiom @{term "A ⊆ carrier V"}
(we have not a structure of carrier in that file).*}
lemma f0_in_V:
assumes indexing_A: "indexing (A,f)"
and A_in_V: "A ⊆ carrier V"
and A_not_empty: "A≠{}" -- "Essential to cardinality"
shows "f 0 ∈ carrier V"
proof -
have "A≠{}" using A_not_empty .
hence "0∈ {..<card A}"
using card_gt_0_iff and indexing_finite[OF indexing_A]
using card_gt_0_iff lessThan_iff by blast
thus ?thesis
using indexing_A A_in_V unfolding indexing_def bij_betw_def by auto
qed
text{*If A is independent, then its firts element is not zero.*}
lemma f0_not_zero:
assumes indexing_A: "indexing (A,f)"
and li_A: "linear_independent A"
and A_not_empty: "A≠{}"
shows "f 0 ≠ \<zero>\<^bsub>V\<^esub>"
proof -
have zero_not_in_A: "\<zero>\<^bsub>V\<^esub> ∉ A" using zero_not_in_linear_independent_set[OF li_A] .
have "0∈ {..<card A}" using A_not_empty and indexing_finite[OF indexing_A]
using card_gt_0_iff lessThan_iff by blast
thus ?thesis using indexing_A and zero_not_in_A unfolding indexing_def bij_betw_def by force
qed
text{*We can also prove that apply the function @{text insert_iset} return us a good set.*}
lemma insert_iset_good_set:
assumes a_notin_A: "a ∉ A"
and indexing: "indexing (A,f)"
and a_in_V: "a ∈ carrier V"
and cb_A: "good_set A"
shows "good_set (fst(insert_iset (A,f) a n))"
unfolding insert_iset_def using a_in_V cb_A unfolding good_set_def by simp
text{*Remove an element and after that insert it is a good set*}
lemma good_set_insert_remove:
assumes B_in_V: "B ⊆ carrier V"
and A_in_V: "A ⊆ carrier V"
and A_not_empty: "A ≠ {}"
and indexing_A: "indexing (A,f)"
and indexing_B: "indexing (B,g)"
and a_in_B: "a ∈ B"
shows "good_set (fst (insert_iset (remove_iset (B, g) (obtain_position a (B, g))) a n))"
proof -
have cb_A: "good_set A" using A_in_V indexing_finite[OF indexing_A] unfolding good_set_def by simp
have cb_B: "good_set B" using B_in_V indexing_finite[OF indexing_B] unfolding good_set_def by simp
have "good_set (fst (insert_iset ((fst(remove_iset (B, g)
(obtain_position a (B, g))),snd(remove_iset (B, g) (obtain_position a (B, g))))) a n))"
proof (rule insert_iset_good_set)
show "a ∉ fst (remove_iset (B, g) (obtain_position a (B, g)))" using a_notin_remove_iset[OF a_in_B indexing_B] .
show " indexing
(fst (remove_iset (B, g) (obtain_position a (B, g))),
snd (remove_iset (B, g) (obtain_position a (B, g))))"
using indexing_remove_iset[OF indexing_B obtain_position_less_card[OF a_in_B indexing_B]] by simp
show "a ∈ carrier V" using a_in_B B_in_V by fast
show "good_set (fst (remove_iset (B, g) (obtain_position a (B, g))))"
using remove_iset_good_set[OF cb_B indexing_B] .
qed
thus ?thesis by simp
qed
text{*The result of applying the function @{term iterate_remove_ld} to any finite set in @{term "carrier V"} will
be always independent (the function finishes).*}
text{*We are going to make the proof firstly by dividing in cases (with respect to the condiction @{term "linear_independent A"})
and after that by total induction over
the cardinal of the set: @{thm measure_induct_rule[no_vars]}.*}
text{*With respect to the induction, it is important to note that we can not make induction over the \emph{structure}
of the set, with the following induction rule for indexed set that we have introduced in section \ref{s:indexed_sets}:*}
text{*@{text indexed_set_induct2}: @{thm indexed_set_induct2[no_vars]}*}
text{*If we make induction over the structure, we will have to prove the case
@{term "insert a (A::'c set)"} and the induction hypothesis will say that the result is true for @{term "A::'c set"}.
However, independently of in what position of the indexation we place the element @{term "a::'c"}, we can not
know if @{term "remove_ld ((insert a A), ((indexing_ext (A,f) a) n))"} will return the same set @{term "A::'c set"} or
it will return another set.
In other words: the result of inserting the element @{term "a::'c"} in any position of the @{term "A::'c set"} set
and after that removing the least element which is a linear combination of the preceding ones (@{term remove_ld} does it)
is not equal to the original set. We can not ensure it even when we insert the element @{term "a::'c"} in the least
position that it can be expressed as a linear combination of the preceding ones: we can not be sure that @{term remove_ld}
will remove that element.
For example, in the set @{term "{(1::nat,0::nat), (2,0), (0,1)}"}, if we insert the element @{term "(0::nat,2::nat)"} in the least position
where it is a linear combination of the preceding ones we achieve the set @{term "{(1::nat,0::nat), (2,0), (0,1), (0,2)}"}.
However, if we apply @{term remove_ld} to this set, it will return @{term "{(1::nat,0::nat), (0,1), (0,2)}"} and this is not
equal to the original set.
*}
lemma
linear_independent_iterate_remove_ld:
assumes A_in_V: "A ⊆ carrier V"
and not_zero: "\<zero>\<^bsub>V \<^esub>∉ A"
and indexing_A_f: "indexing (A, h)"
shows "linear_independent (iterate_remove_ld A h)"
proof (cases "linear_independent A")
case True
show ?thesis using True by simp
next
case False
have fin_A: "finite A" using indexing_finite[OF indexing_A_f] .
have ld_A: "linear_dependent A"
using not_independent_implies_dependent [OF _ False]
unfolding good_set_def using fin_A A_in_V by fast
show ?thesis
using fin_A ld_A A_in_V not_zero indexing_A_f
--"HERE WE APPLY THE INDUCTION RULE:"
proof (induct A arbitrary: h rule:
measure_induct_rule [where f = "card"])
case (less B h)
show "linear_independent (iterate_remove_ld B h)"
proof (cases "B = {}")
case True
thus ?thesis by simp
next
case False
have not_lin_indep: "¬ linear_independent B"
using dependent_implies_not_independent
[OF less.prems (2)] .
obtain Y where Y_def: "Y = fst (remove_ld (B, h))"
and card_less: "card Y < card B"
using False
using remove_ld_decr_card2
[OF less.prems (2) less.prems (4) less.prems (5)]
by fast
def h' == "snd (remove_ld (B, h))"
have i_Y_h': "indexing (Y, h')"
unfolding Y_def h'_def pair_collapse
by (rule indexing_remove_ld) fact+
show ?thesis
proof (cases "linear_independent (fst (remove_ld (B, h)))")
case True
show ?thesis
apply (subst iterate_remove_ld.simps)
apply (subst iterate_remove_ld.simps)
using not_lin_indep using True by simp
next
case False
show ?thesis
proof -
have "linear_independent (iterate_remove_ld Y h')"
proof (rule less.hyps)
show "card Y < card B"
using card_less .
show "finite Y"
using Y_def good_set_finite l_dep_good_set
less(3) less(6) remove_ld_good_set by presburger
show "linear_dependent Y"
unfolding Y_def
apply (rule not_independent_implies_dependent
[OF _ False])
apply (rule remove_ld_good_set)
apply (unfold good_set_def, intro conjI)
by (rule less.prems (1), rule less.prems (3),
rule less.prems (5))
show "Y ⊆ carrier V"
unfolding Y_def
using remove_ld_preserves_carrier
[OF less.prems (3), of h] .
show "\<zero>\<^bsub>V\<^esub> ∉ Y"
unfolding Y_def
using remove_ld_monotone [OF "less.prems" (3), of h]
using less.prems (4) by auto
show "indexing (Y, h')"
unfolding Y_def h'_def pair_collapse
by (rule indexing_remove_ld) fact+
qed
thus ?thesis
unfolding Y_def h'_def
by (subst iterate_remove_ld.simps,
simp add: not_lin_indep)
qed
qed
qed
qed
qed
text{*Similarly to the previous theorem, we can prove that the function @{term iterate_remove_ld} preserves the
@{term span}.*}
lemma iterate_remove_ld_preserves_span:
assumes A_in_V: "A ⊆ carrier V"
and indexing_A_f: "indexing (A,h)"
and not_zero: "\<zero>\<^bsub>V\<^esub> ∉ A"
shows "span (iterate_remove_ld A h) = span A"
proof (cases "linear_independent A")
case True
show ?thesis using True by simp
next
case False
have fin_A: "finite A" using indexing_finite[OF indexing_A_f] .
have ld_A: "linear_dependent A"
using not_independent_implies_dependent [OF _ False]
unfolding good_set_def using fin_A A_in_V by fast
show ?thesis
using fin_A ld_A A_in_V not_zero indexing_A_f
proof (induct A arbitrary: h rule: measure_induct_rule [where f = "card"])
case (less B h)
show "span (iterate_remove_ld B h) = span B"
proof (cases "B = {}")
case True
thus ?thesis by simp
next
case False
have not_lin_indep: "¬ linear_independent B"
using dependent_implies_not_independent [OF less.prems (2)] .
obtain Y where Y_def: "Y = fst (remove_ld (B, h))"
and card_less: "card Y < card B"
using False
using remove_ld_decr_card2 [OF less.prems (2) less.prems (4) less.prems (5)] by fast
def h' == "snd (remove_ld (B, h))"
have i_Y_h': "indexing (Y, h')"
unfolding Y_def h'_def pair_collapse
by (rule indexing_remove_ld) fact+
show ?thesis
proof (cases "linear_independent (fst (remove_ld (B, h)))")
case True
show ?thesis
apply (subst iterate_remove_ld.simps)
apply (subst iterate_remove_ld.simps)
using not_lin_indep using True
apply simp
proof (rule remove_ld_preserves_span)
show "linear_dependent B" using less(3) .
show "\<zero>\<^bsub>V\<^esub> ∉ B" using less(5) .
show "indexing (B, h)" using less(6) .
qed
next
case False
show ?thesis
proof -
have "span (iterate_remove_ld Y h') = span Y"
proof (rule less.hyps)
show "card Y < card B"
using card_less .
show "finite Y"
using Y_def less(2) less(4) remove_ld_monotone rev_finite_subset by metis
show "linear_dependent Y"
unfolding Y_def
proof (rule not_independent_implies_dependent)
show "good_set (fst (remove_ld (B, h)))"
using remove_ld_good_set less.prems(1) less.prems(3) less.prems(5)
unfolding good_set_def by auto
show "¬ linear_independent (fst (remove_ld (B, h)))" using False .
qed
show "Y ⊆ carrier V"
unfolding Y_def
using remove_ld_preserves_carrier [OF less.prems (3), of h] using A_in_V by auto
show "\<zero>\<^bsub>V\<^esub> ∉ Y"
unfolding Y_def
using remove_ld_monotone [OF "less.prems" (3), of h]
using less.prems (4) by auto
show "indexing (Y, h')"
unfolding Y_def h'_def pair_collapse
by (rule indexing_remove_ld) fact+
qed
thus ?thesis
unfolding Y_def h'_def
using iterate_remove_ld.simps less(3) less(5) less(6) not_lin_indep remove_ld_preserves_span by auto
qed
qed
qed
qed
qed
text{*If we have an @{term "indexing (A∪B,h)"} where elements of an independent set A are in its first positions and
after those the elements of a set B, then A will be in @{term "remove_ld (A∪B,h)"} (we will have removed
an element of B). The premisse of @{term "A∩B={}"} is indispensable in order to avoid the notion of multisets.
In the book, Halmos doesn't worry about this: he simply create a set with all elements of A in the first positions
and after that all elements of B...but what does it happen if a element of B are in A? we will have a multiset
because we have the same element in two positions.
However, this is not a limitation for our theorem if we make a trick like these: @{text "A∪B = A∪(B-A)"}.
Using that we avoid the problem.*}
lemma A_in_remove_ld:
assumes indexing: "indexing (A∪B,h)"
and ld_AB: "linear_dependent (A∪B)"
and surj_h_A:"h` {..<card(A)}= A"
(*and surj_h_B:"h` ({..<(card(A)+card(B))}-{..<card(A)})=B"--"It is not necessary."*)
and li_A: "linear_independent A"
and zero_not_in: "\<zero>\<^bsub>V\<^esub> ∉ (A∪B)"
and disjuntos: "A∩B={}"
shows "A ⊆ fst (remove_ld ((A∪B),h))"
proof -
have cb_A: "good_set A" and cb_B: "good_set B"
using l_dep_good_set[OF ld_AB] unfolding good_set_def by auto
let ?P = "(λk. ∃y∈A∪B. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧
k < card (A∪B) ∧ h k = y ∧ y = linear_combination g (h ` {i. i < k}))"
have exK: "(∃k. ?P k)"
using linear_dependent_set_sorted_contains_linear_combination [
OF ld_AB zero_not_in indexing] by auto
have ex_LEAST: "?P (LEAST k. ?P k)"
using LeastI_ex [OF exK] .
let ?k = "(LEAST k. ?P k)"
have "∃y∈A∪B. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ ?k ∧
?k < card (A∪B) ∧ h ?k = y ∧ y = linear_combination g (h ` {i. i < ?k})"
using ex_LEAST by simp
then obtain y s
where one_le_k: "1 ≤ ?k" and k_l_card: "?k < card (A∪B)" and h_k_eq_y: "h ?k = y"
and cf_s: "s∈ coefficients_function (carrier V)" and
combinacion_anteriores: "y = linear_combination s (h ` {i. i < ?k})"
by auto
have rem_eq: "fst (remove_ld (A∪B, h)) = ((A∪B) - {y})" and y_in_AB: "y ∈ A∪B"
using indexing_equiv_img [OF indexing] one_le_k k_l_card h_k_eq_y
unfolding Pi_def unfolding remove_ld_def' by auto
show ?thesis
proof (cases "y∈B")
case True thus ?thesis using rem_eq and disjuntos by auto
next
case False show ?thesis
proof -
have y_in_A: "y∈A" using False and y_in_AB by simp
have k_le_cardA: "?k<card(A)" --"It takes about a seconds"
using y_in_A and h_k_eq_y and surj_h_A and k_l_card and indexing
unfolding indexing_def and bij_betw_def and inj_on_def
by force
have ld_insert: "linear_dependent (insert y (h`{i. i<?k}))"
proof (rule lc1)
show "linear_independent (h`{i. i<?k})"
proof (rule independent_set_implies_independent_subset)
show "linear_independent A" using li_A .
show "h ` {i. i < ?k} ⊆ A" using surj_h_A k_le_cardA by auto
qed
show "y∈ carrier V" using y_in_A cb_A unfolding good_set_def
by auto
show "y∉ h`{i. i<?k}"
using y_in_A and h_k_eq_y and surj_h_A and k_l_card and indexing
unfolding indexing_def and bij_betw_def and inj_on_def
by force
show "∃f. f ∈ coefficients_function (carrier V) ∧
linear_combination f (h `{i. i<?k})=y"
using cf_s and combinacion_anteriores by auto
qed
have "linear_dependent (h`{..<card(A)})"
proof (rule linear_dependent_subset_implies_linear_dependent_set)
show "insert y (h`{i. i<?k})⊆ h ` {..<card A}"
proof -
have igualdad_conjuntos: "{i. i<?k} ∪ {?k}={..?k}" using atMost_def[of "?k"] ivl_disj_un(2) by auto
have "insert y (h`{i. i<?k})=(h`{i. i<?k}) ∪ {y}" by simp
also have "...=h`{i. i<?k} ∪ h` {?k} " using h_k_eq_y by auto
also have "...=h` ({i. i<?k} ∪ {?k})" by auto
also have "...=h`{..?k}" using igualdad_conjuntos by auto
also have "... ⊆ h ` {..<card A}" using k_le_cardA by auto
finally show ?thesis .
qed next
show "good_set (h ` {..<card A})"
using surj_h_A cb_A by auto
show "linear_dependent (insert y (h`{i. i<?k}))" using ld_insert .
qed
--"Contradiction: we have linear dependent A and linear independent A"
thus ?thesis using surj_h_A li_A cb_A independent_implies_not_dependent by auto
qed
qed
qed
text{*This lemma is an extended version of previous one. It shows that we are removing one element of the second set
and preserving the indexation.*}
lemma descomposicion_remove_ld:
assumes indexing: "indexing (A∪B,h)"
and B_not_empty: "B≠{}" --"Due to cardinality, it is indispensable."
and surj_h_A:"h` {..<card(A)}= A"
and surj_h_B:"h` ({..<(card(A)+card(B))}-{..<card(A)})=B"
and li_A: "linear_independent A"
and zero_not_in: "\<zero>\<^bsub>V\<^esub> ∉ (A∪B)"
and ld_AB: "linear_dependent (A∪B)"
and disjuntos: "A∩B={}"
shows "∃y. fst (remove_ld ((A∪B),h))=A∪(B-{y}) ∧ y∈B
∧ (snd (remove_ld (A∪B, h))) ` ({..<card A + card (B-{y})} - {..<card A}) = (B-{y})
∧ snd (remove_ld((A∪B), h)) ` {..<card A}=A ∧ indexing (A ∪ (B-{y}), snd (remove_ld (A∪B, h)))"
proof -
have cb_AB: "good_set (A∪B)" using l_dep_good_set[OF ld_AB] unfolding good_set_def by auto
have cb_A: "good_set A" and cb_B:"good_set B"
using l_dep_good_set[OF ld_AB] unfolding good_set_def by auto
let ?P = "(λk. ∃y∈A∪B. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ k ∧
k < card (A∪B) ∧ h k = y ∧ y = linear_combination g (h ` {i. i < k}))"
have exK: "(∃k. ?P k)"
using linear_dependent_set_sorted_contains_linear_combination [
OF ld_AB zero_not_in indexing] by auto
have ex_LEAST: "?P (LEAST k. ?P k)"
using LeastI_ex [OF exK] .
let ?k = "(LEAST k. ?P k)"
have "∃y∈A∪B. ∃g. g ∈ coefficients_function (carrier V) ∧ 1 ≤ ?k ∧
?k < card (A∪B) ∧ h ?k = y ∧ y = linear_combination g (h ` {i. i < ?k})"
using ex_LEAST by simp
then obtain y s
where one_le_k: "1 ≤ ?k" and k_l_card: "?k < card (A∪B)" and h_k_eq_y: "h ?k = y"
and cf_s: "s∈ coefficients_function (carrier V)" and
combinacion_anteriores: "y = linear_combination s (h ` {i. i < ?k})"
by auto
have rem_eq: "fst (remove_ld (A∪B, h)) = ((A∪B) - {y})" and y_in_AB: "y ∈ A∪B"
using indexing_equiv_img [OF indexing] one_le_k k_l_card h_k_eq_y
unfolding Pi_def unfolding remove_ld_def' by auto
show ?thesis
proof (cases "y∈B")
case True thus ?thesis
proof -
have y_notin_A: "y∉A" using True disjuntos y_in_AB by blast
have k_in_conjunto:"?k∈{..<card(A)+card(B)}-{..<card(A)}"
proof -
have "card(A∪B)=card(A)+card(B)" using disjuntos
card_Un_disjoint cb_A cb_B unfolding good_set_def by blast
hence k_in_cardAB: "?k∈{..<card(A)+card(B)}" using k_l_card by auto
have "?k∉{..<card(A)}" using h_k_eq_y True surj_h_A y_notin_A by auto
thus ?thesis using k_in_cardAB by simp
qed
have 1: "fst (remove_ld (A ∪ B, h)) = A ∪ (B-{y})"
using rem_eq and disjuntos True by auto
have 2: "(snd (remove_ld (A∪B, h))) ` ({..<card A + card (B-{y})} - {..<card A}) = (B-{y})
∧ snd (remove_ld((A∪B), h)) ` {..<card A}=A
∧ indexing (A ∪ (B-{y}), snd (remove_ld (A∪B, h)))"
proof -
have eq_card: "card(fst(remove_iset((A∪B),h) ?k))=card(A)+card(B-{y})"
proof -
have cardB_g_zero: "card B > 0" using B_not_empty cb_B unfolding good_set_def by auto
hence finite_B: "finite B" using cb_B unfolding good_set_def by simp
have 1: "card(B-{y})=card(B)-Suc 0" using card_Diff_singleton[OF finite_B True] by simp
have "card (fst (remove_ld ((A∪B), h))) = card (A∪B) - Suc 0"
using remove_ld_decr_card indexing_remove_ld indexing ld_AB zero_not_in by auto
also have "...=card(A)+card(B)-Suc 0" using disjuntos card_Un_disjoint cb_A cb_B
unfolding good_set_def by force
also have "...=card(A)+(card(B)-Suc 0)" using cardB_g_zero by auto
finally have "card (fst (remove_ld (A ∪ B, h))) = card A + (card B - Suc 0)" .
thus ?thesis using 1 unfolding remove_ld_def by auto
qed
have eq: "snd (remove_ld (A ∪ B, h)) = snd (remove_iset ((A∪B),h) ?k)"
unfolding remove_ld_def using snd_conv using remove_iset_def[of "(A∪B,h)" "?k"] by auto
have surj_rmiset_A: "snd (remove_iset((A∪B), h) ?k) ` {..<card A}=A"
proof -
have "?k≥card A"
proof (cases "?k<card A")
case False thus ?thesis by simp
next
case True thus ?thesis using surj_h_A h_k_eq_y y_notin_A by auto
qed
hence "snd (remove_iset((A∪B), h) ?k) ` {..<card A}=h`{..<card A}" unfolding remove_iset_def by auto
thus ?thesis using surj_h_A by simp
qed
have indexing2: "indexing (A ∪ (B-{y}), snd (remove_ld (A∪B, h)))"
proof -
have "indexing (A ∪ (B-{y}), snd (remove_ld (A∪B, h)))
=indexing (fst(remove_ld (A∪B,h)), snd (remove_ld (A∪B, h)))"
using eq 1 by auto
also have "...=indexing (remove_ld (A∪B,h))" by auto
finally show ?thesis using indexing_remove_ld[OF ld_AB indexing zero_not_in] by auto
qed
have "snd (remove_iset ((A∪B),h) ?k) `{..<card(fst(remove_iset((A∪B),h) ?k))}=fst(remove_iset ((A∪B),h) ?k)"
using indexing_remove_iset[OF indexing k_l_card]
unfolding indexing_def and bij_betw_def by auto
also have "...=(A∪B)-{h ?k}" unfolding remove_iset_def by auto
also have "...=A∪(B-{y})" using h_k_eq_y y_notin_A by auto
finally have eq_final: "snd (remove_iset ((A∪B),h) ?k) `{..<card(fst(remove_iset((A∪B),h) ?k))}=A∪(B-{y})" .
have "(snd (remove_ld (A∪B, h))) ` ({..<card A + card (B-{y})} - {..<card A})
= (snd (remove_ld (A∪B, h))) ` {..<card A + card (B-{y})}
- (snd (remove_ld (A∪B, h))) ` {..<card A}"
proof (rule inj_on_image_set_diff[of _ "{..<card A + card (B-{y})}"],auto)
show "inj_on (snd (remove_ld (A ∪ B, h))) {..<card A + card (B - {y})}"
using eq and eq_card
using indexing_remove_iset[OF indexing k_l_card]
unfolding indexing_def and bij_betw_def by auto
qed
also have "...=snd (remove_iset ((A∪B),h) ?k) ` {..<card A + card (B-{y})}
- snd (remove_iset ((A∪B),h) ?k) `{..<card(A)}"
using eq by auto
also have "...=(A∪(B-{y}))-A" using eq_final surj_rmiset_A eq eq_card by auto
also have "...=B-{y}" using disjuntos y_notin_A True by auto
finally show ?thesis using surj_rmiset_A eq indexing2 by auto
qed
show ?thesis using 1 2 True by auto
qed
next
case False show ?thesis
proof -
have y_in_A: "y∈A" using False and y_in_AB by simp
have k_le_cardA: "?k<card(A)" --"It takes about a seconds"
using y_in_A and h_k_eq_y and surj_h_A and k_l_card and indexing
unfolding indexing_def and bij_betw_def and inj_on_def
by force
have ld_insert: "linear_dependent (insert y (h`{i. i<?k}))"
proof (rule lc1)
show "linear_independent (h`{i. i<?k})"
proof (rule independent_set_implies_independent_subset)
show "linear_independent A" using li_A .
show "h ` {i. i < ?k} ⊆ A" using surj_h_A k_le_cardA by auto
qed
show "y∈ carrier V" using y_in_A cb_A unfolding good_set_def
by auto
show "y∉ h`{i. i<?k}"
using y_in_A and h_k_eq_y and surj_h_A and k_l_card and indexing
unfolding indexing_def and bij_betw_def and inj_on_def
by force
show "∃f. f ∈ coefficients_function (carrier V) ∧
linear_combination f (h `{i. i<?k})=y"
using cf_s and combinacion_anteriores by auto
qed
have "linear_dependent (h`{..<card(A)})"
proof (rule linear_dependent_subset_implies_linear_dependent_set)
show "insert y (h`{i. i<?k})⊆ h ` {..<card A}"
proof -
have igualdad_conjuntos: "{i. i<?k} ∪ {?k}={..?k}" using atMost_def[of "?k"] ivl_disj_un(2) by auto
have "insert y (h`{i. i<?k})=(h`{i. i<?k}) ∪ {y}" by simp
also have "...=h`{i. i<?k} ∪ h` {?k} " using h_k_eq_y by auto
also have "...=h` ({i. i<?k} ∪ {?k})" by auto
also have "...=h`{..?k}" using igualdad_conjuntos by auto
also have "... ⊆ h ` {..<card A}" using k_le_cardA by auto
finally show ?thesis .
qed
show "good_set (h ` {..<card A})"
using surj_h_A cb_A by auto
show "linear_dependent (insert y (h`{i. i<?k}))" using ld_insert .
qed
--"Contradiction: we have linear dependent A and linear independent A"
thus ?thesis using surj_h_A li_A cb_A independent_implies_not_dependent by auto
qed
qed
qed
text{*Finally an important lemma proved using @{thm measure_induct_rule} such as we do in
@{text linear_independent_iterate_remove_ld} and in @{text iterate_remove_ld_preserves_span}. We need above lemmas to
prove it. It shows us that @{text iterate_remove_ld} does not remove any element of A if elements of A are in first
positions and A is linearly independent.*}
lemma A_in_iterate_remove_ld:
assumes indexing: "indexing (A∪B,h)"
and B_in_V: "B ⊆ carrier V"
and surj_h_A:"h` {..<card(A)}= A"
and surj_h_B:"h` ({..<(card(A)+card(B))}-{..<card(A)})=B"
and li_A: "linear_independent A"
and zero_not_in: "\<zero>\<^bsub>V\<^esub> ∉ (A∪B)"
and disjuntos: "A∩B={}"
shows "A ⊆ (iterate_remove_ld (A∪B) h)"
proof (cases "linear_dependent (A∪B)")
have cb_A: "good_set A" using l_ind_good_set[OF li_A] .
have cb_B: "good_set B" using indexing_finite[OF indexing] B_in_V unfolding good_set_def by fast
case False thus ?thesis
proof -
have "linear_independent (A∪B)"
using cb_A cb_B not_dependent_implies_independent[OF _ False]
unfolding good_set_def by auto
hence "iterate_remove_ld (A∪B) h=A∪B"
using iterate_remove_ld_li by simp
thus ?thesis by simp
qed
next
case True
have cb_B: "good_set B" using indexing_finite[OF indexing] B_in_V unfolding good_set_def by fast
show ?thesis
using cb_B and True and surj_h_A and surj_h_B and zero_not_in and disjuntos and indexing
proof (induct B arbitrary: h rule: measure_induct_rule [where f = "card"])
case (less B h)
show "A ⊆ iterate_remove_ld (A∪B) h"
proof (cases "B={}")
case True
thus ?thesis
using Int_lower1 Un_absorb2 disjuntos iterate_remove_ld_li li_A subset_refl by force
next
case False
have "∃y. fst (remove_ld ((A∪B),h))=A∪(B-{y}) ∧ y∈B
∧ (snd (remove_ld (A∪B, h))) ` ({..<card A + card (B-{y})} - {..<card A}) = (B-{y})
∧ snd (remove_ld((A∪B), h)) ` {..<card A}=A ∧ indexing (A ∪ (B-{y}), snd (remove_ld (A∪B, h)))"
proof (rule descomposicion_remove_ld)
show "indexing (A ∪ B, h)" using less.prems(7) .
show "linear_dependent (A ∪ B)" using less(3) .
show "\<zero>\<^bsub>V\<^esub> ∉ A ∪ B" using less.prems(5) .
show "A ∩ B = {}" using less.prems(6) .
show " linear_independent A" using li_A .
show "h ` {..<card A} = A" using less.prems(3) .
show "h ` ({..<card A + card B} - {..<card A}) = B" using less.prems(4) .
show "B≠{}" using False .
qed
from this obtain y
where descomposicion: "fst (remove_ld ((A∪B),h))=A∪(B-{y})"
and y_in_B: "y∈B"
and h'_B: "(snd (remove_ld (A∪B, h))) ` ({..<card A + card (B-{y})} - {..<card A}) = (B-{y})"
and h'_A: "snd (remove_ld((A∪B), h)) ` {..<card A}=A"
and indexing2: "indexing (A ∪ (B-{y}), snd (remove_ld (A∪B, h)))"
by auto
have card_less: "card(B-{y})<card(B)" using y_in_B and less(2)
unfolding good_set_def using card_Diff1_less[of "B" "y"] by auto
have By_subset_B: "(B-{y})⊆B" by blast
have not_lin_indep: "¬ linear_independent (A∪B)"
using dependent_implies_not_independent [OF less.prems (2)] .
def h' == "snd (remove_ld (A∪B, h))"
show ?thesis
proof (cases "linear_independent (fst (remove_ld (A∪B, h)))")
case True
show ?thesis
apply (subst iterate_remove_ld.simps)
apply (subst iterate_remove_ld.simps)
using not_lin_indep and True
apply simp
using A_in_remove_ld[OF less.prems(7) less(3) less.prems(3) li_A less.prems(5) less.prems(6)] by simp
next
case False
show ?thesis
proof -
have cb_By: "good_set (B-{y})" using less.prems(1) y_in_B unfolding good_set_def by auto
have "A⊆iterate_remove_ld (A∪(B-{y})) h'"
proof (cases "linear_dependent (A∪(B-{y}))")
case False
show ?thesis
using cb_By iterate_remove_ld_li not_dependent_implies_independent[OF _ False]
using l_ind_good_set[OF li_A]
unfolding good_set_def by auto
next
case True show ?thesis
proof (rule less.hyps)
show "card (B-{y}) < card B"
using card_less .
show "good_set (B-{y})" using cb_By .
show "linear_dependent (A∪(B-{y}))" using True .
show " h' ` {..<card A} = A" using h'_A h'_def by auto
show "h' ` ({..<card A + card (B-{y})} - {..<card A}) = (B-{y})" using h'_B h'_def by simp
show "\<zero>\<^bsub>V\<^esub> ∉ A ∪ (B-{y})" using By_subset_B less.prems(5) by auto
show "A ∩ (B-{y}) = {}" using By_subset_B less.prems(6) by auto
show "indexing (A ∪ (B-{y}), h')" using indexing2 h'_def by simp
qed
qed
thus ?thesis
using descomposicion h'_def iterate_remove_ld.simps not_lin_indep by simp
qed
qed
qed
qed
qed
text{*Now we are in position to prove that every independent set can be extended to a basis. First we prove it
for any non-empty set.*}
lemma extend_not_empty_independent_set_to_a_basis:
assumes li_A: "linear_independent A"
and A_not_empty: "A≠{}"
shows "∃B. basis B ∧ A ⊆ B"
proof -
have cb_A: "good_set A" using l_ind_good_set[OF li_A] .
def C ≡"X-A"
have igualdad_conjuntos: "A∪X=A∪C" using C_def by auto
have finite_C: "finite C" using finite_X and cb_A C_def unfolding good_set_def by auto
have disjuntos: "A∩C={}" using C_def by auto
have "∃h. indexing (A ∪ C, h) ∧ h ` {..<card A} = A ∧ h ` ({..<card A + card C} - {..<card A}) = C"
using indexing_union [OF disjuntos _ A_not_empty finite_C]
using cb_A unfolding good_set_def by auto
from this obtain h where indexing_AC_h: "indexing ((A∪C),h)" and
surj_h_A: "h ` {..<card A} = A" and surj_h_B: "h ` ({..<card A + card C} - {..<card A}) = C" by auto
have li_iterate: "linear_independent(iterate_remove_ld (A∪C) h)"
proof (rule linear_independent_iterate_remove_ld)
show "A ∪ C ⊆ carrier V"
using l_ind_good_set[OF li_A] good_set_in_carrier C_def good_set_X
unfolding good_set_def by auto
show "\<zero>\<^bsub>V\<^esub> ∉ A ∪ C"
using li_A zero_not_in_linear_independent_set C_def by auto
show "indexing (A ∪ C, h)" using indexing_AC_h .
qed
have "span(iterate_remove_ld (A∪C) h)=span(A∪C)"
proof (rule iterate_remove_ld_preserves_span)
show "A ∪ C ⊆ carrier V"
using l_ind_good_set[OF li_A] good_set_in_carrier C_def good_set_X
unfolding good_set_def by auto
show "indexing (A ∪ C, h)" using indexing_AC_h .
show "\<zero>\<^bsub>V\<^esub> ∉ A ∪ C" using li_A zero_not_in_linear_independent_set C_def by auto
qed
also have "...=carrier V"
using span_union_basis_is_V cb_A igualdad_conjuntos
unfolding good_set_def by force
finally have span_iterate_remove_V:
"span(iterate_remove_ld (A∪C) h)=carrier V" .
have basis_iterate: "basis (iterate_remove_ld (A∪C) h)"
proof (unfold basis_def, rule conjI3)
show "iterate_remove_ld (A ∪ C) h ⊆ carrier V"
using igualdad_conjuntos l_ind_good_set li_iterate
unfolding good_set_def
by presburger
show "linear_independent_ext (iterate_remove_ld (A ∪ C) h)"
unfolding linear_independent_ext_def
using li_iterate good_set_finite l_ind_good_set C_def
using independent_set_implies_independent_subset by blast
show "spanning_set_ext (iterate_remove_ld (A ∪ C) h)"
using l_ind_good_set li_iterate span_V_eq_spanning_set
span_basis_implies_spanning_set[OF span_iterate_remove_V] spanning_imp_spanning_ext
by presburger
qed
have A_in_iterate: "A ⊆ (iterate_remove_ld (A∪C) h)"
proof (rule A_in_iterate_remove_ld)
show "indexing (A ∪ C, h)" using indexing_AC_h .
show "C ⊆ carrier V" using cb_A C_def good_set_X
unfolding good_set_def by auto
show "h ` {..<card A} = A" using surj_h_A .
show " h ` ({..<card A + card C} - {..<card A}) = C" using surj_h_B .
show "linear_independent A" using li_A .
show "\<zero>\<^bsub>V\<^esub> ∉ A ∪ C" using li_A zero_not_in_linear_independent_set C_def by auto
show "A ∩ C = {}" using disjuntos .
qed
show ?thesis using A_in_iterate and basis_iterate by auto
qed
text{*And finally the theorem (case empty is trivial since we add all elements of our fixed basis @{term X} to it.*}
theorem extend_independent_set_to_a_basis:
assumes li_A: "linear_independent A"
shows "∃B. basis B ∧ A ⊆ B"
proof (cases "A={}")
case True show ?thesis
using basis_X True empty_subsetI by fast
next
case False show ?thesis
using extend_not_empty_independent_set_to_a_basis[OF li_A False] .
qed
text{*We have proved that any independent set can be extended
to a basis, but in anywhere we have proved that there exists a basis (we have supposed it as a premisse in the case of
finite dimensional vector spaces). The proof that every vector space has a basis is not made in Halmos:
some additional results as Zorn's lemma, chains or well-ordering are required.
See http://planetmath.org/encyclopedia/EveryVectorSpaceHasABasis.html for a detailed proof.*}
text{*However, we can prove the existence of a basis in a particular case: when @{term "carrier V"} is finite.*}
text{*To prove this result, we are going to apply the function @{term iterate_remove_ld} to @{term "(carrier V - {\<zero>\<^bsub>V\<^esub>})"}.
This function requires
that @{term "\<zero>\<^bsub>V\<^esub>"} doesn't belong to the set where we apply it, so we will not apply it to @{term "carrier V"},
but to @{term "(carrier V - {\<zero>\<^bsub>V\<^esub>})"}. This function will return us a linearly independent set which span
is the same as the span of @{term "carrier V - {\<zero>\<^bsub>V\<^esub>}"}. Proving that @{term "span(carrier V - {\<zero>\<^bsub>V\<^esub>}) = carrier V"}
we will obtain the result (because @{term "carrier V - {\<zero>\<^bsub>V\<^esub>}"} is a spanning set).*}
text{*Let's see the proof. Firstly, we can see that the set $V$ is a @{text spanning_set}. It is trivial.*}
lemma spanning_set_V:
assumes finite_V: "finite (carrier V)"
shows "spanning_set (carrier V)"
using Un_absorb2 assms good_set_X good_set_def
span_union_basis_is_V span_basis_implies_spanning_set
subset_refl by metis
text{*Thanks to that, the span of $V$ is itself (trivially).*}
lemma span_V_is_V:
assumes finite_V: "finite (carrier V)"
shows "span (carrier V) = carrier V"
using assms good_set_def spanning_set_V span_V_eq_spanning_set
subset_refl by simp
text{*Now we need to prove that @{term "spanning_set (carrier V-{\<zero>\<^bsub>V\<^esub>})"}.*}
lemma spanning_set_V_minus_zero:
assumes finite_V: "finite (carrier V-{\<zero>\<^bsub>V\<^esub>})"
shows "spanning_set (carrier V-{\<zero>\<^bsub>V\<^esub>})"
proof (unfold spanning_set_def,auto)
show "good_set (carrier V - {\<zero>\<^bsub>V\<^esub>})"
using finite_V unfolding good_set_def by blast
next
fix x
assume x_in_V: "x ∈ carrier V"
let ?g="(λa. if a=x then \<one>\<^bsub>K\<^esub> else \<zero>\<^bsub>K\<^esub>)"
show "(∃f. f ∈ coefficients_function (carrier V)
∧ linear_combination f (carrier V - {\<zero>\<^bsub>V\<^esub>}) = x)"
proof (cases "x=\<zero>\<^bsub>V\<^esub>")
case True
let ?f="(λa. \<zero>\<^bsub>K\<^esub>)" show ?thesis
proof (rule exI[of _ ?f])
have cf_f: "?f ∈ coefficients_function (carrier V)"
unfolding coefficients_function_def by auto
have lc: "linear_combination ?f (carrier V - {\<zero>\<^bsub>V\<^esub>}) = x"
proof -
have "linear_combination ?f (carrier V - {\<zero>\<^bsub>V\<^esub>})
= (\<Oplus>\<^bsub>V\<^esub>y::'c∈(carrier V - {\<zero>\<^bsub>V\<^esub>}). \<zero>\<^bsub>K\<^esub> · y)"
unfolding linear_combination_def by simp
also have "...=(\<Oplus>\<^bsub>V\<^esub>y::'c∈(carrier V - {\<zero>\<^bsub>V\<^esub>}). \<zero>\<^bsub>V\<^esub>)"
proof (rule finsum_cong',auto)
fix i
assume i_in_V: "i∈ carrier V"
show "\<zero> · i = \<zero>\<^bsub>V\<^esub>"
using zeroK_mult_V_is_zeroV[OF i_in_V] .
qed
also have "...=\<zero>\<^bsub>V\<^esub>" using finsum_zero finite_V by auto
finally show ?thesis using True by simp
qed
show "?f ∈ coefficients_function (carrier V)
∧ linear_combination ?f (carrier V - {\<zero>\<^bsub>V\<^esub>}) = x"
using cf_f and lc by auto
qed
next
case False show ?thesis
proof (rule exI[of _ ?g])
have cf_g: "?g ∈ coefficients_function (carrier V)"
unfolding coefficients_function_def using x_in_V
by simp
have lc: "linear_combination ?g (carrier V - {\<zero>\<^bsub>V\<^esub>}) = x"
proof -
have x_not_zero: "x≠\<zero>\<^bsub>V\<^esub>" using False by simp
have disjuntos: "{x}∩ ((carrier V - {\<zero>\<^bsub>V\<^esub>})-{x})={}" by auto
have igualdad_conjuntos: "carrier V - {\<zero>\<^bsub>V\<^esub>}=({x}∪ ((carrier V - {\<zero>\<^bsub>V\<^esub>})-{x}))" using x_in_V x_not_zero by auto
hence "linear_combination ?g (carrier V - {\<zero>\<^bsub>V\<^esub>})=linear_combination ?g ({x}∪ ((carrier V - {\<zero>\<^bsub>V\<^esub>})-{x}))"
by auto
also have "...=linear_combination ?g {x} ⊕\<^bsub>V\<^esub> linear_combination ?g ((carrier V - {\<zero>\<^bsub>V\<^esub>})-{x})"
unfolding linear_combination_def
proof (rule finsum_Un_disjoint)
show "finite {x}" by simp
show "finite (carrier V - {\<zero>\<^bsub>V\<^esub>} - {x})" using finite_V by auto
show "{x} ∩ (carrier V - {\<zero>\<^bsub>V\<^esub>} - {x}) = {}" using disjuntos .
show "(λy. (if y = x then \<one> else \<zero>) · y) ∈ {x} -> carrier V" using mult_closed[OF x_in_V _] by auto
show "(λy. (if y = x then \<one> else \<zero>) · y) ∈ carrier V - {\<zero>\<^bsub>V\<^esub>} - {x} -> carrier V"
unfolding Pi_def using zeroK_mult_V_is_zeroV by auto
qed
also have "...=\<one>·x ⊕\<^bsub>V \<^esub>\<zero>\<^bsub>V\<^esub>"
proof -
have "linear_combination ?g (carrier V - {\<zero>\<^bsub>V\<^esub>} - {x})=(\<Oplus>\<^bsub>V\<^esub>y::'c∈(carrier V - {\<zero>\<^bsub>V\<^esub>}-{x}). \<zero>\<^bsub>V\<^esub>)"
proof (unfold linear_combination_def,rule finsum_cong',auto)
fix i
assume i_in_V: "i ∈ carrier V"
show "\<zero> · i = \<zero>\<^bsub>V\<^esub>" using zeroK_mult_V_is_zeroV[OF i_in_V] .
qed
also have "...=\<zero>\<^bsub>V\<^esub>" using finsum_zero finite_V by auto
finally show ?thesis using linear_combination_singleton[OF cf_g x_in_V] by auto
qed
also have "...= x"
using V.add.r_one mult_1 x_in_V by presburger
finally show ?thesis .
qed
show "?g ∈ coefficients_function (carrier V) ∧ linear_combination ?g (carrier V - {\<zero>\<^bsub>V\<^esub>}) = x"
using cf_g and lc by auto
qed
qed
qed
text{*As a corollary we have that @{term "span (carrier V-{\<zero>\<^bsub>V\<^esub>})=carrier V"}*}
corollary span_V_minus_zero_is_V:
assumes finite_V: "finite (carrier V-{\<zero>\<^bsub>V\<^esub>})"
shows "span (carrier V-{\<zero>\<^bsub>V\<^esub>})=carrier V"
using assms spanning_set_V_minus_zero
spanning_set_implies_span_basis by blast
text{*Finally, the theorem:*}
theorem finite_V_implies_ex_basis:
assumes finite_V: "finite (carrier V)"
shows "∃B. basis B"
proof -
have finite_V_zero: "finite (carrier V - {\<zero>\<^bsub>V\<^esub>})"
using finite_V by simp
from finite_V_zero obtain f
where indexing: "indexing (carrier V-{\<zero>\<^bsub>V\<^esub>},f)"
using obtain_indexing by auto
have 1:"span (iterate_remove_ld (carrier V-{\<zero>\<^bsub>V\<^esub>}) f)=carrier V"
using iterate_remove_ld_preserves_span[OF _ indexing _]
and span_V_minus_zero_is_V[OF finite_V_zero]
by auto
have 2:
"linear_independent (iterate_remove_ld (carrier V-{\<zero>\<^bsub>V\<^esub>}) f)"
using DiffE Diff_subset indexing insertI1
linear_independent_iterate_remove_ld by metis
have 3:"good_set (iterate_remove_ld (carrier V-{\<zero>\<^bsub>V\<^esub>}) f)"
using "2" l_ind_good_set by fast
have "basis (iterate_remove_ld (carrier V-{\<zero>\<^bsub>V\<^esub>}) f)"
using 1 and 2 and 3 using basis_def' by auto
thus ?thesis
by (rule exI[of _ "iterate_remove_ld (carrier V-{\<zero>\<^bsub>V\<^esub>}) f"])
qed
text{*A similar result than @{text spanning_set_V_minus_zero} is the next. We will use this theorem in the future.*}
lemma spanning_set_minus_zero:
assumes finite_B: "finite B"
and B_in_V: "B ⊆ carrier V"
and sg_B: "spanning_set B"
shows "spanning_set (B-{\<zero>\<^bsub>V\<^esub>})"
proof (unfold spanning_set_def,auto)
show " good_set (B - {\<zero>\<^bsub>V\<^esub>})"
unfolding good_set_def using finite_B B_in_V by fast
show "!!x. x ∈ carrier V ==> ∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f (B - {\<zero>\<^bsub>V\<^esub>}) = x"
proof (cases "\<zero>\<^bsub>V\<^esub> ∈ B")
case False
fix x
assume x_in_V: "x ∈ carrier V"
from this obtain f where cf_f: "f ∈ coefficients_function (carrier V)" and lc_B: "linear_combination f B = x"
using sg_B unfolding spanning_set_def by blast
show "∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f (B - {\<zero>\<^bsub>V\<^esub>}) = x"
using Diff_idemp Diff_insert_absorb False cf_f lc_B by auto
next
case True
fix x
assume x_in_V: "x ∈ carrier V"
from this obtain f where cf_f: "f ∈ coefficients_function (carrier V)" and lc_B: "linear_combination f B = x"
using sg_B unfolding spanning_set_def by blast
show "∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f (B - {\<zero>\<^bsub>V\<^esub>}) = x"
proof -
have lc_B0: "linear_combination f (B - {\<zero>\<^bsub>V\<^esub>}) = x"
proof -
have igualdad_conjuntos: "(insert \<zero>\<^bsub>V\<^esub> (B-{\<zero>\<^bsub>V\<^esub>}))=B" using True by fast
have "x=linear_combination f B" using lc_B by simp
also have "...=linear_combination f (insert \<zero>\<^bsub>V\<^esub> (B-{\<zero>\<^bsub>V\<^esub>}))"
using arg_cong2[OF _ igualdad_conjuntos, of f f linear_combination] by simp
also have "... = (f \<zero>\<^bsub>V\<^esub>) · \<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub> linear_combination f (B-{\<zero>\<^bsub>V\<^esub>})"
proof (rule linear_combination_insert,auto)
show "good_set (B - {\<zero>\<^bsub>V\<^esub>})" using B_in_V finite_B unfolding good_set_def by fast
show "f ∈ coefficients_function (carrier V)" using cf_f .
qed
also have "...=\<zero>\<^bsub>V\<^esub> ⊕\<^bsub>V\<^esub>linear_combination f (B-{\<zero>\<^bsub>V\<^esub>})"
using scalar_mult_zeroV_is_zeroV[of "f \<zero>\<^bsub>V\<^esub>"] cf_f zero_closed
unfolding coefficients_function_def by force
also have "...=linear_combination f (B-{\<zero>\<^bsub>V\<^esub>})"
using l_zero[OF linear_combination_closed[OF _ cf_f]] B_in_V finite_B
unfolding good_set_def by blast
finally show ?thesis by simp
qed
thus ?thesis using cf_f by fast
qed
qed
qed
text{*Every finite or infinite vector space contains a @{text spanning_set_ext} (in particular, @{term "carrier V"}
fullfills this condition):*}
lemma spanning_set_ext_carrier_V:
shows "spanning_set_ext (carrier V)"
proof (unfold spanning_set_ext_def, auto)
fix x
assume x_in_V: "x ∈ carrier V"
show "∃A. good_set A ∧ A ⊆ carrier V ∧ (∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f A = x)"
proof (rule exI[of _ "{x}"], rule conjI3)
show "good_set {x}" unfolding good_set_def using x_in_V by fast
show "{x} ⊆ carrier V" using x_in_V by fast
show "∃f. f ∈ coefficients_function (carrier V) ∧ linear_combination f {x} = x"
proof (rule exI[of _ "(λy. if y=x then \<one> else \<zero>)"], rule conjI)
show cf: "(λy. if y = x then \<one> else \<zero>) ∈ coefficients_function (carrier V)"
unfolding coefficients_function_def using x_in_V by simp
show "linear_combination (λy. if y = x then \<one> else \<zero>) {x} = x"
proof -
have "linear_combination (λy. if y = x then \<one> else \<zero>) {x}= (λy. if y = x then \<one> else \<zero>) x · x"
using linear_combination_singleton[OF cf x_in_V] .
also have "...= \<one> · x" by simp
also have "...= x" using mult_1[OF x_in_V] .
finally show ?thesis .
qed
qed
qed
qed
lemma vector_space_contains_spanning_set_ext:
shows "∃A. spanning_set_ext A ∧ A ⊆ carrier V"
using spanning_set_ext_carrier_V by blast
end
end