What's wrong with this proof that commutativity is implied by the other field axioms?

Since we are talking about Fields here and the field axioms are an extension of the ring axioms (a field can be defined as a commutative ring with $1$), you are correct to see redundancy.
However, since the field axioms are constructed from ring axioms and in rings the property is not redundant, it's justified to keep this redundancy. The essential part of the field axioms that generates the redundancy is that $1\in F$ (the field has a multiplicative identity) and it is a ring.

Without this property $-(b+a)$ (the additive inverse of $b+a$) is not guaranteed to be $-1 \cdot (b+a)$ since $-1$ may not even exist. Instead, $-(b+a) = (-a)+(-b)$ because $b+a+(-a)+(-b)=0$.

We can prove that for a Ring to have commutative addition it suffices that it has a $1$:

$$\begin{align*} a+a+b+b & = (1+1)\cdot a+(1+1)\cdot b & \text{left-distributivity}; 1\cdot a = a \\ & = (1+1)\cdot(a+b) & \text{right-distributivity}\\ &= 1\cdot(a+b) + 1\cdot(a+b) & \text{left-distributivity}\\ & = a+b+a+b &\text{right-distributivity} \\ \Rightarrow a+b&=b+a & \text{cancellation} \end{align*}$$ Proof taken from here.
Now although the property is redundant for fields, it isn't in the context of a commutative ring so it's a good idea to still keep all the (non-redundant) ring axioms for consistency since every field is a ring.


Yes, commutativity of addition is a logical consequence of the other field axioms. Nothing wrong with being a little bit redundant.

The missing lemma for the proof:

Let $x \in k$. Then

$$0 = 0 \cdot x = (1 + (-1))\cdot x = 1 \cdot x + (-1) \cdot x = x + (-1)\cdot x$$

Similarly,

$$0 = 0 \cdot x = (-1 + 1)\cdot x = (-1) \cdot x + 1 \cdot x = (-1)\cdot x + x$$

So $(-1)\cdot x$ is the additive inverse of $x$,

$$-x = (-1) \cdot x$$