avewright/proofwiki-math huggingface dataset:
Theorem: Kernel of Character on Unital Commutative Banach Algebra is Maximal Ideal

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital commutative Banach algebra over $\C$. 
Let $\phi : A \to \C$ be a character on $A$. 
Then $\ker \phi$ is a maximal ideal of $A$.

Proof:
From Kernel of Ring Homomorphism is Ideal, $\ker \phi$ is a ring ideal of $A$. 
From the First Ring Isomorphism Theorem, we have:
:$\phi \sqbrk A$ and $\dfrac A {\ker \phi}$ are isomorphic as rings.
From Character on Banach Algebra is Surjective, we have that $\phi \sqbrk A = \C$.
Hence:
:$\dfrac A {\ker \phi} \cong \C$
That is:
:$\dfrac A {\ker \phi}$ is a field.
From Maximal Ideal iff Quotient Ring is Field, we conclude that $\ker \phi$ is a maximal ideal of $A$ in the sense of a ring.
From Kernel of Linear Transformation is Linear Subspace, $\ker \phi$ is a maximal ideal in the sense of an algebra as well.
{{qed}}
Theorem: Kernel of Character on Unital Commutative Banach Algebra is Maximal Ideal

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital commutative Banach algebra over $\C$. 
Let $\phi : A \to \C$ be a character on $A$. 
Then $\ker \phi$ is a maximal ideal of $A$.

Proof:
Let $I$ be an ideal of $A$ such that:
:$\ker \phi \subsetneq I$
We need to show $I = A$.
That is, we need to show:
:${\mathbf 1}_A \in I$
Let:
:$x \in I \setminus \ker \phi$
Then:
:$\map \phi x \ne 0$
Thus we can define:
:$\ds \tilde x := {\map \phi x}^{-1} x$
Then:
{{begin-eqn}}
{{eqn | l = \map \phi { {\mathbf 1}_A - \tilde x}
      | r = \map \phi { {\mathbf 1}_A } - \map \phi {\tilde x}
}}
{{eqn | r = 1 - \map \phi {\tilde x}
      | c = {{Defof|Unital Algebra Homomorphism}}
}}
{{eqn | r = 1 - \map \phi { {\map \phi x}^{-1} x}
}}
{{eqn | r = 1 - {\map \phi x}^{-1} \map \phi x
}}
{{eqn | r = 0
}}
{{end-eqn}}
Thus:
:${\mathbf 1}_A = \underbrace{ {\mathbf 1}_A - \tilde x}_{\in \ker \phi} + \underbrace{\paren { {\map \phi x}^{-1} {\mathbf 1}_A} }_{\in A} \underbrace{x}_{\in I} \in I$
{{qed}}
Theorem: Character on Unital Banach Algebra is Uniquely Identified by Kernel

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital Banach algebra over $\C$. 
Let $\phi, \psi : A \to \C$ be characters on $A$ such that:
:$\ker \phi = \ker \psi$
Then $\phi = \psi$.

Proof:
From Character on Unital Banach Algebra is Unital Algebra Homomorphism, we have $\map \phi { {\mathbf 1}_A} = 1$ and $\map \psi { {\mathbf 1}_A} = 1$. 
Let $x \in A$.
We have:
{{begin-eqn}}
{{eqn	| l = \map \phi {x - \map \phi x {\mathbf 1}_A}
		| r = \map \phi x - \map \phi {\map \phi x {\mathbf 1}_A}
}}
{{eqn	| r = \map \phi x - \map \phi x \map \phi { {\mathbf 1}_A}
}}
{{eqn	| r = \map \phi x - \map \phi x
}}
{{eqn	| r = 0
}}
{{end-eqn}}
So we have $x - \map \phi x {\mathbf 1}_A \in \ker \phi$.
Since $\ker \phi = \ker \psi$, we have $x - \map \phi x {\mathbf 1}_A \in \ker \psi$.
So, we have:
:$\map \psi {x - \map \phi x {\mathbf 1}_A} = 0$
We therefore obtain that:
{{begin-eqn}}
{{eqn	| l = 0
		| r = \map \psi {x - \map \phi x {\mathbf 1}_A}
}}
{{eqn	| r = \map \psi x - \map \psi {\map \phi x {\mathbf 1}_A}
}}
{{eqn	| r = \map \psi x - \map \phi x \map \psi { {\mathbf 1}_A}
}}
{{eqn	| r = \map \psi x - \map \phi x
}}
{{end-eqn}}
So we have $\map \phi x = \map \psi x$.
Since $x \in A$ was arbitrary, we obtain $\phi = \psi$.
{{qed}}
Category:Characters (Banach Algebras)
keklid997gfy145ui0zudvktga0qx29
Theorem: Character on Banach Algebra is Continuous

