avewright/proofwiki-math huggingface dataset:
Theorem: Algebra over Field Embeds into Unitization as Vector Subspace

Let $K$ be a field.
Let $A$ be an algebra over $K$ that is not unital. 
Let $A_+$ be the unitization of $A$.
Let:
:$A_0 = \set {\tuple {x, 0_K} : x \in A} \subseteq A_+$.
Then $A_0$ is a vector subspace of $A_+$.

Proof:
This follows from Vector Subspace of Algebra over Field Embeds into Unitization as Vector Subspace.
{{qed}}
Category:Unitizations of Algebras over Fields
442yj1xu778eqhj0v737phnaoxaucby
Theorem: Unitization of Normed Algebra is Unital Normed Algebra

Let $\GF \in \set {\R, \C}$. 
Let $\struct {A, \norm {\, \cdot \,} }$ be a normed algebra that is not unital as an algebra. 
Let $A_+$ be the unitization of $A$.
Define $\norm {\, \cdot \,}_{A_+} : A_+ \to \hointr 0 \infty$ by: 
:$\norm {\tuple {x, \lambda} }_{A_+} = \norm x + \cmod \lambda$
for each $\tuple {x, \lambda} \in A_+$.
Then $\struct {A_+, \norm {\, \cdot \,}_{A_+} }$ is a unital normed algebra.

Proof:
From Unitization of Algebra over Field is Unital Algebra over Field, $A_+$ is a unital algebra.
We show that $\norm {\, \cdot \,}_{A_+}$ is an algebra norm and that $\norm { {\mathbf 1}_{A_+} } = 1$.
Theorem: Equation for Perpendicular Bisector of Two Points in Complex Plane/Standard Form

$L$ can be expressed by the equation:
:$\map \Re {z_2 - z_1} x + \map \Im {z_2 - z_1} y = \dfrac {\cmod {z_2}^2 - \cmod {z_1}^2} 2$

Proof:
Let $z_1$ and $z_2$ be represented by the points $A = \tuple {x_1, y_1}$ and $B = \tuple {x_2, y_2}$ respectively in the complex plane.
By Equation for Perpendicular Bisector of Two Points, the equation of their perpendicular bisector can be expressed as:
{{begin-eqn}}
{{eqn | l = y - \frac {y_1 + y_2} 2
      | r = \frac {x_1 - x_2} {y_2 - y_1} \paren {x - \dfrac {x_1 + x_2} 2}
}}
{{eqn | ll= \leadsto
      | l = \paren {y_2 - y_1} y - \frac {\paren {y_2 - y_1} \paren {y_2 + y_1} } 2
      | r = - \paren {x_2 - x_1} x + \frac {\paren {x_2 - x_1} \paren {x_2 + x_1} } 2
}}
{{eqn | ll= \leadsto
      | l = \paren {x_2 - x_1} x + \paren {y_2 - y_1} y
      | r = \frac {x_2^2 - x_1^2 + y_2^2 - y_1^2} 2
      | c = Difference of Two Squares
}}
{{eqn | ll= \leadsto
      | l = \map \Re {z_2 - z_1} x + \map \Im {z_2 - z_1} y
      | r = \frac {\cmod {z_2}^2 - \cmod {z_1}^2} 2
      | c = {{Defof|Real Part}}, {{Defof|Imaginary Part}}, {{Defof|Complex Modulus}}
}}
{{end-eqn}}
{{qed}}
Category:Equation for Perpendicular Bisector of Two Points in Complex Plane
2zfiznqv232gtzb327980v9yut5cm0p
Theorem: Extend Theory to Satisfy Witness Property

