Alternate Property Z

[Rob Beezer]

Manley Perkel has suggested the following theorem (or more
appropriately, lemma) to add to Subsection VSP of Section VS.

Theorem: Suppose u is a vector in the vector space V. Then u = 0
if and only if u+u = u.

Of course, the forward direction is trivial, but the other direction
captures several steps of other proofs in this section. So the proofs
for uniqeuness of the zero vector (ZVU), zero scalar in scalar
multiplication (ZSSM), zero vector in scalar multiplication (ZVSM) all
become much simpler with this lemma.

My thought is to also create a homework exercise as follows.

~~~~~~~~~~~~~
Replace Property Z of the vector space definition by:

New Property Z: There is a vector u in V such that u + u = u. (We
would denote such a u by 0 once we know it is unique.)

With the replacement, begin with the new set of ten axioms, and prove
the theorem:

Theorem: Let u be the vector guaranteed in New Property Z. Then u +
x = x for all x in V.
~~~~~~~~~~~~~

So the hard part of proving this theorem is that you cannot use the
standard Property Z (its what you are to prove) and you can only use
theorems about vector spaces that have proofs devoid of any use of
Property Z (and I'm not yet certain just which these are).

Here's a partial answer:

Let x be any vector in V. Then by Property AI there exists -x,
such that x + (-x) = 0 (where 0 is notation for any u in New Property
Z). Then

(0 + x) + (-x)
= 0 + (x + (-x)) Associativity
= 0 + 0 Additive inverses
= 0 New Property Z

So (0+x) is an additive inverse of (-x). Another additive inverse of
(-x) is x. So *IF* additive inverses are unique, then x = 0 + x, as
both are additive inverses of (-x).

However, the proof of additive inverses' uniqueness (AIU) uses the
standard Property Z twice, and it feels even harder to prove with the
replaced axiom.

Can anyone provide a proof of the proposed theorem arguing from just
the ten (adjusted) axioms? Of course, proofs of any other needed
theorems based on the ten axioms is a way to go.