[proofplan]
We prove that a chart identifies tangent vectors at $p$ with coordinate velocities in $\mathbb{R}^n$. The definition of tangency makes the coordinate-velocity map well-defined and injective, while surjectivity follows by lifting straight coordinate lines through $\varphi(p)$ back to curves in $M$. Finally, we check that changing charts only composes this identification with the derivative of a smooth transition map, whose inverse is the derivative of the inverse transition map; hence the [vector space](/page/Vector%20Space) structure is chart-independent and has dimension $n$.
[/proofplan]
[step:Define the coordinate-velocity map using a chart around $p$]
Fix a smooth chart $(U,\varphi)$ with $p \in U$, where
\begin{align*}
\varphi: U \to \varphi(U) \subseteq \mathbb{R}^n
\end{align*}
is a diffeomorphism onto the [open set](/page/Open%20Set) $\varphi(U)$. Let $\gamma: I \to M$ be a smooth curve, where $I \subseteq \mathbb{R}$ is an open interval with $0 \in I$ and $\gamma(0)=p$. Since $U$ is open and $\gamma$ is continuous, there exists an open interval $J \subseteq I$ with $0 \in J$ and $\gamma(J) \subseteq U$. Therefore the coordinate curve
\begin{align*}
\varphi \circ \gamma|_J: J \to \mathbb{R}^n
\end{align*}
is smooth, so its velocity at $0$ is defined.
Define
\begin{align*}
\Phi_\varphi: T_pM &\longrightarrow \mathbb{R}^n \\
[\gamma] &\longmapsto \frac{d}{dt}\Big|_{t=0}(\varphi \circ \gamma)(t).
\end{align*}
By the definition of the [equivalence relation](/page/Equivalence%20Relation) defining $T_pM$, two curves represent the same tangent vector exactly when their coordinate velocities agree in one, equivalently every, smooth chart about $p$. Hence $\Phi_\varphi$ is well-defined.
[/step]
[step:Prove that the coordinate-velocity map is injective]
Let $[\gamma_1],[\gamma_2] \in T_pM$, where
\begin{align*}
\gamma_1: I_1 \to M, \qquad \gamma_2: I_2 \to M
\end{align*}
are smooth curves with $0 \in I_1 \cap I_2$ and $\gamma_1(0)=\gamma_2(0)=p$. Suppose
\begin{align*}
\Phi_\varphi([\gamma_1])=\Phi_\varphi([\gamma_2]).
\end{align*}
By definition of $\Phi_\varphi$, this means
\begin{align*}
\frac{d}{dt}\Big|_{t=0}(\varphi \circ \gamma_1)(t)
=
\frac{d}{dt}\Big|_{t=0}(\varphi \circ \gamma_2)(t).
\end{align*}
Thus $\gamma_1$ and $\gamma_2$ are tangent at $p$ in the chart $(U,\varphi)$. By the defining equivalence relation on smooth curves through $p$, this gives
\begin{align*}
[\gamma_1]=[\gamma_2].
\end{align*}
Therefore $\Phi_\varphi$ is injective.
[/step]
[step:Lift each vector in $\mathbb{R}^n$ to a curve through $p$]
Let $v \in \mathbb{R}^n$. Since $\varphi(U)$ is open and $\varphi(p) \in \varphi(U)$, there exists $\varepsilon>0$ such that
\begin{align*}
\varphi(p)+tv \in \varphi(U)
\end{align*}
for every $t \in (-\varepsilon,\varepsilon)$. Define the smooth curve
\begin{align*}
\gamma_v: (-\varepsilon,\varepsilon) &\to M \\
t &\mapsto \varphi^{-1}(\varphi(p)+tv).
\end{align*}
Then $\gamma_v(0)=p$, and
\begin{align*}
(\varphi \circ \gamma_v)(t)=\varphi(p)+tv
\end{align*}
for every $t \in (-\varepsilon,\varepsilon)$. Differentiating at $t=0$ gives
\begin{align*}
\Phi_\varphi([\gamma_v])
=
\frac{d}{dt}\Big|_{t=0}(\varphi(p)+tv)
=
v.
\end{align*}
Thus $\Phi_\varphi$ is surjective.
[/step]
[step:Transport the vector space structure from $\mathbb{R}^n$ to $T_pM$]
Since $\Phi_\varphi$ is bijective, define addition and scalar multiplication on $T_pM$ by transporting the usual vector space operations from $\mathbb{R}^n$. For $[\gamma_1],[\gamma_2] \in T_pM$ and $a \in \mathbb{R}$, set
\begin{align*}
[\gamma_1]+[\gamma_2]
&:=
\Phi_\varphi^{-1}\bigl(\Phi_\varphi([\gamma_1])+\Phi_\varphi([\gamma_2])\bigr), \\
a[\gamma_1]
&:=
\Phi_\varphi^{-1}\bigl(a\,\Phi_\varphi([\gamma_1])\bigr).
\end{align*}
With these operations, $\Phi_\varphi$ is linear by construction. Since $\mathbb{R}^n$ is a real vector space and $\Phi_\varphi$ is a bijection preserving the transported operations, $T_pM$ is a real vector space and $\Phi_\varphi$ is a vector space isomorphism.
[/step]
[step:Check that changing charts gives the same vector space structure]
Let $(V,\psi)$ be another smooth chart with $p \in V$, where
\begin{align*}
\psi: V \to \psi(V) \subseteq \mathbb{R}^n
\end{align*}
is a diffeomorphism onto the open set $\psi(V)$. Define the transition map near $\varphi(p)$ by
\begin{align*}
\theta: \varphi(U \cap V) &\to \psi(U \cap V) \\
x &\mapsto (\psi \circ \varphi^{-1})(x).
\end{align*}
The map $\theta$ is smooth, and its inverse is
\begin{align*}
\theta^{-1}: \psi(U \cap V) &\to \varphi(U \cap V) \\
y &\mapsto (\varphi \circ \psi^{-1})(y).
\end{align*}
Let $a:=\varphi(p)$. For every $[\gamma] \in T_pM$, the chain rule gives
\begin{align*}
\Phi_\psi([\gamma])
=
D\theta_a\bigl(\Phi_\varphi([\gamma])\bigr),
\end{align*}
where
\begin{align*}
D\theta_a: \mathbb{R}^n \to \mathbb{R}^n
\end{align*}
is the total derivative of $\theta$ at $a$.
Since $\theta^{-1}\circ \theta=\operatorname{id}_{\varphi(U \cap V)}$ and $\theta\circ\theta^{-1}=\operatorname{id}_{\psi(U \cap V)}$, differentiating at $a$ and at $\psi(p)$ gives
\begin{align*}
D(\theta^{-1})_{\psi(p)} \circ D\theta_a
&=
\operatorname{id}_{\mathbb{R}^n}, \\
D\theta_a \circ D(\theta^{-1})_{\psi(p)}
&=
\operatorname{id}_{\mathbb{R}^n}.
\end{align*}
Hence $D\theta_a$ is a linear isomorphism. Therefore the two identifications $\Phi_\varphi$ and $\Phi_\psi$ differ by a linear isomorphism:
\begin{align*}
\Phi_\psi = D\theta_a \circ \Phi_\varphi.
\end{align*}
Transporting the vector space operations through either chart gives the same operations on curve classes, because composition with a linear isomorphism preserves addition and scalar multiplication.
[/step]
[step:Conclude that the tangent space has dimension $n$]
For the chosen chart $(U,\varphi)$, the map
\begin{align*}
\Phi_\varphi: T_pM \to \mathbb{R}^n
\end{align*}
is a vector space isomorphism. Therefore $T_pM$ is isomorphic to $\mathbb{R}^n$ as a real vector space. Since $\mathbb{R}^n$ has dimension $n$, it follows that
\begin{align*}
\dim_{\mathbb{R}} T_pM = n.
\end{align*}
This proves both the asserted coordinate identification and the dimension statement.
[/step]