Let $\LL$ be a language of predicate logic.
Let $T$ be a set of $\LL$-sentences.
Then there exists a language $\LL^*$ and a set of $\LL^*$-sentences $T^*$ satisfying the following properties:
* $T^*$ is finitely satisfiable {{iff}} $T$ is finitely satisfiable.
* If $T^*$ is satisfiable, then $T$ is also.
* For every $\LL^*$-WFF of $1$ free variable $\map \phi x$, there exists some constant $c_\phi$ such that:
::$T^* \models \paren {\exists x: \map \phi x} \implies \map \phi {x := c_\phi}$
* $T^*$ satisfies the witness property.

Proof:
{{Proofread}}
We will recursively define a sequence of languages.
Define:
:$\LL_0 := \LL$
Let the set of predicates in $\LL$ be $\PP$.
Let the set of functions in $\LL$ be $\FF = \set {\KK, \FF_1, \FF_2, \dotsc}$.
For every $i \in \N$, define:
:$\Phi_i$ as the set of $\LL_i$-WFFs of $1$ free variable.
:$\KK_i$ as the set of constants in $\LL_i$.
:$\LL_{i + 1}$ as the language of predicate logic with:
::Predicates $\PP$.
::Functions $\set {\KK_i \cup \Phi_i, \FF_1, \dotsc}$.
Define:
:$\ds \LL^* = \bigcup_{i \mathop \in \N} \LL_i$
:$T^* = T \cup \set {\sqbrk {\paren {\exists x : \map \phi x} \implies \map \phi {x := \phi}} : \phi \in \Phi}$
where $\Phi$ is the set of $\LL^*$-WFFs of $1$ free variable.
It remains to show that all of the stated properties hold.
Theorem: Maximal Finitely Satisfiable Theory with Witness Property is Satisfiable

{{Tidy|If we are using the $\mathrm{PL}$ semantics, then only sentences exist in a theory. We can then show that $T$ is a theory in Finitely Satisfiable Set of Sentences has Maximal Finitely Satisfiable Extension, and make some of this reasoning a little simpler.}}
Let $\LL$ be a language of predicate logic.
Let $T$ be a set of $\LL$-sentences such that:
* $T$ is finitely satisfiable
* For every $\LL$-sentence $\phi$, either:
::$\phi \in T$
:or:
::$\sqbrk {\neg \phi} \in T$
* $T$ satisfies the witness property

Proof:
Let $M$ be the set of all $\LL$-terms that contain no variables.
For each $n$-ary function $f$ in $\LL$, define:
:$\map {F_f} {t_1, \dotsc, t_n} = \sqbrk {\map f {t_1, \dotsc, t_n}}$
For each $n$-ary predicate $p$ in $\LL$, define:
:$\map {P_p} {t_1, \dotsc, t_n} = \begin{cases}
\top & : \sqbrk {\map p {t_1, \dotsc, t_n}} \in T \\
\bot & : \sqbrk {\map p {t_1, \dotsc, t_n}} \notin T
\end{cases}$
Define:
:$\MM = \tuple {M, \set {F_f}, \set {P_p}}$
We will now show that:
:$\MM \models_{\mathrm{PL}} T$
Specifically, we will prove that, for every $\LL$-sentence $\phi$:
:$\phi \in T \iff \MM \models_{\mathrm{PL}} \phi$
First, it can be easily seen that, for every term $t$ containing no variables:
:$\map {\operatorname{val}_\MM} t = t$
where $\operatorname{val}$ is the value of a term.
Let $\map P n$ be defined as:
:For every $\LL$-sentence $\phi$ with $n$ quantifiers, $\phi \in T \iff \MM \models_{\mathrm{PL}} \phi$
We proceed by induction on $\map P n$.
The cases for $\map P 0$ and $\map P {k + 1}$ are very similar, except that one of our cases will not apply in the former, so we will prove them simultaneously.
Let $n \in \N$ be arbitrary.
Let $\map Q m$ be defined as:
:For every $\LL$-sentence $\phi$ with $n$ quantifiers and $m$ logical connectives, $\phi \in T \iff \MM \models_{\mathrm{PL}} \phi$
Now, perform complete induction on $\map Q m$, using the alternate formulation:
:$\forall m \in \N, \paren {\forall \ell < m : \map Q \ell} \implies \map Q m$
Let $m \in \N$ be arbitrary.
Let $\phi$ be an arbitrary $\LL$-sentence with $n$ quantifiers and $m$ logical connectives.
By the definition of WFF, at least one of the following hold:
:There exists an $k$-ary predicate $p$ and terms $t_1, \dotsc, t_k$ such that:
::$\phi = \map p {t_1, \dotsc, t_k}$
:There exists a WFF $\psi$ such that:
::$\phi = \neg \psi$
:There exist WFFs $\chi$ and $\psi$, as well as $\circ$ one of $\lor$, $\land$, $\implies$, or $\iff$ such that:
::$\phi = \paren {\chi \circ \psi}$
:Only if $n > 0$, there exists a variable $x$ and WFF $\psi$ such that:
::$\phi = \paren {\forall x: \psi}$ or $\phi = \paren {\exists x: \psi}$
We will examine these case by case.
Theorem: Spectrum of Idempotent in Algebra over Complex Numbers