Let $\struct {A, \norm {\, \cdot \,} }$ be a Banach algebra over $\C$.
Let $\phi : A \to \C$ be a character on $A$.
Then $\phi$ is continuous and further:
:$\norm \phi_{A^\ast} \le 1$

Proof:
Let $\map G A$ be the group of units of $A$.
Suppose first that $\struct {A, \norm {\, \cdot \,} }$ is unital.
We show that:
:$\cmod {\map \phi x} \le \norm x$ for each $x \in A$.
From Continuity of Linear Functionals, we will then have that $\phi$ is continuous with $\norm \phi_{A^\ast} \le 1$.
{{AimForCont}} that $x \in A$ is such that:
:$\cmod {\map \phi x} > \norm x$ 
Since then $\map \phi x \ne 0$, we have $x \ne {\mathbf 0}_A$.
From {{NormAxiomVector|2}}, we have:
:$\ds \norm {\frac x {\map \phi x} } < 1$
From Element of Unital Banach Algebra Close to Identity is Invertible, we have that:
:$\ds {\mathbf 1}_A - \frac x {\map \phi x} \in \map G A$
So there exists $z \in A$ such that:
:$\ds z \paren { {\mathbf 1}_A - \frac x {\map \phi x} } = {\mathbf 1}_A$
From Character on Unital Banach Algebra is Unital Algebra Homomorphism, we have $\map \phi { {\mathbf 1}_A} = 1$. 
So, we have:
{{begin-eqn}}
{{eqn	| l = 1
		| r = \map \phi { {\mathbf 1}_A}
}}
{{eqn	| r = \map \phi {z \paren { {\mathbf 1}_A - \frac x {\map \phi x} } }
}}
{{eqn	| r = \map \phi z \map \phi { {\mathbf 1}_A - \frac x {\map \phi x} }
}}
{{eqn	| r = \map \phi z \paren {\map \phi { {\mathbf 1}_A} - \frac {\map \phi x} {\map \phi x} }
}}
{{eqn	| r = \map \phi z \paren {1 - 1}
}}
{{eqn	| r = 0
}}
{{end-eqn}}
This is a contradiction since $A \ne \set { {\mathbf 0}_A}$.
Hence we have:
:$\norm {\map \phi x} \le \norm x$ for all $x \in A$.
So we have that $\phi$ is continuous with:
:$\norm \phi_{A^\ast} \le 1$ 
Now suppose that $\struct {A, \norm {\, \cdot \,} }$ is not unital.
Let $\struct {A_+, \norm {\, \cdot \,}_{A_+} }$ be the normed unitization of $\struct {A, \norm {\, \cdot \,} }$.
Define $\phi_+ : A_+ \to \C$ by: 
:$\map {\phi_+} {\tuple {x, \lambda} } = \map \phi x + \lambda$
for each $\tuple {x, \lambda} \in A_+$.
From Character on Non-Unital Banach Algebra induces Character on Unitization, $\phi_+$ is a character on $A_+$.
Further:
:$\map {\phi_+} {\tuple {x, 0} } = \map \phi x$ for each $x \in A$.
From the unital case, we have that $\phi_+$ is continuous with $\norm {\phi_+}_{A_+^\ast} \le 1$.
Then, we have:
{{begin-eqn}}
{{eqn	| l = \cmod {\map \phi x}
		| r = \cmod {\map {\phi_+} {\tuple {x, 0} } }
}}
{{eqn	| o = \le
		| r = \norm {\tuple {x, 0} }_{A_+}
}}
{{eqn	| r = \norm x
}}
{{end-eqn}}
So $\phi$ is continuous with $\norm \phi_{A^\ast} \le 1$.
{{qed}}
Category:Characters (Banach Algebras)
Category:Character on Banach Algebra is Continuous
53eyza0ntgtfe4ipu75w449esfb3bhv
Theorem: Closure of Proper Ideal in Unital Banach Algebra is Proper Ideal

