The proof theoretic strength of the Steinitz exchange theorem

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