Bauer maximum principle

For each $y\in K$ put $L_y=\{x\in K:f(x)\ge f(y)\}$, which is closed by [F1]. Any finite subfamily has nonempty intersection: choose from its finite list an index at which the finitely many real values $f(y)$ are largest, and the corresponding $y$ belongs to every listed $L_y$; the empty finite intersection is $K\mathrm{\ne }\mathrm{\varnothing }$. Thus [F4] supplies $z\in {\bigcap }_{y\in K}{L}_y$, so $m:=f(z)$ is the maximum of $f$ on $K$.

The maximizer set $M=\{x\in K:f(x)=m\}=\{x\in K:f(x)\ge m\}$ is nonempty and closed by [F1]. Call a subset $S\subseteq K$ $K$-extremal when $(1-t)x+ty\in S$, for $x,y\in K$ and $0<t<1$, implies $x,y\in S$.

The set $M$ is $K$-extremal. Indeed, if $w=(1-t)x+ty\in M$ with $0<t<1$, convexity and maximality give $m=f(w)\le (1-t)f(x)+tf(y)\le m$; positivity of both coefficients and $f(x),f(y)\le m$ force $f(x)=f(y)=m$.

Let $\mathcal{P}$ be the nonempty closed $K$-extremal subsets of $M$, ordered by reverse inclusion. It is nonempty because $M\in \mathcal{P}$.

An empty chain has upper bound $M$. For a nonempty chain $\mathcal{C}\subseteq \mathcal{P}$, every finite intersection is its inclusion-smallest listed member and hence nonempty. Because every member is closed in compact $K$, [F4] makes $H={\bigcap }_{S\in \mathcal{C}}S$ nonempty and closed. If a strict convex combination lies in $H$, extremality in every $S$ puts both endpoints in every $S$, so $H$ is $K$-extremal. Thus $H\in \mathcal{P}$ and is an upper bound in the reverse-inclusion order.

By [F5], with AC declared in [F6], $\mathcal{P}$ has a maximal element $M_0$, equivalently an inclusion-minimal nonempty closed $K$-extremal subset of $M$.

Suppose $p,q\in M_0$ are distinct. By [F7], AC supplies HB, so [F3] gives a continuous $f_0\in X^{\mathrm{\prime }}$ for which $u=\mathrm{Re}{f}_0$ has $u(p)\mathrm{\ne }u(q)$.

Apply the finite-intersection argument of step 1.1 to the continuous real function $u{\mathrm{\mid }}_{M_0}$: its superlevels in $M_0$ are closed in $K$ because $M_0$ is closed and $u$ is continuous, and the family indexed by $y\in M_0$ has the finite-intersection property. Hence $u$ has a maximum $c$ on $M_0$, and $N=\{x\in M_0:u(x)=c\}$ is nonempty and closed in $K$. It is proper because $u(p)\mathrm{\ne }u(q)$.

The set $N$ is $K$-extremal: if $(1-t)x+ty\in N$ with $x,y\in K$ and $0<t<1$, extremality of $M_0$ first gives $x,y\in M_0$; linearity yields $c=(1-t)u(x)+tu(y)$ while $u(x),u(y)\le c$, so positivity forces $u(x)=u(y)=c$ and $x,y\in N$. Thus $N\in \mathcal{P}$ is a proper subset of $M_0$, contradicting minimality.

Therefore $M_0=\{e\}$ for some $e\in M$. Since this singleton is $K$-extremal, it satisfies the singleton face condition in [F2], so $e$ is extreme in $K$; and $e\in M$ gives $f(e)=m={\max }_{K}f$.

The preceding maximum and extremality argument constructs a nonempty closed extremal maximizer set, the Zorn argument produces a minimal one, and the separating-functional argument proves it is a singleton consisting of the required extreme maximizer.