The automorphisms theta and zeta are commuting involutions (Theorem 2.1)

import Mathlib
import Definitions.Def_FRV_alg
import Definitions.Def_FRV_tor

namespace FRV

/-!  Milestone 1 (Theorem 2.1, involutions): the automorphisms theta and
zeta_1, ..., zeta_k of the universal virtual braid group are commuting
involutions. Each zeta_l fixes the virtual generators, sends the l-th
sigma family to its conjugate rho_i sigma_(i,l) rho_i, and fixes the other
families; theta inverts every sigma generator; the compositions are
mutually commuting involutions. -/
theorem theta_zeta_involutions {n k : ℕ} {V Q1 Q2 QM1 QM2 Mk U : Type*}
    [Group V] [Group Q1] [Group Q2] [Group QM1] [Group QM2] [Group Mk] [Group U]
    (W : ForbiddenWorld n k V Q1 Q2 QM1 QM2 Mk U) :
    IsInvolutive W.theta ∧
    (∀ l : Fin k, IsInvolutive (W.zeta l)) ∧
    (∀ l : Fin k, ∀ x : V, W.theta (W.zeta l x) = W.zeta l (W.theta x)) ∧
    (∀ l m : Fin k, ∀ x : V, W.zeta l (W.zeta m x) = W.zeta m (W.zeta l x)) := by sorry

end FRV