(Geometric) Proof for the projective bundle formula in K-theory I'm trying to piece together a proof of the projective bundle formula from several incomplete sources. Here's the statement I'd like to prove:

Projective bundle formula: Let $\pi: E \to X$ be a vector bundle of rank $r$ over a compact space $X$. Let $\mathbb{P}(E)$ be the projective bundle of $E$ with distinguished line bundle $H$. Then we have the following formula:
   $K(\mathbb{P}(E))=K(X)[H]/( \sum^r_{k=0}(-1)^k [H]^k[\bigwedge^k E] )$.

At this point I feel like I have all the ingredients for the proof but I can't seem to piece them together. Here's what I have:
There's a canonical Kozul complex over $E$:
$$0 \to \mathbb{C} \to E \to \bigwedge^2 E \to \dots \to \bigwedge^r E \to 0$$
Over each point $e \in E$ the maps are given by wedge multiplication $(-) \wedge e$. Therefore this complex is exact outside of the zero section and gives us the thom class in $\lambda_E \in K(E,E-0)=\tilde{K}(Th(E))$. What's a neat way of proving that $K(E,E-0)$ is a free rank 1 module generated by $\lambda_E$? 
Suppose wer'e past that. Observe that there's a cofiber sequence
$$\mathbb{P}(E) \to \mathbb{P}(E \oplus \mathbb{C}) \to Th(E)$$
This suggests that the pullback of $\lambda_E$ to $\mathbb{P}(E \oplus \mathbb{C})$ might tell me the relavant information. Two things are not clear to me here. 


*

*Why is the pullback of $\lambda_E$ to $\mathbb{P}(E \oplus \mathbb{C})$ equal to $\sum^r_{k=0}(-1)^k [H]^k[\bigwedge^k E]$? (Twisting the kozul complex by powers of $[H]$ must have some geometric interpratation... no?)

*It seems rather implausible that for every cofiber sequence $X \to Y \to C$ one has $K(X) = K(Y)/Im(K(C)\to K(Y))$. So can we really justify and prove the formula using these ingredients? Maybe there's an inductive step here that might help simplify the statement?


I apologize if there's a well known source that discusses this in detail. The very reason I'm here is I didn't find one.
 A: First, for any bundle $V$ of dimension $d$ over $Y$ put 
$$ \lambda(V)(t) = \sum (-1)^k[\Lambda^k(V)]t^{d-k} \in K^0(Y)[t]. $$
This is a monic polynomial of degree $d$ over $K^0(Y)$.  It satisfies $\lambda(L)(t)=t-[L]$ if $L$ is a line bundle, and $\lambda(A\oplus B)(t)=\lambda(A)(t)\lambda(B)(t)$.  Thus, if $L$ is isomorphic to a subbundle of $V$ then $V\simeq L\oplus W$ for some $W$ and we find that $\lambda(V)([L])=0$.
Let $p\colon \mathbb{P}(E)\to X$ be the obvious projection.  For any $U\subseteq X$, put 
\begin{align*}
 A^*(U) &= K^*(U)[t]/\lambda(E|_U)(t) \\
 B^*(U) &= K^*(p^{-1}(U))
\end{align*}
The bundle $H$ over $\mathbb{P}(E)$ is tautologically a subbundle of $p^*E$, and using this we obtain a ring map $A^*(X)\to B^*(X)$ sending $t$ to $[H]$.  Essentially the same construction gives maps $\phi_U\colon A^*(U)\to B^*(U)$ for all $U$.  Recall also that $\lambda(E)(t)$ is a monic polynomial of degree $d$.  It follows that the set $T=\{1,t,\dotsc,t^{d-1}\}$ is a basis for $A^*(U)$ over $K^0(U)$.
Now suppose we have open subsets $U$ and $V$.  There is a Mayer-Vietoris sequence relating the $K^*$ groups of $U$, $V$, $U\cup V$ and $U\cap V$.  Using the basis $T$, we obtain a long exact sequence relating the $A^*$ groups of $U$, $V$, $U\cup V$ and $U\cap V$.  The Mayer-Vietoris sequence for $p^{-1}(U)$ and $p^{-1}(V)$ gives another long exact sequence relating the $B^*$ groups of $U$, $V$, $U\cup V$ and $U\cap V$.  The maps $\phi$ link these two long exact sequences.  They are obviously compatible with ther restriction maps $A^*(U)\to A^*(U\cap V)$ and so on, but a little work is needed to check that they are also compatible with the connecting morphisms.  
Now put $\mathcal{U}=\{U\;|\;\phi_U \text{ is iso } \}$.  If $U$ is contractible then $E|_U\simeq U\times\mathbb{C}^d$ and the standard calculation of $K^*(\mathbb{C}P^{d-1})$ shows that $U\in\mathcal{U}$.  If $U$, $V$ and $U\cap V$ lie in $\mathcal{U}$ then the Mayer-Vietoris sequences together with the five lemma show that $U\cup V\in\mathcal{U}$.  Now suppose that $X$ can be covered by open sets $U_1,\dotsc,U_n$ such that all intersections $U_{i_1}\cap\dotsb\cap U_{i_r}$ are empty or contractible.   Then one can check by induction on $n$ that $\phi_X$ is iso.  If $X$ is a finite simplicial complex then the open stars of vertices provide a cover of the required type, so $\phi_X$ is iso.  The case of a completely general $X$ follows by homotopy invariance and a limit argument.