Let $A$ be an algebra over $\C$.
Let $p \in A$ be idempotent, that is:
:$p^2 = p$
Let $\map {\sigma_A} p$ be the spectrum of $p$ in $A$. 
Then:
:$\map {\sigma_A} p \subseteq \set {0, 1}$

Proof:
Suppose first that $A$ is not unital and let $p \in A$ be idempotent.
Let $A_+$ be the unitization of $A$. 
Then we have:
{{begin-eqn}}
{{eqn	| l = \tuple {p, 0} \tuple {p, 0}
		| r = \tuple {p^2 + 0p + 0 p, 0}
}}
{{eqn	| r = \tuple {p, 0}
}}
{{end-eqn}}
So $\tuple {p, 0}$ is an idempotent in $A_+$.
Since, by definition of the spectrum in a non-unital algebra, we have:
:$\map {\sigma_A} p = \map {\sigma_{A_+} } {\tuple {p, 0} }$
with $A_+$ unital and $\tuple {p, 0}$ idempotent.
{{WLOG}} we can therefore take $A$ to be unital.
Let $\lambda \in \C$ be such that $\lambda \not \in \set {0, 1}$.
That is, such that $\lambda \paren {1 - \lambda} \ne 0$.
We have:
{{begin-eqn}}
{{eqn	| l = \paren {\lambda {\mathbf 1}_A - p} \paren {\paren {1 - \lambda} {\mathbf 1}_A - p}
		| r = \lambda \paren {1 - \lambda} {\mathbf 1}_A - \paren {1 - \lambda} p - \lambda p + p^2
}}
{{eqn	| r = \lambda \paren {1 - \lambda} {\mathbf 1}_A - p + \lambda p - \lambda p + p
}}
{{eqn	| r = \lambda \paren {1 - \lambda} {\mathbf 1}_A
}}
{{end-eqn}}
so that:
:$\ds \paren {\lambda {\mathbf 1}_A - p} \paren {\frac {\paren {1 - \lambda} {\mathbf 1}_A - p} {\lambda \paren {1 - \lambda} } } = {\mathbf 1}_A$
Since $p$ and ${\mathbf 1}_A$ commute, we also have:
:$\ds \paren {\frac {\paren {1 - \lambda} {\mathbf 1}_A - p} {\lambda \paren {1 - \lambda} } } \paren {\lambda {\mathbf 1}_A - p} = {\mathbf 1}_A$
Hence:
:$\lambda {\mathbf 1}_A - p \in \map G A$ for $\lambda \not \in \set {0, 1}$
where $\map G A$ is the group of units of $A$.
Hence, we have:
:$\map {\sigma_A} p = \set {\lambda \in \C : \lambda {\mathbf 1}_A - p \not \in \map G A} \subseteq \set {0, 1}$
{{qed}}
Theorem: Commutativity of Spectrum in Algebra over Complex Numbers

