Dimension d'un espace vectoriel

On utilise le point (iv) du nœud Familles libres, bases : si $L$ est libre et $x \notin \operatorname{Vect}(L)$, alors $L \cup \{x\}$ est libre. Aucun choix n'intervient.

(i) Soit $(g_1, \dots, g_n)$ génératrice. Parmi ses sous-familles libres, dont le nombre d'éléments est au plus $n$ (Lemme d'échange), il y en a une de nombre d'éléments maximal ; par ce point (iv), chaque $g_j$ appartient au sous-espace qu'elle engendre, qui est donc $E$ : c'est une base finie.

Soit $B$ cette base finie, à $n$ éléments, et $B'$ une base quelconque. Toute sous-famille finie de $B'$ est libre, donc a au plus $n$ éléments par le lemme d'échange, $B$ étant génératrice. Ainsi $B'$ est finie, sinon on y prendrait un à un $n + 1$ éléments distincts, ce qui ne demande qu'un nombre fini de choix, et $|B'| \leqslant n$. Le même lemme, appliqué à $B'$ génératrice et à $B$ libre, donne $n \leqslant |B'|$.

(ii) Une base, à $n$ éléments, est génératrice : le lemme d'échange borne les familles libres par $n$. Si $L$ est libre à $n$ éléments et non génératrice, on lui ajoute un vecteur hors de $\operatorname{Vect}(L)$ et l'on obtient une famille libre à $n + 1$ éléments : contradiction.

Une famille génératrice contient une base, comme dans (i), donc a au moins $n$ éléments, et si elle en a exactement $n$, cette base est la famille entière.

(iii) Soit $L$ libre et $B$ une base. Parmi les familles libres formées de $L$ et de vecteurs de $B$, en nombre au plus $n$, on en prend une de nombre d'éléments maximal ; elle engendre chaque vecteur de $B$, par ce même point, donc $E$.

Pour un sous-espace $F$, on prend de même une famille libre de $F$ à nombre d'éléments maximal, au plus $n$ : elle engendre $F$, et c'en est une base. Si $\dim F = n$, cette base est une famille libre à $n$ éléments de $E$, donc une base de $E$ par (ii), et $F = E$.