De todo gerador finito extrai-se uma base
Todo espaço vetorial \(V\neq\{0\}\) gerado por um conjunto finito possui base. Mais precisamente: de todo conjunto gerador finito pode-se extrair uma base.
A demonstração é um algoritmo: ela não só garante a existência como diz como achar a base. Isso é usado toda vez que um subespaço vem dado por geradores.
Demonstração
Seja \(G = \{u_1,\ldots,u_m\}\) com \([G] = V\). Se \(G\) é LI, ele já é base e acabou. Se não é, pela Proposição 2.46 algum \(u_j\) é combinação linear dos demais; e, pelo Lema 2.42, retirar de um gerador um vetor que é combinação dos outros não altera o subespaço gerado, logo \(G\setminus\{u_j\}\) ainda gera \(V\).
Repetimos o procedimento. Ele termina, porque a cada passo o conjunto perde um elemento e começamos com um número finito deles. E ele não pode chegar ao conjunto vazio, porque \([\,\emptyset\,] = \{0\}\neq V\). O conjunto que sobra gera \(V\) e é LI: é base.