Antisymmetric contractions vanish and $m{U}^{\mathrm{\prime }}=q\mathrm{\Phi }(U)$ preserves $\eta (U,U)$

For each $u\in V$ the map $w\mapsto F(w,u)$ is linear: by bilinearity of $F$ [L2] one has $F(aw+a^{\mathrm{\prime }}{w}^{\mathrm{\prime }},u)=aF(w,u)+a^{\mathrm{\prime }}F(w^{\mathrm{\prime }},u)$ for all reals $a,a^{\mathrm{\prime }}$ and all $w,w^{\mathrm{\prime }}\in V$, so $F(\cdot ,u)\in V^{\ast }$.

The flat map ${\eta }^{\mathrm{♭}}:V\to V^{\ast }$, ${\eta }^{\mathrm{♭}}(x)(w):=\eta (x,w)$, is a bijection: $\eta$ is nondegenerate on the four-dimensional space $V$, so by [L3] its flat map is an isomorphism; equivalently, no nonzero $x$ satisfies $\eta (x,w)=0$ for all $w$.

For each $u\in V$ there is exactly one $\mathrm{\Phi }(u)\in V$ with $\eta (\mathrm{\Phi }(u),w)=F(w,u)$ for all $w\in V$, namely $\mathrm{\Phi }(u):=({\eta }^{\mathrm{♭}}{)}^{-1}(F(\cdot ,u))$: the functional $F(\cdot ,u)$ lies in $V^{\ast }$ by step 1.1 and ${\eta }^{\mathrm{♭}}$ is a bijection by step 1.2, so exactly one $x\in V$ satisfies ${\eta }^{\mathrm{♭}}(x)=F(\cdot ,u)$, that is $\eta (x,w)=F(w,u)$ for all $w$.

$\mathrm{\Phi }:V\to V$ is linear: for all $u,u^{\mathrm{\prime }}\in V$, all reals $a,a^{\mathrm{\prime }}$ and every $w\in V$, bilinearity of $F$ and $\eta$ [L1, L2] gives $\eta (\mathrm{\Phi }(au+a^{\mathrm{\prime }}{u}^{\mathrm{\prime }}),w)=F(w,au+a^{\mathrm{\prime }}{u}^{\mathrm{\prime }})=aF(w,u)+a^{\mathrm{\prime }}F(w,u^{\mathrm{\prime }})=a\eta (\mathrm{\Phi }(u),w)+a^{\mathrm{\prime }}\eta (\mathrm{\Phi }(u^{\mathrm{\prime }}),w)=\eta (a\mathrm{\Phi }(u)+a^{\mathrm{\prime }}\mathrm{\Phi }(u^{\mathrm{\prime }}),w)$; since $w$ is arbitrary, the uniqueness in step 2.1 gives $\mathrm{\Phi }(au+a^{\mathrm{\prime }}{u}^{\mathrm{\prime }})=a\mathrm{\Phi }(u)+a^{\mathrm{\prime }}\mathrm{\Phi }(u^{\mathrm{\prime }})$, which is linearity in the sense of [L5].

Coordinate formula: writing $F_{\alpha \beta }:=F(e_{\alpha },e_{\beta })$ and letting ${\eta }^{\nu \alpha }$ denote the entry of the inverse of the matrix $({\eta }_{\alpha \beta })=\mathrm{diag}(-1,1,1,1)$, one has $\mathrm{\Phi }(u{)}^{\nu }={\eta }^{\nu \alpha }{F}_{\alpha \beta }{u}^{\beta }$, the sum running over $\alpha ,\beta \in \{0,1,2,3\}$: substituting this candidate into the defining pairing gives ${\eta }_{\mu \nu }{\eta }^{\nu \alpha }{F}_{\alpha \beta }{u}^{\beta }={\delta }_{\mu }^{\alpha }{F}_{\alpha \beta }{u}^{\beta }=F_{\mu \beta }{u}^{\beta }=F(e_{\mu },u)$, because ${\eta }_{\mu \nu }{\eta }^{\nu \alpha }={\delta }_{\mu }^{\alpha }$ is the inverse-matrix identity and the matrix $\mathrm{diag}(-1,1,1,1)$ is its own inverse [L1]; the candidate therefore satisfies the defining property in step 2.1, and uniqueness gives the formula, that is $\mathrm{\Phi }(u{)}^0=-F_{0\beta }{u}^{\beta }$ and $\mathrm{\Phi }(u{)}^i=F_{i\beta }{u}^{\beta }$ for $i=1,2,3$.

$\eta (u,\mathrm{\Phi }(u))=0$ for every $u\in V$: symmetry of $\eta$ [L1] and the defining equation of step 2.1 give $\eta (u,\mathrm{\Phi }(u))=\eta (\mathrm{\Phi }(u),u)=F(u,u)$, which is $0$ by the skew-symmetry of $F$ [L2].

