$\newcommand{\plcypmf}[2]{\pi(#1\,|\,#2)}$
$\newcommand{\condpmf}[2]{p(#1\,|\,#2)}$
$\newcommand{\condpmfsym}[3]{#1(#2\,|\,#3)}$
$\newcommand{\cpwrt}[3]{P_{#1}\{#2\:|\, #3\}}$
$\newcommand{\Ecwrt}[3]{E_{#1}[#2\:|\, #3]}$
$\newcommand{\argmax}[1]{\text{arg max}_{#1}\,}$
$\newcommand{\cases}[1]{\begin{cases}#1\end{cases}}$
$\newcommand{\mcalA}{\mathcal{A}}$
$\newcommand{\mcalR}{\mathcal{R}}$
$\newcommand{\mcalS}{\mathcal{S}}$
$\newcommand{\qd}{\quad}$
$\newcommand{\wR}{\mathbb{R}}$
$\newcommand{\Bop}{\Big(}$
$\newcommand{\Bcp}{\Big)}$
$\newcommand{\Prn}[1]{\Bop #1\Bcp}$
$\newcommand{\align}[1]{\begin{align*}#1\end{align*}}$
$\newcommand{\wes}{\blacksquare}$

We assume that the Markov Property holds:

$$\align{
&\condpmf{g_{t+1}}{s',a,s}=\condpmf{g_{t+1}}{s'} \\\\
&\condpmf{g_{t+1}}{s',r,a,s}=\condpmf{g_{t+1}}{s'}\tag{MDP.0} \\\\
&\condpmf{r_{t+2}}{s',a,s}=\condpmf{r_{t+2}}{s'} \\\\
}$$

__Proposition MDP.5__ Let $T$ be the time variable and let $t$ be a particular time. Let $s_0\in\mcalS$, let $a_0\in\mcalA(s)$, and let $\pi$ be any policy on $\mcalS$. Define the family of policies $\phi_T$ on $\mcalS$ by

$$
\cpwrt{\phi_T}{A_T=a}{S_T=s}=\condpmfsym{\phi_T}{a}{s}\equiv\cases{\condpmfsym{\pi}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_0\\0&\text{else}}
$$

Then

$$
q_{\phi_{t}}(s_0,a_0) = q_{\pi}(s_0,a_0) \\
$$

__Proof__ If $g_{t+1}$ is a possible outcome of $G_{t+1}$, then $\condpmf{g_{t+1}}{s',\phi_t}=\condpmf{g_{t+1}}{s',\pi}$ since $\phi_t=\pi$ for $T=t+1,t+2,\dots$. Also note that $\condpmf{s'}{s_0,a_0,\phi_t}=\condpmf{s'}{s_0,a_0,\pi}$. That is, if we know the state and action in the current time step, then the policy is irrelevant to determining the next state. Hence

$$\align{
q_{\phi_t}(s_0,a_0) &= \Ecwrt{\phi}{G_t}{S_t=s_0,A_t=a_0} \\
 &= \Ecwrt{\phi_t}{R_{t+1}+\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\Ecwrt{\phi_t}{\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\condpmf{g_{t+1}}{s_0,a_0,\phi_t} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',s_0,a_0,\phi_t}\cdot\condpmf{s'}{s_0,a_0,\phi_t} \\
 &= \Ecwrt{\phi_t}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',\phi_t}\cdot\condpmf{s'}{s_0,a_0,\phi_t}\tag{by MDP.0} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',\pi}\cdot\condpmf{s'}{s_0,a_0,\pi} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\sum_{s'}\condpmf{g_{t+1}}{s',s_0,a_0,\pi}\cdot\condpmf{s'}{s_0,a_0,\pi} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\sum_{g_{t+1}}\gamma g_{t+1}\cdot\condpmf{g_{t+1}}{s_0,a_0,\pi} \\
 &= \Ecwrt{\pi}{R_{t+1}}{S_t=s_0,A_t=a_0}+\Ecwrt{\pi}{\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\
 &= \Ecwrt{\pi}{R_{t+1}+\gamma G_{t+1}}{S_t=s_0,A_t=a_0} \\
 &= \Ecwrt{\pi}{G_t}{S_t=s_0,A_t=a_0} \\
 &= q_{\pi}(s_0,a_0) \\
}$$

$\wes$

Define $v_{*}:\mcalS\mapsto\wR$ by

$$
v_{*}(s)\equiv\max_{\pi}v_{\pi}(s)\qd\text{for all }s\in\mcalS
$$

Define $q_{*}:\mcalS\times\mcalA\mapsto\wR$ by

$$
q_{*}(s,a)\equiv\max_{\pi}q_{\pi}(s,a)\qd\text{for all }s\in\mcalS,a\in\mcalA(s)
$$

__Proposition MDP.6__ Let $s_0\in\mcalS$ and define $a_{*}$ by

$$
a_{*}\in\argmax{a\in\mcalA(s_0)}\Prn{\argmax{\pi}q_{\pi}(s_0,a)}=\argmax{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$

And define the policy $\pi_{**}$ by

$$
\pi_{**}\in\argmax{\pi}q_{\pi}(s_0,a_{*})
$$

And define the family of policies $\phi_T$ by

$$
\cpwrt{\phi_T}{A_T=a}{S_T=s}=\condpmfsym{\phi_T}{a}{s}\equiv\cases{\condpmfsym{\pi_{**}}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_{*}\\0&\text{else}}
$$

Then $\phi_t$ is an optimal policy:

$$
\phi_t\in\argmax{\pi}v_{\pi}(s_0)
$$

and

$$
v_{\phi_t}(s_0)=v_{*}(s_0)=\max_{\pi}v_{\pi}(s_0)
$$

__Proof__ For any policy $\pi$, we have

$$\align{
v_{\pi}(s_0) &= \sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0}\cdot q_{\pi}(s_0,a) \\
 &\leq \sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0}\cdot q_{*}(s_0,a) \\
 &\leq \sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0}\cdot q_{*}(s_0,a_{*}) \\
 &= q_{*}(s_0,a_{*})\cdot\sum_{a\in\mcalA(s_0)}\condpmfsym{\pi}{a}{s_0} \\
 &= q_{*}(s_0,a_{*}) \\
 &= q_{\pi_{**}}(s_0,a_{*}) \\
 &= q_{\phi_t}(s_0,a_{*})\tag{by MDP.5} \\
 &= \sum_{a\in\mcalA(s_0)}\condpmfsym{\phi_t}{a}{s_0}\cdot q_{\phi_t}(s_0,a) \\
 &= v_{\phi_t}(s_0)
}$$

$\wes$

__Proposition MDP.7__ For all $s\in\mcalS$, we have

$$
v_{*}(s) = \max_{a\in\mcalA(s)}q_{*}(s,a)
$$

__Proof__ Let $s_0\in\mcalS$ and define $a_{*}\in\argmax{a\in\mcalA(s_0)}q_{*}(s_0,a)$. Then for any policy $\pi$, we have

$$\align{
v_{\pi}(s_0) &= \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{\pi}(s_0,a) \\
 &\leq \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{*}(s_0,a) \\
 &\leq \sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0}\cdot q_{*}(s_0,a_{*}) \\
 &= q_{*}(s_0,a_{*})\cdot\sum_{a\in\mcalA({s_0})}\plcypmf{a}{s_0} \\
 &= q_{*}(s_0,a_{*}) \\
 &= \max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
}$$

Since this is true for all policies $\pi$, then it must be that

$$
v_{*}(s_0)=\max_{\pi}v_{\pi}(s_0)\leq\max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$

Suppose, by way of contradiction, that we have strict inequality:

$$
v_{*}(s_0)\lt\max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
\tag{MDP.7.1}
$$

Define the policy $\pi_{**}$ by

$$
\pi_{**}\in\argmax{\pi}q_{\pi}(s_0,a_{*})
$$

Then

$$
q_{\pi_{**}}(s_0,a_{*}) = \max_{\pi}q_{\pi}(s_0,a_{*}) = q_{*}(s_0,a_{*}) = \max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$

And MDP.6 gives the first equality:

$$
v_{\pi_{**}}(s_0)=\max_{\pi}v_{\pi}(s_0)=v_{*}(s_0)\lt\max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$

Also define the family of policies $\phi_T$ by

$$
\cpwrt{\phi_T}{A_T=a}{S_T=s}=\condpmfsym{\phi_T}{a}{s}\equiv\cases{\condpmfsym{\pi_{**}}{a}{s}&\text{if }T\neq t\text{ or }s\neq s_0\\1&\text{else if }a=a_{*}\\0&\text{else}}
$$

Then MDP.5 gives the third equality:

$$\align{
v_{\phi_t}(s_0) = \sum_{a\in\mcalA(s_0)}\condpmfsym{\phi_t}{a}{s_0}q_{\phi_t}(s_0,a) = q_{\phi_t}(s_0,a_{*})= q_{\pi_{**}}(s_0,a_{*}) = \max_{a\in\mcalA(s_0)}q_{*}(s_0,a) \gt v_{*}(s_0)
}$$

This contradicts the definition of $v_{*}(s_0)\equiv\max_{\pi}v_{\pi}(s_0)$. Hence assumption MDP.7.1 is false and we have

$$
v_{*}(s_0)=\max_{a\in\mcalA(s_0)}q_{*}(s_0,a)
$$

Since $s_0\in\mcalS$ was chosen arbitrarily, then this equality holds for all $s\in\mcalS$.

$\wes$