Let $\struct {A, \norm {\, \cdot \,} }$ be a Banach algebra over $\C$.
Let $I$ be a proper ideal of $A$.
Then $I^-$ is a proper ideal of $A$.

Proof:
From Closure of Subspace of Normed Vector Space is Subspace, $I^-$ is a vector subspace of $A$. 
Let $x \in I^-$ and $y \in A$.
We need to show that $x y \in I^-$. 
From the definition of a closed set in a normed vector space, there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ valued in $I$ such that:
:$x_n \to x$ 
Since $I$ is an ideal, we have $x_n y \in I$ for each $n \in \N$.
From Product Rule for Sequence in Normed Algebra, we have:
:$x_n y \to x y$
From the definition of closure, we have $x y \in I^-$. 
So $I^-$ is an ideal.
It remains to show that it is proper.
Let $\map G A$ be the group of units of $A$.
From Ideal of Unit is Whole Ring, we have:
:$J \cap \map G A = \O$
From Group of Units in Unital Banach Algebra is Open, $\map G A$ is open.
Hence from Open Set Disjoint from Set is Disjoint from Closure, we have that:
:$J^- \cap \map G A = \O$
From Ideal of Unit is Whole Ring, we conclude that $I^-$ is a proper ideal of $A$.
{{qed}}
Category:Banach Algebras
13jrk13210sjvvy8c7c2mjyj5yp3kt7
Theorem: Maximal Ideal in Unital Banach Algebra is Closed

Let $\struct {A, \norm {\, \cdot \,} }$ be a Banach algebra over $\C$.
Let $I$ be a maximal ideal of $A$.
Then $I$ is closed.

Proof:
From Closure of Proper Ideal in Unital Banach Algebra is Proper Ideal, the closure $I^-$ is a proper ideal of $A$ with $I \subseteq I^-$.
Since $I$ is a maximal ideal, we have $I = I^-$.
From Set is Closed iff Equals Topological Closure, we conclude that $I$ is closed.
{{qed}}
Category:Banach Algebras
d2kvhsrycz8cqxcg75m0p5ew42sp4n6
Theorem: Product of Commuting Elements in Monoid is Unit iff Each Element is Unit

Let $A$ be a monoid.
Let $\map G A$ be the group of units of $A$.
Let $n \ge 2$ be an integer. 
Let $x_1, \ldots, x_n$ be commuting elements in $A$.
Let:
:$\ds x = \prod_{i \mathop = 1}^n x_i$
Then:
:$x \in \map G A$ {{iff}} $x_i \in \map G A$ for each $1 \le i \le n$.

