Theorem: Convex Envelope of Lower Semicontinuous Proper Convex Function is Equal to Original Function

Let $\struct {X, \PP}$ be a Hausdorff locally convex space over $\R$.
Let $f : X \to \overline \R$ be a lower semicontinuous proper convex function.
Let $\check f$ be the convex envelope of $f$.
Then $\check f = f$.

Proof:
From Convex Envelope is Convex Minorant of Function, we have $\check f \le f$. 
Let $\Dom f$ be the effective domain of $f$.
Let $\map {\operatorname {epi} } f$ be the epigraph of $f$.
Let $x \in X$.
Then $-\infty < \map f x$.
We argue that it is sufficient to show that for all $\alpha \in \R$ with $\alpha < \map f x$, there exists a continuous affine functional $g \le f$ such that $\map g x \ge \alpha$. 
If this is the case, then we have $\map {\check f} x \ge \alpha$ for each $\alpha \in \R$ with $\alpha < \map f x$.
Hence by taking $\alpha \to \map f x$, we obtain $\map {\check f} x \ge \map f x$.
Since $\map {\check f} x \le \map f x$, we will then obtain $\map {\check f} x = \map f x$.
Now let $\alpha \in \R$.
If $x \in \Dom f$, then there exists a continuous affine $g < f$ such that $\map g x = \alpha$.
Now consider the case $x \not \in \Dom f$, so that $\map f x = \infty$.
We can take $\alpha > 0$.
Since $\alpha < \map f x$, we do not have $\map f x \le \alpha$ and hence $\tuple {x, \alpha} \not \in \map {\operatorname {epi} } f$. 
Following the proof of Existence of Continuous Affine Minorant of Lower Semicontinuous Proper Convex Function with Prescribed Point Evaluation, there exists a continuous linear functional $\phi : X \to \R$, $\lambda \in \R$ and $\epsilon > 0$ such that:
:$\map \phi x + \lambda \alpha + \epsilon < \map \phi y + \lambda \beta$ for each $\tuple {y, \beta} \in \map {\operatorname {epi} } f$.
If $\lambda > 0$, then the proof proceeds as in Existence of Continuous Affine Minorant of Lower Semicontinuous Proper Convex Function with Prescribed Point Evaluation.
Suppose that $\lambda = 0$.
Then:
:$\map \phi x + \epsilon < \map \phi y$ for each $\tuple {y, \beta} \in \map {\operatorname {epi} } f$.
Define $h : X \to \R$ by:
:$\ds \map h z = \map \phi {x - z} + \frac \epsilon 2$ 
We then have:
:$\ds \map h x = \frac \epsilon 2 > 0$
For $z \in \Dom f$, we have that $\tuple {z, \map f z} \in \map {\operatorname {epi} } f$.
Hence:
:$\map \phi {x - z} + \epsilon < 0$
so that:
:$\map \phi {x - z} < -\epsilon$
We therefore have:
:$\ds \map h z < -\frac \epsilon 2 < 0$
Now fix $\overline y \in \Dom f$.
From Existence of Continuous Affine Minorant of Lower Semicontinuous Proper Convex Function with Prescribed Point Evaluation, there exists a continuous affine functional $\overline g : X \to \R$ such that $\overline g < f$ and:
:$\map {\overline g} {\overline y} = \map f {\overline y} - 1 < \map f {\overline y}$ 
Let:
:$\ds \gamma = \frac 1 {\map h x} \paren {\size {\map {\overline g} x} + \alpha}$
Since $\map h x > 0$, we have $\gamma > 0$. 
Let $g : X \to \R$ be such that:
:$\map g z = \gamma \map h z + \map {\overline g} z$ for each $z \in X$.
For $z \in \Dom f$, we have $\map h z < 0$.
By construction of $\overline g$, we have $\map {\overline g} z < \map f z$.
Hence we have $\map g z < \map f z$ in the case $z \in \Dom f$.
For $z \not \in \Dom f$, we have $\map g z < \infty$, while $\map f z = \infty$.
Hence we have $\map g z < \map f z$ in the case $z \not \in \Dom f$.
Hence we have $\map g z < \map f z$ for all $z \in X$.
Further:
:$\ds \map g x = \size {\map {\overline g} x} + \alpha + \map {\overline g} x \ge \alpha \ge \alpha$
Hence $g$ is a continuous affine functional with $g \le f$ and $\map g x \ge \alpha$. 
{{qed}}