So I'm working on Viro's "Elementary Topology" textbook and I got stuck on this question:
Consider a loop $u : I \to X$ at $x_0$ , a loop $v : I \to Y$ at $y_0$ , and the loop $w = u \times v : I \to X \times Y$ . We introduce the loops $u^′ : I \to X \times Y : t \mapsto (u(t), y _0 )$ and $v ′ : I \to X \times Y : t \mapsto (x_0 , v(t))$. Prove that $u^′ v^′ \sim w \sim v^′ u^′$ .
Where $f \sim g$ means $f$ homotopic to $g$. My thoughts on this are: I've proven earlier in Viro that $ f,g: X \to Y \times Z $ are homotopic iff $pr_L \circ f$ is homotopic to $ pr_L \circ g$, where $L \in \{Y,Z\}$. So it suffices to show that $ pr \circ u^′ v^′ \sim pr \circ w $. Easy to see that $ pr_X \circ w \equiv u $ and $$ pr_X \circ u^′ v^′ = \begin{cases} u(2t): t \in [0,\frac{1}{2}] \\ x_0 : t \in [\frac{1}{2},1] \end{cases} $$ Consider $\varphi: I \to I: t \mapsto \frac{t}{2}$. Then $pr_X \circ u^′ v^′ \circ \varphi \equiv u $. Since $\varphi \sim id$, then $ pr_X \circ u^′ v^′ \sim pr_X \circ w$. The same is for $pr_Y$ with $\varphi: t \mapsto \frac{t+1}{2}$. So $u^′ v^′ \sim w$. Analogously $v^′ u^′ \sim w$.
Is my proof correct? I'm not confident for that.
Just in order to give this question an answer; the answer is yes. The proof is correct.