[proofplan] We pull $E$ back along the whole homotopy $F$ and work on the bundle $F^*E \to X \times I$. Since $X$ is paracompact and $I$ is compact, the base $X \times I$ is paracompact, so $F^*E$ admits a smooth connection. Parallel transport for this connection along the vertical paths $t \mapsto (x,t)$ gives fibrewise linear isomorphisms between the restrictions over $X \times \{0\}$ and $X \times \{1\}$. Smooth dependence of solutions of the resulting linear ordinary differential equations on the parameter $x$ shows that these fibrewise maps assemble into a smooth vector bundle isomorphism, and the endpoint restrictions are exactly $f_0^*E$ and $f_1^*E$. [/proofplan]

[step:Pull the bundle back to the cylinder over $X$] Let \begin{align*} p: F^*E \to X \times I \end{align*} denote the pullback vector bundle. Explicitly, \begin{align*} F^*E = \{(x,t,e) \in X \times I \times E : q(e) = F(x,t)\}, \end{align*} with projection $p: F^*E \to X \times I$ given by \begin{align*} p(x,t,e) = (x,t). \end{align*} For each $i \in \{0,1\}$, define the smooth inclusion $\iota_i: X \to X \times I$ by \begin{align*} \iota_i(x) = (x,i). \end{align*} Then the restriction $\iota_i^*(F^*E)$ is naturally isomorphic to $f_i^*E$ over $X$, because The elements of $\iota_i^*(F^*E)$ are exactly the triples $(x,(x,i,e)) \in X \times F^*E$ satisfying $q(e)=F(x,i)$. Under the projection $(x,(x,i,e)) \mapsto (x,e)$ this bundle is identified with \begin{align*} \{(x,e) \in X \times E : q(e) = f_i(x)\} = f_i^*E. \end{align*} Let $\operatorname{id}_X: X \to X$ denote the identity map on $X$. Thus it is enough to construct a smooth vector bundle isomorphism \begin{align*} \iota_0^*(F^*E) \to \iota_1^*(F^*E) \end{align*} over $\operatorname{id}_X$. [/step]

[step:Choose a smooth connection on $F^*E$] Since $X$ is paracompact and $I$ is compact, the smooth manifold with boundary $X \times I$ is paracompact. By the existence of smooth connections on vector bundles over paracompact manifolds, the vector bundle $p: F^*E \to X \times I$ admits a smooth connection; denote it by $\nabla$. Concretely, this result is obtained by choosing local trivializations of $F^*E$, taking the corresponding local flat connections, and gluing their connection forms with a smooth [partition of unity](/page/Partition%20of%20Unity) subordinate to a locally finite trivializing cover of $X \times I$. The partition of unity exists by paracompactness of $X \times I$, and the locally finite sum of the local connection forms defines a global smooth connection. [/step]

[step:Define parallel transport along the vertical paths]For each $x \in X$, define the smooth vertical path $\gamma_x: I \to X \times I$ by \begin{align*} \gamma_x(t) = (x,t). \end{align*} Let $T$ denote the smooth vector field on $X \times I$ tangent to the interval direction, characterized by \begin{align*} T_{(x,t)} = \dot{\gamma}_x(t). \end{align*} For $v \in (F^*E)_{(x,0)}$, the existence and uniqueness theorem for linear ordinary differential equations applied in a local frame gives a unique smooth section $s_v: I \to F^*E$ along $\gamma_x$ satisfying \begin{align*} s_v(0) = v. \end{align*} It also satisfies the parallel transport equation \begin{align*} \nabla_{\dot{\gamma}_x(t)} s_v(t) = 0 \end{align*} for all $t \in I$. Define the [linear map](/page/Linear%20Map) $P_x: (F^*E)_{(x,0)} \to (F^*E)_{(x,1)}$ by \begin{align*} P_x(v) = s_v(1). \end{align*} Linearity of the covariant derivative in the section variable implies that $P_x$ is linear. Moreover, $P_x$ is an isomorphism. Indeed, parallel transport along the reversed path $\bar{\gamma}_x: I \to X \times I$ defined by \begin{align*} \bar{\gamma}_x(t) = (x,1-t) \end{align*} defines a linear map from $(F^*E)_{(x,1)}$ to $(F^*E)_{(x,0)}$, and uniqueness of solutions of the parallel transport equation shows that the two maps are inverse to each other.[/step]