Let $A$ be an algebra over $\C$.
Let $x, y \in A$.
Let $\map {\sigma_A} {x y}$ and $\map {\sigma_A} {y x}$ be the spectrum of $x y$ and $y x$ respectively in $A$.
Then:
:$\map {\sigma_A} {x y} \cup \set 0 = \map {\sigma_A} {y x} \cup \set 0$

Proof:
Let $\map G A$ be the group of units of $A$.
{{WLOG}}, by replacing $A$ by its unitization if necessary, that $A$ is unital.
Let $x, y \in A$.
We show that ${\mathbf 1}_A - x y \in \map G A$ {{iff}} ${\mathbf 1}_A - y x \in \map G A$.
By swapping $x$ and $y$, it suffices to show that if ${\mathbf 1}_A - x y \in \map G A$, then ${\mathbf 1}_A - y x \in \map G A$. 
Specifically, we show that $\paren { {\mathbf 1}_A - y x}^{-1} = 1 + y \paren {{\mathbf 1}_A - x y}^{-1} x$.
We have:
{{begin-eqn}}
{{eqn	| l = \paren { {\mathbf 1}_A - y x} \paren { {\mathbf 1}_A + y \paren { {\mathbf 1}_A - x y}^{-1} x}
		| r = {\mathbf 1}_A - y x + \paren {1 - y x} y \paren { {\mathbf 1}_A - x y}^{-1} x
}}
{{eqn	| r = {\mathbf 1}_A - y x + y \paren { {\mathbf 1}_A - x y}^{-1} x
}}
{{eqn	| r = {\mathbf 1}_A + y \paren {- {\mathbf 1}_A + \paren { {\mathbf 1}_A - x y}^{-1} - \paren { {\mathbf 1}_A - x y}^{-1} } x
}}
{{eqn	| r = {\mathbf 1}_A + y \paren {- {\mathbf 1}_A + \paren { {\mathbf 1}_A - x y} \paren { {\mathbf 1}_A - x y}^{-1} } x
}}
{{eqn	| r = {\mathbf 1}_A + y \paren {- {\mathbf 1}_A + {\mathbf 1}_A} x
}}
{{eqn	| r = {\mathbf 1}_A
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \paren { {\mathbf 1}_A + y \paren { {\mathbf 1}_A - x y}^{-1} x} \paren { {\mathbf 1}_A - y x}
		| r = {\mathbf 1}_A + y \paren { {\mathbf 1}_A - x y}^{-1} x - y x - y \paren { {\mathbf 1}_A - x y}^{-1} x y x
}}
{{eqn	| r = {\mathbf 1}_A + y \paren {\paren { {\mathbf 1}_A - x y}^{-1} - {\mathbf 1}_A - \paren { {\mathbf 1}_A - x y}^{-1} x y} x
}}
{{eqn	| r = {\mathbf 1}_A + y \paren { \paren { {\mathbf 1}_A - x y}^{-1} \paren { {\mathbf 1}_A - x y} - {\mathbf 1}_A} x
}}
{{eqn	| r = {\mathbf 1}_A + y \paren {- {\mathbf 1}_A + {\mathbf 1}_A} x
}}
{{eqn	| r = {\mathbf 1}_A
}}
{{end-eqn}}
Hence we have shown that for $x, y \in A$, we have ${\mathbf 1}_A - x y \in \map G A$ {{iff}} ${\mathbf 1}_A - y x \in \map G A$.
Now fix $x, y \in A$ and take $\lambda \ne 0$.
We have ${\mathbf 1}_A - \paren {\lambda^{-1} x} y \in \map G A$ {{iff}} ${\mathbf 1}_A - y \paren {\lambda^{-1} x} \in \map G A$. 
That is, $\lambda {\mathbf 1}_A - x y \in \map G A$ {{iff}} $\lambda {\mathbf 1}_A - y x \in \map G A$ for $\lambda \ne 0$. 
Hence we have $\map {\sigma_A} {x y} \setminus \set 0 = \map {\sigma_A} {y x} \setminus \set 0$.
That is, $\map {\sigma_A} {x y} \cup \set 0 = \map {\sigma_A} {y x} \cup \set 0$. 
{{qed}}
Theorem: Norm on Unitization of Normed Algebra is Equivalent to Direct Product Norm

