Suppose I have two metric spaces $(X, d)$ and $(Y, d')$. Let $x_0, x_1 \in X$ and $y_0, y_1 \in Y$ arbitrarily. Suppose $s(t) : I \to X$ parameterizes the shortest possible path from $x_0$ to $x_1$ in $X$ and $j(t) : I \to Y$ likewise parameterizes the shortest possible path from $y_0$ to $y_1$ in $Y$.
We get a natural metric $D : (X \times Y)^2 \to \mathbb{R}_{\geq 0}$ defined by $$D : ((x, y), (x', y')) \mapsto \sqrt{ d(x, x')^2 + d'(y, y')^2 }$$ Intuitively, this makes me think we should also get a natural parameterization of the shortest possible path under $D$ from $(x_0, y_0)$ to $(x_1, y_1)$ in $X \times Y$ defined by $$k : t \mapsto (s(t), j(t))$$ ... but I don't really know how I would go about proving that this path is or is not optimal. What does a proof sketch look like for showing something like this? (I am happy to do the proof myself; I just don't know where to start and would like a point in the right direction.) Thanks!
EDIT: Here is my progress toward a proof:
I think am correct, and can prove it as follows.
A line from $u$ to $v$ in a metric space $(U, d)$ is a set $\{ a \in U \mid d(u, a) + d(a, v) = d(u, v) \}$.
Since we assume $s$ is optimal, it follows that $s$ follows a segment of a line from $x_0$ to $x_1$. Were this not the case, we could use the triangle inequality to find an at-least-as-good solution which does follow a segment of a line from $x_0$ to $x_1$. So, assume $s$ follows a segment of a line from $x_0$ to $x_1$. Apply this same logic to $j$ which goes from $y_0$ to $y_1$.
Let $k$ be as in the problem statement. Then $k$ follows a line-segment from $(x_0, y_0)$ to $(x_1, y_1)$:
$$ \iff D((x_0, y_0), k(t)) + D(k(t), (x_1, y_1)) = D((x_0, y_0), (x_1, y_1))$$
$$\iff D((x_0, y_0), (s(t), j(t))) + D((s(t), j(t)), (x_1, y_1)) = D((x_0, y_0), (x_1, y_1))$$
$$\iff \sqrt{ d(x_0, s(t))^2 + d'(y_0, j(t))^2 } + \sqrt{ d(s(t), x_1)^2 + d'(j(t), y_1)^2 } = \sqrt{ d(x_0, x_1)^2 + d'(y_0, y_1)^2 }$$
When I try to untangle this, the algebra is grotesque. Is this actually the proof structure? Just brute-forcing this despicable mess of algebra? Or is there a better way to do it?
If you clean up the vagueness of the phrase "parameterizes the shortest possible path", then things become clearer.
The hypothesis you want is simply that the path $s(t) : [0,1] \to X$ is a reparameterized geodesic, meaning that $d(s(u),s(v))=|u-v| \cdot d(x_0,x_1)$ for all $u,v \in [0,1]$, and similarly for $j(t)$.
With that, it's then simple algebra to check that $k(t)$ is also a reparameterized geodesic.
By the way, n actual geodesic in this context would be a path of the form $s(t) : [0,d(x_0,x_1)] \to X$ such that $d(s(u),s(v)) = |u-v|$ for all $(u,v) \in [0,d(x_0,x_1)]$, and similarly for $j(t)$. But then the formula for $k$ would not make sense.