Given an opening $(m, r)$ of a Pedersen commitment $c = g^m h^r$, where $g, h$ are the generators of a group $G$ with prime order $q$ (public), a PPT prover wants to prove to a verifier the opening of $c$ in zero-knowledge. Let us see the following procedure. Here we note that the DLP in $G$ is hard.
Prover randomly pick $s, t < q$, computes $y = g^s h^t$.
The verifier checks whether $y \in G$. If it is, the verifier sends a random challenge $e$ to the prover.
The prover sends to the verifier $z_1 = s + em \bmod q$, $z_2 = t + er \bmod q$.
The verifier accepts if $g^{z_1} h^{z_2} = y c^e$.
It seems that this argument works for our requirements. It is complete and special honest-verifier zero-knowledge.
But for the soundness, if a malicious prover provides $z_1' \ne z_1$, $z_2' \ne z_2$, such that $g^{z_1'}h^{z_2'} = yc^e$, it seems that such a prover can cheat in the procedure above. I know that a PPT prover cannot do this except for a negligible probability. But how can we formally prove this fact? Is it possible to provide a formal reduction that, if a malicious prover can cheat in this way, using this malicious prover we can provide two openings of a Pedersen commitment? If we can't, how can we show the soundness of this procedure? In a formal proof, do we need to always provide a reduction?