avewright/proofwiki-math huggingface dataset:
Theorem: Bound for Norm of Difference of Element with Non-Negative Multiple of Element in Unital C*-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra. 
Let $\le_A$ be the canonical preordering of $A$.
Let $a, b \in A$ be such that:
:${\mathbf 0}_A \le_A a \le_A b \le_A {\mathbf 1}_A$
Then we have:
:$\norm {x - b x}^2 \le \norm {x^\ast \paren { {\mathbf 1}_A - a} x}$
and:
:$\norm {x - x b}^2 \le \norm {x \paren { {\mathbf 1}_A - a} x^\ast}$
for each $x \in A$.

Proof:
We have from Scalar Multiplication by Minus One reverses Preordering in Vector Space:
:$-{\mathbf 1}_A \le_A -b \le_A -a \le_A {\mathbf 0}_A$
From $(1)$ in the definition of a preordered vector space, we have:
:${\mathbf 1}_A - {\mathbf 1}_A \le_A {\mathbf 1}_A - b \le_A {\mathbf 1}_A$
so that:
:${\mathbf 0}_A \le_A {\mathbf 1}_A - b \le_A {\mathbf 1}_A$
From Bounds on Hermitian Element of Unital C*-Algebra in terms of Bounds on Spectrum, we have:
:$\map {\sigma_A} { {\mathbf 1}_A - b} \subseteq \closedint 0 1$
We have:
{{begin-eqn}}
{{eqn	| l = \norm {x - b x}^2
		| r = \norm {\paren { {\mathbf 1}_A - b} x}^2
}}
{{eqn	| r = \norm {x^\ast \paren { {\mathbf 1}_A - b}^2 x}
		| c = {{Defof|C* Identity}}
}}
{{end-eqn}}
For $t \in \closedint 0 1$, we have:
:$0 \le t^2 \le t$ 
Hence we have:
:${\mathbf 0}_A \le_A \paren { {\mathbf 1}_A - b}^2 \le_A {\mathbf 1}_A - b$
from Continuous Function applied to Normal Element of Unital C*-Algebra is Positive iff Function is Non-Negative: Corollary.
From Conjugation in C*-Algebra preserves Positivity: Corollary, we have:
:${\mathbf 0}_A \le_A x^\ast \paren { {\mathbf 1}_A - b}^2 x \le_A x^\ast \paren { {\mathbf 1}_A - b} x$
From Norm Preserves Ordering on Positive Elements of C*-Algebra, we have:
:$\norm {x^\ast \paren { {\mathbf 1}_A - b}^2 x} \le \norm {x^\ast \paren { {\mathbf 1}_A - b} x}$
From the inequality:
:$-b \le_A -a$
we apply $(1)$ in the definition of a preordered vector space to obtain:
:${\mathbf 1}_A - b \le_A {\mathbf 1}_A - a$
Applying Conjugation in C*-Algebra preserves Positivity: Corollary, we have:
:${\mathbf 0}_A \le_A x^\ast \paren { {\mathbf 1}_A - b} x \le_A x^\ast \paren { {\mathbf 1}_A - a} x$
From Norm Preserves Ordering on Positive Elements of C*-Algebra, we have:
:$\norm {x^\ast \paren { {\mathbf 1}_A - b} x} \le \norm {x^\ast \paren { {\mathbf 1}_A - a} x}$
Hence we have shown:
:$\norm {x - b x}^2 \le \norm {x^\ast \paren { {\mathbf 1}_A - a} x}$
To finish we now have:
{{begin-eqn}}
{{eqn	| l = \norm {x - x b}^2
		| r = \norm {x^\ast - b x^\ast}^2
		| c = {{Defof|Banach *-Algebra}}
}}
{{eqn	| o = \le
		| r = \norm {\paren {x^\ast}^\ast \paren { {\mathbf 1}_A - a} x^\ast}
		| c = from what we have shown already
}}
{{eqn	| r = \norm {x \paren { {\mathbf 1}_A - a} x^\ast}
		| c = {{Defof|Involution on Algebra}}
}}
{{end-eqn}}
{{qed}}
Theorem: Vector Space obtains Norm Structure through Linear Isomorphism

