Lemme d'échange et théorème de la dimension

[btsix]

Bonjour,

Je connais le lemme de Steinitz qui énonce que si dans un ev $ E $ on a une famille génératrice de $ k $ vecteurs, toute famille d'au moins $ k+1 $ vecteurs est liée et sa démonstration par récurrence. Je sais aussi qu'il permet de montrer que les bases d'un ev de dimension finie ont même cardinal.
Cependant j'ai vu dans le cours de Troesch un lemme qu'il appelle théorème d'échange :

Soient $ E $ un ev, $ F \subset E $ et $ x $,$ y \in E $ tels que $ x \notin \text{Vect}(F) $ et $ x\in \text{Vect}(F \cup \{y\}) $. Alors $ \text{Vect}(F\cup \{x\}) = \text{Vect}(F \cup \{y\}) $.

Ce lemme permettrait également de montrer le théorème de la dimension, mais je n'ai pas réussi à trouver une démarche n'utilisant pas le lemme de Steinitz. Peut-être que celui-ci même peut être prouvé simplement par le lemme d'échange, mais je n'en sais rien.

Merci de vos éclaircissements.

[GaBuZoMeu]

Si on a une base B de E et un système générateur G, on peut en utilisant le lemme d'échange remplacer un par un les éléments de B par des éléments de G en gardant la propriété d'être une base de E et on extrait ainsi de G une base ayant le même nombre d'éléments que B.

[btsix]

Ok merci