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.