description/proof of that vectors space has basis
Topics
About: vectors space
The table of contents of this article
Starting Context
- The reader knows a definition of %field name% vectors space.
- The reader knows a definition of basis of module.
- The reader admits the proposition that for any vectors space, any generator of the space, and any linearly independent subset contained in the generator, the generator can be reduced to be a basis with the linearly independent subset retained.
Target Context
- The reader will have a description and a proof of the proposition that any vectors space has a basis.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(F\): \(\in \{\text{ the fields }\}\)
\(V\): \(\in \{\text{ the } F \text{ vectors spaces }\}\)
//
Statements:
\(\exists B \in \{\text{ the bases for } V\}\)
//
\(V\) does not need to be finite-dimensional.
2: Proof
Whole Strategy: Step 1: apply the proposition that for any vectors space, any generator of the space, and any linearly independent subset contained in the generator, the generator can be reduced to be a basis with the linearly independent subset retained.
Step 1:
Let us apply the proposition that for any vectors space, any generator of the space, and any linearly independent subset contained in the generator, the generator can be reduced to be a basis with the linearly independent subset retained.
\(S' := V\) is a generator of \(V\).
When \(V = \{0\}\), \(\emptyset\) is the basis.
Let us suppose that \(V \neq \{0\}\) hereafter.
Let us take any \(v \in V\) such that \(v \neq 0\).
\(S := \{v\}\) is a linearly independent subset of \(V\) contained in \(S'\).
By the proposition that for any vectors space, any generator of the space, and any linearly independent subset contained in the generator, the generator can be reduced to be a basis with the linearly independent subset retained, \(S'\) can be reduced to \(B\) such that \(S \subseteq B\).
So, there is the basis, \(B\).