Let $\GF \in \set {\R, \C}$. 
Let $\struct {A, \norm {\, \cdot \,} }$ be a normed algebra over $\GF$ that is not unital as an algebra. 
Let $\struct {A_+, \norm {\, \cdot \,}_1 }$ be the normed unitization of $\struct {A, \norm {\, \cdot \,} }$.
Let $\norm {\, \cdot \,}_2$ be the direct product norm on $A \times \GF$.
Then $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ are equivalent norms.

Proof:
Let $u, v \in \R$. 
We have:
:$\ds \frac 1 2 \paren {\size u + \size v} \le \frac 1 2 \paren {\max \set {\size u, \size v} + \max \set {\size u, \size v} } = \max \set {\size u, \size v}$
and:
:$\ds \max \set {\size u, \size v} \le \max \set {\size u, \size v} + \min \set {\size u, \size v} = \size u + \size v$
Let $x \in A$ and $\lambda \in \GF$. 
Taking $u = \norm x$ and $v = \cmod \lambda$ in the above we obtain:
:$\ds \frac 1 2 \paren {\norm x + \cmod \lambda} \le \max \set {\norm x, \size \lambda} \le \norm x + \cmod \lambda$
That is:
:$\ds \frac 1 2 \norm {\tuple {x, \lambda} }_1 \le \norm {\tuple {x, \lambda} }_2 \le \norm {\tuple {x, \lambda} }_1$
So $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ are equivalent norms.
{{qed}}
Category:Unitizations of Normed Algebras
gufc627mijsipnuil7s297z6o69fo3k
Theorem: Normed Algebra Embeds into Unitization as Closed Ideal

Let $\GF \in \set {\R, \C}$. 
Let $\struct {A, \norm {\, \cdot \,} }$ be a normed algebra over $\GF$ that is not unital as an algebra. 
Let $\struct {A_+, \norm {\, \cdot \,}_{A_+} }$ be the normed unitization of $\struct {A, \norm {\, \cdot \,} }$.
Let:
:$A_0 = \set {\tuple {x, 0} : x \in A} \subseteq A_+$
Then $A_0$ is a closed ideal of $A$.

Proof:
From Algebra over Field Embeds into Unitization as Ideal, $A_0$ is an ideal of $A$.
From Norm on Unitization of Normed Algebra is Equivalent to Direct Product Norm, $\norm {\, \cdot \,}_{A_+}$ is equivalent to the direct product norm $\norm {\, \cdot \,}_{A \times \GF}$.
Let $\sequence {\tuple {x_n, 0} }_{n \in \N}$ be a convergent sequence in $\struct {A_+, \norm {\, \cdot \,}_{A_+} }$ with limit $\tuple {x, \lambda} \in A_+$.
From Convergence in Direct Product Norm and Convergent Sequences in Vector Spaces with Equivalent Norms Coincide, we have $x_n \to x$ and $\lambda = 0$.
So every convergent sequence in $A_0$ has a limit in $A_0$.
So by the definition of a closed set in a normed vector space, $A_0$ is closed.
{{qed}}
Category:Unitizations of Normed Algebras
rbl6hfvq0j8ya47y5gkhaabglmnbn1n
Theorem: Resolvent Set of Element of Banach Algebra is Open

Let $\struct {A, \norm {\, \cdot \,} }$ be a Banach algebra over $\C$. 
Let $x \in A$.
Let $\map {\rho_A} x$ be the resolvent set of $x$ in $A$.
{{mistake|The resolvent set is only defined for unital algebras}}
Then $\map {\rho_A} x$ is open.