Proof:
If $x_1, \ldots, x_n \in \map G A$, then:
:$\ds \prod_{i \mathop = 1}^k x_i \in \map G A$
by Inverse of Product: Monoid: General Result.
Conversely, suppose:
:$\ds \prod_{i \mathop = 1}^k x_i \in \map G A$
That is, there is a $z \in A$ such that:
:$(1):\quad \ds z \paren {\prod_{i \mathop = 1}^k x_i} = \paren {\prod_{i \mathop = 1}^k x_i} z = e$
We shall show:
:$\forall i \in \set {1, \ldots, n} : x_i \in \map G A$
It suffices to show this for $i=1$, since $x_1, \ldots, x_n$ are commuting.
Define:
:$\ds z_1 := \paren {\prod_{i \mathop = 2}^k x_i} z$
Then:
:$x_1 z_1 = z_1 x_1 = e$
so that $x_1 \in \map G A$.
Indeed:
{{begin-eqn}}
{{eqn | l = x_1 z_1
      | r = x_1 \paren {\prod_{i \mathop = 2}^k x_i} z
      | c = Definition of $z_1$
}}
{{eqn | r = \paren {\prod_{i \mathop = 1}^k x_i} z
}}
{{eqn | r = e
}}
{{end-eqn}}
Moreover:
{{begin-eqn}}
{{eqn | l = z_1 x_1
      | r = \paren {\prod_{i \mathop = 2}^k x_i} z x_1
      | c = Definition of $z_1$
}}
{{eqn | r =  e \paren {\prod_{i \mathop = 2}^k x_i} z x_1
}}
{{eqn | r = z \paren {\prod_{i \mathop = 1}^k x_i} \paren {\prod_{i \mathop = 2}^k x_i} z x_1
      | c = by $(1)$
}}
{{eqn | r = z \paren {\prod_{i \mathop = 2}^k x_i} \paren {\prod_{i \mathop = 1}^k x_i} z x_1
      | c = $x_1$ commutes with $x_2, \ldots, x_n$
}}
{{eqn | r = z \paren {\prod_{i \mathop = 2}^k x_i} e x_1
      | c = by $(1)$
}}
{{eqn | r = z \paren {\prod_{i \mathop = 2}^k x_i} x_1
}}
{{eqn | r = z \paren {\prod_{i \mathop = 1}^k x_i}
      | c = $x_1$ commutes with $x_2, \ldots, x_n$
}}
{{eqn | r = e
      | c = by $(1)$
}}
{{end-eqn}}
{{qed}}
Theorem: Resolvent Mapping is Continuous/Banach Algebra

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital Banach algebra over $\C$. 
Let ${\mathbf 1}_A$ be the identity element of $A$. 
Let $x \in A$.
Let $\map {\rho_A} x$ be the resolvent set of $x$ in $A$.
Define $R : \map {\rho_A} x \to A$ by:
:$\map R \lambda = \paren {\lambda {\mathbf 1}_A - x}^{-1}$
Then $R$ is continuous.

Proof:
=== Lemma ===
{{:Resolvent Mapping is Continuous/Banach Algebra/Lemma}}{{qed|lemma}}
From the Lemma, we have:
:the mapping $S : \C \to A$ defined by:
::$\map S \lambda = \lambda {\mathbf 1}_A - x$
:for each $\lambda \in \C$, is continuous.
From Restriction of Continuous Mapping is Continuous, $S \restriction_{\map {\rho_A} x}$ is continuous.
From the definition of the resolvent set, we have $S \sqbrk {\map {\rho_A} x} \subseteq \map G A$.
From Inverse Mapping on Group of Units in Unital Banach Algebra is Continuous, the mapping $\phi : \map G A \to \map G A$ defined by:
:$\map \phi x = x^{-1}$ for each $x \in \map G A$
is continuous.
From Composite of Continuous Mappings is Continuous, $\phi \circ \paren {S \restriction_{\map {\rho_A} x} } : \map {\rho_A} x \to A$ is continuous.
Since $\phi \circ S = R$, we have that $R$ is continuous.
{{qed}}
Category:Spectral Theory of Banach Algebras
Category:Resolvent Mapping is Continuous
s6mvrlyv65hi8tb4hp46oqfe6b29xwp
Theorem: Triangular Numbers are Primitive Recursive

Let $t : \N \to \N$ be defined as:
:$\map t k = T_k$
where $T_k$ is the $k$-th triangular number.
Then $t$ is a primitive recursive function.

