The proof consists of two parts. First we need to show that such a vector $\vct{b}$ satisfying the linear system exists and further can be computed in $O(m)$ time. Second we need to show that $\numocc{G}{\tri}, \numocc{G}{\threedis}$ can indeed be computed in time $O(1)$.
The lemma claims that for $\vct{M}=
\begin{pmatrix}
1 - 3p & -(3\prob^2 - \prob^3)\\
10(3\prob^2 - \prob^3) & 10(3\prob^2 - \prob^3)
\end{pmatrix}$, $\vct{x} =
\begin{pmatrix}
\numocc{G}{\tri}]\\
\numocc{G}{\threedis}
\end{pmatrix}$
that the system $\vct{M}\cdot\vct{x}=\vct{b}$.
To prove the first step, we use \cref{lem:qE3-exp} to derive the following equality (dropping the superscript and referring to $G^{(1)}$ as $G$:
Note that the RHS of \Cref{eq:b1-alg-2} is indeed the product $\vct{M}[1]\cdot\vct{x}[1]$. Further note that this product is equal to the LHS of \Cref{eq:b1-alg-2}, where every term is computable in $O(m)$ time (by equations~\ref{eq:1e}-~\ref{eq:3p-3tri}). We set $\vct{b}[1]$ to the RHS of \Cref{eq:b1-alg-2}.
We follow the same process in deriving an equality for $G^{(2)}$. Replacing occurrences of $G$ with $G^{(2)}$, we obtain \Cref{eq:b1-alg-2} for $G^{(2)}$. Substituting identities from \cref{lem:3m-G2} and \cref{lem:tri} we obtain
As in the previous equality derivation for $G$, note that the RHS of \Cref{eq:b2-final} is the same as $\vct{M}[2]\cdot\vct{x}[2]$. The RHS of \Cref{eq:b2-final} has terms all computable (by equations~\ref{eq:1e}-~\ref{eq:3p-3tri}) in $O(m)$ time. Setting $\vct{b}[2]$ to the RHS then completes the proof of step 1.
From ~\cref{eq:det-final} it can easily be seen that the roots of $\dtrm{\vct{M}}$ are $0, 1,$ and $3$. Hence there are no roots in $(0, 1)$ and ~\cref{lem:lin-sys} follows.
%For every value $\kElem \geq 3$, there exists a query with $\kElem$ product width that is hard.
%\end{Corollary}
%\begin{proof}[Proof of Corollary ~\ref{cor:single-p-gen-k}]
%Consider $\poly^3_{G}$ and $\poly' = 1$ such that $\poly'' = \poly^3_{G} \cdot \poly'$. By ~\cref{th:single-p}, query $\poly''$ with $\kElem = 4$ has $\Omega(\numvar^{\frac{4}{3}})$ complexity.