[proofplan]
The inequality is just the defining supremum for the Fenchel conjugate, evaluated at the point $x$ when $f(x)$ is finite. If $x$ is outside the effective domain, the left-hand side is already $+\infty$, so equality cannot occur. For $x \in \operatorname{dom} f$, equality is equivalent to saying that the supremum defining $f^*(y)$ is attained at $x$, and rewriting that condition gives exactly the subgradient inequality.
[/proofplan]
[step:Derive the Fenchel inequality from the defining supremum]
Fix $x,y \in \mathbb{R}^n$. Suppose first that $x \in \operatorname{dom} f$. By definition of $f^*(y)$ as the supremum over all $z \in \mathbb{R}^n$, the value at $z=x$ is bounded above by the supremum:
\begin{align*}
x \cdot y - f(x) \le f^*(y).
\end{align*}
Since $f(x) \in \mathbb{R}$, adding $f(x)$ to both sides gives
\begin{align*}
x \cdot y \le f(x)+f^*(y).
\end{align*}
If $x \notin \operatorname{dom} f$, then $f(x)=+\infty$. Since $f$ is proper, there exists $z_0 \in \operatorname{dom} f$, and hence
\begin{align*}
f^*(y) \ge z_0 \cdot y - f(z_0) > -\infty.
\end{align*}
Therefore $f(x)+f^*(y)=+\infty$, and the inequality
\begin{align*}
f(x)+f^*(y)\ge x\cdot y
\end{align*}
holds.
[guided]
Fix $x,y \in \mathbb{R}^n$. The definition of the conjugate says that $f^*(y)$ is the least upper bound of all numbers of the form $z \cdot y - f(z)$, with $z$ ranging over $\mathbb{R}^n$. Thus, whenever $f(x)$ is finite, the particular choice $z=x$ gives one member of that family, so it must lie below the supremum:
\begin{align*}
x \cdot y - f(x) \le f^*(y).
\end{align*}
Because $x \in \operatorname{dom} f$ means exactly that $f(x)<+\infty$, and because $f$ takes no value $-\infty$, the number $f(x)$ is real. We may therefore add $f(x)$ to both sides and obtain
\begin{align*}
x \cdot y \le f(x)+f^*(y).
\end{align*}
Now consider the case $x \notin \operatorname{dom} f$. By definition of the effective domain, this means $f(x)=+\infty$. We also need to know that adding $f^*(y)$ does not create an indeterminate expression. Since $f$ is proper, there exists $z_0 \in \mathbb{R}^n$ such that $f(z_0)<+\infty$. For this point $z_0$, the quantity $z_0 \cdot y - f(z_0)$ is real, so the supremum defining $f^*(y)$ is at least this real number:
\begin{align*}
f^*(y) \ge z_0 \cdot y - f(z_0) > -\infty.
\end{align*}
Hence
\begin{align*}
f(x)+f^*(y)=+\infty.
\end{align*}
Since $x \cdot y$ is a finite real number, the inequality follows in this case as well.
[/guided]
[/step]
[step:Exclude equality outside the effective domain]
If $x \notin \operatorname{dom} f$, then the previous step gives
\begin{align*}
f(x)+f^*(y)=+\infty.
\end{align*}
The Euclidean [inner product](/page/Inner%20Product) $x \cdot y$ is finite for $x,y \in \mathbb{R}^n$. Therefore equality
\begin{align*}
f(x)+f^*(y)=x\cdot y
\end{align*}
is impossible when $x \notin \operatorname{dom} f$.
[/step]
[step:Translate equality into the subgradient inequality]
Assume now that $x \in \operatorname{dom} f$. Then $f(x)\in \mathbb{R}$, so equality in the Fenchel inequality is equivalent to
\begin{align*}
f^*(y)=x\cdot y-f(x).
\end{align*}
By definition of the supremum, this equality holds if and only if
\begin{align*}
z\cdot y-f(z)\le x\cdot y-f(x)
\end{align*}
for every $z \in \mathbb{R}^n$. Rearranging this inequality gives
\begin{align*}
f(z)\ge f(x)+y\cdot (z-x)
\end{align*}
for every $z \in \mathbb{R}^n$. By the definition of $\partial f(x)$, this condition is exactly $y \in \partial f(x)$.
Thus, for $x \in \operatorname{dom} f$, equality holds if and only if $y \in \partial f(x)$. Together with the exclusion of equality outside $\operatorname{dom} f$, this proves the stated equality characterization.
[/step]