Proof:
Define $f : \N^0 \to \N$ as:
:$\map f {} = 0$.
Define $g : \N^2 \to \N$ as:
$\map g x y = x + y + 1$.
By Constant Function is Primitive Recursive and Addition is Primitive Recursive:
:$f$ and $g$ are primitive recursive.
By definition of primitive recursive, it suffices to show that $t$ is obtained by primitive recursion from $f$ and $g$.
That is, to show that, for all $n \in \N$:
:$\map t n = \begin{cases}
\map f {} & : n = 0 \\
\map g {n - 1, \map t {n - 1}} & : n > 0
\end{cases}$
As:
:$\map f {} = 0$
:$\map g {n - 1, \map t {n - 1}} = n - 1 + \map t {n - 1} + 1$
:$\map t k = T_k$ for all $k \in \N$
that is equivalent to showing:
:$T_n = \begin{cases}
0 & : n = 0 \\
n + T_{n - 1} & : n > 0
\end{cases}$
which is the definition of triangular numbers.
{{qed}}
Category:Primitive Recursive Functions
Category:Triangular Numbers
eylg7gxxiy2zzmzpp60nz76r9jrs4qi
Theorem: Inverse of Cantor Pairing Function is Primitive Recursive

Define $k : \N \to \N$ as:
:$\map k z$ is the largest $k$ such that $T_k \le z$
where $T_k$ is the $k$-th triangular number.
Let $\pi_1 : \N \to \N$ be defined as:
:$\ds \map {\pi_1} z = z - T_{\map k z}$
Let $\pi_2 : \N \to \N$ be defined as:
:$\map {\pi_2} z = \map k z - \map {\pi_1} z$
Then, $\pi_1$ and $\pi_2$ are primitive recursive functions.

Proof:
As $n = \map k z$ is the largest $n$ such that:
:$T_n \le z$
holds, it follows that $n = \map k z + 1$ is the smallest $n$ such that:
:$T_n \le z$
fails.
Or, in other words, $n = \map k z$ the smallest $n$ such that:
:$T_{n + 1} > z$
holds.
It follows that we can define $k : \N \to \N$ as:
:$\map k z = \map {\mu n} {T_{n + 1} > z}$
In order for $k$ to be primitive recursive in this way, we need the minimization to be bounded.
We will define:
:$\map k z = \map {\mu n \le z} {T_{n + 1} > z}$
{{AimForCont}} for $z \in \N$, every $n \le z$ fails $T_{n + 1} > z$.
Then, in particular, $T_{z + 1} > z$ fails.
But by definition of triangular number:
:$T_{z + 1} = z + 1 + T_z \ge z + 1 > z$
which is a contradiction.
Therefore, for every $z \in \N$:
:$\map {\mu n \le z} {T_{n + 1} > z} = \map {\mu n} {T_{n + 1} > z}$
Define $t : \N \to \N$ as:
:$\map t k = T_k$
which is primitive recursive by Triangular Numbers are Primitive Recursive.
Thus, we have:
:$\map k z = \map {\mu n \le z} {\map t {n + 1} > z}$
which is primitive recursive by:
* Bounded Minimization is Primitive Recursive
* Ordering Relations are Primitive Recursive
* Addition is Primitive Recursive
* Constant Function is Primitive Recursive
{{qed|lemma}}
By Inverse of Cantor Pairing Function, $\pi_1$ and $\pi_2$ are well-defined.
That is, for every $z$:
:$\map {\pi_1} z \ge 0$
:$\map {\pi_2} z \ge 0$
or:
:$z \ge T_{\map k z}$
:$\map k z \ge \map {\pi_1} z$
Since these always hold, we have:
:$\map {\pi_1} z = z \mathop {\dot -} T_{\map k z}$
:$\map {\pi_2} z = \map k z \mathop {\dot -} \map {\pi_1} z$
where $\dot -$ denotes partial subtraction.
Thus, we have:
:$\map {\pi_1} z = z \mathop {\dot -} \map t {\map k z}$
From Cut-Off Subtraction is Primitive Recursive, this is primitive recursive.
By the same reasoning, $\pi_2$ is primitive recursive as well.
{{qed}}
Category:Cantor Pairing Function
Category:Primitive Recursive Functions
pq5tge723dnd983w7gfsxqbzizu0ea3
Theorem: Resolvent Mapping is Analytic/Banach Algebra

