theorem CommutingRepetition.VN.Modular.two_smul_Pre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω ξ : K) : 2 • (Pre M Ω) ξ = (R M Ω) ξ + (Am M Ω) ξ

theorem CommutingRepetition.VN.Modular.two_smul_Qre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω ξ : K) : 2 • (Qre M Ω) ξ = (R M Ω) ξ - (Am M Ω) ξ

theorem CommutingRepetition.VN.Modular.sub_Pre_mem_orthogonal {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω ξ : K) : ξ - (Pre M Ω) ξ ∈ (↑(Kre M Ω))ᗮ

theorem CommutingRepetition.VN.Modular.R_eq_of_proj {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (R' : K →L[ℂ] K) (A : K →L⋆[ℂ] K) (hfix : ∀ ξ ∈ Kre M Ω, R' ξ + A ξ = 2 • ξ) (hker : ∀ ξ ∈ (↑(Kre M Ω))ᗮ, R' ξ + A ξ = 0) : R' = R M Ω ∧ ∀ (ξ : K), A ξ = (Am M Ω) ξ

Uniqueness of the modular data. If R̃ is complex-linear, A conjugate-linear, (R̃ + A)/2 is the identity on 𝒦 and vanishes on 𝒦^⊥, then R̃ = R and A = P − Q.

theorem CommutingRepetition.VN.Modular.Jm_eq_of_proj {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (J' : K →L⋆[ℂ] K) (hfix : ∀ ξ ∈ Kre M Ω, (R M Ω) ξ + (Tm M Ω) (J' ξ) = 2 • ξ) (hker : ∀ ξ ∈ (↑(Kre M Ω))ᗮ, (R M Ω) ξ + (Tm M Ω) (J' ξ) = 0) (ξ : K) : J' ξ = (Jm M Ω) ξ

With A = T̃ J̃: also J̃ = J once T̃ = T.