Theorem: Size of Linearly Independent Subset is at Most Size of Finite Generator

Let $R$ be a division ring.
Let $V$ be an $R$-vector space.
Let $F \subseteq V$ be a finite generator of $V$ over $R$.
Let $L \subseteq V$ be linearly independent over $R$.
Then:
:$\size L \le \size F$

Proof:
We first consider the case where $L$ is finite.
Let $S \subseteq \N$ be the set of all $n \in \N$ such that:
:For every finite generator $F$ of $V$, if $\card {L \setminus F} \le n$, then $\card L \le \card F$
where:
:$L \setminus F$ denotes the set difference between $L$ and $F$
:$\card L$ and $\card F$ denote the cardinality of $L$ and $F$ respectively.
We use the Principle of Finite Induction to prove that $S = \N$.
=== Basis of the Induction ===
Let $\card {L \setminus F} \le 0$.
Then from Cardinality of Empty Set:
:$L \setminus F = \O$
By Set Difference with Superset is Empty Set:
:$L \subseteq F$
By Cardinality of Subset of Finite Set:
:$\card L \le \card F$
Hence:
:$0 \in S$
This is the basis for the induction.
=== Induction Hypothesis ===
It is to be shown that if $k \in S$ where $k \ge 1$, then it follows that $k + 1 \in S$.
This is the induction hypothesis:
:For every finite generator $F$ of $V$, if $\card {L \setminus F} \le k$, then $\card L \le \card F$
It is to be demonstrated that it follows that:
:For every finite generator $F$ of $V$, if $\card {L \setminus F} \le k + 1$, then $\card L \le \card F$
=== Induction Step ===
This is the induction step:
Assume the induction hypothesis that $n \in S$.
Let $F$ be a finite generator of $V$ such that:
:$\card {L \setminus F} = n + 1$
Let $v \in L \setminus F$.
Let $L' = L \cap \paren {F \cup \set v}$.
By Intersection is Subset:
:$L' \subseteq L$
By Subset of Linearly Independent Set is Linearly Independent, it follows that $L'$ is linearly independent over $R$.
Also by Intersection is Subset:
:$L' \subseteq F \cup \set v$
Therefore, by Vector Space has Basis Between Linearly Independent Set and Finite Spanning Set:
:there exists a basis $B$ of $V$ such that:
::$L' \subseteq B \subseteq F \cup \set v$
Since $v \notin F$ is a linear combination of $F$, it follows that $F \cup \set v$ is linearly dependent over $R$.
Therefore:
:$B \subsetneq F \cup \set v$
By Cardinality of Subset of Finite Set:
:$\card B < \card {F \cup \set v} = \card F + 1$
Hence:
:$\card B \le \card F$
We have that:
{{begin-eqn}}
{{eqn | l = \card {L \setminus B}
      | o = \le
      | r = \card {L \setminus L'}
      | c = Relative Complement inverts Subsets and Cardinality of Subset of Finite Set
}}
{{eqn | r = \card {L \setminus \paren {F \cup \set v} }
      | c = Set Difference with Intersection is Difference
}}
{{eqn | r = \card {\paren {L \setminus F} \setminus \set v}
      | c = Set Difference with Union
}}
{{eqn | r = n + 1 - 1
      | c = Cardinality of Set Difference with Subset
}}
{{eqn | r = n
}}
{{end-eqn}}
Since $n \in S$:
:$\card L \le \card B \le \card F$
Hence:
:$n + 1 \in S$
and so the induction step has been completed.
By Set Difference is Subset:
:$L \setminus F \subseteq L$
From Subset of Finite Set is Finite:
:$L \setminus F$ is finite.
Therefore, we can apply the fact that $S = \N$ to conclude that:
:$\card L \le \card F$
Let $L$ be infinite.
Then by Set is Infinite iff exist Subsets of all Finite Cardinalities, there exists a finite subset $L' \subseteq L$ such that:
:$\card {L'} = \card F + 1$
By Subset of Linearly Independent Set is Linearly Independent, it follows that $L'$ is linearly independent over $R$.
It is proven above that this is impossible.
Hence the result.
{{qed}}