I am trying to prove the associativity of the tensor product $\otimes$ of vector spaces, along the line with the sketch discussed on a previously-asked question, but I got stuck on the last point.
Question in brief
Do we need the axiom of choice to prove associativity of the tensor product of vector spaces which are not necessarily finitely generated (along this line, in particular)? If not, why not?
What I have managed to do
Hereafter let $X,Y,Z$ be a vector space (on a field $K$). I have managed to show that a map $$(y,z)\mapsto (x\otimes y)\otimes z$$ is bilinear for any fixed $x\in X$, and (after some argument) I realized that this eventually induces a unique bilinear map $$\psi_1:(x\in X,t\in Y\otimes Z)\mapsto A_x(t),$$ where $A_x: Y\otimes Z\rightarrow (X\otimes Y)\otimes Z$ is a linear map which satisfies $$A_x(y\otimes z)=(x\otimes y)\otimes z.$$ Then, it follows from the universal property of the tensor product that there uniquely exists a linear map $F_1:X\otimes(Y\otimes Z)\rightarrow (X\otimes Y)\otimes Z$ such that $$\psi_1(x,t)=A_x(t)=F_1(x\otimes t).$$ Similarly one can induce a bilinear map $$\psi_2:(s\in X\otimes Y,z\in Z)\mapsto B_z(s)$$ where $$B_z(x\otimes y)=x\otimes(y\otimes z),$$ and show that there uniquely exists a linear map $F_2:(X\otimes Y)\otimes Z\rightarrow X\otimes(Y\otimes Z)$ such that $$\psi_2(s,z)=B_z(s)=F_2(s\otimes z).$$ Now the remaining task is to show that $F_1$ is an isomorphism from $X\otimes(Y\otimes Z)$ to $(X\otimes Y)\otimes Z$ (and $F_2$ from $(X\otimes Y)\otimes Z$ to $X\otimes(Y\otimes Z)$). I can easily observe that $$F_2 \circ F_1(x\otimes(y\otimes z))=F_2((x\otimes y)\otimes z)=x\otimes(y\otimes z),$$ $$F_1\circ F_2((x\otimes y)\otimes z)=F_1(x\otimes(y\otimes z))=(x\otimes y)\otimes z.$$
My concern
The above observation, however, does not immediately suggest that $F_1\circ F_2=\mathrm{id}$. The problem is that whether we can extend this observation to the cases where the tensor $t\in Y\otimes Z$ cannot be expressed in terms of the tensor product of two vectors.
I am aware that the thing would be way easier if the vector spaces $X,Y,Z$ were finitely generated: In this case, bases would be guaranteed to exist and every tensor could be expressed in terms of linear combination of some "basis tensor" (tensor product of basis vectors in $Y$ and $Z$), as $Y\otimes Z$ would be also finitely generated (though proof would be necessary for completeness). Then bilinearity of the tensor product and linearity of $F_1,F_2$ would enable me to finish the job.
Unfortunately, however, existence of basis in general vector spaces is equivalent to the axiom of choice (if my knowledge is correct), which may be rejected in some systems of mathematics. Currently I have not come out with a way to work around this issue. I looked up some literature, but explicit mention to the axiom of choice was not found. So it is quite likely that I am missing something very elementary and eventually we do not need the axiom to prove the associativity, but what is the missing point?
You do not need bases for this proof (e.g. associativity continues to hold for tensor products of modules which are not necessarily free). Every element of a tensor product can be expressed as a finite sum of pure tensors (this does not require bases, just the explicit construction of the tensor product) so you can use (bi)linearity.
Alternatively, if you are comfortable with the universal property of the tensor product, here is to my mind a much cleaner proof: $X \otimes (Y \otimes Z)$ and $(X \otimes Y) \otimes Z$ are naturally isomorphic because they represent the same functor, namely the functor of trilinear maps out of $X \times Y \times Z$. (So secretly I am reducing to associativity of the cartesian product.) This proof generalizes with no modification to modules.