Theory Dimension_of_a_Subspace

theory Dimension_of_a_Subspace
  imports Calculus_of_Subspaces
begin

section{*Dimension of a Subspace*}

context finite_dimensional_vector_space
begin

subsection{*Theorem 1.*}

text{*The theorem states that the subspace is itself a vector space and
  that its dimesion is less than or equal to the one of @{term V}. We split
  both conclusions in two different lemmas that later will be merged.*}
text{*The first part of the theorem has been already proved:*}

lemma theorem_1_part_1:
  assumes m: "subspace M"
  shows "vector_space K (V(|carrier:=M|)),) (op ·)"
  using subspace_is_vector_space [OF m] .

text{*The second part of the theorem requires a definition of dimension.
  The dimension of a (finite) vector space should be defined as the cardinal
  of any of its basis, once we have proved that every basis has the same cardinal 
  (file @{text Finite_Vector_Space.thy}). In the meanwhile, I use @{term dim}*}

text{*Its proof should be direct by reduction ad absurdum, following 
  the one in Halmos.*}

lemma theorem_1_part_2:
  assumes m: "subspace M"
  shows "dim (V(|carrier:=M|)),) ≤ dimension" 
  sorry

subsection{*Theorem 2.*}

text{*The notation in the following statement might be a bit confusing. 
  The indexing @{term f} is just necessary to later select the first 
  @{term m} elements of a base, with @{term m} being the dimension of the
  subspace @{term M}. These @{term m} elements can be completed
  up to a basis of @{term V}.*}

text{*The proof should be done using that @{term M} is a vector space of dimension
  less or equal to the one of @{term V}. Therefore we can find a basis of it which 
  cardinal is less than or equal to @{term "dimension"}. This basis is a collection
  of linearly independent vectors, and therefore can be completed up to a basis
  of @{term V}, thanks to one of the lemmas proved in 
  @{text Finite_Vector_Space.thy}.*}

lemma theorem_2:
  assumes m: "subspace M"
  shows "(∃B f. (basis B) ∧ indexing (B, f) ∧
  (vector_space.basis K (V(|carrier:=M|)),) (op ·) (f ` {..dim (V(|carrier:=M|)),)})))"
proof -
  interpret M: vector_space K "(V(|carrier:=M|)),)" "(op ·)" 
    using subspace_is_vector_space [OF m] .
  show ?thesis
   sorry    
qed

end

end