Proof:
{{WLOG}} suppose that $A$ is unital, swapping $A$ for its unitization if necessary.
Let $\map G A$ be the group of units of $A$. 
Define $S : \C \to A$ by:
:$\map S \lambda = \lambda {\mathbf 1}_A - x$
From Resolvent Mapping is Continuous: Continuous, $S$ is continuous.
From Group of Units in Unital Banach Algebra is Open, $\map G A$ is open. 
From the definition of the resolvent set, we have:
:$\map {\rho_A} x = \set {\lambda \in \C : \lambda {\mathbf 1}_A - x \in \map G A}$
That is:
:$\map {\rho_A} x = S^{-1} \sqbrk {\map G A}$ 
Since $S$ is continuous, and $\map G A$ is open, $S^{-1} \sqbrk {\map G A}$ is open.
We conclude that $\map {\rho_A} x$ is open.
{{qed}}
Category:Resolvent Sets
Category:Spectral Theory of Banach Algebras
0uqne6rlfm8onml4eq5i33q760nwdax
Theorem: Spectrum of Element of Banach Algebra is Closed

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$ is closed.

Proof:
{{WLOG}} suppose that $A$ is unital, swapping $A$ for its unitization if necessary.
Let $\map {\rho_A} x$ be the resolvent set of $x$ in $A$.
From Resolvent Set of Element of Banach Algebra is Open, $\map {\rho_A} x$ is open.
From the definition of the spectrum, we have $\map {\sigma_A} x = \C \setminus \map {\rho_A} x$.
From the definition of a closed set, $\map {\sigma_A} x$ is therefore closed.
{{qed}}
Category:Spectra (Spectral Theory)
Category:Spectral Theory of Banach Algebras
kc6ii1qd53eemwbsb7khsyh13l9m6yz
Theorem: Spectrum of Element of Banach Algebra is Bounded

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$ is bounded, and in particular:
:$\cmod \lambda \le \norm x$ for all $\lambda \in \map {\sigma_A} x$

Proof:
Suppose first that $\struct {A, \norm {\, \cdot \,} }$ is unital.
Let $\map G A$ be the group of units.
Let $\lambda \in \C$ be such that $\cmod \lambda > \norm x$.
Then from {{NormAxiomVector|2}}, we have:
:$\ds \norm {\frac x \lambda} < 1$
From Element of Unital Banach Algebra Close to Identity is Invertible:
:$\ds {\mathbf 1}_A - \frac x \lambda \in \map G A$
Hence:
:$\lambda {\mathbf 1}_A - x \in \map G A$
So, we have:
:$\set {\lambda \in \C : \cmod \lambda > \norm x} \subseteq \set {\lambda \in \C : \lambda {\mathbf 1}_A - x \in \map G A}$
so that:
:$\set {\lambda \in \C : \lambda {\mathbf 1}_A - x \not \in \map G A} \subseteq \set {\lambda \in \C : \cmod \lambda \le \norm x}$
So we have:
:$\map {\sigma_A} x \subseteq \set {\lambda \in \C : \cmod \lambda \le \norm x}$
in the case that $\struct {A, \norm {\, \cdot \,} }$ is unital.
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 \,} }$.
From the definition of the spectrum in a non-unital algebra, we have:
:$\map {\sigma_A} x = \map {\sigma_{A_+} } {\tuple {x, 0} }$
From the unital case, we have that $\map {\sigma_{A_+} } {\tuple {x, 0} }$ is bounded with:
:$\cmod \lambda \le \norm {\tuple {x, 0} }_{A_+}$ for all $\lambda \in \map {\sigma_A} x$.
We have:
:$\norm {\tuple {x, 0} }_{A_+} = \norm x$
and so:
:$\cmod \lambda \le \norm x$ for all $\lambda \in \map {\sigma_A} x$.
{{qed}}
Category:Spectra (Spectral Theory)
Category:Banach Algebras
Category:Spectrum of Element of Banach Algebra is Bounded
ejds95zf0isd1i7m5fwmi18i2adt4k9
Theorem: Spectrum of Element of Banach Algebra is Compact

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$ is compact.

