[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*}[/step]

[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: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]