Más como un ejercicio privado que para responder a esta pregunta en particular, he intentado escribir una prueba de los principales hechos que conducen a la definición de dimensión, utilizando solo las definiciones básicas de combinación lineal, espacio generado, dependencia lineal, conjunto generador y base; aparte de eso, solo asumo algunos hechos intuitivamente (y formalmente) obvios como que un subconjunto de un conjunto linealmente independiente es linealmente independiente. Trabajo en espacios vectoriales finitamente generados, pero como no conozco la existencia de bases desde el principio, no puedo limitarme a espacios $\Bbb R^n$.
Sé que el lema de intercambio de Steinitz logra esto, haciendo todo de una sola vez, pero creo que la prueba inductiva resultante es algo técnica, y me gustaría evitar la vaguedad como "hasta el reordenamiento" y "sin pérdida de generalidad". He intentado lograr esto dividiendo en diferentes niveles de detalle, lo que lleva a evitar las ecuaciones casi por completo. Sin embargo, estoy algo insatisfecho con mi formulación, especialmente con la prueba final que parece más difícil en papel de lo que lo hizo en mi imaginación.
Uno debe usar en algún momento la inversibilidad de escalares distintos de cero; para deshacerse de eso, comienzo con un sencillo lema sobre dependencia lineal. Luego viene una proposición que construye bases, explícitamente, pero sin preocuparse por contar elementos. Esto se hace en el teorema final, que es realmente solo un comentario sobre la construcción en la proposición.
Hablo principalmente sobre familias de vectores en lugar de conjuntos, porque todo depende de una manera esencial del orden implícito por los índices (y porque no se excluyen las múltiples ocurrencias del mismo vector); sin embargo, uso la notación de construcción de conjuntos por conveniencia, que realmente no es coherente con ese punto de vista. Creo que la proposición a continuación se puede generalizar a la situación de dimensión infinita usando familias de vectores indexadas por un conjunto bien ordenado, pero para el teorema dudaría que se pueda hacer.
Para constancia, todo esto no requiere conmutatividad, y funciona sin problemas para módulos derechos generados finitamente (digamos) sobre un anillo de división. Esperaría que esto sea cierto para cualquier prueba de estos asuntos, si se escribe cuidadosamente.
Lema. Si alguna relación lineal entre miembros de un conjunto $X$ de vectores implica algún vector $v\in X$ con coeficiente distinto de cero $c_v$, entonces $v$ es una combinación lineal de los vectores restantes: $\def\Span{\operatorname{Span}}v\in\Span(X-\{v\})$.
Escriba la relación $\sum_{x\in X}c_xx=0$ como $c_vv=-\sum_{x\in X-\{v\}}c_xx$; ahora multiplique por $c_v^{-1}$ (usando que $c_v\neq0$).
Proposición. Si $S=\{f_1,\ldots,f_k\}$ es una familia linealmente independiente de vectores en$~V$, y $T=\{g_1,\ldots,g_l\}$ es una familia de vectores que genera$~V$, entonces $V$ tiene una base $S\cup C$, donde $$C=\{\,g_i\mid\,g_i\notin\Span(S\cup\{g_1,\ldots,g_{i-1}\})\}\subseteq T.$$
Para $0\leq i\leq l$, ponga $X_i=S\cup\{g_1,\ldots,g_i\}$ y $X_i'=S\cup(\{g_1,\ldots,g_i\}\cap C)$; mostramos por inducción sobre $i$ que el conjunto $X_i'$ es una familia linealmente independiente que genera$~\Span(X_i)$ (en otras palabras, una base de ese subespacio); la instancia $i=l$ da la proposición ya que $\Span(X_l)\supseteq\Span(T)=V$. Para $i=0$ esto se cumple por la independencia lineal de $S$. Para $i>0$ se distinguen los casos $g_i\notin C$ y $g_i\in C$, ambos de los cuales son fáciles. Para $g_i\notin C$ se usa que agregar al conjunto $X_{i-1}$ el vector $g_i$ que ya está en su espacio no cambia ese espacio. Para $g_i\in C$ se usa que agregar el mismo vector $g_i$ a dos conjuntos $X_{i-1},X_{i-1}'$ con el mismo espacio mantiene su espacio sin cambios, mientras que $g_i\notin\Span(X_{i-1})=\Span(X_{i-1}')$ asegura que la familia independiente $X_{i-1}'$ permanece independiente después de agregar$~g_i$ (la contrapositiva del lema dice que cualquier relación lineal involucra solo a $X_{i-1}'$, y por lo tanto es trivial).
Ahora, para cualquier familia independiente$~S$ y familia generadora$~T$, denotemos por $C(S,T)$ al conjunto $C$ de la proposición, y por $E(S,T)$ la base $S\cup C(S,T)=S\cup C$ de la proposición. Obtenemos en particular, para cualquier espacio que admita un conjunto generador finito$~T$ (espacio finitamente generado), una base $E(\emptyset,T)$ de$~V$. Por otro lado, para cualquier base $B$ de$~V$ se tiene $E(B,T)=B$, ya que $C=\emptyset$ en la proposición. Ahora podemos mostrar que la dimensión está bien definida en el caso de espacios finitamente generados.
Teorema. Para cualquier $S,T$ como arriba, la base $E(S,T)$ tiene el mismo número de elementos que $E(\emptyset,T)$.
La demostración es por inducción sobre el tamaño de$~S$, siendo trivial el caso $S=\emptyset$. Entonces considere $S=\{f_1,\ldots,f_k\}$ con $k>0$, y asumiendo que el resultado se cumple para $S^-=\{f_1,\ldots,f_{k-1}\}$. A partir de la definición es claro que $C(S,T)\subseteq C(S^-,T)$, y debemos mostrar que el complemento $C(S^-,T)\setminus C(S,T)$ contiene exactamente un elemento. Dado que $E(S^-,T)$ es una base de$~V$, hay una expresión única de $f_k$ como combinación lineal$~L$ de sus elementos. Esa combinación involucra algún elemento de$~C(S^-,T)$ con coeficiente distinto de cero, porque la familia$~S$ es linealmente independiente. Si $i$ es maximal tal que $g_i\in C(S^-,T)$ aparece con coeficiente distinto de cero en$~L$, entonces por el lema $g_i\in\Span(f_1,\ldots,f_k,g_1,\ldots,g_{i-1})$, y por lo tanto $g_i\in C(S^-,T)\setminus C(S,T)$. Recíprocamente, si $g_j\in C(S^-,T)\setminus C(S,T)$ entonces $g_j\in\Span(\{f_1,\ldots,f_k,g_1,\ldots,g_{j-1}\}\cap E(S,T))$ y la combinación lineal que atestigua esto debe involucrar a $f_k$ con un coeficiente distinto de cero (debido a $g_j\in C(S^-,T)$); por el lema y la unicidad de la expresión$~L$ para $f_k$ esto fuerza $j=i$, completando la prueba.