Let $\GF \in \set {\R, \C}$. 
Let $X$ and $Y$ be vector spaces over $\GF$.
Let $\norm {\, \cdot \,}_Y$ be a norm on $Y$.
Let $\phi : X \to Y$ be a linear isomorphism.
Define $\norm {\, \cdot \,}_X : X \to \R$ by:
:$\norm x_X = \norm {\map \phi x}_Y$
for each $x \in X$.
Then $\norm {\, \cdot \,}_X$ is a norm on $X$.

Proof:
First since $\norm y_Y \in \hointr 0 \infty$ for each $y \in Y$, we have $\norm {\map \phi x}_Y \in \hointr 0 \infty$ for each $x \in X$.
Theorem: Algebra obtains Norm Structure through Algebra Isomorphism

Let $\GF \in \set {\R, \C}$. 
Let $A$ and $B$ be algebras over $\GF$.
Let $\norm {\, \cdot \,}_B$ be an algebra norm on $B$.
Let $\phi : A \to B$ be an algebra isomorphism.
Define $\norm {\, \cdot \,}_A : A \to \R$ by:
:$\norm a_A = \norm {\map \phi a}_B$
Then $\norm {\, \cdot \,}_A$ is an algebra norm on $A$.

Proof:
From Vector Space obtains Norm Structure through Linear Isomorphism:
:$\norm {\, \cdot \,}$ is a vector space norm on $A$.
We want to show that:
:$\norm {a b}_A \le \norm a_A \norm b_A$
for each $a, b \in A$.
Let $a, b \in A$.
We have:
{{begin-eqn}}
{{eqn	| l = \norm {a b}_A
		| r = \norm {\map \phi {a b} }_B 
}}
{{eqn	| r = \norm {\map \phi a \map \phi b}_B 
		| c = {{Defof|Algebra Homomorphism}}
}}
{{eqn	| o = \le 
		| r = \norm {\map \phi a}_B \norm {\map \phi b}_B 
		| c = {{Defof|Norm on Algebra}}
}}
{{eqn	| r = \norm a_A \norm b_A 
}}
{{end-eqn}}
So $\norm {\, \cdot \,}_A$ is an algebra norm.
{{qed}}
Category:Normed Algebras
0g570ggeo61onc4gi2u3xv4ojyc6nzx
Theorem: *-Algebra obtains Banach *-Algebra Structure through *-Algebra Isomorphism

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $\struct {B, \square, \norm {\, \cdot \,}_B}$ be a Banach $\ast$-algebra.
Let $\phi : A \to B$ be a $\ast$-algebra isomorphism. 
Define $\norm {\, \cdot \,}_A : A \to \R$ by:
:$\norm a_A = \norm {\map \phi a}_B$
Then $\struct {A, \ast, \norm {\, \cdot \,}_A}$ is a Banach $\ast$-algebra.
Further if $\struct {B, \square, \norm {\, \cdot \,}_B}$ is a $\text C^\ast$-algebra, then so is $\struct {A, \ast, \norm {\, \cdot \,}_A}$.

