Theorem Proof for "The number 0 times a vector is 0" 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$
 A: It is in principle possible to add things as axioms that are redundant. It is actually not uncommon not to have absolutely minimal descriptions for various reasons, such as to be more clear or more intuitive.  
That said, there is a price to having more axioms. If you want to show that some structure is a vector space, then you have to check all the axioms are verified. Thus, if you add redundant axioms to your list you add extra work down the road, each and every time you want to check that something is a vector space.
I don't know much about software development but maybe this analogy makes sense. If you want to test something and cover all possibilities, then you can either think hard to have good test case or think less hard and have more test. What is preferable will depend on various circumstance.
A: We need to prove and not define that $0v =0 $ for any vector $v$ because multiplication by scalars is already defined for a given vector space. You cannot redefine $0v$ to be something else unless that value match with the value given by our scalar multiplication which in this case, turns out to be $0$.
Regarding the axiom part, we always try to choose a system with the least number of axioms needed to achieve what we require, and these axioms, of course should not seem to contradict each other. Again in your case, since distibutive property already gives you a value for $0v$,  defining $0v$ to be another than $0$ is just a contradiction and defining it to be $0$ is just redundant.
A: 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.
A: We define $0$ as a value where $a+0=a$ and have an axiom to assume such a number exists.  We have no reason assume that this number $0$ has any other magical properties. 
We could write an axiom that there is some soul-crushing number $\Omega$ with the property $\Omega\cdot a = 0$ or maybe some blob all-smothering number $\Xi$ where $\Xi\cdot a = \Xi$.  But we have no reason to think those might be the same number that has magical additive identity property.  And it'd be really poor axiomatic system building to make an axiom that a necessary magical number has two different magical properties.
(Now I suppose it is moot to argue why we have axioms for some magic properties but not others.  It seems useful and aesthetic that we have magical identity numbers where $a+0=a$ and $1*a = a$, but it doesn't seem necessary that why have a soul-eating number where $\Omega\cdot a=0$ or a blob-smothering number where $\Xi\cdot a = \Xi$.  Why not?  I dont know.  It doesn't really seem to build a system I find necessary.)
(Not to mention such numbers are inconsistent.  $\Omega\cdot 1 = 0$ because $\Omega$ is the soul-crusher.  But $\Omega\cdot 1 = \Omega$ because $1$ is the multiplicative identity.  And $\Xi\cdot \Omega = 0$ because $\Omega$ is the soul-crusher but $\Xi\cdot \Omega = \Xi$ because $\Xi$ is the smotherer.)
More to the point, we have a property relating $+$ to $\times$ of distribution that all $a\cdot(b + c) = a\cdot b + a\cdot c$.  It is more powerful and enlightening and humbling to realize that these are forces larger than ourselves, that such a relationship must yield the result that $a\cdot 0 = a(0+0)= a\cdot 0 + a\cdot 0$ so we must have that $a\cdot 0 = 0$ and $0$ although only defined to be an additive identity must, whether we want it or not, must also be a the multiplicative soul-crusher.
