[proofplan]
Represent the state $\varphi$ as a vector state in its GNS representation, with cyclic separating vector $\Omega_\varphi$. The Tomita operator fixes $\Omega_\varphi$, and its adjoint also fixes $\Omega_\varphi$, so the modular operator $\Delta_\varphi=S^*S$ fixes $\Omega_\varphi$. Functional calculus then shows that every modular unitary $\Delta_\varphi^{it}$ fixes $\Omega_\varphi$. Finally, the implementation formula for the modular automorphism group reduces the desired equality to the vector-state formula for $\varphi$.
[/proofplan]
[step:Represent the state by its GNS cyclic vector]
Let
\begin{align*}
\pi_\varphi:M\to \mathcal{L}(H_\varphi)
\end{align*}
be the GNS representation of the normal state $\varphi$, and let $\Omega_\varphi\in H_\varphi$ be the GNS cyclic vector. Thus, for every $x\in M$,
\begin{align*}
\varphi(x)=(\pi_\varphi(x)\Omega_\varphi,\Omega_\varphi)_{H_\varphi}.
\end{align*}
Since $\varphi$ is faithful, $\Omega_\varphi$ is separating for $\pi_\varphi(M)$. Therefore the Tomita operator associated to the pair $(\pi_\varphi(M),\Omega_\varphi)$ is defined on the dense subspace $\pi_\varphi(M)\Omega_\varphi\subset H_\varphi$ by the antilinear rule
\begin{align*}
S_0(\pi_\varphi(x)\Omega_\varphi)=\pi_\varphi(x)^*\Omega_\varphi,
\end{align*}
for $x\in M$. Let $S$ denote the closure of $S_0$, and let
\begin{align*}
S=J_\varphi\Delta_\varphi^{1/2}
\end{align*}
be its [polar decomposition](/theorems/3074), where $J_\varphi$ is the modular conjugation and $\Delta_\varphi$ is the positive self-adjoint modular operator.
[/step]
[step:Show that the modular operator fixes the GNS vector]
Because $\pi_\varphi(1_M)\Omega_\varphi=\Omega_\varphi$, the definition of $S_0$ gives
\begin{align*}
S\Omega_\varphi=S_0(\pi_\varphi(1_M)\Omega_\varphi)=\pi_\varphi(1_M)^*\Omega_\varphi=\Omega_\varphi.
\end{align*}
The adjoint Tomita operator $S^*$ is the Tomita operator associated to the commutant $\pi_\varphi(M)'$ and the same vector $\Omega_\varphi$. Since $1_{\pi_\varphi(M)'}\Omega_\varphi=\Omega_\varphi$, the same defining relation gives
\begin{align*}
S^*\Omega_\varphi=\Omega_\varphi.
\end{align*}
Therefore $\Omega_\varphi$ belongs to the domain of $S^*S$, and
\begin{align*}
\Delta_\varphi\Omega_\varphi=S^*S\Omega_\varphi=S^*\Omega_\varphi=\Omega_\varphi.
\end{align*}
[guided]
The point of this step is to prove that the modular dynamics leaves the implementing vector fixed. The Tomita operator $S$ is first defined on vectors of the form $\pi_\varphi(x)\Omega_\varphi$ by sending them to $\pi_\varphi(x)^*\Omega_\varphi$. Taking $x=1_M$, we obtain
\begin{align*}
S\Omega_\varphi=S_0(\pi_\varphi(1_M)\Omega_\varphi)=\pi_\varphi(1_M)^*\Omega_\varphi=\Omega_\varphi.
\end{align*}
The adjoint Tomita operator $S^*$ plays the same role for the commutant $\pi_\varphi(M)'$. Since the identity operator in the commutant also fixes $\Omega_\varphi$, the same Tomita formula gives
\begin{align*}
S^*\Omega_\varphi=\Omega_\varphi.
\end{align*}
Now the modular operator is, by definition, the positive self-adjoint operator
\begin{align*}
\Delta_\varphi=S^*S.
\end{align*}
Because $S\Omega_\varphi=\Omega_\varphi$ and $S^*\Omega_\varphi=\Omega_\varphi$, the vector $\Omega_\varphi$ lies in the domain of $S^*S$, and hence
\begin{align*}
\Delta_\varphi\Omega_\varphi=S^*S\Omega_\varphi=S^*\Omega_\varphi=\Omega_\varphi.
\end{align*}
Thus $\Omega_\varphi$ is an eigenvector of $\Delta_\varphi$ with eigenvalue $1$.
[/guided]
[/step]
[step:Apply functional calculus to the modular operator]
For each $t\in\mathbb R$, define the Borel function
\begin{align*}
f_t:(0,\infty)\to\mathbb C,\qquad f_t(\lambda)=\lambda^{it}.
\end{align*}
The modular unitary is
\begin{align*}
\Delta_\varphi^{it}=f_t(\Delta_\varphi)
\end{align*}
by the functional calculus for positive [self-adjoint operators](/page/Self-Adjoint%20Operators). Since $\Delta_\varphi\Omega_\varphi=\Omega_\varphi$, the spectral measure of $\Delta_\varphi$ applied to $\Omega_\varphi$ is concentrated at the point $1$. Therefore, for every $t\in\mathbb R$,
\begin{align*}
\Delta_\varphi^{it}\Omega_\varphi=f_t(1)\Omega_\varphi=\Omega_\varphi.
\end{align*}
Taking adjoints gives
\begin{align*}
\Delta_\varphi^{-it}\Omega_\varphi=\Omega_\varphi.
\end{align*}
[/step]
[step:Compute the vector state after applying the modular automorphism]
By the [Tomita-Takesaki theorem](/theorems/9302) [citetheorem:9302], the modular automorphism group is implemented in the GNS representation by
\begin{align*}
\pi_\varphi(\sigma_t^\varphi(x))=\Delta_\varphi^{it}\pi_\varphi(x)\Delta_\varphi^{-it}
\end{align*}
for every $x\in M$ and $t\in\mathbb R$. Hence, using the vector-state formula for $\varphi$,
\begin{align*}
\varphi(\sigma_t^\varphi(x))=(\pi_\varphi(\sigma_t^\varphi(x))\Omega_\varphi,\Omega_\varphi)_{H_\varphi}.
\end{align*}
Substituting the implementation formula gives
\begin{align*}
\varphi(\sigma_t^\varphi(x))=(\Delta_\varphi^{it}\pi_\varphi(x)\Delta_\varphi^{-it}\Omega_\varphi,\Omega_\varphi)_{H_\varphi}.
\end{align*}
Since $\Delta_\varphi^{-it}\Omega_\varphi=\Omega_\varphi$, this becomes
\begin{align*}
\varphi(\sigma_t^\varphi(x))=(\Delta_\varphi^{it}\pi_\varphi(x)\Omega_\varphi,\Omega_\varphi)_{H_\varphi}.
\end{align*}
The operator $\Delta_\varphi^{it}$ is unitary, and the Hilbert-space [inner product](/page/Inner%20Product) is linear in the first variable, so
\begin{align*}
(\Delta_\varphi^{it}\pi_\varphi(x)\Omega_\varphi,\Omega_\varphi)_{H_\varphi}=(\pi_\varphi(x)\Omega_\varphi,\Delta_\varphi^{-it}\Omega_\varphi)_{H_\varphi}.
\end{align*}
Using again $\Delta_\varphi^{-it}\Omega_\varphi=\Omega_\varphi$, we obtain
\begin{align*}
\varphi(\sigma_t^\varphi(x))=(\pi_\varphi(x)\Omega_\varphi,\Omega_\varphi)_{H_\varphi}=\varphi(x).
\end{align*}
This holds for every $x\in M$ and every $t\in\mathbb R$, so $\varphi$ is invariant under its modular automorphism group.
[/step]
