Once again about the $1\cdot\boldsymbol x=\boldsymbol x$ axiom of a vector space This is a continuation of my previous question
A unitarity axiom in the vector space axioms
concerning the unitarity law $1\cdot\boldsymbol x =\boldsymbol x$ in
the set of axioms defining the vector space $V$ over a field $F$:
\begin{align}
\alpha\cdot(\beta\cdot\boldsymbol x)&=(\alpha\,\beta)\cdot\boldsymbol x,\tag1\\
(\alpha+\beta)\cdot\boldsymbol x&=\alpha\cdot\boldsymbol x+\beta\cdot\boldsymbol x,\tag2\\
\alpha\cdot(\boldsymbol x +\boldsymbol y)&=\alpha\cdot\boldsymbol x+\alpha\cdot\boldsymbol y,\tag3\\
1\cdot\boldsymbol x &=\boldsymbol x\,.\tag4
\end{align}
I do not display here the remaining axioms of a commutative group
$G=\{+;\boldsymbol x,\boldsymbol y,\ldots\}$ and of the field $F$
above.
We thus have defined set of objects $\boldsymbol x,\boldsymbol
y,\ldots\in V$ supplemented with an external object set
$\alpha,\beta,\ldots\in F$ and interbred them by $(1){-}(4)$. The axiom
$(4)$ is needed to identify the formally independent elements
$\boldsymbol x$ and $1\cdot\boldsymbol x$. This was nicely
elucidated  to me by  user lhf in the post mentioned above.
Well, let us redefine the $V\to \tilde V$ to be a set of the ordered
pairs $(\alpha,\boldsymbol x)\ni\tilde V$ being equivalent to the
objects $\alpha\cdot\boldsymbol x\ni V$, and their formal (group) sums
$(\alpha,\boldsymbol x)+(\beta,\boldsymbol y)+\cdots\equiv
(\gamma,\boldsymbol z)$. It is also assumed that symbols $\boldsymbol x,\boldsymbol
y,\boldsymbol z,\ldots$ belong to some infinite set $S$. It follows that
we may rewrite the rules $(1){-}(4)$ in the form
\begin{align*}
(\alpha,(\beta,\boldsymbol x))&=(\alpha\,\beta,\boldsymbol x),\\
(\alpha+\beta,\boldsymbol x)&=(\alpha,\boldsymbol x)+(\beta,\boldsymbol x),\\
(\gamma,(\alpha,\boldsymbol x) +(\beta,\boldsymbol
y))&=(\gamma\,\alpha,\boldsymbol x)+(\gamma\,\beta,\boldsymbol
y),\tag5
\end{align*}
which counts one fewer axiom than $(1){-}(4)$.
Hereof I conclude that axiom $(4)$ carries just a
$\textit{nomenclature}$ meaning and does not touch the algebraic
mathematics $(1){-}(3)$ itself. That is notation change
$\alpha\cdot\boldsymbol x\rightleftarrows(\alpha,\boldsymbol x)$,
$\boldsymbol x\rightleftarrows (1,\boldsymbol x)$; not more. In
contrast to this, I $\textit{cannot get rid of}$ $(1){-}(3)$ by any
change of notation.
It seems that I can thus formally use this version of the vector
space algebra without loss of further generality. May I spare $(4)$ by
that or any other way?
PS. Perhaps undefined working rules with (vague)
objects/sums like
\begin{equation*}
(\alpha,\boldsymbol x)+(\beta,\boldsymbol y)+\cdots
\end{equation*}
miss here. Well, what about
\begin{equation*}
(\gamma,(\alpha,\boldsymbol x) +(\beta,\boldsymbol y)+\cdots)=(\gamma\,\alpha,\boldsymbol x)+(\gamma\,\beta,\boldsymbol y)+\cdots\,\quad?
\end{equation*}
which follows from recursive associativity wrt group action $+$:
\begin{equation*}
A+B+\cdots=A+(B+\cdots).
\end{equation*}
This is exactly sum of two elements as $(5)$ requires. To put it differently, if the rule $(4)$ can be actually hidden by certain renotation then this axiom is really fictituous and may be discarded in a way.
 A: It seems like your $\tilde{V}$ is an attempt at expressing the free vector space over $V$, i.e., $\tilde{V} \equiv F(V)$, with scalar multiplication written as $(\alpha,\mathbf{x})$. I will work under this definition for the remainder of this answer. 
