The proof theoretic strength of the Steinitz exchange theorem

We show that the logical theory QLAQLA proves the Cayley–Hamilton theorem from the Steinitz exchange theorem together with a strengthening of the linear independence principle. Since QLAQLA is a fairly weak theory (in the sense that its quantifier-free fragment, LALA, translates into tautologies with TC0TC0-Frege proofs—when restricted to the field QQ of the rationals), it follows that the proof complexity of matrix algebra can be distilled to the Steinitz exchange theorem.