Finite generation of vector identities

Question

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.

Answer 1

I suspect that $\mathcal{E}$ is finitely generated. Consider the axiom:

$$DA = D_1X + D_2Y + D_3Z.$$

where $D=$

\begin{vmatrix} X.X & Y.X & Z.X \\ X.Y & Y.Y & Z.Y \\ X.Z & Y.Z & Z.Z \end{vmatrix}

and $D_i$ is the result of replacing the ith column of $D$ with $(A.X,\ A.Y,\ A.Z)^T$, as in Cramer's rule.

This axiom states that $R^3$ requires only three coordinates. I suspect that this is the only interesting axiom needed, and the remaining axioms are all assertions of linearity.

UPDATE: Here is a more precise claim.

Let $\mathcal{A}$ consist of the identity above, the identity for the scalar triple product, and an appropriate finite list of claims of associativity, commutativity, and distributivity of the basic operations. (The first eight items on the Wikipedia list are most of what we need, though we have to add (cA.B)=c(A.B), etc.)

Let $\mathcal{E_S}$ be the scalar expressions which are identically equal to 0, and let $\mathcal{E_V}$ be the vector expressions which are identically equal to 0. Then:

1) For any $e_s \in \mathcal{E_S}$, there is some $c_s \notin \mathcal{E_S}$ such that $c_s e_s = 0$ follows from $\mathcal{A}$

2) For any $e_v \in \mathcal{E_V}$, there is some $c_s \notin \mathcal{E_S}$ such that $c_s e_v = 0$ follows from $\mathcal{A}$

For example, the ninth and following claims on Wikipedia, starting with the vector triple product, should be provable from $\mathcal{A}$ in this form.