From Linear Algebra Done Right, the first theorem for vector spaces is the title of the question. I follow the mechanics of the proof in the book which employs the distributive property, but as someone who did not fully grasp the technical details of mathematical proofs from early education, I'm very confused about this use of the distributive property.
Specifically, why does this make sense? As a full time Software Engineer, why not just define this operation as an axiom or a given? I guess the meta question is how and when do we choose to define an axiom? I assume we draw the line because proofs that build off this don't work?
EDIT: The proof from the book, For $a\in F$, we have $a0 = a(0+0) = a0 + a0$
We would only need to add an axiom specifying the behavior of multiplication by $0$ if it didn't already follow from the axioms that $0v=0$. Since it does, there's no reason to specify this.
You seem to be worried about whether the axioms handle $0$ "correctly." They do, and the proof you describe shows this. It shows that, given the axioms in the book, $0v=0$ for all $v$. Once you've proven this, you accept it as a fact and never have to worry about it again.
An analogy is to think about what would happen if you wanted to add an axiom that handles $2$ "correctly," namely $$2v = v+v$$ Why not specify this as an axiom? Well, we can prove this too. $$2v = (1+1)v = v+v$$ Do we have to specify that multiplication by any positive integer is repeated addition? No, this follows from the distributive law, so there's no need to add it as an axiom.