Multiplication by a loop of symmetric matrices is symmetric on $L^2(S^1,\mathbb{R}^{2n})$

Let $S^1=\mathbb R/\mathbb Z$ with its Haar probability measure and let $L^2_n=L^2(S^1,\mathbb R^{2n})$ with inner product $\langle f,g\rangle_{L^2}=\int_{S^1}\langle f(t),g(t)\rangle\,dt$. For $f\in L^2_n$ and $k\in\mathbb Z$ let $\hat f_k=\int_{S^1}e^{-2\pi ikt}f(t)\,dt\in\mathbb C^{2n}$ be its $k$-th Fourier coefficient, computed componentwise after viewing the real entries of $f$ as complex numbers.

Let $S:S^1\to\mathbb R^{2n\times2n}$ be continuous with $S(t)^{\mathsf T}=S(t)$ for every $t$. Let $f,g,m,m'\in L^2_n$ with $\hat m_k=(Sf)^\wedge_k$ and $\hat m'_k=(Sg)^\wedge_k$ for every $k\in\mathbb Z$, where $(Sf)^\wedge_k=\int_{S^1}e^{-2\pi ikt}S(t)f(t)\,dt$. Then

In other words, multiplication by a loop of symmetric matrices is a symmetric operator on $L^2(S^1,\mathbb R^{2n})$. This is the zeroth-order part of the symmetry of the asymptotic operator $A_S=-J_0\partial_t-S$.

Formalization note: L2 n, coeff, coeffMul and IsSymLoop come from the definition module AsymptoticOperator_Setting; coeff m k is $\hat m_k$, coeffMul S f k is $(Sf)^\wedge_k$ (with $S(t)$ applied to the complexified vector $f(t)$), and inner ℝ is the $L^2$ inner product.