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. 


1. 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?)
2. 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.



(Geometric) Proof for the projective bundle formula in K-theory
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.