Proof:
From Algebra obtains Norm Structure through Algebra Isomorphism:
:$\norm {\, \cdot \,}_A$ is an algebra norm.
We want to show that:
:$\norm {a^\ast}_A = \norm a_A$
for each $a \in A$. 
Let $a \in A$.
We have:
{{begin-eqn}}
{{eqn	| l = \norm {a^\ast}_A
		| r = \norm {\map \phi {a^\ast} }_B 
}}
{{eqn	| r = \norm {\map \phi a^\square}_B 
		| c = {{Defof|*-Algebra Homomorphism}}
}}
{{eqn	| r = \norm {\map \phi a}_B 
		| c = {{Defof|Banach *-Algebra}} 
}}
{{eqn	| r = \norm a_A 
}}
{{end-eqn}}
By definition, $\phi : A \to B$ is an isometric isomorphism.
Hence from Inverse of Isometric Isomorphism between Normed Vector Spaces is Isometric Isomorphism, $\phi^{-1} : B \to A$ is an isometric isomorphism.
From Metric Space Completeness is Preserved by Isometry, the completeness of $B$ implies the completeness of $A$.
So $\struct {A, \norm {\, \cdot \,}_A}$ is a Banach algebra.
Hence $\struct {A, \ast, \norm {\, \cdot \,}_A}$ is a Banach $\ast$-algebra.
Now suppose that $\struct {B, \square, \norm {\, \cdot \,}_B}$ is a $\ast$-algebra so that:
:$\norm {b b^\square}_B = \norm b^2_B$
for each $b \in B$.
We want to show that:
:$\norm {a a^\ast}_A = \norm a^2_A$
for each $a \in A$.
We have:
{{begin-eqn}}
{{eqn	| l = \norm {a a^\ast}_A
		| r = \norm {\map \phi {a a^\ast} }_B 
}}
{{eqn	| r = \norm {\map \phi a \map \phi {a^\ast} }_B 
		| c = {{Defof|Algebra Homomorphism}}
}}
{{eqn	| r = \norm {\map \phi a \map \phi a^\square}_B 
		| c = {{Defof|*-Algebra Homomorphism}}
}}
{{eqn	| r = \norm {\map \phi a}_B^2 
}}
{{eqn	| r = \norm a_A^2 
}}
{{end-eqn}}
{{qed}}
Category:Banach *-Algebras
Category:C*-Algebras
n5pjpmicslbzshzaba8vagpcd0mqkbm
Theorem: Direct Product of Algebras is Algebra

Let $K$ be a field.
Let $A$ and $B$ be algebras over $K$. 
Let $\tuple {A \times B, +_{A \times B}, \cdot_{A \times B} }$ be the direct product of $A$ and $B$ as vector spaces.
Define $\cdot_{A \times B} : A \times B \to A \times B$ by:
:$\tuple {a, b} \tuple {a', b'} = \tuple {a a', b b'}$
for each $\tuple {a, b}, \tuple {a', b'} \in A \times B$. 
Then $\tuple {A \times B, +_{A \times B}, \cdot_{A \times B}, \circ_{A \times B} }$ is an algebra.

Proof:
We show that $\circ_{A \times B}$ is bilinear.
Let $\lambda \in K$ and $\tuple {a_1, b_1}, \tuple {a_2, b_2}, \tuple {a_3, b_3} \in A \times B$ .
We have:
{{begin-eqn}}
{{eqn	| l = \paren {\tuple {a_1, b_1} +_{A \times B} \lambda \tuple {a_2, b_2} } \circ_{A \times B} \tuple {a_3, b_3}
		| r = \tuple {a_1 + \lambda a_2, b_1 + \lambda b_2} \circ_{A \times B} \tuple {a_3, b_3} 
}}
{{eqn	| r = \tuple {\paren {a_1 + \lambda a_2} a_3, \paren {b_1 + \lambda b_2} b_3} 
}}
{{eqn	| r = \tuple {a_1 a_3 + \lambda a_2 a_3, b_1 b_3 + \lambda b_2 b_3} 
}}
{{eqn	| r = \tuple {a_1 a_3, b_1 b_3} +_{A \times B} \lambda \tuple {a_2 a_3, b_2 b_3} 
}}
{{eqn	| r = \tuple {a_1, b_1} \circ_{A \times B} \tuple {a_3, b_3} +_{A \times B} \lambda \paren {\tuple {a_2, b_2} \circ_{A \times B} \tuple {a_3, b_3} }
}}
{{end-eqn}}
We also have:
{{begin-eqn}}
{{eqn	| l = \tuple {a_1, b_1} \circ_{A \times B} \paren { \tuple {a_2, b_2} +_{A \times B} \lambda \tuple {a_3, b_3} }
		| r = \tuple {a_1, b_1} \circ_{A \times B} \tuple {a_2 + \lambda a_3, b_2 + \lambda b_3} 
}}
{{eqn	| r = \tuple {a_1 \paren {a_2 + \lambda a_3}, b_1 \paren {b_2 + \lambda b_3} }
}}
{{eqn	| r = \tuple {a_1 a_2 + \lambda a_1 a_3, b_1 b_2 + \lambda b_1 b_3} 
}}
{{eqn	| r = \tuple {a_1 a_2, b_1 b_2} +_{A \times B} \lambda \tuple {a_1 a_3, b_1 b_3}
}}
{{eqn	| r = \tuple {a_1, b_1} \circ_{A \times B} \tuple {a_2, b_2} +_{A \times B} \lambda \paren {\tuple {a_1, b_1} \circ_{A \times B} \tuple {a_3, b_3} }
}}
{{end-eqn}}
So $\circ_{A \times B}$ is bilinear and $\tuple {A \times B, +_{A \times B}, \cdot_{A \times B}, \circ_{A \times B} }$ is an algebra.
{{qed}}
Category:Algebras over Fields
1kxngs8erq33ajl6jqzb762ovpd5rxc
Theorem: Direct Product of Normed Algebras is Normed Algebra with Direct Product Norm

