[proofplan] The proof has two parts. First we show that the two alternatives cannot hold simultaneously, using the defining property of the adjoint and the dual cone. Then we assume the primal system has no solution, so $b\notin A(K)$, and separate the point $b$ from the closed convex cone $A(K)$. The conic structure upgrades the separating inequality to non-negativity on all of $A(K)$, which is exactly the statement that $A^*y$ lies in $K^*$. [/proofplan] [step:Show that the two alternatives cannot hold simultaneously] Assume that there exist $x\in K$ and $y\in F$ such that $Ax=b$, $A^*y\in K^*$, and $(b,y)_F<0$. Since $A^*y\in K^*$ and $x\in K$, the definition of $K^*$ gives \begin{align*} (x,A^*y)_E \geq 0. \end{align*} By the defining property of the adjoint $A^*:F\to E$, \begin{align*} (b,y)_F = (Ax,y)_F = (x,A^*y)_E \geq 0. \end{align*} This contradicts $(b,y)_F<0$. Hence at most one of the two alternatives can hold. [guided] Suppose, toward a contradiction, that both alternatives hold. Then there is a vector $x\in K$ solving the primal equation $Ax=b$, and there is a vector $y\in F$ satisfying $A^*y\in K^*$ and $(b,y)_F<0$. The condition $A^*y\in K^*$ means, by definition of the dual cone, that every vector in $K$ has non-negative [inner product](/page/Inner%20Product) with $A^*y$. Since our primal vector $x$ belongs to $K$, we get \begin{align*} (x,A^*y)_E \geq 0. \end{align*} Now use the adjoint relation. The adjoint $A^*:F\to E$ is defined by the identity \begin{align*} (Au,v)_F = (u,A^*v)_E \end{align*} for every $u\in E$ and every $v\in F$. Applying this with $u=x$ and $v=y$ gives \begin{align*} (Ax,y)_F = (x,A^*y)_E. \end{align*} Because $Ax=b$, this becomes \begin{align*} (b,y)_F = (x,A^*y)_E \geq 0. \end{align*} This contradicts the strict inequality $(b,y)_F<0$ from the second alternative. Therefore both alternatives cannot be true at the same time. [/guided] [/step] [step:Separate $b$ from the closed convex cone $A(K)$] Assume that the first alternative fails. Define the subset $C\subset F$ by \begin{align*} C := A(K). \end{align*} Since $K$ is a convex cone and $A:E\to F$ is linear, $C$ is a convex cone in $F$. By hypothesis, $C$ is closed. The failure of the first alternative means exactly that $b\notin C$. By the strong separation theorem for a point and a closed convex set in a finite-dimensional [inner product space](/page/Inner%20Product%20Space), applied to the closed convex set $C\subset F$ and the point $b\notin C$, there exist $y\in F$ and $\alpha\in\mathbb{R}$ such that \begin{align*} (z,y)_F \geq \alpha > (b,y)_F \end{align*} for every $z\in C$. Here we are citing a result not yet in the wiki: Strong Separation Theorem for a point and a closed convex set in a finite-dimensional inner product space. [/step] [step:Use the conic structure to normalize the separating inequality] Since $K$ is a cone, $0_E\in K$, and hence $0_F=A0_E\in C$. Substituting $z=0_F$ into the separating inequality gives \begin{align*} 0=(0_F,y)_F \geq \alpha. \end{align*} Together with $\alpha>(b,y)_F$, this implies \begin{align*} (b,y)_F<0. \end{align*} We next prove that $(z,y)_F\geq 0$ for every $z\in C$. Fix $z\in C$. Since $C$ is a cone, $tz\in C$ for every $t>0$. Therefore the separating inequality gives \begin{align*} t(z,y)_F = (tz,y)_F \geq \alpha \end{align*} for every $t>0$. If $(z,y)_F<0$, then choosing $t>\alpha/(z,y)_F$ when $\alpha<0$, and choosing any sufficiently large $t>0$ when $\alpha=0$, would give $t(z,y)_F<\alpha$, contradicting the displayed inequality. Hence \begin{align*} (z,y)_F\geq 0 \end{align*} for every $z\in C$. [/step] [step:Translate non-negativity on $A(K)$ into membership in the dual cone] Let $x\in K$. Since $C=A(K)$, the vector $Ax$ belongs to $C$. From the preceding step, \begin{align*} (Ax,y)_F\geq 0. \end{align*} Using the adjoint identity again gives \begin{align*} (x,A^*y)_E\geq 0. \end{align*} Since this holds for every $x\in K$, the definition of $K^*$ implies \begin{align*} A^*y\in K^*. \end{align*} Together with $(b,y)_F<0$, this proves the second alternative. Thus, if the first alternative fails, the second alternative holds. Combined with mutual exclusion, exactly one of the two alternatives holds. [/step]