The extremal function for Petersen minors

We prove that every graph with n vertices and at least 5n−8 edges contains the Petersen graph as a minor, and this bound is best possible. Moreover we characterise all Petersen-minor-free graphs with at least 5n−11 edges. It follows that every graph containing no Petersen minor is 9-colourable and has vertex arboricity at most 5. These results are also best possible.