[proofplan]
We build the GNS [Hilbert space](/page/Hilbert%20Space) from the positive semidefinite form induced by $\phi$, using the Hilbert-space convention that the [inner product](/page/Inner%20Product) is linear in the first variable. With that convention we let $M$ act by left multiplication, which gives a complex-linear $*$-representation and produces the required vector-state formula. The cyclicity and unitality are immediate from the construction, while normality is proved by testing increasing bounded positive nets against the dense cyclic subspace and then extending the resulting convergence to all vectors by approximation.
[/proofplan]
[step:Construct the Hilbert space from the positive form induced by $\phi$]
Define a sesquilinear form
\begin{align*}
q:M\times M\to\mathbb C
\end{align*}
by
\begin{align*}
q(a,b)=\phi(b^*a)
\end{align*}
for $a,b\in M$. Since $\phi$ is positive, $q(a,a)=\phi(a^*a)\ge 0$ for every $a\in M$.
Let
\begin{align*}
N_\phi=\{a\in M:\phi(a^*a)=0\}.
\end{align*}
Since $M$ is a unital $*$-algebra and $\phi$ is a positive complex-linear functional on $M$, the [Cauchy-Schwarz inequality for positive linear functionals](/theorems/8558) applies and gives
\begin{align*}
|\phi(b^*a)|^2\le \phi(a^*a)\phi(b^*b)
\end{align*}
for all $a,b\in M$. Hence $N_\phi$ is exactly the null space of $q$. Hence $q$ descends to an inner product on the quotient [vector space](/page/Vector%20Space) $M/N_\phi$. For $a\in M$, write $[a]$ for its class in $M/N_\phi$, and define
\begin{align*}
([a],[b])_0=\phi(b^*a).
\end{align*}
Let $H_\phi$ be the Hilbert space completion of $M/N_\phi$ with respect to the norm induced by $(\cdot,\cdot)_0$.
[guided]
The inner product convention matters here. Androma uses Hilbert-space inner products linear in the first variable, and the desired formula is
\begin{align*}
\phi(a)=(\pi_\phi(a)\Omega_\phi,\Omega_\phi)_{H_\phi}.
\end{align*}
For that reason we define the preliminary form by
\begin{align*}
q(a,b)=\phi(b^*a).
\end{align*}
This form is linear in $a$ and conjugate-linear in $b$, matching the convention, and it is the choice for which left multiplication gives the desired vector-state identity.
The form is positive semidefinite because $\phi$ is a positive functional:
\begin{align*}
q(a,a)=\phi(a^*a)\ge 0.
\end{align*}
Its null space is
\begin{align*}
N_\phi=\{a\in M:\phi(a^*a)=0\}.
\end{align*}
To quotient by this null space, we need the form to vanish against every vector whenever it vanishes on the diagonal. Since $M$ is a unital $*$-algebra and $\phi$ is a positive complex-linear functional on $M$, the [Cauchy-Schwarz inequality](/theorems/432) for positive linear functionals applies:
\begin{align*}
|\phi(b^*a)|^2\le \phi(a^*a)\phi(b^*b)
\end{align*}
for all $a,b\in M$. Thus if $a\in N_\phi$, then $\phi(b^*a)=0$ for every $b\in M$. Therefore the formula
\begin{align*}
([a],[b])_0=\phi(b^*a)
\end{align*}
is independent of the representatives $a$ and $b$. After quotienting by $N_\phi$, the form is positive definite, so it is an inner product on $M/N_\phi$. Completing this pre-Hilbert space gives the Hilbert space $H_\phi$.
[/guided]
[/step]
[step:Define the representation by left multiplication]
For $x\in M$, let $\|x\|_{\mathrm{op}}$ denote the operator norm inherited from $\mathcal{L}(K)$. Define a [linear map](/page/Linear%20Map) on $M/N_\phi$ by
\begin{align*}
\pi_0(x):M/N_\phi\to M/N_\phi,\qquad [a]\mapsto [xa].
\end{align*}
This is well-defined: if $a\in N_\phi$, then
\begin{align*}
\phi((xa)^*(xa))=\phi(a^*x^*xa)\le \|x^*x\|_{\mathrm{op}}\phi(a^*a)=\|x\|_{\mathrm{op}}^2\phi(a^*a)=0,
\end{align*}
because $0\le x^*x\le \|x\|_{\mathrm{op}}^2 1$ and positivity of $\phi$ preserves the operator order. Hence $xa\in N_\phi$.
For $a\in M$,
\begin{align*}
\|\pi_0(x)[a]\|_0^2=\phi(a^*x^*xa)\le \|x\|_{\mathrm{op}}^2\phi(a^*a)=\|x\|_{\mathrm{op}}^2\|[a]\|_0^2.
\end{align*}
Thus $\pi_0(x)$ is bounded with
\begin{align*}
\|\pi_0(x)\|_{\mathcal{L}(M/N_\phi)}\le \|x\|_{\mathrm{op}},
\end{align*}
and it extends uniquely to a bounded operator
\begin{align*}
\pi_\phi(x)\in\mathcal{L}(H_\phi).
\end{align*}
[/step]
[step:Verify that the action is a unital $*$-representation]
For $x,y,a\in M$,
\begin{align*}
\pi_\phi(x)\pi_\phi(y)[a]=\pi_\phi(x)[ya]=[xya]=\pi_\phi(xy)[a].
\end{align*}
Also
\begin{align*}
\pi_\phi(1)[a]=[a],
\end{align*}
so $\pi_\phi(1)=I_{H_\phi}$.
To verify the adjoint relation, let $a,b\in M$. Then
\begin{align*}
(\pi_\phi(x)[a],[b])_0=\phi(b^*xa).
\end{align*}
Since $(x^*b)^*=b^*x$, this equals
\begin{align*}
\phi((x^*b)^*a)=([a],\pi_\phi(x^*)[b])_0.
\end{align*}
Because the classes $[a]$ and $[b]$ are dense in $H_\phi$, it follows that
\begin{align*}
\pi_\phi(x)^*=\pi_\phi(x^*).
\end{align*}
Therefore $\pi_\phi:M\to\mathcal{L}(H_\phi)$ is a unital $*$-representation.
[/step]
[step:Identify the cyclic vector and compute the vector state]
Define
\begin{align*}
\Omega_\phi=[1]\in H_\phi.
\end{align*}
For every $a\in M$,
\begin{align*}
\pi_\phi(a)\Omega_\phi=[a].
\end{align*}
Since the set $\{[a]:a\in M\}$ is dense in $H_\phi$ by construction, $\Omega_\phi$ is cyclic for $\pi_\phi(M)$.
For $a\in M$,
\begin{align*}
(\pi_\phi(a)\Omega_\phi,\Omega_\phi)_{H_\phi}=([a],[1])_0=\phi(1^*a)=\phi(a).
\end{align*}
Thus the state $\phi$ is represented by the vector $\Omega_\phi$.
[/step]
[step:Prove normality by testing increasing positive nets on cyclic vectors]
Let $(x_i)_{i\in I}$ be an increasing bounded net of positive elements of $M$, and let $x=\sup_{i\in I}x_i$ in $M$. By the definition of normality in the statement, it suffices to show that
\begin{align*}
\pi_\phi(x_i)\to\pi_\phi(x)
\end{align*}
strongly for every such net.
Fix $b\in M$. Since $(x_i)_{i\in I}$ is an increasing bounded net of [self-adjoint operators](/page/Self-Adjoint%20Operators) with supremum $x$ in $M$, the [bounded monotone convergence theorem for self-adjoint operators](/theorems/9262) gives $x_i\to x$ strongly on $K$. Therefore $x_i b\xi\to xb\xi$ for every $\xi\in K$, and hence $b^*x_i b\to b^*xb$ strongly on $K$. The net $(b^*x_i b)_{i\in I}$ is increasing and bounded in $M_+$. By [citetheorem:9263] applied to this increasing bounded net and the positive normal functional $\phi$,
\begin{align*}
\phi(b^*x_i b)\uparrow \phi(b^*xb).
\end{align*}
Therefore
\begin{align*}
\phi(b^*(x-x_i)b)\to 0.
\end{align*}
Now
\begin{align*}
\|(\pi_\phi(x)-\pi_\phi(x_i))[b]\|_{H_\phi}^2
=\|[(x-x_i)b]\|_{H_\phi}^2
=\phi(b^*(x-x_i)^2b).
\end{align*}
Because $0\le x-x_i\le x$ and the net is bounded, there is a constant $C=\|x\|_{\mathrm{op}}$ such that
\begin{align*}
0\le (x-x_i)^2\le C(x-x_i).
\end{align*}
Hence
\begin{align*}
0\le \phi(b^*(x-x_i)^2b)\le C\phi(b^*(x-x_i)b)\to 0.
\end{align*}
Thus
\begin{align*}
\pi_\phi(x_i)[b]\to\pi_\phi(x)[b]
\end{align*}
in $H_\phi$ for every $b\in M$.
[guided]
The goal is to prove normality of the representation in the sense stated in the theorem: an increasing bounded net of positive elements should be sent to its strong operator limit. So let $(x_i)_{i\in I}$ be an increasing bounded net in $M_+$, and let
\begin{align*}
x=\sup_{i\in I}x_i.
\end{align*}
First we test convergence on a dense set of vectors, namely the cyclic vectors $[b]$ with $b\in M$. Fix such a $b$. Since $(x_i)_{i\in I}$ is an increasing bounded net of self-adjoint operators with supremum $x$ in the von Neumann algebra $M\subseteq\mathcal{L}(K)$, the bounded [monotone convergence theorem](/theorems/509) for self-adjoint operators gives strong convergence $x_i\to x$ on $K$. Multiplication by the fixed bounded operators $b$ and $b^*$ preserves strong convergence on bounded nets: for every $\xi\in K$, $x_i b\xi\to xb\xi$, and then $b^*x_i b\xi\to b^*xb\xi$. Hence
\begin{align*}
b^*x_i b\to b^*xb
\end{align*}
strongly on $K$. Also, because multiplication on the left by $b^*$ and on the right by $b$ preserves positivity, the net $(b^*x_i b)_{i\in I}$ is increasing and bounded in $M_+$.
Now we use normality of the state $\phi$ in its monotone convergence form. The theorem [citetheorem:9263] says that a positive normal functional preserves bounded increasing strong limits of self-adjoint operators in a von Neumann algebra. Applying it to the increasing bounded net $(b^*x_i b)_{i\in I}$ gives
\begin{align*}
\phi(b^*x_i b)\uparrow \phi(b^*xb).
\end{align*}
Subtracting gives
\begin{align*}
\phi(b^*(x-x_i)b)\to 0.
\end{align*}
We must convert this scalar convergence into norm convergence in $H_\phi$. By the definition of the representation,
\begin{align*}
(\pi_\phi(x)-\pi_\phi(x_i))[b]=[(x-x_i)b].
\end{align*}
Therefore
\begin{align*}
\|(\pi_\phi(x)-\pi_\phi(x_i))[b]\|_{H_\phi}^2
=\phi(b^*(x-x_i)^2b).
\end{align*}
Let $C=\|x\|_{\mathrm{op}}$. Since $0\le x-x_i\le x$, we have $0\le x-x_i\le C1$, and functional calculus for the positive operator $x-x_i$ gives
\begin{align*}
0\le (x-x_i)^2\le C(x-x_i).
\end{align*}
Multiplying by $b^*$ and $b$ and applying positivity of $\phi$ yields
\begin{align*}
0\le \phi(b^*(x-x_i)^2b)\le C\phi(b^*(x-x_i)b).
\end{align*}
The right-hand side tends to $0$, so
\begin{align*}
\pi_\phi(x_i)[b]\to\pi_\phi(x)[b]
\end{align*}
in $H_\phi$ for every cyclic vector $[b]$.
[/guided]
[/step]
[step:Extend strong convergence from cyclic vectors to all vectors]
The operators $\pi_\phi(x_i)$ and $\pi_\phi(x)$ are uniformly bounded by $\|x\|_{\mathrm{op}}$. Let $\eta\in H_\phi$ and let $\varepsilon>0$. Choose $b\in M$ such that
\begin{align*}
\|\eta-[b]\|_{H_\phi}<\frac{\varepsilon}{3\|x\|_{\mathrm{op}}+3}
\end{align*}
using density of $\{[b]:b\in M\}$ in $H_\phi$. From the previous step, choose $i_0\in I$ such that for all $i\ge i_0$,
\begin{align*}
\|(\pi_\phi(x)-\pi_\phi(x_i))[b]\|_{H_\phi}<\frac{\varepsilon}{3}.
\end{align*}
For such $i$,
\begin{align*}
\|(\pi_\phi(x)-\pi_\phi(x_i))\eta\|_{H_\phi}
\le \|\pi_\phi(x)(\eta-[b])\|_{H_\phi}+\|(\pi_\phi(x)-\pi_\phi(x_i))[b]\|_{H_\phi}+\|\pi_\phi(x_i)([b]-\eta)\|_{H_\phi}.
\end{align*}
Using
\begin{align*}
\|\pi_\phi(x)\|_{\mathcal{L}(H_\phi)}\le \|x\|_{\mathrm{op}}
\end{align*}
and
\begin{align*}
\|\pi_\phi(x_i)\|_{\mathcal{L}(H_\phi)}\le \|x_i\|_{\mathrm{op}}\le \|x\|_{\mathrm{op}},
\end{align*}
the right-hand side is less than $\varepsilon$. Hence
\begin{align*}
\pi_\phi(x_i)\eta\to\pi_\phi(x)\eta
\end{align*}
for every $\eta\in H_\phi$. Therefore $\pi_\phi(x_i)\to\pi_\phi(x)$ strongly.
Thus $\pi_\phi$ preserves suprema of increasing bounded positive nets, so $\pi_\phi$ is normal. Together with the previous steps, this proves the existence of the Hilbert space $H_\phi$, the normal unital $*$-representation $\pi_\phi$, and the cyclic vector $\Omega_\phi$ satisfying the required identity.
[/step]