Proof:
The result follows immediately from:
:Spectrum of Element of Banach Algebra is Bounded
:Spectrum of Element of Banach Algebra is Closed
{{qed}}
Category:Spectra (Spectral Theory)
Category:Banach Algebras
ky0zt3jh1z769hy75uudpejradwrek7
Theorem: Real Number Line is not Topological Continuum

The real number line is not a '''continuum''' in the topological sense.

Proof:
{{Recall|Continuum (Topology)|continuum}}
{{:Definition:Continuum (Topology)}}
However, we have the result Real Number Line is not Compact.
Hence the result.
{{qed}}
Theorem: Real Number Line is not Compact

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Then $\struct {\R, \tau_d}$ is not compact.

Proof:
We have:
:Compact Space is Countably Compact
:Real Number Line is not Countably Compact
Hence, as $\struct {\R, \tau_d}$ is not countably compact, it follows that it is not compact.
{{qed}}
Category:Real Number Line with Euclidean Topology
Category:Examples of Compact Topological Spaces
kspi9j5em2ftdhm328t16x9051tgq57
Theorem: Equivalence of Definitions of Inconsistent (Logic)

{{TFAE|def = Inconsistent (Logic)|view = Inconsistent|context = Logic}}
Let $\LL$ be a logical language.
Let $\mathscr P$ be a proof system for $\LL$.

Proof:
=== Definition $(1)$ implies Definition $(2)$ ===
Let $\FF$ be an inconsistent set of logical formulas by definition $1$.
Let $\phi$ be an arbitrary logical formula in $\FF$.
Then {{hypothesis}}:
:$\phi \land \lnot \phi$
is a logical formula in $\FF$.
Thus $\FF$ is an inconsistent set of logical formulas by definition $2$.
{{qed|lemma}}
Theorem: Three Points are Coplanar

Let $P_1$, $P_2$ and $P_3$ be points in Euclidean $3$-space.
Then there exists a plane $\PP$ such that $P_1$, $P_2$ and $P_3$ all lie in $\PP$.
That is, $P_1$, $P_2$ and $P_3$ are coplanar.

Proof:
Let the straight line $P_1 P_2$ be constructed according to Euclid's first postulate.
Let the straight line $P_2 P_3$ be constructed according to Euclid's first postulate.
Thus $P_1 P_2$ and $P_2 P_3$ intersect at $P_2$.
From Two Intersecting Straight Lines are in One Plane, $P_1 P_2$ and $P_2 P_3$ are coplanar.
Hence as $P_1$, $P_2$ and $P_3$ all lie on either $P_1 P_2$ or $P_2 P_3$, it follows that $P_1$, $P_2$ and $P_3$ are likewise coplanar.
{{qed}}
Theorem: Condition for 4 Points to be Coplanar

Let:
{{begin-eqn}}
{{eqn | l = p_1
      | r = \tuple {x_1, y_1, z_1}
}}
{{eqn | l = p_2
      | r = \tuple {x_2, y_2, z_2}
}}
{{eqn | l = p_3
      | r = \tuple {x_3, y_3, z_3}
}}
{{eqn | l = p_4
      | r = \tuple {x_4, y_4, z_4}
}}
{{end-eqn}}
be distinct points in Cartesian $3$-space.
Then $p_1$, $p_2$, $p_3$ and $p_4$ are coplanar {{iff}}:
:$\begin {vmatrix} x_1 & y_1 & z_1 & 1 \\ x_2 & y_2 & z_2 & 1 \\ x_3 & y_3 & z_3 & 1 \\ x_4 & y_4 & z_4 & 1 \end {vmatrix} = 0$
where the construct is evaluated as a determinant.