Let $\struct {A, \norm {\, \cdot \,} }$ be a unital Banach algebra over $\C$. 
Let ${\mathbf 1}_A$ be the identity element of $A$. 
Let $x \in A$.
Let $\map {\rho_A} x$ be the resolvent set of $x$ in $A$.
Define $R : \map {\rho_A} x \to A$ by:
:$\map R \lambda = \paren {\lambda {\mathbf 1}_A - x}^{-1}$
Then $R$ is analytic with derivative:
:$\map {R'} \lambda = -\paren {\lambda {\mathbf 1}_A - x}^{-2}$

Proof:
Let $\lambda, \mu \in \map {\rho_A} x$ be such that $\lambda \ne \mu$.
Then, we have:
{{begin-eqn}}
{{eqn | l = \frac {\paren {\mu {\mathbf 1}_A - x}^{-1} - \paren {\lambda {\mathbf 1}_A - x}^{-1} } {\mu - \lambda}
      | r = \frac {\paren {\mu {\mathbf 1}_A - x}^{-1} \paren { {\mathbf 1}_A - \paren {\mu {\mathbf 1}_A - x} \paren {\lambda {\mathbf 1}_A - x}^{-1} } } {\mu - \lambda}
}}
{{eqn | r = \frac {\paren {\mu {\mathbf 1}_A - x}^{-1} \paren { \paren {\lambda {\mathbf 1}_A - x} - \paren {\mu {\mathbf 1}_A - x} } \paren {\lambda {\mathbf 1}_A - x}^{-1} } {\mu - \lambda}
}}
{{eqn | r = \frac {\paren {\mu {\mathbf 1}_A - x}^{-1} \paren {\lambda - \mu} \paren {\lambda {\mathbf 1}_A - x}^{-1} } {\mu - \lambda}
}}
{{eqn | r = -\paren {\mu {\mathbf 1}_A - x}^{-1} \paren {\lambda {\mathbf 1}_A - x}^{-1}
}}
{{end-eqn}}
From Resolvent Mapping is Continuous: Banach Algebra, we have:
:$\paren {\mu {\mathbf 1}_A - x}^{-1} \to \paren {\lambda {\mathbf 1}_A - x}^{-1}$ as $\mu \to \lambda$ in $\map {\rho_A} x$. 
So, from Product Rule for Sequence in Normed Algebra, we have:
:$-\paren {\mu {\mathbf 1}_A - x}^{-1} \paren {\lambda {\mathbf 1}_A - x}^{-1} \to -\paren {\lambda {\mathbf 1}_A - x}^{-2}$ as $\mu \to \lambda$.
So, we have that:
:$\ds \lim_{\mu \mathop \to \lambda} \frac {\paren {\mu {\mathbf 1}_A - x}^{-1} - \paren {\lambda {\mathbf 1}_A - x}^{-1} } {\mu - \lambda}$ exists
and:
:$\ds \lim_{\mu \mathop \to \lambda} \frac {\map R \mu - \map R \lambda} {\mu - \lambda} = \lim_{\mu \mathop \to \lambda} \frac {\paren {\mu {\mathbf 1}_A - x}^{-1} - \paren {\lambda {\mathbf 1}_A - x}^{-1} } {\mu - \lambda} = -\paren {\lambda {\mathbf 1}_A - x}^{-2}$
So, we obtain:
:$\map {R'} \lambda = -\paren {\lambda {\mathbf 1}_A - x}^{-2}$
{{qed}}
Category:Resolvent Mapping is Analytic
Category:Banach Algebras
2p1jibck0568c7ph0l0pda08ch5ojqz
Theorem: Analytic Function on Banach Space is Continuous

Let $U$ be an open subset of $\C$.
Let $\struct {X, \norm {\, \cdot \,} }$ be a Banach space over $\C$.
Let $f : U \to X$ be an analytic function.
Then $f$ is continuous.

Proof:
Let $x \in U$. 
Since $f : U \to X$ is analytic function, the limit:
:$\ds \lim_{y \mathop \to x} \frac {\map f y - \map f x} {y - x} = \map {f'} x$ exists.
We have, from {{NormAxiomVector|2}}:
:$\ds \norm {\map f y - \map f x} = \cmod {y - x} \norm {\frac {\map f y - \map f x} {y - x} }$
From Modulus of Limit: Normed Vector Space, we have:
:$\ds \lim_{y \mathop \to x} \norm {\frac {\map f y - \map f x} {y - x} } = \norm {\map {f'} x}$
We also have:
:$\ds \lim_{y \mathop \to x} \cmod {y - x} = 0$
So from Product Rule for Complex Sequences, we have:
:$\ds \lim_{y \mathop \to x} \norm {\map f y - \map f x} = 0$
So, we have that $f$ is continuous at $x$.
Since $x \in U$ was arbitrary, we have that $f$ is continuous.
{{qed}}
Category:Analytic Functions
Category:Banach Spaces
2owhcowbsy49gom9hora7n899l9yfz1
Theorem: Spectrum of Element of Banach Algebra is Non-Empty

Let $\struct {A, \norm {\, \cdot \,} }$ be a Banach algebra over $\C$. 
Let $x \in A$.
Let $\map {\sigma_A} x$ be the spectrum of $x$ in $A$.
Then $\map {\sigma_A} x \ne \O$.

Proof:
Suppose first that $\struct {A, \norm {\, \cdot \,} }$ is a unital Banach algebra.
Let $\map {\rho_A} x$ be the resolvent set of $x$ in $A$.
{{AimForCont}} that $\map {\sigma_A} x = \O$.
Then $\map {\rho_A} x = \C$.
Define $R : \C \to A$ by:
:$\map R \lambda = \paren {\lambda {\mathbf 1}_A - x}^{-1}$
for each $\lambda \in \C$.
From Resolvent Mapping is Analytic: Banach Algebra, $R$ is analytic.
With view to apply Liouville's Theorem (Complex Analysis): Banach Space, we show that $R$ is bounded.
Let $\lambda \in \C$ be such that $\cmod \lambda > \norm x + 1$.
Then $\cmod \lambda > \norm x$, and so:
:$\ds \norm {\frac x \lambda} < 1$
from {{NormAxiomVector|2}}.
From Element of Unital Banach Algebra Close to Identity is Invertible, we have:
:$\ds \norm {\paren { {\mathbf 1}_A - \frac x \lambda}^{-1} } \le \frac 1 {1 - \norm {\frac x \lambda} } = \frac {\cmod \lambda} {\cmod \lambda - \norm x}$
by {{NormAxiomVector|2}}.
Hence, we have:
:$\ds \norm {\paren {\lambda {\mathbf 1}_A - x}^{-1} } = \cmod \lambda^{-1} \norm {\paren { {\mathbf 1}_A - \frac x \lambda}^{-1} } \le \frac 1 {\cmod \lambda - \norm x} < 1$
From Resolvent Mapping is Continuous: Banach Algebra, $R$ is continuous.
From Continuous Function on Compact Space is Bounded, there exists $M > 0$ such that:
:$\norm {\paren {\lambda {\mathbf 1}_A - x}^{-1} } \le M$ for $\lambda \in \C$ with $\cmod \lambda \le \norm x + 1$.
Then:
:$\norm {\paren {\lambda {\mathbf 1}_A - x}^{-1} } \le \max \set {1, M}$ for all $\lambda \in \C$. 
From Liouville's Theorem (Complex Analysis): Banach Space, $R$ is constant. 
Then:
:$\paren {2 {\mathbf 1}_A - x}^{-1} = \paren { {\mathbf 1}_A - x}^{-1}$.
Note that for $y, z \in A$ we have:
:$y^{-1} = z^{-1}$ {{iff}} $y = z$.
So, we have:
:$2 {\mathbf 1}_A - x = {\mathbf 1}_A - x$
giving:
:${\mathbf 1}_A = {\mathbf 0}_A$
This is impossible since $\struct {A, \norm {\, \cdot \,} }$ is unital. 
Hence we have reached a contradiction and we have $\map {\sigma_A} x \ne \O$.
Suppose now that $\struct {A, \norm {\, \cdot \,} }$ is not unital.
Then, we have:
:$\map {\sigma_A} x = \map {\sigma_{A_+} } {\tuple {x, 0} }$
where $A_+$ is the normed unitization of $A$.
From the previous case, we have $\map {\sigma_{A_+} } {\tuple {x, 0} } \ne \O$ and hence $\map {\sigma_A} x \ne \O$.
{{qed}}
Category:Spectral Theory of Banach Algebras
Category:Spectrum of Element of Banach Algebra is Non-Empty
t03unz9fegyss7jdhi0cucrjzos3dwz
Theorem: Least Fixed Point of Enumeration Operator is Recursively Enumerable

Let $\psi : \powerset \N \to \powerset \N$ be an enumeration operator.
Then there exists a recursively enumerable set $A$ such that:
:$A$ is a fixed point of $\psi$
:Every fixed point of $\psi$ is a superset of $A$

Proof:
By Least Fixed Point of Enumeration Operator, such an $A$ can be defined as:
:$\ds \bigcup_{i \mathop \in \N} A_i$
where:
:$A_0 = \O$
:$A_{n + 1} = \map \psi {A_n}$
By definition of enumeration operator, there exists a recursively enumerable set $\phi \subseteq \N$ such that:
:$\map \psi A = \set {x \in \N : \exists \text { finite } B \subseteq A : \map \pi {x, b} \in \phi}$
where:
:$b \in \N$ is the code number for $B$
:$\pi : \N^2 \to \N$ is the Cantor pairing function
Suppose that there is no $x_0 \in \N$ such that:
:$\map \pi {x_0, 0} \in \phi$
Then, for every $x \in \N$:
:$\map \pi {x, 0} \notin \phi$
By induction, we will show that every $A_i = \O$.
$A_0 = \O$ by definition.
If $A_i = \O$, then by Subset of Empty Set iff Empty, for every $B \subseteq A_i$:
:$B = \O$
Therefore:
:$b = 0$
But then:
:$\map \pi {x, b} \notin \phi$
for every $x \in \N$.
Thus, by definition of $A_{i + 1}$:
:$A_{i + 1} = \O$
By Principle of Mathematical Induction:
:$A_i = \O$
for every $i \in \N$.
Thus:
:$\ds A = \bigcup_{i \mathop \in \N} A_i = \O$
As $\phi$ is recursively enumerable and $A = \phi$:
:$A$ is recursively enumerable
{{qed|lemma}}
Now, suppose there is some $x_0 \in \N$ such that:
:$\map \pi {x_0, 0} \in \phi$
Then:
:$x_0 \in A_1 \subseteq A$
as $0$ codes the empty set.
Thus, $A$ is non-empty.
By {{Corollary|Recursively Enumerable Set is Image of Primitive Recursive Function}}:
:There exists a primitive recursive function $f : \N \to \N$ such that:
::$\Img f = \phi$
Define:
:<nowiki>$\map g {t, b} = \begin{cases}
\map {\pi_1} {\map f t} & : \map {\RR_\subseteq} {\map {\pi_2} {\map f t}, b} \\
x_0 & : \text {otherwise}
\end{cases}$</nowiki>
where:
:$\pi_1$ and $\pi_2$ are the projections of the Cantor pairing function
:$\map {\RR_\subseteq} {x, y}$ {{iff}} $x$ and $y$ respectively code finite sets $X$ and $Y$ such that $X \subseteq Y$
{{WIP|Need proof that $\RR_\subseteq$ is primitive recursive; in progress}}
ij5a3iwimk9dprrg2qb7o6qaa1x1idw