[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*}[/step]

[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: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]