[guided]The connection $\nabla$ lets us compare fibres of $F^*E$ over different points of $X \times I$. For this theorem we only need to compare points [lying over](/theorems/2876) the same $x \in X$ and different times $0$ and $1$, so we use the vertical path $\gamma_x: I \to X \times I$ defined by \begin{align*} \gamma_x(t) = (x,t). \end{align*} The tangent vector to this path is the interval-direction vector \begin{align*} \dot{\gamma}_x(t) = T_{(x,t)}. \end{align*} Given a vector $v \in (F^*E)_{(x,0)}$, parallel transport asks for a section along $\gamma_x$, \begin{align*} s_v: I \to F^*E, \end{align*} such that $s_v(t) \in (F^*E)_{(x,t)}$ and \begin{align*} s_v(0) = v. \end{align*} The section is parallel along $\gamma_x$, meaning \begin{align*} \nabla_{\dot{\gamma}_x(t)}s_v(t) = 0. \end{align*} In a local frame this equation is a linear ordinary differential equation in $t$ with smooth coefficients, so the existence and uniqueness theorem for linear ordinary differential equations gives one and only one transported section $s_v$ on the compact interval $I$. We then define $P_x: (F^*E)_{(x,0)} \to (F^*E)_{(x,1)}$ by \begin{align*} P_x(v) = s_v(1). \end{align*} This map is linear because if $v,w \in (F^*E)_{(x,0)}$ and $a,b \in \mathbb{R}$, then $a s_v + b s_w$ satisfies \begin{align*} (a s_v + b s_w)(0) = av + bw. \end{align*} Using linearity of $\nabla$ in the section variable, \begin{align*} \nabla_{\dot{\gamma}_x(t)}(a s_v(t) + b s_w(t)) = a\nabla_{\dot{\gamma}_x(t)}s_v(t) + b\nabla_{\dot{\gamma}_x(t)}s_w(t) = 0. \end{align*} By uniqueness, $a s_v + b s_w$ is the parallel section with initial value $av+bw$, hence \begin{align*} P_x(av+bw) = aP_x(v)+bP_x(w). \end{align*} Finally, $P_x$ is invertible because the same construction can be run backward along the smooth path $\bar{\gamma}_x: I \to X \times I$ defined by \begin{align*} \bar{\gamma}_x(t) = (x,1-t). \end{align*} Transporting from $t=0$ to $t=1$ and then back along the reversed path gives a parallel section with the original initial value. Uniqueness of the parallel transport equation forces the composite to be the identity on $(F^*E)_{(x,0)}$, and the reverse composite is the identity on $(F^*E)_{(x,1)}$.[/guided]