Proof:
=== Sufficient Condition ===
Let $p_1$, $p_2$, $p_3$ and $p_4$ be on a plane $P$.
By the equation of plane, determinant form on the points $p_2$, $p_3$ and $p_4$, the equation of $P$ is:
{{begin-eqn}}
{{eqn | n = 1
      | l = \begin {vmatrix} x & y & z & 1 \\ x_2 & y_2 & z_2 & 1 \\ x_3 & y_3 & z_3 & 1 \\ x_4 & y_4 & z_4 & 1 \end {vmatrix}
      | r = 0}}
{{end-eqn}}
Since $p_1$ lies on the plane $P$, $p_1$ satisfies the equation $(1)$.
Therefore:
:$\begin {vmatrix} x_1 & y_1 & z_1 & 1 \\ x_2 & y_2 & z_2 & 1 \\ x_3 & y_3 & z_3 & 1 \\ x_4 & y_4 & z_4 & 1 \end {vmatrix} = 0$
{{qed|lemma}}
Theorem: Coordinate Axes are Copunctal

Let $\CC$ be a coordinate system in ordinary $3$-dimensional space.
Then the coordinate axes of $S$ are copunctal.

Proof:
Implicit by definition of coordinate system.
{{qed}}
Theorem: Character on Unital Banach Algebra is Unital Algebra Homomorphism

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

Proof:
By the definition of a character, $\phi$ is a non-zero algebra homomorphism.
We only need to verify that:
:$\map \phi { {\mathbf 1}_A} = 1$
We have:
:$\map \phi { {\mathbf 1}_A} = \map \phi { {\mathbf 1}_A^2} = \paren {\map \phi { {\mathbf 1}_A} }^2$
So, we have:
:$\map \phi { {\mathbf 1}_A} \in \set {0, 1}$
Note that for all $x \in A$, we have:
:$\map \phi x = \map \phi { {\mathbf 1}_A} \map \phi x$
Hence if we had $\map \phi { {\mathbf 1}_A} = 0$, we would have $\phi = 0$.
Since $\phi \ne 0$, we must therefore have $\map \phi { {\mathbf 1}_A} = 1$.
So $\phi$ is a unital algebra homomorphism.
{{qed}}
Theorem: Character on Banach Algebra is Surjective

Let $\struct {A, \norm {\, \cdot \,} }$ be a Banach algebra over $\C$. 
Let $\phi : A \to \C$ be a character on $A$. 
Then $\phi$ is surjective.

Proof:
From Image of Submodule under Linear Transformation is Submodule, $\phi \sqbrk A$ is a vector subspace of $\C$. 
From Dimension of Proper Subspace is Less Than its Superspace, we have:
:$\dim \phi \sqbrk A \le \dim \C = 1$
and so we either have $\phi \sqbrk A = \set 0$ or $\phi \sqbrk A = \C$.
Since $\phi \ne 0$ by the definition of a character, we have $\phi \sqbrk A = \C$.
{{qed}}
Theorem: Character on Banach Algebra is Surjective

Let $\struct {A, \norm {\, \cdot \,} }$ be a Banach algebra over $\C$. 
Let $\phi : A \to \C$ be a character on $A$. 
Then $\phi$ is surjective.

Proof:
As $\phi$ is non-zero, there exists an $x_0 \in A$ such that:
:$\map \phi {x_0} \in \C \setminus \set 0$
Thus, for each $a \in \C$:
{{begin-eqn}}
{{eqn | l = \frac a {\map \phi {x_0} } x_0
      | o = \in
      | r = A
      | c = as $A$ is a $\C$-algebra
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map \phi {\frac a {\map \phi {x_0} } x_0}
      | r = \frac a {\map \phi {x_0} } \map \phi {x_0}
      | c = as $\phi$ is a $\C$-algebra homomorphism
}}
{{eqn | r = a
}}
{{end-eqn}}
{{qed}}