The space $\tilde{V}$ consists of all formal linear combinations of the elements of $V$. What you've observed is that when we define formal linear combinations by your conditions $(5)$, then they automatically satisfy property $(4)$:
$$(1,(1,\mathbf{x})) \equiv (1\cdot 1, \mathbf{x}) = (1,\mathbf{x}).$$ 
This is of course no accident, since $\tilde{V}$ was constructed to be a vector space and it only points towards the naturality of $(4)$. But the question isn't about whether $(4)$ is natural, it is whether the axiom is really necessary as an additional assumption for the general definition of a vector space, especially since it seems like we can "recover" $V$ from $\tilde{V}$ all the while inheriting the fact that $1\cdot \mathbf{x} = \mathbf{x}$ for free. Let us take a closer look.
First, note that $\tilde{V}$ is not $V$. They are two very different vector spaces. The problem is that $\tilde{V}$ is vastly larger than $V$. In fact, $\tilde{V}$ is of uncountably infinite dimension: $\dim(\tilde{V}) = \mathrm{card}(V).$ In $V$, the elements $\mathbf{x}$ and $2\mathbf{x}$ are of course linearly dependent. In $\tilde{V}$ however, there is nothing relating them, and they are linearly independent vectors. This is the cost of stripping $V$ down to formal symbols; you've lost the original scalar multiplication structure on $V$. This is absolutely key. Scalar multiplication on $\tilde{V}$ is completely independent of scalar multiplication of $V$. Any method of trying to identify $V$ with $\tilde{V}$ must somehow link the respective scalar multiplications.
Let us look at your proposed method of identification, namely $(\alpha,\mathbf{x}) \leftrightarrow \alpha\mathbf{x}$. This is admittedly very natural. However, the problem with this identification is that it is nowhere close to being a one-to-one map. In particular, recall that $(\alpha,\beta\mathbf{x})$ and $(\alpha\beta,\mathbf{x})$ have nothing to do with each other; they are linearly independent as elements of $\tilde{V}$. If you wish to identify both of them as $\alpha\beta\mathbf{x} \in V$ then you have induced a non-trivial equivalence relation on $\tilde{V}$, namely
$$(\alpha,\beta\mathbf{x}) \sim (\alpha\beta,\mathbf{x}).$$
This missing equivalence relation is precisely the relation which implies $1\cdot \mathbf{x} = \mathbf{x}$. Indeed, the above relation tells us that
$$(1,\mathbf{x}) = (1\cdot 1,\mathbf{x}) \sim (1,1\cdot \mathbf{x}),$$
so that this identification forces $1\cdot \mathbf{x} = \mathbf{x}$ in $V$.
We can make all of this slightly more concrete by thinking of "construction" instead of "identification". One of the most useful things about the free vector space is its abundance of interesting quotients; the free vector space is the space with the fewest constraints (i.e., the "freest" space), so virtually any other vector space can be built out of a free space with the appropriate quotients. 
So let us give ourselves the task of realizing $V$ as a particular quotient of $\tilde{V}$. What relations must we quotient out to get $V$ from $\tilde{V}$? The answer is precisely the equivalence relation we previously identified.
Formally, let $T:\tilde{V} \rightarrow V$ denote the linear map such that $T(\alpha,\mathbf{x}) = \alpha\mathbf{x}$, extended linearly. The kernel of this map is the subspace spanned by the elements
$$(\alpha,\mathbf{x}) - (1,\alpha\mathbf{x}).$$
In particular, one of the elements in this subspace is $(1,\mathbf{x}) - (1,1\cdot \mathbf{x})$, which is the imposition of our axiom. The space $V$ is then given as
$$V \cong \tilde{V}/{\ker(T)}.$$
So $V$ isn't simply a "change of nomenclature" for $\tilde{V}$, but instead the imposition of a particular equivalence relation. This equivalence relation is what allows us to relate scalar multiplication on $\tilde{V}$ with scalar multiplication on $V$, which were a priori independent. One consequence of this equivalence relation is that $V$ inherits the property that $1\cdot\mathbf{x} = \mathbf{x}$. You have not spared $(4)$, merely hidden it away.
As a final addendum, let us contruct an algebraic structure which satisfies all the vector space axioms except $(4)$. Let us fix a field $\mathbb{F}$ and let $V = G$ be an abelian group. Define scalar multiplication $\mathbb{F}\times G \rightarrow G$ as $(\lambda, g) \mapsto 0$. Then you can easily show that all the vector space axioms are satisfied with the exception of $(4)$, so that the axiom is independent of the others and cannot be removed. In fact, one of the key purposes of including $(4)$ is to rule out trivial situations like this.
