Prove a variant of Farkas' Lemma Farkas' Lemma is given as follows
Let $\pmb A\in\mathbb R^{m\times n}$ and $\pmb b\in\mathbb R^m$. Then exactly one of the following two assertions is true:
1.1. There exists an $\pmb x\in\mathbb R^n$ such that $\pmb A\pmb x=\pmb b$ and $\pmb x\ge 0$
1.2. There exists a $\pmb y\in\mathbb R^m$ such that $\pmb A^\top\pmb y\ge \pmb0$ and $\pmb b^\top\pmb y<0$
A variant of Farkas' Lemma is given as follows
Let $\pmb A\in\mathbb R^{m\times n}$ and $\pmb b\in\mathbb R^m$. Then exactly one of the following two assertions is true:
2.1. There exists an $\pmb x\in\mathbb R^n$ such that $\pmb A\pmb x\le\pmb b$
2.2. There exists a $\pmb y\ge 0$ such that $\pmb A^\top\pmb y= \pmb0$ and $\pmb b^\top\pmb y=-1$
I'm confused about how to get $\pmb A^\top\pmb y=\pmb 0$ in 2.2.
I've read several proofs online, but none of them can help me understand it. For example,
this proof constructs $\pmb A'=
\begin{bmatrix}\pmb A&-\pmb A&\pmb I\end{bmatrix}$ and $\pmb x'=\begin{bmatrix}\pmb x^+\\\pmb x^-\\\pmb s\end{bmatrix}\ge \pmb 0$. If there is no $\pmb x$ such that $\pmb A'\pmb x'\le \pmb b$, following Farkas' Lemma, there exists $\pmb y\ge 0$ such that $\pmb y^\top\pmb A'\ge\pmb 0$ and $\pmb y^\top\pmb b<0$. Then it derives $\pmb y^\top\pmb A=\pmb 0$ because $\pmb y^\top\pmb A\ge \pmb 0$ and $-\pmb y^\top\pmb A\ge\pmb 0$. But from $\pmb y^\top\pmb A'\ge \pmb 0$, I can only get $\pmb y^\top\pmb A - \pmb y^\top\pmb A + \pmb y^\top\ge \pmb 0$. How can I get "$\pmb y^\top\pmb A\ge \pmb 0$ and $-\pmb y^\top\pmb A\ge\pmb 0$"?
 A: If there is no $\pmb x \in \mathbb{R}^n$ such that $\pmb A\pmb x \leq \pmb b$, then there is no $\pmb x \geq \pmb 0$ such that $\pmb A'\pmb x' = \pmb b$. Following Farkas' Lemma, there exists $\pmb y\in\mathbb R^m$ such that $\pmb A'^\top \pmb y \ge\pmb 0$ (1) and $\pmb y^\top\pmb b< 0$ (2). Note that (1) is equivalent to $\pmb A^\top \pmb y \geq \pmb 0$ (3), $-\pmb A^\top \pmb y \geq \pmb 0$ (4) and $\pmb y \geq \pmb 0$ (5). Combining (3) and (4) gives $\pmb A^\top \pmb y = \pmb 0$. From (2) you get $\pmb y^\top\pmb b = -1$ because you can always rescale $\pmb y$.
A: Variants of Farkas' Lemma

Let $A\in\mathbb{R}^{m\times n}$ and $b\in\mathbb{R}^m$. The following two variants of Farkas' lemma are equivalent:
\begin{align*}
&\exists y\in\mathbb{R}^m:\ A^Ty\geq 0,\ b^Ty<0 &&\overset{(F)}{\nLeftrightarrow} &&\exists x\in\mathbb{R}^n:\ Ax=b,\ x\geq 0\\
&\exists y\in\mathbb{R}^m:\ A^Ty=0,\ y\geq 0,\ b^Ty<0&&\overset{(V)}{\nLeftrightarrow} &&\exists x \in \mathbb{R}^n:\ Ax \leq b
\end{align*}
$(F)\Rightarrow(V)$

\begin{align*}
 &\exists y \in \mathbb{R}^m: &&A^Ty=0,\ y\geq 0, &&b^Ty<0\\
 \Leftrightarrow\ &\exists y \in \mathbb{R}^m: &&
 \begin{pmatrix}
  -A^T\\
  A^T\\
  E
 \end{pmatrix}
 y \geq 0, &&b^Ty<0\\
 \overset{(F)}{\nLeftrightarrow}\ &\exists
 \begin{pmatrix}
  \hat{x}\\
  \check{x}\\
  \tilde{x}
 \end{pmatrix}
 \in \mathbb{R}^{2n+m}: &&
 \begin{pmatrix}
  -A^T\\
  A^T\\
  E
 \end{pmatrix}^T
 \begin{pmatrix}
  \hat{x}\\
  \check{x}\\
  \tilde{x}
 \end{pmatrix}
 = b,
 &&
 \begin{pmatrix}
  \hat{x}\\
  \check{x}\\
  \tilde{x}
 \end{pmatrix}
 \geq 0\\
 \Leftrightarrow\ &\hat{x},\check{x}\in\mathbb{R}^n, \tilde{x}\in\mathbb{R}^m: &&-A\hat{x} + A\check{x} + \tilde{x} = b &&\hat{x},\check{x},\tilde{x}\geq 0\\
 \Leftrightarrow\ &\hat{x},\check{x}\in\mathbb{R}^n: &&-A\hat{x} + A\check{x} \leq b &&\hat{x},\check{x}\geq 0\\
 \Leftrightarrow\ &\hat{x},\check{x}\in\mathbb{R}^n: &&A\left(\check{x} - \hat{x}\right) \leq b &&\hat{x},\check{x}\geq 0\\
 \overset{(*)}{\Leftrightarrow}\ &\exists x \in \mathbb{R}^n: &&Ax = b