[step:Show that the fibrewise transports vary smoothly with $x$] Define a bundle map $P: \iota_0^*(F^*E) \to \iota_1^*(F^*E)$ over $\operatorname{id}_X$ by \begin{align*} P(x,v) = (x,P_xv). \end{align*} We prove that $P$ is smooth locally on $X$. Let $x_0 \in X$. For each $t \in I$, local triviality gives an open neighbourhood $W_t \subset X \times I$ of $(x_0,t)$ over which $F^*E$ is trivial. Since $\{x_0\} \times I$ is compact, choose $t_1,\dots,t_N \in I$ such that the corresponding sets $W_{t_j}$ cover $\{x_0\} \times I$. By the [tube lemma](/theorems/960) applied to the finite cover, after shrinking to an open neighbourhood $U \subset X$ of $x_0$ and choosing a subdivision \begin{align*} 0 = \tau_0 < \tau_1 < \dots < \tau_M = 1, \end{align*} each closed subcylinder $U \times [\tau_{m-1},\tau_m]$ is contained in some trivializing neighbourhood $W_{t_j}$. It is therefore enough to prove smoothness of the transport map on one such subcylinder: the total transport from $0$ to $1$ is the finite composition of these local transport maps, with the transition maps between adjacent local frames inserted at the subdivision times, and each transition map is smooth. The endpoint values agree by uniqueness of parallel transport, so the finite composition is independent of the chosen local-frame description. Fix one subinterval $J = [a,b] \subset I$ from this subdivision and a trivialization over $U \times J$. Let $r$ be the rank of $E$, and choose a smooth local frame \begin{align*} e_1,\dots,e_r: U \times J \to F^*E \end{align*} for $F^*E$ over $U \times J$. In this frame, a section along $\gamma_x$ has the form \begin{align*} s(t) = \sum_{a=1}^r u_a(t)e_a(x,t), \end{align*} where $u: J \to \mathbb{R}^r$ is the coefficient map defined by \begin{align*} u(t) = (u_1(t),\dots,u_r(t)). \end{align*} Define smooth coefficient functions $A_{ba}: U \times J \to \mathbb{R}$ by \begin{align*} \nabla_T e_a = \sum_{b=1}^r A_{ba}e_b. \end{align*} The parallel transport equation $\nabla_Ts=0$ becomes \begin{align*} \frac{d u_b}{dt}(t) + \sum_{a=1}^r A_{ba}(x,t)u_a(t)=0, \qquad b=1,\dots,r. \end{align*} Equivalently, \begin{align*} \frac{d u}{dt}(t) = -A(x,t)u(t), \end{align*} where $A: U \times J \to \mathbb{R}^{r \times r}$ is the smooth matrix-valued map defined by \begin{align*} A(x,t) = (A_{ba}(x,t))_{b,a}. \end{align*} Let $I_r \in \mathbb{R}^{r \times r}$ denote the identity matrix. For the fixed subinterval $J=[a,b]$, let $\Phi_J: U \times J \to \mathbb{R}^{r \times r}$ be the fundamental matrix solution of the initial value problem \begin{align*} \frac{\partial \Phi_J}{\partial t}(x,t) = -A(x,t)\Phi_J(x,t). \end{align*} The initial condition is \begin{align*} \Phi_J(x,a) = I_r. \end{align*} By smooth dependence of ODE solutions on parameters, applied to this linear system with smooth coefficient matrix $A$, the map $\Phi_J$ is smooth in $(x,t)$. In the chosen frame, the transport from time $a$ to time $b$ is represented by the matrix $\Phi_J(x,b)$, so its local representative is the map $U \times \mathbb{R}^r \to U \times \mathbb{R}^r$ given by \begin{align*} (x,\xi) \mapsto (x,\Phi_J(x,b)\xi). \end{align*} This map is smooth. Composing the finitely many smooth local transports and smooth frame-transition maps from the subdivision gives a smooth representative for the full map $P$ near $x_0$. Since $x_0$ was arbitrary, $P$ is a smooth vector bundle map. [/step]

[step:Identify the transported map with an isomorphism between the endpoint pullbacks] For every $x \in X$, the map $P_x$ is a linear isomorphism, so the smooth bundle map \begin{align*} P: \iota_0^*(F^*E) \to \iota_1^*(F^*E) \end{align*} is a smooth vector bundle isomorphism over $\operatorname{id}_X$. Using the natural endpoint identifications $\iota_0^*(F^*E) \cong f_0^*E$ and $\iota_1^*(F^*E) \cong f_1^*E$, the map $P$ therefore induces a smooth vector bundle isomorphism \begin{align*} f_0^*E \cong f_1^*E \end{align*} over $X$. This proves the homotopy invariance of pullback vector bundles. [/step]