Dimension of the preimage of a vector subspace (source code)

= Dimension of the preimage of a vector subspace
{title2=$\dim T^{-1}(X)=\dim(X\cap\operatorname{im}T)+\dim\ker T$}

Let $T:U\to V$ be a <linear map> between finite-dimensional <vector spaces> and $X$ a <vector subspace> of $V$. The <preimage> $T^{-1}(X)$ is a <vector subspace> containing $\ker T$. To compute its <dimension>, choose a <basis> $k_1,\ldots,k_s$ of $\ker T$ and a <basis> $y_1,\ldots,y_d$ of $X\cap\operatorname{im}T$. Lift each $y_j$ to $u_j\in U$ with $Tu_j=y_j$. Then $k_1,\ldots,k_s,u_1,\ldots,u_d$ is a <basis> of $T^{-1}(X)$: applying $T$ proves <linear independence>, and subtracting a suitable <linear combination> of the lifts reduces every element of the <preimage> to the <kernel>. This proves the displayed formula without using the <rank-nullity theorem>. Taking $X=V$ then proves the <rank-nullity theorem> itself.