*This question is partially motivated by https://mathoverflow.net/questions/158451/looking-for-a-comprehensive-referece-for-vector-identities, although that question may not be appropriate for MO.*

Consider the set $\mathcal{E}$ of all valid equalities (without parameters) over the two-sorted structure $(\mathbb{R}, \mathbb{R}^3)$ in the language consisting of symbols for: the arithmetic operations addition, subtraction, and multiplication on $\mathbb{R}$; the vector operations of vector addition, vector subtraction, dot product, and cross product on $\mathbb{R}^3$; scalar multiplication; and constant symbols for the real numbers 0 and 1 and the zero-vector $\bf0$. (These are equalities in arbitrarily many variables.)

By Tarski's Theorem, $\mathcal{E}$ is decidable. However, beyond that the structure of $\mathcal{E}$ is somewhat mysterious to me. My question, in particular, is:

Is $\mathcal{E}$ finitely generated?

To make this totally precise, I am asking if the two-sorted variety determined by $\mathcal{E}$ is also determined by some finite set of equations. I would also be interested in the same question for slight variations on $\mathcal{E}$, e.g. in higher dimension (with cross product appropriately altered/removed) or with different language.