Let $\GF \in \set {\R, \C}$. 
Let $\struct {A, \norm {\, \cdot \,}_A}$ and $\struct {B, \norm {\, \cdot \,}_B}$ be normed algebras over $\GF$.
Let $A \times B$ be the direct product of $A$ and $B$.
Let $\norm {\, \cdot \,}_{A \times B}$ be the direct product norm on $A \times B$.
Then $\struct {A \times B, \norm {\, \cdot \,}_{A \times B} }$ is a normed algebra.

Proof:
From Direct Product Norm is Norm, $\struct {A \times B, \norm {\, \cdot \,}_{A \times B} }$ is a normed vector space.
We just need to show that $\norm {\, \cdot \,}_{A \times B}$ is an algebra norm.
Let $\tuple {a, b}, \tuple {a', b'} \in A \times B$. 
We hae:
:$\norm {\tuple {a, b} \tuple {a', b'} }_{A \times B} = \norm {\tuple {a a', b b'} }_{A \times B} = \max \set {\norm {a a'}_A, \norm {b b'}_B}$
Since $\norm {\, \cdot \,}$ is an algebra norm, we have:
:$\norm {a a'}_A \le \norm a_A \norm {a'}_A \le \max \set {\norm a_A, \norm b_B} \max \set {\norm {a'}, \norm {b'}_B}$
and:
:$\norm {b b'}_B \le \norm b_B \norm {b'}_B \le \max \set {\norm a_A, \norm b_B} \max \set {\norm {a'}, \norm {b'}_B}$
Hence we obtain:
:$\max \set {\norm {a a'}_A, \norm {b b'}_B} \le \max \set {\norm a_A, \norm b_B} \max \set {\norm {a'}, \norm {b'}_B}$
that is:
:$\norm {\tuple {a a', b b'} }_{A \times B} \le \norm {\tuple {a, b} }_{A \times B} \norm {\tuple {a', b'} }_{A \times B}$
{{qed}}
Category:Normed Algebras
i8oizfiyug35fj5fn8eabidv52uj6h7
Theorem: Direct Product of *-Algebras is *-Algebra

Let $\tuple {A, \square}$ and $\tuple {B, \diamond}$ be $\ast$-algebras over $\C$. 
Let $A \times B$ be the direct product of $A$ and $B$.
Define $\ast : A \times B \to A \times B$ by:
:$\tuple {a, b}^\ast = \tuple {a^\square, b^\diamond}$
for each $\tuple {a, b} \in A \times B$. 
Then $\tuple {A \times B, \ast}$ is a $\ast$-algebra.

Proof:
We show that $\ast$ is a involution.
Theorem: Direct Product of C*-Algebras is C*-Algebra

Let $\struct {A, \square, \norm {\, \cdot \,}_A}$ and $\struct {B, \diamond, \norm {\, \cdot \,}_B}$ be $\text C^\ast$-algebras.
Let $A \times B$ be the direct product of $A$ and $B$.
Define $\ast : A \times B \to A \times B$ by:
:$\tuple {a, b}^\ast = \tuple {a^\square, b^\diamond}$
for each $\tuple {a, b} \in A \times B$.
Let $\norm {\, \cdot \,}_{A \times B}$ be the direct product norm on $A \times B$. 
Then $\struct {A \times B, \ast, \norm {\, \cdot \,}_{A \times B} }$ is a $\text C^\ast$-algebra.