\end{align*}
$\overset{(*)}{\Leftarrow}$: For $x\in\mathbb{R}^n$ with $Ax=b$ choose $\check{x},\hat{x}\in\mathbb{R}^n$ with:
\begin{align*}
 &\check{x}_i :=
 \begin{cases}
  x_i, &x_i\geq0\\
  0, &x_i < 0
 \end{cases}
 &&
 \hat{x}_i :=
 \begin{cases}
  0, &x_i\geq0\\
  -x_i, &x_i < 0
 \end{cases}
\end{align*}
Then we have $\check{x}, \hat{x} \geq 0$ as well as $x=\check{x}-\hat{x}$ and therefore $A(\check{x} - \hat{x}) = b$.
$(F)\Leftarrow(V)$

\begin{align*}
 &\exists x\in\mathbb{R}^n: &&Ax=b, &&x\geq 0\\
 \Leftrightarrow\ &\exists x\in\mathbb{R}^n: &&Ax=b, &&-x\leq 0\\
 \Leftrightarrow\ &\exists x\in\mathbb{R}^n: &&
 \begin{pmatrix}
  A\\
  -A\\
  -E
 \end{pmatrix}
 x \leq
 \begin{pmatrix}
  b\\
  -b\\
  0
 \end{pmatrix}\\
 \overset{(L)}{\nLeftrightarrow}\ &\exists
 \begin{pmatrix}
  \hat{y}\\
  \check{y}\\
  \tilde{y}
 \end{pmatrix}
 \in\mathbb{R}^{2m+n}:
 &&
 \begin{pmatrix}
  A\\
  -A\\
  -E
 \end{pmatrix}^T
 \begin{pmatrix}
  \hat{y}\\
  \check{y}\\
  \tilde{y}
 \end{pmatrix}
 =0,\
 \begin{pmatrix}
  \hat{y}\\
  \check{y}\\
  \tilde{y}
 \end{pmatrix}
 \geq 0,
 &&
 \begin{pmatrix}
  b\\
  -b\\
  0
 \end{pmatrix}^T
 \begin{pmatrix}
  \hat{y}\\
  \check{y}\\
  \tilde{y}
 \end{pmatrix}
 < 0\\
 \Leftrightarrow\ &\exists \hat{y},\check{y}\in\mathbb{R}^{m}:
 &&A^T\hat{y} - A^T\check{y} = 0,\ \hat{y},\check{y}\geq 0, &&b^T\hat{y}-b^T\check{y}<0\\
 \Leftrightarrow\ &\exists \hat{y},\check{y}\in\mathbb{R}^{m}:
 &&A^T\left(\hat{y} -\check{y}\right) = 0,\ \hat{y},\check{y}\geq 0, &&b^T\left(\hat{y}-\check{y}\right)<0\\
 \overset{(*)}{\Leftrightarrow}\ &\exists y\in\mathbb{R}^{m}:
 &&A^Ty = 0,\ y\geq 0, &&b^Ty<0
\end{align*}
$\overset{(*)}{\Leftarrow}$: Analogous.
Note

Your variant of Farkas' lemma looked like this:
\begin{align*}
&\exists y'\in\mathbb{R}^m:\ A^Ty'=0,\ y'\geq 0,\ b^Ty'=-1&&\overset{(V')}{\nLeftrightarrow} &&\exists x \in \mathbb{R}^n:\ Ax \leq b
\end{align*}
However, $(V)$ and $(V')$ are equivalent for the following reason:
\begin{align*}
&\exists y\in\mathbb{R}^m: &&A^Ty=0, &&y\geq 0, &&b^Ty<0\\
\overset{(*)}{\Leftrightarrow}\ &\exists y'\in\mathbb{R}^m: &&A^Ty'=0, &&y'\geq 0, &&b^Ty'=-1
\end{align*}
$\overset{(*)}{\Rightarrow}$: Choose $y' := -\left(b^Ty\right)^{-1} y \in \mathbb{R}^m$ for $y \in \mathbb{R}^m$ with $A^Ty=0$, $y\geq 0$ and $b^Ty<0$. Then we have $A^Ty'=0$, $y'\geq 0$ and $b^Ty'=-1$.
