Finite equational basis for trigonometric identities Consider the structure $(\mathbb{R}, +,-,*,\sin,\cos,0,1)$, where $+$ is addition, $-$ is additive inverse, $*$ is multiplication, $\sin$ is the sine function, and $\cos$ is the cosine function.
Is there a finite basis for the equational identities of that structure? In fact, I conjecture that, in addition to the axioms of a commutative ring, all you need are that $\sin(0)=0$, $\cos(0)=1$, $\sin(-x)=-\sin(x)$,$\cos(-x)=\cos(x)$, the sine of sum formula, the cosine of sum formula, and $\sin^2(x)+\cos^2(x)=1$.

I don't know the answer to this question, but it reminds me of a lemma I read in
Equations on real intervals
Walter Taylor
Algebra universalis 55 (2006) 409-456.
Lemma 5.2. (Expanded, so that it makes sense here.) 
Suppose that $\mathbb R$ is the real line considered as a topological space. Suppose also that
$$
\mathbb A = \langle \mathbb R; \oplus, \odot, \ominus, \stackrel{\cdot}{0}, \stackrel{\cdot}{1}, c(x), s(x), \lambda(x)\rangle
$$
is a topological algebra (meaning all operations are continuous) which satisfies the following identities: 

* identities saying that 
$
\langle \mathbb R; \oplus, \odot, \ominus, \stackrel{\cdot}{0}, \stackrel{\cdot}{1}\rangle
$
is a commutative ring, 

* 
 $c(x + y) = (c(x) · c(y)) − (s(x) · s(y))$,

*
$s(x + y) = (c(x) · s(y)) + (s(x) · c(y))$,

* $c(\stackrel{\cdot}{0}) = \stackrel{\cdot}{1}$, $c(\stackrel{\cdot}{1}) = \stackrel{\cdot}{0}$, $s(\stackrel{\cdot}{1}) = \stackrel{\cdot}{1}$,

* $c(s(x)) = (\lambda(x))^2$.
Let $\mathbb A^-$ be the topological algebra $\mathbb A$ with $\lambda(x)$ deleted from the signature.
There is a unique self-homeomorphism $\phi:\mathbb R\to \mathbb R$ that is
an algebra isomorphism of $\mathbb A^-$ onto the algebra 
$$
\mathbb B = \left\langle \mathbb R; +, \cdot, -, 0, 1, \cos\left(\frac{\pi}{2}x\right), \sin\left(\frac{\pi}{2}x\right)\right\rangle.
$$