Proof:
From Direct Product of Normed Algebras is Normed Algebra with Direct Product Norm, $\struct {A \times B, \norm {\, \cdot \,}_{A \times B} }$ is a normed algebra. 
From Direct Product of Banach Spaces is Banach Space, $\struct {A \times B, \norm {\, \cdot \,}_{A \times B} }$ is a Banach algebra. 
From Direct Product of *-Algebras is *-Algebra, $\struct  {A \times B, \ast}$ is a $\ast$-algebra.
It remains to show $(\text C^\ast 5)$, that:
:$\norm {\tuple {a, b} \tuple {a, b}^\ast}_{A \times B} = \norm {\tuple {a, b} }^2_{A \times B}$
for each $\tuple {a, b} \times A \times B$. 
We have:
{{begin-eqn}}
{{eqn	| l = \norm {\tuple {a, b} \tuple {a, b}^\ast}_{A \times B}
		| r = \norm {\tuple {a, b} \tuple {a^\square, b^\diamond} }_{A \times B}
}}
{{eqn	| r = \norm {\tuple {a a^\square, b b^\diamond} }_{A \times B}
}}
{{eqn	| r = \max \set {\norm {a a^\square}_A, \norm {b b^\diamond}_B}
}}
{{eqn	| r = \max \set {\norm a^2_A, \norm b^2_B}
		| c = $(\text C^\ast 5)$ in {{Defof|C*-Algebra}}
}}
{{eqn	| r = \max \set {\norm a_A, \norm b_B}^2
		| c = since $\norm a_A, \norm b_B \ge 0$
}}
{{eqn	| r = \norm {\tuple {a, b} }^2_{A \times B}
}}
{{end-eqn}}
{{qed}}
Category:C*-Algebras
9hcvuhsbtosec5b4550tpucvxlpwj00
Theorem: Unitization of *-Algebra is *-Algebra

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $A_+$ be the unitization of $A$.
Define:
:$\tuple {a, \lambda}^\dagger = \tuple {a^\ast, \overline \lambda}$
for each $\tuple {a, \lambda} \in A_+$.
Then $\struct {A_+, \dagger}$ is a $\ast$-algebra.

