[proofplan]
We compare the partition sums that define path length. A partition of the parameter interval for $\gamma\circ\phi$ maps under $\phi$ to a nondecreasing list of parameter values for $\gamma$; after deleting repetitions, its length sum is bounded by $L(\gamma)$. Conversely, every partition of $[0,1]$ for $\gamma$ has ordered preimages under the nondecreasing surjection $\phi$, giving the same partition sum for $\gamma\circ\phi$. Taking suprema over partitions gives both inequalities, including the case of infinite length.
[/proofplan]
[step:Define the partition sums used to compute length]
Let $\mathcal{P}([0,1])$ denote the set of finite partitions $P=(r_0,\dots,r_m)$ of $[0,1]$, meaning
\begin{align*}
0=r_0<r_1<\cdots<r_m=1.
\end{align*}
Define the partition-sum map
\begin{align*}
S:X^{[0,1]}\times\mathcal{P}([0,1])\to[0,\infty)
\end{align*}
by
\begin{align*}
S(\alpha,P):=\sum_{i=1}^{m} d(\alpha(r_i),\alpha(r_{i-1}))
\end{align*}
for every map $\alpha:[0,1]\to X$ and every partition $P=(r_0,\dots,r_m)\in\mathcal{P}([0,1])$. The length functional is the map
\begin{align*}
L:X^{[0,1]}\to[0,\infty]
\end{align*}
defined by
\begin{align*}
L(\alpha):=\sup\{S(\alpha,P):P\in\mathcal{P}([0,1])\}.
\end{align*}
[/step]
[step:Map partitions forward to prove $L(\gamma\circ\phi)\leq L(\gamma)$]
Let $P=(t_0,\dots,t_m)$ be an arbitrary finite partition of $[0,1]$. Since $\phi$ is nondecreasing and satisfies $\phi(0)=0$ and $\phi(1)=1$, the list
\begin{align*}
\phi(t_0),\phi(t_1),\dots,\phi(t_m)
\end{align*}
is nondecreasing, starts at $0$, and ends at $1$.
Delete repeated values from this list and denote the resulting strictly increasing partition by $Q=(s_0,\dots,s_k)$. The terms removed are precisely those for which $\phi(t_i)=\phi(t_{i-1})$, and such terms contribute
\begin{align*}
d(\gamma(\phi(t_i)),\gamma(\phi(t_{i-1})))=d(\gamma(\phi(t_i)),\gamma(\phi(t_i)))=0.
\end{align*}
Therefore
\begin{align*}
S(\gamma\circ\phi,P)=S(\gamma,Q).
\end{align*}
Since $Q$ is a finite partition of $[0,1]$, the definition of $L(\gamma)$ gives
\begin{align*}
S(\gamma\circ\phi,P)\leq L(\gamma).
\end{align*}
Taking the supremum over all finite partitions $P$ yields
\begin{align*}
L(\gamma\circ\phi)\leq L(\gamma).
\end{align*}
[guided]
We start with an arbitrary partition $P=(t_0,\dots,t_m)$ of the parameter interval for the reparametrized path $\gamma\circ\phi$, so
\begin{align*}
0=t_0<t_1<\cdots<t_m=1.
\end{align*}
The corresponding partition sum is
\begin{align*}
S(\gamma\circ\phi,P)=\sum_{i=1}^{m} d(\gamma(\phi(t_i)),\gamma(\phi(t_{i-1}))).
\end{align*}
Because $\phi$ is nondecreasing, the image list
\begin{align*}
\phi(t_0),\phi(t_1),\dots,\phi(t_m)
\end{align*}
is nondecreasing. Because $\phi(0)=0$ and $\phi(1)=1$, this list begins at $0$ and ends at $1$. It may fail to be a partition only because some consecutive values can be equal. We remove repeated values and call the resulting strictly increasing list $Q=(s_0,\dots,s_k)$. Then
\begin{align*}
0=s_0<s_1<\cdots<s_k=1,
\end{align*}
so $Q$ is a finite partition of $[0,1]$.
Why does deleting repeated values preserve the partition sum? If $\phi(t_i)=\phi(t_{i-1})$, then the corresponding distance term is
\begin{align*}
d(\gamma(\phi(t_i)),\gamma(\phi(t_{i-1})))=d(\gamma(\phi(t_i)),\gamma(\phi(t_i)))=0.
\end{align*}
Thus the only terms discarded have value $0$, and the remaining terms are exactly the distances appearing in $S(\gamma,Q)$. Hence
\begin{align*}
S(\gamma\circ\phi,P)=S(\gamma,Q).
\end{align*}
Since $Q$ is an admissible partition for the definition of $L(\gamma)$, we have
\begin{align*}
S(\gamma,Q)\leq L(\gamma).
\end{align*}
Therefore
\begin{align*}
S(\gamma\circ\phi,P)\leq L(\gamma).
\end{align*}
The partition $P$ was arbitrary, so taking the supremum over all partitions $P$ gives
\begin{align*}
L(\gamma\circ\phi)\leq L(\gamma).
\end{align*}
[/guided]
[/step]
[step:Pull partitions back to prove $L(\gamma)\leq L(\gamma\circ\phi)$]
Let $Q=(s_0,\dots,s_k)$ be an arbitrary finite partition of $[0,1]$. Thus
\begin{align*}
0=s_0<s_1<\cdots<s_k=1.
\end{align*}
Set $t_0:=0$ and $t_k:=1$. For each $i\in\{1,\dots,k-1\}$, surjectivity of $\phi$ gives a point $t_i\in[0,1]$ such that
\begin{align*}
\phi(t_i)=s_i.
\end{align*}
If $0\leq i<j\leq k$ and $t_i\geq t_j$, then monotonicity of $\phi$ gives
\begin{align*}
s_i=\phi(t_i)\geq \phi(t_j)=s_j,
\end{align*}
contradicting $s_i<s_j$. Hence
\begin{align*}
0=t_0<t_1<\cdots<t_k=1,
\end{align*}
so $P=(t_0,\dots,t_k)$ is a finite partition of $[0,1]$.
For this partition $P$,
\begin{align*}
S(\gamma\circ\phi,P)=\sum_{i=1}^{k} d(\gamma(\phi(t_i)),\gamma(\phi(t_{i-1}))).
\end{align*}
Using $\phi(t_i)=s_i$ for every $i\in\{0,\dots,k\}$, this becomes
\begin{align*}
S(\gamma\circ\phi,P)=\sum_{i=1}^{k} d(\gamma(s_i),\gamma(s_{i-1}))=S(\gamma,Q).
\end{align*}
Since $P$ is admissible in the definition of $L(\gamma\circ\phi)$,
\begin{align*}
S(\gamma,Q)\leq L(\gamma\circ\phi).
\end{align*}
Taking the supremum over all finite partitions $Q$ yields
\begin{align*}
L(\gamma)\leq L(\gamma\circ\phi).
\end{align*}
[/step]
[step:Combine the two inequalities]
The previous two steps give
\begin{align*}
L(\gamma\circ\phi)\leq L(\gamma)
\end{align*}
and
\begin{align*}
L(\gamma)\leq L(\gamma\circ\phi).
\end{align*}
Since both quantities lie in the ordered extended interval $[0,\infty]$, these inequalities imply
\begin{align*}
L(\gamma\circ\phi)=L(\gamma).
\end{align*}
This proves the claimed invariance of length under the orientation-preserving reparametrization $\phi$.
[/step]
