I'd like to request tips on improving proof writing by taking a standard proof in linear in algebra which is nonetheless difficult to write well, and asking for verification and improvements.
I also want to verify exactly which underlying axioms are needed.
Prove that matrix multiplication is associative, using the computational definition of matrix multiplication.
Proof:
Given $A$ (a $m \times n$ matrix), $B$ ($n \times p$), the computational definition of matrix multiplication is $$[AB]_{ij} = \sum_{t \leq t}A_{it}B_{tj}.$$
With $C$ $(p \times q)$, we have $$\begin{align} [A(BC)]_{ij} &= \sum_{t \leq n}A_{it}[BC]_{tj} \\ &= \sum_{t \leq n}A_{it}[\sum_{u \leq p}B_{tu}C_{uj}] \\ &= \sum_{t \leq n}\sum_{u \leq p}A_{it}B_{tu}C_{uj} \tag{*} \\ &= \sum_{u \leq p}\sum_{t \leq n}A_{it}B_{tu}C_{uj} \tag{**} \\ &= \sum_{u \leq p}(AB)_{iu}C_{uj} \\ &= [(AB)C]_{ij}. \\ \end{align}$$
$(*)$ use the distributive property. $(**)$ use both the associative and commutative properties of addition. It is interesting to note that while matrix multiplication is not commutative, its associativity depends on the commutativity of the underlying field, as it is that which allows us to reverse the order of summation.
Update
Based on the feedback, I've revised the final paragraph. Changes are in bold. Review requested.
$(*)$ use the distributive property. $(**)$ use both the associative and commutative properties of addition. It is interesting to note that while matrix multiplication is not commutative, its multiplicative associativity depends on the additive commutativity of the underlying field, as it is that which allows us to reverse the order of summation.
It’s great to ask which axioms are are being used where.
Your proof steps are correct and clear but we never need to use commutativity of the field multiplication. When we swap the order of summation, we are just grouping the summands in a different way. Within any summand, the three factors still multiply (associatively) in the same order.
For example, multiplication of matrices of (non-commutative) quaternions is still associative, even though quaternions do not even form a field, but rather a “division algebra”.