avewright/proofwiki-math huggingface dataset:
Theorem: Boolean Lattice is Heyting Lattice

Let $\struct{B, \vee, \wedge, \neg, \preceq}$ be a Boolean lattice.
Then:
:$\struct{B, \vee, \wedge, \preceq}$ is a Heyting lattice where:
::$\forall x, y \in B : x \to y = \neg x \vee y$
:and:
::$x \to y$ denotes the relative pseudocomplement of $x$ with respect to $y$

Proof:
By definition of Boolean lattice and Heyting lattice it remains to show that for all $x, y \in B$ the relative pseudocomplement of $x$ with respect to $y$ exists.
It will be shown that:
:$\forall x, y \in B : \neg x \vee y$ is the relative pseudocomplement of $x$ with respect to $y$
By definition of relative pseudocomplement, it will be shown that:
:$\forall x, y \in B : z \preceq \neg x \vee y$ {{iff}} $z \wedge x \preceq y$
Let:
:$z \in B : z \preceq \neg x \vee y$.
We have:
{{begin-eqn}}
{{eqn | l = z \wedge x
      | o = \preceq
      | r = \paren{\neg x \vee y} \wedge x
      | c = Meet Semilattice is Ordered Structure
}}
{{eqn | r = \paren{\neg x \wedge x} \vee \paren{y \wedge x}
      | c = Boolean lattice is disributive
}}
{{eqn | r = \bot \vee \paren{y \wedge x}
      | c = {{Defof|Complement (Lattice Theory)|Complement}}
}}
{{eqn | r = \paren{y \wedge x}
      | c = Join Semilattice has Smallest Element iff has Identity
}}
{{eqn | o = \preceq
      | r = y
      | c = {{Defof|Meet}}
}}
{{end-eqn}}
Let:
:$z \in B : z \wedge x \preceq y$.
We have:
{{begin-eqn}}
{{eqn | l = z
      | r = z \wedge \top
      | c = Meet Semilattice has Greatest Element iff has Identity
}}
{{eqn | r = z \wedge \paren{\neg x \vee x}
      | c = {{Defof|Complement (Lattice Theory)|Complement}}
}}
{{eqn | r = \paren{z \wedge \neg x} \vee \paren{z \wedge x}
      | c = Boolean lattice is disributive
}}
{{eqn | o = \preceq
      | r = \neg x \vee y
      | c = Join Semilattice is Ordered Structure
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Boolean Lattices
Category:Heyting Algebras
p4amfbevcdry5fxj17ixj6f6z9rd5k1
Theorem: Odd Function/Examples/x^3

Let $f: \R \to \R$ denote the cube function on $\R$.
:$\forall x \in \R: \map f x = x^3$
Then $f$ is an odd function.

Proof:
{{ProofWanted|A specific instance of Odd Power Function is Odd which bizarrely we don't have}}
Theorem: Equivalence of Definitions of Odd Permutation

{{TFAE|def = Odd Permutation}}
Let $n \in \N$ be a natural number.
Let $S_n$ denote the symmetric group on $n$ letters.
Let $\rho \in S_n$ be a permutation in $S_n$.

Proof:
The '''sign of $\rho$''' is defined as:
:$\map \sgn \rho = \begin {cases} 1 & : \text {$k$ even} \\ -1 & : \text {$k$ odd} \\ \end {cases}$
The result follows.
{{qed}}
Category:Odd Permutations
ftgvi42cd03vppbmaetmhg0qenqs5ol
Theorem: Characterization of Homeomorphic Topological Spaces

Let $T_1 = \struct{S_1, \tau_1}$ be topological space.
Let $S_2$ be a set.
Let $\tau_2$ be a subset of the powerset $\powerset {S_2}$.
Then:
:$\struct{S_2, \tau_2}$ is a topological space homeomorphic to $T_1$
{{iff}}:
:there exists a mapping $f : S_1 \to S_2$:
::$(1)\quad f$ is a bijection
::$(2)\quad f^\to \restriction_{\tau_1}$ is a surjection from $\tau_1$ to $\tau_2$
:where
::$f^\to \restriction_{\tau_1}$ denotes the restriction of $f^\to$ to $\tau_1$
::$f^\to$ denotes the direct image mapping of $f$

Proof:
=== Necessary Condition ===
Let $\struct{S_2, \tau_2}$ be a topological space homeomorphic to $T_1$.
{{:Characterization of Homeomorphic Topological Spaces/Necessary Condition}}{{qed|lemma}}
Theorem: Spectrum of Locale is Sober Space

Let $\struct{L, \preceq}$ be a locale.
Let $\map {\operatorname{Sp}} L$ denote the spectrum of $L$.
Then:
:$\map {\operatorname{Sp}} L$ is a sober space.

Proof:
Let $\map {\operatorname{Sp}} L$ denote the spectrum of $L$ as completely prime filters.
From Spectrum of Locale as Completely Prime Filters is Sober Space:
:$\map {\operatorname{Sp}} L$ is a sober space
From Homeomorphism Preserves Sobriety:
:every topological space homeomorphic to $\map {\operatorname{Sp}} L$ is a sober space
From Topological Equivalence of Definitions of Spectrum of Locale:
:each definition of the spectrum of $L$ is homeomorphic to $\map {\operatorname{Sp}} L$
Hence each definition of the spectrum  $\map {\operatorname{Sp}} L$ of $L$ is a sober space
{{qed}}
Category:Spectra of Locales
40uq0llo367uniic9ykjrxt7ack2sq7
Theorem: Topological Equivalence of Definitions of Spectrum of Locale

Let $\struct{L, \preceq}$ be a locale.
{{TFAETop|def = Spectrum of Locale|view = spectrum of locale}}

Proof:
From 
:* Spectrum of Locale as Completely Prime Filters is Sober Space:
the spectrum of $L$ as completely prime filters is a sober space.
From:
:* Canonical Bijection from Completely Prime Filters to Frame Homomorphisms
:* Characterization of Homeomorphic Topological Spaces
the spectrum of $L$ as frame homomorphisms is a topological space homeomorphic to the spectrum of $L$ as completely prime filters.
From:
:* Canonical Bijection from Completely Prime Filters to Meet Irreducible Elements
:* Characterization of Homeomorphic Topological Spaces
the spectrum of $L$ as meet-irreducible elements is a topological space homeomorphic to the spectrum of $L$ as completely prime filters.
From:
:* Canonical Bijection from Frame Homomorphisms to Continuous Maps
:* Characterization of Homeomorphic Topological Spaces
the spectrum of $L$ as continuous maps is a topological space homeomorphic to the spectrum of $L$ as frame homomorphisms.
The result follows by definition of topological equivalence.
{{qed}}
Category:Spectra of Locales
qzgp7o83byib776r8grvn1np0dsh4hz
Theorem: Spectrum Functor is Covariant Functor

Let $\mathbf{Loc}$ denote the category of locales.
Let $\mathbf{Top}$ denote the category of topological spaces.
Then:
:the spectrum functor $\operatorname {Sp} : \mathbf{Loc} \to \mathbf{Top}$ is a covariant functor

Proof:
Recall that the category of locales $\mathbf{Loc}$ is the dual category of the category of frames $\mathbf{Frm}$ by definition.
For each continuous map $f: L_1 \to L_2$ in $\mathbf{Loc}$, let:
:$f^*: L_2 \to L_1$ denote the frame homomorphism in $\mathbf{Frm}$ such that $f = \paren{f^*}^{\text{op} }$.
Let $\operatorname {Fs} : \mathbf{Frm} \to \mathbf{Top}$ denote the frame spectrum functor.
From Frame Spectrum Functor is Contravariant Functor:
:$\operatorname {Fs}$ is a contravariant functor
From Contravariant Functor Induces Covariant Functor from Dual Category:
:the functor $\operatorname {Fs}^*$ defined by:
::* each locale $L$ of $\mathbf {Loc}$ is assigned to the topological space $\map {\operatorname {Fs}} L$ of $\mathbf {Top}$, that is:
::::$\map {\operatorname {Fs}^*} {L} = \map {\operatorname {Fs}} {L}$
::* each continuous map $f : L_1 \to L_2$ of $\mathbf {Loc}$ is assigned to the continuous mapping $\map {\operatorname {Fs}} {f^*} : \map {\operatorname {Fs}} {L_1} \to \map {\operatorname {Fs}} {L_2}$ of $\mathbf {Top}$, that is:
::::$\map {\operatorname {Fs}^*} f = \map {\operatorname {Fs}} {f^*}$
:is a covariant functor.
It is now shown that:
:$\mathbf {\operatorname {Fs}}^* = \mathbf {\operatorname {Sp}}$.
Theorem: Character on Unital C*-Algebra has Modulus One at Unitary Elements

Let $\tuple {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $\phi$ be a character on $A$.
Let $x \in A$ be unitary.
Then:
:$\cmod {\map \phi x} = 1$

Proof:
Let ${\mathbf 1}_A$ be the identity element of $A$. 
Since $x$ is unitary, we have:
:$x x^\ast = {\mathbf 1}_A$
Hence:
:$\map \phi {x x^\ast} = \map \phi { {\mathbf 1}_A}$
From Character on C*-Algebra is *-Algebra Homomorphism, we have:
:$\map \phi {x x^\ast} = \map \phi x \map \phi {x^\ast} = \map \phi x \overline {\map \phi x}$
From Product of Complex Number with Conjugate, we therefore have:
:$\map \phi {x x^\ast} = \cmod {\map \phi x}^2$ 
From Character on Unital Banach Algebra is Unital Algebra Homomorphism, we have:
:$\map \phi { {\mathbf 1}_A} = 1$ 
So we have:
:$\cmod {\map \phi x}^2 = 1$
giving:
:$\cmod {\map \phi x} = 1$ 
{{qed}}
Category:Characters (Banach Algebras)
Category:C*-Algebras
Category:Unitary Elements of Unital *-Algebras
mm213g221x8xwr5w5x13zx07cv3gk31
Theorem: Spectrum of Unitary Element in Unital C*-Algebra is Subset of Unit Circle

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be unitary. 
Let $\map {\sigma_A} x$ denote the spectrum of $x$ in $A$.
Then $\map {\sigma_A} x \subseteq \set {z \in \C : \cmod z = 1}$.

Proof:
Let $A' \subseteq A$ be the $\text C^\ast$-algebra generated by $\set { {\mathbf 1}_A, x, x^\ast}$.
By C*-Algebra Generated by Commutative Self-Adjoint Set is Commutative, $A'$ is commutative. 
Let $\Phi_{A'}$ be the spectrum of $A'$.
From Spectrum of Element of Unital C*-Subalgebra of Unital C*-Algebra, we have:
:$\map {\sigma_A} x = \map {\sigma_{A'} } x$
From Spectrum of Element of Unital Commutative Banach Algebra, we have $\map {\sigma_A} x = \map {\sigma_{A'} } x = \set {\map \phi x : \phi \in \Phi_{A'} }$. 
From Character on Unital C*-Algebra has Modulus One at Unitary Elements, we have $\cmod {\map \phi x} = 1$ for each $\phi \in \Phi_{A'}$.
Hence $\map {\sigma_A} x \subseteq \set {z \in \C : \cmod z = 1}$. 
{{qed}}
Category:C*-Algebras
Category:Unitary Elements of Unital *-Algebras
kpf6epb26l58k7r66andtuuou082z7b
Theorem: Continuous Mapping Induced by Continuous Map is Continuous

Let $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ be locales.
Let $f : L_1 \to L_2$ be a continuous map.
Let:
:$\map {\operatorname{Sp}} f : \map {\operatorname{Sp}} {L_1} \to \map {\operatorname{Sp}} {L_2}$ denote the continuous mapping induced by $f$
where:
:$\map {\operatorname{Sp}} {L_1}$ and $\map {\operatorname{Sp}} {L_2}$ denote the spectra as completely prime filters of $L_1$ and $L_2$, respectively
Then:
:$\map {\operatorname{Sp}} f$ is a continuous mapping

Proof:
Let $f^* : L_2 \to L_1$ denote the frame homomorphism in the category of frames $\mathbf {Frm}$ such that:
:$f = \paren{f^*}^{\text{op} }$ in the category of locales $\mathbf {Loc}$.
Let:
:$\map {\operatorname{Sp}} {f^*} : \map {\operatorname{Sp}} {L_1} \to \map {\operatorname{Sp}} {L_2}$ denote the continuous mapping induced by frame homomorphism $f^*$
From Continuous Mapping Induced by Frame Homomorphism is Continuous:
:$\map {\operatorname{Sp}} {f^*}$ is a continuous mapping
We have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{Sp} } f
      | r = \paren{f^*}^\gets \restriction_{\paren{\map {\operatorname{Sp} } {L_2} \times \map {\operatorname{Sp} } {L_1} } } 
      | c = {{Defof|Continuous Mapping Induced by Continuous Map}}
}}
{{eqn | r = \map {\operatorname{Sp} } {f^*}
      | c = {{Defof|Continuous Mapping Induced by Frame Homomorphism}}
}}
{{end-eqn}}
Hence:
:$\map {\operatorname{Sp}} f$ is a continuous mapping.
{{qed}}
Theorem: Transpose of Outer Product

Let $\mathbf u = \tuple {u_1, u_2, \ldots, u_m}$ and $\mathbf v = \tuple {v_1, v_2, \ldots, v_n}$ be vectors.
Let $\mathbf u \otimes \mathbf v$ denote the outer product of $\mathbf u$ and $\mathbf v$.
Then:
:$\mathbf u \otimes \mathbf v = \paren {\mathbf v \otimes \mathbf u}^\intercal$
where ${}^\intercal$ denotes the transpose operation.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \mathbf u \otimes \mathbf v
      | r = <nowiki>\begin {bmatrix}
u_1 v_1 & u_1 v_2 & \dots & u_1 v_n \\ 
u_2 v_1 & u_2 v_2 & \dots & u_2 v_n \\
 \vdots & \vdots & \ddots & \vdots \\
u_m v_1 & u_m v_2 & \dots & u_m v_n
\end {bmatrix}</nowiki>
      | c = {{Defof|Outer Product}}
}}
{{eqn | l = \mathbf v \otimes \mathbf u
      | r = <nowiki>\begin {bmatrix}
v_1 u_1 & v_1 u_2 & \dots & v_1 u_m \\ 
v_2 u_1 & v_2 u_2 & \dots & v_2 u_m \\
 \vdots & \vdots & \ddots & \vdots \\
v_n u_1 & v_n u_2 & \dots & v_n u_m
\end {bmatrix}</nowiki>
      | c = {{Defof|Outer Product}}
}}
{{eqn | ll= \leadsto
      | l = \paren {\mathbf v \otimes \mathbf u}^\intercal
      | r = <nowiki>\begin {bmatrix}
v_1 u_1 & v_2 u_1 & \dots & v_n u_1 \\ 
v_1 u_2 & v_2 u_2 & \dots & v_n u_2 \\
 \vdots & \vdots & \ddots & \vdots \\
v_1 u_m & v_2 u_m & \dots & v_n u_m
\end {bmatrix}</nowiki>
      | c = {{Defof|Transpose of Matrix}}
}}
{{eqn | r = \mathbf u \otimes \mathbf v
      | c = by inspection
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Outer Products
Category:Transposes of Matrices
n59770626w3qg46sl0s0jjmnqkw396l
Theorem: Subalgebra Generated by Inclusion and Conjugate is Everywhere Dense in Space of Continuous Functions on Compact Subset of Complex Numbers

Let $K \subseteq \C$ be compact. 
Let $\map \CC K$ be the space of continuous functions on $K$.
Let $\iota : K \to \C$ be the inclusion mapping.
Let $\overline \iota : K \to \C$ be the complex conjugate.
Let $\AA$ be the subalgebra generated by $1$, $\iota$ and $\overline \iota$.
That is, by Explicit Form for Generated Subalgebra:
:$\ds \AA = \set {\sum_{j \mathop = 1}^n \alpha_j z^{n_j} \overline z^{m_j} : n \in \N, \, \alpha_j \in \C, \, n_j, m_j \ge 0}$
Then $\AA$ is everywhere dense in $\map \CC K$.

Proof:
From Subalgebra Generated by Self-Adjoint Set is Self-Adjoint, $\AA$ is a $\ast$-subalgebra of $\map \CC K$.
We use the Complex-Valued Stone-Weierstrass Theorem: Compact Space.
We clearly have $1, \iota \in \AA$ by the definition of the generated algebra.
We have $\map \iota z = \map \iota w$ for $z, w \in K$ with $z \ne w$. 
Hence $\AA$ separates points. 
Hence from the Complex-Valued Stone-Weierstrass Theorem: Compact Space, $\AA$ is dense in $\map \CC K$.
{{qed}}
Category:Space of Continuous Functions on Compact Hausdorff Space
oqnhe6i5qg6me1kz4gl6lm786veld9v
Theorem: Spectral Mapping Theorem

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be normal. 
Let $\map {\sigma_A} x$ denote the spectrum of $x$ in $A$.
Let $\map \CC {\map {\sigma_A} x}$ be the space of continuous functions on $\map {\sigma_A} x$.
Let $f \in \map \CC {\map {\sigma_A} x}$.
Let $\map {\Theta_x} f = \map f x$ be the continuous functional calculus of $x$ applied to $f$. 
Then:
:$\map {\sigma_A} {\map f x} = f \sqbrk {\map {\sigma_A} x}$

Proof:
Let $B \subseteq A$ be the $\text C^\ast$-algebra generated by $\set { {\mathbf 1}_A, x, x^\ast}$.
In the proof of Existence and Uniqueness of Continuous Functional Calculus, it is shown that $\Theta_x : \map \CC {\map {\sigma_A} x} \to B$ is an isometric unital $\ast$-algebra isomorphism.
Hence by Spectrum of Image of Element of Unital Algebra under Unital Algebra Homomorphism, we have:
:$\map {\sigma_{\map \CC {\map {\sigma_A} x} } } f = \map {\sigma_B} {\map {\Theta_x} f}$
From Spectrum of Element of Space of Continuous Functions on Compact Hausdorff Space, we have:
:$\map {\sigma_{\map \CC {\map {\sigma_A} x} } } f = \set {\map f z : z \in \map {\sigma_A} x} = f \sqbrk {\map {\sigma_A} x}$
Hence:
:$\map {\sigma_B} {\map f x} = f \sqbrk {\map {\sigma_A} x}$
From Spectrum of Element of Unital C*-Subalgebra of Unital C*-Algebra we have $\map {\sigma_A} x = \map {\sigma_B} x$ and hence:
:$\map {\sigma_A} {\map f x} = \map {\sigma_A} {\map {\Theta_x} f} = f \sqbrk {\map {\sigma_A} x}$
{{qed}}
Theorem: Continuous Functional Calculus obeys Composition

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be normal. 
Let $\map {\sigma_A} x$ denote the spectrum of $x$ in $A$.
Let $\map \CC {\map {\sigma_A} x}$ be the space of continuous functions on $\map {\sigma_A} x$.
Let $f \in \map \CC {\map {\sigma_A} x}$.
Let $g \in \map \CC {f \sqbrk {\map {\sigma_A} x} }$.
Let $\map {\Theta_x} {g \circ f} = \map {\paren {g \circ f} } x$ be the continuous functional calculus of $x$ applied to $g \circ f$.
Let $\map {\Theta_{\map f x} } g = \map g {\map f x}$ be the continuous functional calculus of $\map f x$ applied to $g$.
Then $\map {\paren {g \circ f} } x = \map g {\map f x}$.

Proof:
Note from Existence and Uniqueness of Continuous Functional Calculus that $\map f x$ is normal.
From the Spectral Mapping Theorem, we have:
:$f \sqbrk {\map {\sigma_A} x} = \map {\sigma_A} {\map f x}$
and hence $g \in \map \CC {\map {\sigma_A} {\map f x} }$.
We are hence assured that $\map g {\map f x}$ is well-defined.
Let $B \subseteq A$ be the $\text C^\ast$-algebra generated by $\set { {\mathbf 1}_A, x, x^\ast}$.
Let $C \subseteq A$ be the $\text C^\ast$-algebra generated by $\set { {\mathbf 1}_A, \map f x, \map f x^\ast}$.
From Existence and Uniqueness of Continuous Functional Calculus, we have $C \subseteq B$. 
By C*-Algebra Generated by Commutative Self-Adjoint Set is Commutative, $B$ and $C$ are commutative.
Let $\Phi_B$ and $\Phi_C$ be the spectrums of $B$ and $C$ respectively. 
Let $\phi \in \Phi_B$ so that $\phi \restriction C \in \Phi_C$.
We then have:
{{begin-eqn}}
{{eqn	| l = \map \phi {\map {\paren {g \circ f} } x}
		| r = \map {\paren {g \circ f} } {\map \phi x}
		| c = Continuous Functional Calculus Commutes with Character on Generated C*-Subalgebra
}}
{{eqn	| r = \map g {\map f {\map \phi x} }
}}
{{eqn	| r = \map g {\map {\paren {\phi \restriction C} } {\map f x} }
		| c = since $\map f x \in C$ 
}}
{{eqn	| r = \map {\paren {\phi \restriction C} } {\map g {\map f x} }
		| c = Continuous Functional Calculus Commutes with Character on Generated C*-Subalgebra
}}
{{eqn	| r = \map \phi {\map g {\map f x} }
}}
{{end-eqn}}
Hence we have:
:$\widehat {\map {\paren {g \circ f} } x} = \widehat {\map g {\map f x} }$
where $\hat \cdot$ is the Gelfand transform.
From Gelfand-Naimark Theorem: Commutative Case, we therefore have:
:$\map {\paren {g \circ f} } x = \map g {\map f x}$
{{qed}}
Category:Continuous Functional Calculus
9cd5a4aswa6olt5jh921jetqyxaabl1
Theorem: Normal Element of C*-Algebra is Hermitian iff Spectrum is Real

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $x \in A$ be normal. 
Let $\map {\sigma_A} x$ denote the spectrum of $x$ in $A$.
Then $x$ is Hermitian {{iff}}:
:$\map {\sigma_A} x \subseteq \R$

Proof:
We first take $A$ unital.
Theorem: Normal Element of Unital C*-Algebra is Unitary iff Spectrum is Subset of Unit Circle

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be normal. 
Let $\map {\sigma_A} x$ denote the spectrum of $x$ in $A$.
Then $x$ is unitary {{iff}}:
:$\map {\sigma_A} x \subseteq \set {z \in \C : \cmod z = 1}$

Proof:
=== Necessary Condition ===
Let $A' \subseteq A$ be the $\text C^\ast$-algebra generated by $\set { {\mathbf 1}_A, x}$. 
By C*-Algebra Generated by Commutative Self-Adjoint Set is Commutative, $A'$ is commutative.
Let $\Phi_{A'}$ be the spectrum of $A'$.
From Spectrum of Element of Unital C*-Subalgebra of Unital C*-Algebra, we have:
:$\map {\sigma_A} x = \map {\sigma_{A'} } x$
From Spectrum of Element of Unital Commutative Banach Algebra, we have $\map {\sigma_A} x = \map {\sigma_{A'} } x = \set {\map \phi x : \phi \in \Phi_{A'} }$. 
From Character on Unital C*-Algebra has Modulus One at Unitary Elements, we have $\cmod {\map \phi x} = 1$ for each $\phi \in \Phi_{A'}$.
Hence $\map {\sigma_A} x \subseteq \set {z \in \C : \cmod z = 1}$. 
{{qed|lemma}}
Theorem: Existence of Generated C*-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $S \subseteq A$.
Then there exists a $\text C^\ast$-subalgebra $B \subseteq A$ containing $S$ which is $\subseteq$-minimal among $\text C^\ast$-subalgebras with this property.

Proof:
Let $\SS$ be the set of $\text C^\ast$-subalgebras $C \subseteq A$ containing $S$.
We have $A \in \SS$ and hence $\SS \ne \O$.
Let $B = \bigcap \SS$.
From Intersection of C*-Subalgebras is C*-Subalgebra, $B$ is a $\text C^\ast$-algebra.
Further, since $S \subseteq C$ for each $C \in \SS$, we have $S \subseteq B$. 
We now just need to assure ourselves that $B \subseteq A$ is $\subseteq$-minimal in $\SS$.
Let $C \subseteq A$ be a $\text C^\ast$-subalgebra with $C \supseteq B$. 
Then $C \in \SS$.
Hence $B \subseteq C$ from Intersection is Subset.
So $B$ is $\subseteq$-minimal in $\SS$. 
{{qed}}
Category:C*-Algebras
dv88znuzc6pmd6fqru0k2p9t4s4ub77
Theorem: Unital C*-Algebra is Unital Banach Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra that is unital as an algebra, with identity element ${\mathbf 1}_A \ne {\mathbf 0}_A$.
Then $A$ is unital as a Banach algebra.

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \norm { {\mathbf 1}_A}^2
		| r = \norm { {\mathbf 1}_A {\mathbf 1}_A^\ast}
		| c = {{Defof|C*-Algebra}}
}}
{{eqn	| r = \norm { {\mathbf 1}_A^2}
		| c = Identity Element in Unital *-Algebra is Hermitian
}}
{{eqn	| r = \norm { {\mathbf 1}_A} 
}}
{{end-eqn}}
From {{NormAxiomVector|1}}, we have $\norm { {\mathbf 1}_A} \ne 0$. 
Hence $\norm { {\mathbf 1}_A} = 1$.
{{qed}}
Theorem: Surface Area of Cuboid

Let $\CC$ be a cuboid whose edges are of length $a$, $b$ and $c$.
The surface area $S$ of $\CC$ is given as:
:$S = 2 \paren {a b + b c + a c}$

Proof:
Each of the faces of $\CC$ are rectangles:
:$2$ of these faces are adjacent to edges of length $a$ and $b$
:$2$ of these faces are adjacent to edges of length $b$ and $c$
:$2$ of these faces are adjacent to edges of length $a$ and $c$.
Hence from Area of Rectangle:
:there are $2$ faces with area $a b$
:there are $2$ faces with area $a c$
:there are $2$ faces with area $b c$.
Hence the result.
{{qed}}
Theorem: Intersection of *-Subalgebras is *-Subalgebra

Let $\tuple {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ be an $I$-indexed family of $\ast$-subalgebras of $A$.
Let:
:$\ds B = \bigcap_{\alpha \mathop \in I} A_\alpha$
Then $B$ is a $\ast$-subalgebra of $A$.

Proof:
From Intersection of Subalgebras is Subalgebra, $B$ is a subalgebra of $A$.
It remains to show that for each $x \in B$ we have $x^\ast \in B$.
Let $x \in B$.
Then $x \in A_\alpha$ for each $\alpha \in I$. 
Since each $A_\alpha$ is a $\ast$-subalgebra, we have $x^\ast \in A_\alpha$ for each $\alpha \in I$. 
Hence we have:
:$\ds x^\ast \in \bigcap_{\alpha \mathop \in I} A_\alpha$
So $x^\ast \in B$.
{{qed}}
Category:*-Algebras
8gh42tn7whcl83k5sa1w10oh6jiklby
Theorem: Intersection of C*-Subalgebras is C*-Subalgebra

Let $\tuple {A, \norm {\, \cdot \,}, \ast}$ be a $\text C^\ast$-algebra.
Let $\family {A_\alpha}_{\alpha \mathop \in I}$ be an $I$-indexed family of $\text C^\ast$-subalgebras of $A$.
Let:
:$\ds B = \bigcap_{\alpha \mathop \in I} A_\alpha$
Then $B$ is a $\text C^\ast$-subalgebra of $A$.

Proof:
From Intersection of *-Subalgebras is *-Subalgebra, $B$ is a $\ast$-subalgebra of $A$. 
By definition, $A_\alpha$ is a complete metric subspace of $A$ for each $\alpha \in I$.
Hence from Subspace of Complete Metric Space is Closed iff Complete, $A_\alpha$ is closed in $A$.
Hence as the intersection of closed sets, $B$  is closed in $A$.
Hence from Closed *-Subalgebra of C*-Algebra is C*-Algebra, $B$ is a $\text C^\ast$-subalgebra of $A$.
{{qed}}
Category:C*-Algebras
hvkn2jbhf2byx48ji2cf6w9gnzuah30
Theorem: Continuous Function applied to Normal Element of Unital C*-Algebra is Positive iff Function is Non-Negative

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be normal. 
Let $\map {\sigma_A} x$ denote the spectrum of $x$ in $A$.
Let $f : \map {\sigma_A} x \to \C$ be continuous.
Let $\map {\Theta_x} f = \map f x$ be the continuous functional calculus of $x$ applied to $f$. 
Then $\map f x$ is positive {{iff}} $\map f z \in \hointr 0 \infty$ for each $z \in \map {\sigma_A} x$.

Proof:
From the definition of a positive element, we have that $\map f x$ is positive {{iff}} Hermitian and $\map {\sigma_A} {\map f x} \subseteq \hointr 0 \infty$. 
Note that $\map {\sigma_A} {\map f x} \subseteq \hointr 0 \infty$ implies that $\map {\sigma_A} {\map f x} \subseteq \R$. 
From Normal Element of C*-Algebra is Hermitian iff Spectrum is Real we have that $\map f x$ is Hermitian if $\map {\sigma_A} {\map f x} \subseteq \hointr 0 \infty$.
So $\map f x$ is positive {{iff}} $\map {\sigma_A} {\map f x} \subseteq \hointr 0 \infty$.
From the Spectral Mapping Theorem, we have:
:$\map {\sigma_A} {\map f x} = f \sqbrk {\map {\sigma_A} x}$
Hence we have $\map {\sigma_A} {\map f x} \subseteq \hointr 0 \infty$ {{iff}} $\map f z \in \hointr 0 \infty$ for each $z \in \map {\sigma_A} x$.
{{qed}}
Category:Positive Elements of C*-Algebras
Category:Continuous Functional Calculus
Category:Continuous Function applied to Normal Element of Unital C*-Algebra is Positive iff Function is Non-Negative
3r0gtesbnpr7cg1fan5vy1zkpvmkyvo