Component form: $u_{\mu }{F}^{\mu }{}_{\nu }{u}^{\nu }=0$, where $u_{\mu }:={\eta }_{\mu \alpha }{u}^{\alpha }$ and $F^{\mu }{}_{\nu }:={\eta }^{\mu \alpha }{F}_{\alpha \nu }$; indeed $u_{\mu }{F}^{\mu }{}_{\nu }{u}^{\nu }=u^{\alpha }{\eta }_{\alpha \mu }{\eta }^{\mu \beta }{F}_{\beta \nu }{u}^{\nu }=u^{\beta }{F}_{\beta \nu }{u}^{\nu }=F(u,u)=0$ by [L2], the middle equality using the inverse-matrix identity of step 3.2 and the last equally following from step 3.3 with the coordinate formula, since $u^{\beta }{F}_{\beta \nu }{u}^{\nu }=\eta (u,\mathrm{\Phi }(u))$.

Norm conservation for a constant form: assume $m{U}^{\mathrm{\prime }}(s)=q\mathrm{\Phi }(U(s))$ on $J$ with $m\mathrm{\ne }0$; then $f(s):=\eta (U(s),U(s))$ is constant on $J$. Indeed, by [L1] and [L6], $f(s)={\sum }_{a=0}^3{ϵ}_a(U^a(s){)}^2$ with $ϵ=(-1,1,1,1)$ is differentiable on $J$ with $f^{\mathrm{\prime }}(s)={\sum }_{a}2{ϵ}_a{U}^a(s)(U^a{)}^{\mathrm{\prime }}(s)=2\eta (U(s),U^{\mathrm{\prime }}(s))$, using the product rule and sum rule [L7]; the equation gives $\eta (U(s),U^{\mathrm{\prime }}(s))=(q\mathrm{/}m)\eta (U(s),\mathrm{\Phi }(U(s)))=0$ by step 3.3, so $f^{\mathrm{\prime }}=0$ everywhere on $J$; $f$ is continuous on $J$ by [L8] and the interval $J$ is order-convex with every point interior [L10], so [L9] gives that $f$ is constant on $J$.

Varying-form clause: let $F_s$, $s\in J$, be skew-symmetric bilinear forms and let ${\mathrm{\Phi }}_s$ be defined pointwise by $\eta ({\mathrm{\Phi }}_s(u),w)=F_s(w,u)$, with $m{U}^{\mathrm{\prime }}(s)=q{\mathrm{\Phi }}_s(U(s))$ on $J$; then $s\mapsto \eta (U(s),U(s))$ is again constant on $J$. Indeed the computation of step 4.2 applies verbatim — it differentiates only $U$, never ${\mathrm{\Phi }}_s$ or $F_s$ — giving $f^{\mathrm{\prime }}(s)=2\eta (U(s),U^{\mathrm{\prime }}(s))$, while at each fixed $s$ one has $\eta (U(s),{\mathrm{\Phi }}_s(U(s)))=F_s(U(s),U(s))=0$ by the skew-symmetry of $F_s$ [L2]; hence $\eta (U,U^{\mathrm{\prime }})=(q\mathrm{/}m)\eta (U,{\mathrm{\Phi }}_s(U))=0$ and $f^{\mathrm{\prime }}=0$ on $J$, so [L9] gives that $f$ is constant as in step 4.2. In particular, for a varying field $F_x$ and a differentiable trajectory $x(s)$ one may take $F_s:=F_{x(s)}$ and the corresponding pointwise operator ${\mathrm{\Phi }}_s$.

Conclusion: for every $u\in V$ there is exactly one $\mathrm{\Phi }(u)$ with $\eta (\mathrm{\Phi }(u),w)=F(w,u)$ for all $w$ (step 2.1); $\mathrm{\Phi }$ is linear (step 3.1) and has the index-raised coordinate formula $\mathrm{\Phi }(u{)}^{\mu }={\eta }^{\mu \alpha }{F}_{\alpha \beta }{u}^{\beta }$ (step 3.2); $\eta (u,\mathrm{\Phi }(u))=0$ (step 3.3), in components $u_{\mu }{F}^{\mu }{}_{\nu }{u}^{\nu }=0$ (step 4.1); and both $m{U}^{\mathrm{\prime }}=q\mathrm{\Phi }(U)$ and its varying-form version $m{U}^{\mathrm{\prime }}=q{\mathrm{\Phi }}_s(U)$ make $s\mapsto \eta (U(s),U(s))$ constant on the nonempty open interval $J$ (steps 4.2 and 5.1). The statement is conditional on the displayed equation and asserts nothing about particles.