Added the holomorphic functional calculus.

src/op/banach/spectrum.tex

@@ -34,6 +34,22 @@
     By \autoref{proposition:banach-algebra-inverse}, the mapping $y \mapsto y^{-1}$ is smooth on $G(A)$. Hence $R_x: \complex \setminus \sigma_A(x) \to A$ is holomorphic. 
 \end{proof}
 
+\begin{lemma}[Resolvent Equation]
+\label{lemma:resolvent-equation}
+    Let $A$ be a unital Banach algebra, $x \in A$, and $\lambda, \mu \in \complex \setminus \sigma_A(x)$, then
+    \[
+    R_x(\lambda) - R_x(\mu) = (\mu - \lambda)R_x(\lambda) R_x(\mu)
+    \]
+\end{lemma}
+\begin{proof}
+    \begin{align*}
+        [R_x(\lambda) - R_x(\mu)](\mu - x) &= (\lambda - x)^{-1}(\mu - x) - 1 \\
+        (\lambda - x)[R_x(\lambda) - R_x(\mu)](\mu - x)&= (\mu - x) - (\lambda - x) = \mu - \lambda \\
+        R_x(\lambda) - R_x(\mu) &= (\mu - \lambda)R_x(\lambda)R_x(\mu)
+    \end{align*}
+\end{proof}
+
+
 
 \begin{proposition}
 \label{proposition:spectrum-non-empty}