I'm trying to understand a proof of a corollary to the Farkas lemma in some lecture notes. For completeness sake I'll first state the Farkas lemma and then the corollary + proof, as stated in these lecture notes.
(Farkas lemma) Given $A \in \mathbb{R}^{m\times n}$, $b \in \mathbb{R}^m$. Then $Ax = b$ has a nonnegative solution if and only if there is no vector $y$ satisfying $y^{T}A \geq 0$ and $y^{T}b < 0$.
(Corollary) The system $Ax \leq b$ has a solution if and only if there is no vector $y$ satisfying $y \geq 0$, $y^T A = 0$ and $y^T b < 0$.
(Proof of corollary) Let $A'$ be the matrix $A' :=[A\quad -A\quad I]$, where $I$ is the identity matrix. Then $Ax \leq b$ has a solution $x$ iff the system $A'x' = b$ has a nonnegative solution $x'$. Applying the Farkas lemma to the latter system gives the corollary.
Here, I parse $[A\quad -A\quad I]$ as being the matrix created by appending $A$, $-A$ and $I$. What I don't understand is how I should calculate $A'x'$ and of what dimension $x'$ should be. It seems to me that $A'$ has dimensions $m \times 3n$ so that $x'$ has dimensions $3n \times 1$, but this isn't right since $b$ is of dimension $m \times 1$. I'm guessing I'm missing something really obvious but alas I can't see it.
Best Answer
Note that the Farkas lemma says something about non-negative solutions of $Ax=b$ whereas in the corollary, the solution $x$ of $Ax \leq b$ may have negative entries. To express an arbitrary vector $x$ in terms of non-negative vectors write $x = x^+-x^-$ with $x^+,x^- \geq 0$. Then translate the statement "$\exists x: Ax \leq b$" into an equivalent statement of the form "$\exists x'\geq 0: A'x'=b'$" to apply the Farkas lemma: \begin{align*} &\exists x : Ax \leq b\\ \Leftrightarrow & \exists x^+,x^- \geq 0: Ax^+-Ax^- \leq b\\ \Leftrightarrow & \exists x^+,x^-,y \geq 0 : Ax^+-Ax^- + y = b\\ \Leftrightarrow & \exists \left( \begin{matrix}x^+\\x^-\\y \end{matrix}\right) \geq 0: \left(\begin{matrix}A & -A & I\end{matrix}\right) \left( \begin{matrix}x^+\\x^-\\y \end{matrix}\right) = b \end{align*}