Pure proof that multiplying $c*({\bf 0} + {\bf 0}) == c*{\bf 0}$ I'm trying to formalize vectorspaces in a proof checker (Coq), and that means one does not get away with forgetting to state assumptions, etc.
Many proofs of $a{\bf 0} = {\bf 0}$, for instance here and here assume without any explicit justification that $$a {\bf 0} = a({\bf 0} + {\bf 0} )$$ How is this derived purely from the vectorspace axioms?
In more techical terms, I have a function $scal : R\rightarrow V \rightarrow V$ and an equivalence relation $equ : V \rightarrow V \rightarrow Prop$ with infix notation $==$. I want to prove that $$\forall a, {\bf u}\ == {\bf v} \implies a{\bf u} == a{\bf v}$$ i.e. that one can "rewrite" in the arguments of the scalar multiplication.  However, this is usually not stated as an axiom, and seems to be silently assumed in many pen-and-paper proofs.  So do I have to add some more assumption about $scal$ than is usually given in the vectorspace axioms, or can $a {\bf 0} = a({\bf 0} + {\bf 0} )$ be proved purely from the axioms?
To moderators: I asked a related question about this earlier, and got some comments (which had the same problem as above) but the question was removed by the moderators.  If you are again removing this question, please let me know why this is an irrelevant question for math.stackexchange.com as I'm new to this forum.
Update: (Sorry if my use of the word "respectful" below is not the standard name, it is what the property happens to be called in the software I'm using)  @Hagen von Eitzen says that the unstated assumption is that scalar multiplication is "respectful" of the equivalence; $\forall P x y, x == y \implies P(x) == P(y)$.  I wonder if it is not a more complicated assumption than necessary, as "respectfulness" with respect to scalar multiplication is implied by $$ {\bf v} == {\bf 0} \implies a \cdot {\bf v} == {\bf 0} \qquad (1)$$  If that is the case, I think it would make more sense to say (1) explicitly rather than silently assuming "respectfulness".  As this is not usually stated, I still wonder if there is a proof of the above that does not rest upon "respectfulness" (making it circular).
 A: From the axioms, $0+b=b$ for all $b$ (recall that a vector space is in particlar an abelian group with addition where $0$ is the neutral element), so in particular, setting $b=0$ we have $0+0=0$. Therefore $a0=a(0+0)$.
A: Using the axioms from wikipedia.
Let us call a vector $\bf z$ a zero if $\forall \mathbf{v}, \mathbf{v} + \mathbf{z} = \mathbf{z}$.
Lemma All zeros are equal.
proof: Let $\mathbf{z}, \mathbf{z'}$ be zeros. Then using commutativity of vector addition we have $\mathbf{z} = \mathbf{z} + \mathbf{z'}  = \mathbf{z'} + \mathbf{z} = \mathbf{z'}$.
Proposition For any $\mathbf{v}$, $\mathbf{v} = 1 \cdot \mathbf{v} = (0 + 1) \cdot \mathbf{v} = 0 \cdot \mathbf{v} + 1 \cdot \mathbf{v} = 0 \cdot \mathbf{v} + \mathbf{v}$.
Theorem $0 \cdot \mathbf v = \mathbf 0$.
proof: By the proposition we have that $0 \cdot \mathbf v$ is a zero. And by definition $\mathbf 0$ is a zero, so by the lemma they are equal.

Edit: To prove that $c \cdot (\mathbf{0} + \mathbf{0}) = c \cdot \mathbf{0}$ start with $\mathbf{0} + \mathbf{0} = \mathbf{0}$ from "Identity element" axiom and the apply the function $\lambda \mathbf{v}. (c \cdot \mathbf{v})$ to both sides of the equation.