Proof:
=== Proof of $(\text C^\ast 1)$ ===
Let $\tuple {a, \lambda} \in A_+$.
We have:
{{begin-eqn}}
{{eqn	| l = \tuple {a, \lambda}^{\dagger \dagger }
		| r = \tuple {a^\ast, \overline \lambda}^\dagger
}}
{{eqn	| r = \tuple {a^{\ast \ast}, \overline {\overline \lambda} }
}}
{{eqn	| r = \tuple {a, \lambda}
		| c = $(\text C^\ast 1)$ from {{Defof|Involution on Algebra}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Continuous Functional Calculus of Reciprocal is Inverse Element

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $x \in A$ be normal and invertible.
Let $\map {\sigma_A} x$ be the spectrum of $x$ in $A$.
Let $\Theta_x$ be the continuous functional calculus for $x$.
Let $\iota : \map {\sigma_A} x \to \C$ be the inclusion.
Define $1/\iota : \map {\sigma_A} x \to \C$ by:
:$\map {\paren {1/\iota} } z = \dfrac 1 z$
for each $z \in \map {\sigma_A} x$.
Then:
:$\map {\Theta_x} {1/\iota} = x^{-1}$

Proof:
Since $x$ is invertible, we have that $0 \not \in \map {\sigma_A} x$ and indeed $1/\iota$ is well-defined.
We have:
{{begin-eqn}}
{{eqn	| l = x \map {\Theta_x} {1/\iota}
		| r = \map {\Theta_x} \iota \map {\Theta_x} {1/\iota}
		| c = {{Defof|Continuous Functional Calculus}}
}}
{{eqn	| r = \map {\Theta_x} 1
		| c = since $\Theta_x$ is an algebra homomorphism
}}
{{eqn	| r = {\mathbf 1}_A
		| c = since $\Theta_x$ is unital
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \map {\Theta_x} {1/\iota} x
		| r = \map {\Theta_x} {1/\iota} \map {\Theta_x} \iota
		| c = {{Defof|Continuous Functional Calculus}}
}}
{{eqn	| r = \map {\Theta_x} 1
		| c = since $\Theta_x$ is an algebra homomorphism
}}
{{eqn	| r = {\mathbf 1}_A
		| c = since $\Theta_x$ is unital
}}
{{end-eqn}}
Hence we have:
:$\map {\Theta_x} {1/\iota} = x^{-1}$
{{qed}}
Category:Continuous Functional Calculus
plgmmpyyb1p457dydxxalgvibhlc3na
Theorem: Vector Subspace of Algebra over Field Embeds into Unitization as Vector Subspace

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

Proof:
Clearly $B_0 \ne \O$. 
From One-Step Vector Subspace Test, it is sufficient to show that for each $u, v \in B_0$ and $\lambda \in K$, we have:
:$u + \lambda v \in B_0$
Let $u, v \in B_0$ and $\lambda \in K$. 
Then there exists $x, y \in A$ such that:
:$u = \tuple {x, 0_K}$
and:
:$v = \tuple {y, 0_K}$
Then by the definition of the unitization, we have:
:$\tuple {x, 0_K} + \lambda \tuple {y, 0_K} = \tuple {x + \lambda y, 0_K} \in B_0$
So by the One-Step Vector Subspace Test, $B_0$ is a vector subspace of $A_+$.
{{qed}}
Category:Unitizations of Algebras over Fields
52amffwcx0jinhg168tscvhlix4a4dr
Theorem: Ideal of Algebra over Field Embeds into Unitization as Ideal

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

Proof:
From the definition of an ideal, $I$ is a vector subspace of $A$. 
Hence from Vector Subspace of Algebra over Field Embeds into Unitization as Vector Subspace, $I_0$ is a vector subspace of $A_+$. 
Let $\tuple {x, 0_K} \in I$ and $\tuple {y, \lambda} \in A_+$. 
Then we have:
:$\tuple {x, 0_K} \tuple {y, \lambda} = \tuple {x y + \lambda x, 0_K}$
Since $I$ is an ideal, we have $x y \in I$.
Since $I$ is a vector subspace of $A$, we have $x y + \lambda x \in I$.
Hence we have $\tuple {x, 0_K} \tuple {y, \lambda} \in I_0$.
Similarly we have:
:$\tuple {y, \lambda} \tuple {x, 0_K} = \tuple {y x + \lambda x, 0_K}$
Since $I$ is an ideal, we have $y x \in I$.
Since $I$ is a vector subspace of $A$, we have $y x + \lambda x \in I$.
Hence we have $\tuple {y, \lambda} \tuple {x, 0_K} \in I_0$.
{{qed}}
Category:Unitizations of Algebras over Fields
2n5eq4bp91ck0e5x2ft720xxtkpm44s
Theorem: Set of Positive Elements of Everywhere Dense Ideal is Dense in Set of Positive Elements of C*-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $I$ be an everywhere dense ideal of $A$.
Let $A^+$ be the set of positive elements of $A$.
Let $I^+ = I \cap A^+$.
Then $I^+$ is everywhere dense in $A^+$.

Proof:
Let $x \in A^+$. 
From Existence and Uniqueness of Positive Nth Root of Positive Element of C*-Algebra, there exists a positive $y \in A$ such that $x = y^2$.
Since $I$ is everywhere dense in $A$, there exists a sequence $\sequence {y_n}_{n \mathop \in \N}$ in $I$ such that $y_n \to y$. 
From Product of Element of C*-Algebra with its Star is Positive, we have that $y_n^\ast y_n$ is positive for each $n \in \N$. 
Further since $I$ is an ideal, we have $y_n^\ast y_n \in I$ for each $n \in \N$. 
Hence $y_n^\ast y_n \in I^+$ for each $n \in \N$. 
From Multiplication on Normed Algebra is Continuous and since $\ast$ is an isometry, we have $y_n^\ast y_n \to y^\ast y = y^2 = x$ as $n \to \infty$. 
Hence $\sequence {y_n^\ast y_n}_{n \mathop \in \N}$ is a sequence in $I^+$ converging to $x$. 
Hence $I_+$ is everywhere dense in $A^+$.
{{qed}}
Category:Positive Elements of C*-Algebras
7ht9simlyqmosxgsnwwpj7xy1ka4e9g
Theorem: Approximate Identity for Everywhere Dense Subset is Approximate Identity of C*-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\DD \subseteq A$ be everywhere dense.
Let $\tuple {\Lambda, \preceq}$ be a directed set. 
Let $\family {e_\lambda}_{\lambda \in \Lambda}$ be a net such that: 
:$e_\lambda$ is Hermitian for each $\lambda \in \Lambda$ with $\map {\sigma_A} {e_\lambda} \subseteq \closedint 0 1$
:for each $x \in \DD$, $\family {x e_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$.
Then $\family {e_\lambda}_{\lambda \mathop \in \Lambda}$ is an approximate identity of $A$.

Proof:
We only need to show that for each $x \in A$, the net $\family {x e_\lambda}_{\lambda \mathop \in \Lambda}$ converges to $x$. 
First, for each $\lambda \in \Lambda$ we have:
:$\map {\sigma_A} {e_\lambda} \subseteq \closedint 0 1$
Hence, from the definition of spectral radius:
:$\map {r_A} {e_\lambda} \le 1$ 
From Spectral Radius of Normal Element of C*-Algebra Equal to Norm, we have $\norm {e_\lambda} \le 1$ for each $\lambda \in \Lambda$.
Let $x \in A$. 
Let $\epsilon > 0$.
Since $\DD$ is everywhere dense in $A$, there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $\DD$ with $x_n \to x$. 
Now, we have:
{{begin-eqn}}
{{eqn	| l = \norm {x - x e_\lambda}
		| o = \le
		| r = \norm {\paren {x - x_n} - \paren {x - x_n} e_\lambda} + \norm {x_n - x_n e_\lambda}
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| o = \le
		| r = \norm {x - x_n} + \norm {\paren {x - x_n} e_\lambda} + \norm {x_n - x_n e_\lambda} 
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| o = \le
		| r = 2 \norm {x - x_n} + \norm {x_n - x_n e_\lambda}
		| c = {{Defof|Norm on Algebra}} and $\norm {e_\lambda} \le 1$
}}
{{end-eqn}}
Take $n \in \N$ large enough to have:
:$\norm {x - x_n} < \dfrac \epsilon 3$ 
By hypothesis, since $x_n \in \DD$, we can take $a \in \Lambda$ such that for $\lambda \succeq a$ we have:
:$\norm {x_n - x_n e_\lambda} < \dfrac \epsilon 3$
Then for $\lambda \succeq a$ we have:
:$\norm {x - x e_\lambda} < \epsilon$
Hence the net $\family {x e_\lambda}_{\lambda \in \Lambda}$ converges to $x$. 
So $\family {e_\lambda}_{\lambda \mathop \in \Lambda}$ is an approximate identity of $A$.
{{qed}}
Category:Approximate Identities of C*-Algebras
ehra0l1g5o6oia8yqukoejwjsta58a3
Theorem: Locale Isomorphism is Isomorphism in Loc

Let $\mathbf{Loc}$ denote the category of locales.
Let $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ be locales.
Let $f:S_1 \to S_2$ be a continuous map of $\mathbf{Loc}$.
Then:
:$f$ is an isomorphism of $\mathbf{Loc}$ {{iff}} $f$ is a locale isomorphism.

Proof:
By definition of category of locales:
:$\mathbf{Loc}$ is the dual category of the category of frames $\mathbf{Frm}$
From Isomorphism iff Isomorphism in Dual Category:
:$f$ is an isomorphism of $\mathbf{Loc}$
{{iff}}:
:$f = h^{\text{op}}$ for some isomorphism $h$ in $\mathbf{Frm}$
From Frame Isomorphism is Isomorphism in Category Frm:
:$h$ is an isomorphism in $\mathbf{Frm}$
{{iff}}:
:$h$ is a frame isomorphism
By definition of locale isomorphism:
:$f$ is a locale isomorphism
{{iff}}:
:$f = h^{\text{op}}$ for some frame homomorphism
The result follows.
{{qed}}
Category:Locales
rs6vpj1m1x4aod4guiyh5vwx7qqhvwn
Theorem: Star of Closed Subset of Banach *-Algebra is Closed

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a Banach $\ast$-algebra over $\C$.
Let $C \subseteq A$ be closed.
Let:
:$C^\ast = \set {x^\ast : x \in C}$
Then $C^\ast$ is closed.

Proof:
Define $\phi : A \to A$ by $\map \phi a = a^\ast$ for each $a \in A$.
We have $C^\ast = \phi \sqbrk C$. 
From the definition of a Banach $\ast$-algebra, we have $\norm {\map \phi a} = \norm a$.
We have $\map \phi {a - b} = \map \phi a - \map \phi b$ for each $a, b \in A$ so:
:$\norm {a - b} = \norm {\map \phi a - \map \phi b}$ for each $a, b \in A$.
By the proof of Image of Closed Set under Linear Isometry from Banach Space to Normed Vector Space is Closed, $C^\ast$ is then closed.
{{qed}}
Category:Banach *-Algebras
c3c6t6s02aezafgqeruyc8lbq7nsfrz
Theorem: Intersection of Algebra Ideals is Ideal

Let $K$ be a field.
Let $A$ be an algebra over $K$.
Let $\family {I_\alpha}_{\alpha \mathop \in I}$ be an $I$-indexed family of ideals of $A$.
Let:
:$\ds I = \bigcap_{\alpha \mathop \in I} I_\alpha$
Then $I$ is an ideal of $A$.

Proof:
From Set of Linear Subspaces is Closed under Intersection, $I$ is a vector subspace of $A$.
Now, let $a, b \in I$.
Then we have $a, b \in I_\alpha$ for all $\alpha \in I$. 
Since $I_\alpha$ is an ideal for each $\alpha \in I$, we have $a b \in I_\alpha$ and $b a \in I_\alpha$ for each $\alpha \in I$.
Hence we have $a b \in I$ and $b a \in I$. 
So $I$ is an ideal of $A$.
{{qed}}
Category:Ideals of Algebras
Category:Set Intersection
9h0q0qig0eued6r8oupruizosjoeytw
Theorem: Star of Vector Subspace of *-Algebra is Vector Subspace

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$. 
Let $B$ be a vector subspace of $A$.
Define:
:$B^\ast = \set {x^\ast : x \in B}$ 
Then $B^\ast$ is a vector subspace of $A$.

Proof:
We use the One-Step Vector Subspace Test.
From Zero Vector in *-Algebra is Hermitian, we have:
:${\mathbf 0}_A^\ast = {\mathbf 0}_A$
Hence ${\mathbf 0}_A \in B$.
In particular $B \ne \O$. 
Now let $u, v \in B^\ast$ and $\lambda \in \C$.
We can then write $u = x^\ast$ and $v = y^\ast$ for $x, y \in B$. 
Then we have:
{{begin-eqn}}
{{eqn	| l = u + \lambda v
		| r = x^\ast + \lambda y^\ast 
}}
{{eqn	| r = x^\ast + \paren {\overline \lambda}^\ast 
		| c = $(\text C^\ast 4)$ in {{Defof|Involution on Algebra}}
}}
{{eqn	| r = \paren {x + \overline \lambda y}^\ast 
		| c = $(\text C^\ast 2)$ in {{Defof|Involution on Algebra}} 
}}
{{end-eqn}}
Since $B$ is a vector subspace, we have $x + \overline \lambda y \in B$.
Hence $u + \lambda v \in B^\ast$.
So by One-Step Vector Subspace Test, $B^\ast$ is a vector subspace of $A$.
{{qed}}
Category:*-Algebras
pxov1ohz3bz0dh6ffe7a86g0l6ghguu