Symplectic loops fixing a basis vector are homotopic to loops in $\mathrm{Sp}(2n)\diamond\mathrm{Id}$

Let $B:[0,1]\to\mathrm{Sp}(2n+2,\mathbb R)$ be a continuous loop with $B(0)=B(1)=\mathrm{Id}$ such that $B(t)e=e$ for all $t$, where $e$ is the last basis vector of the $q$-block of $\mathbb R^{2n+2}=\mathbb R^{n+1}_q\times\mathbb R^{n+1}_p$. Then there are a continuous loop $B':[0,1]\to\mathrm{Sp}(2n,\mathbb R)$ with $B'(0)=B'(1)=\mathrm{Id}$ and a continuous $\Phi:[0,1]\times[0,1]\to\mathrm{Sp}(2n+2,\mathbb R)$ with

Here $A\diamond C$ is the block-diagonal embedding $\mathrm{Sp}(2n)\times\mathrm{Sp}(2)\to\mathrm{Sp}(2n+2)$, $(q',p')\oplus(q'',p'')\mapsto(q',q'',p',p'')$.

Thus every based loop in the stabiliser of $e$ is homotopic, through based symplectic loops, to a loop coming from $\mathrm{Sp}(2n)$.

Formalization Note. $\mathbb R^{2n\times2n}$ is Mat n (real matrices indexed by Fin n ⊕ Fin n, first block $q$, second block $p$) and $J_0=\begin{pmatrix}0&-\mathrm{Id}\\ \mathrm{Id}&0\end{pmatrix}$ is Matrix.J; IsSymplectic A is membership in Matrix.symplecticGroup. Vectors of $\mathbb R^{2n}$ are functions Fin n ⊕ Fin n → ℝ and $Av$ is A *ᵥ v. $e$ is Pi.single (Sum.inl (Fin.last n)) 1, and $A\diamond C$ is ConleyZehnder.diamond A C from the Conley-Zehnder setting definitions (Mat there is the same type), here with C = (1 : Mat 1).