avewright/proofwiki-math huggingface dataset:
Theorem: Spectrum of Projection in *-Algebra/Corollary

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $p$ be a projection on $A$.
Let $\map {\sigma_A} p$ be the spectrum of $p$ in $A$.
Then:
:$p = {\mathbf 0}_A$ {{iff}} $\map {\sigma_A} p = \set 0$
:$p = {\mathbf 1}_A$ {{iff}} $\map {\sigma_A} p = \set 1$
:$p \not \in \set { {\mathbf 0}_A, {\mathbf 1}_A}$ {{iff}} $\map {\sigma_A} p = \set {0, 1}$.

Proof:
Note first that since $p$ is Hermitian, it is normal.
Theorem: Normal Element of C*-Algebra is Projection iff Spectrum contains only Zero and One

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

Proof:
We first take $A$ unital.
Theorem: Platonic Solid is Isogonal

Let $P$ be a Platonic solid.
Then $P$ is also isogonal.

Proof:
{{ProofWanted|Various symmetry group realizations, or just rotational arguments needed}}
Category:Platonic Solids
Category:Isogonal Polyhedra
b2hvdb6lu9ewgzshyaal0klbiipx5so
Theorem: Platonic Solid is Uniform Polyhedron

Let $P$ be a Platonic solid.
Then $P$ is also uniform.

Proof:
{{Recall|Uniform Polyhedron}}
{{:Definition:Uniform Polyhedron}}
{{Recall|Platonic Solid}}
{{:Definition:Platonic Solid}}
From Platonic Solid is Isogonal, $P$ is isogonal.
That all the faces are regular polygons follows {{afortiori}}.
Hence the result.
{{qed}}
Theorem: Characterization of Partial Isometries

Let $\struct {\HH_1, \innerprod \cdot \cdot_1}$ and $\struct {\HH_2, \innerprod \cdot \cdot_2}$ be Hilbert spaces. 
Let $T : \HH_1 \to \HH_2$ be a bounded linear transformation.
{{TFAE}}
:$(1) \quad$ $T$ is a partial isometry
:$(2) \quad$ $T = T T^\ast T$
:$(3) \quad$ $T^\ast T$ is a Hilbert space projection
:$(4) \quad$ $T T^\ast$ is a Hilbert space projection.

Proof:
=== $(2)$ implies $(3)$ ===
Suppose that $T = T T^\ast T$.
We then have $T^\ast T = T^\ast \paren {T T^\ast T} = \paren {T^\ast T}^2$.
From Product of Element in *-Star Algebra with its Star is Hermitian, $T^\ast T$ is Hermitian.
Hence from Characterization of Projections, $T^\ast T$ is a Hilbert space projection.
{{qed|lemma}}
Theorem: Uniform Prism is Uniform Polyhedron

Let $P$ be a uniform prism.
Then $P$ is a uniform polyhedron.

Proof:
{{Recall|Uniform Polyhedron}}
{{:Definition:Uniform Polyhedron}}
{{Recall|Uniform Prism}}
{{:Definition:Uniform Prism}}
From Uniform Prism is Isogonal, $P$ is isogonal.
That all the faces of $P$ are regular polygons follows {{afortiori}} from the definition of regular prism.
Hence the result.
{{qed}}
Theorem: Uniform Antiprism is Uniform Polyhedron

Let $P$ be a uniform antiprism.
Then $P$ is a uniform polyhedron.

Proof:
{{Recall|Uniform Polyhedron}}
{{:Definition:Uniform Polyhedron}}
{{Recall|Uniform Antiprism}}
{{:Definition:Uniform Antiprism}}
From Uniform Antiprism is Isogonal, $P$ is isogonal.
Hence the result.
{{qed}}
Theorem: Extension of Bounded Linear Transformation from Closed Subspace of Hilbert Space to Whole Space

Let $\GF \in \set {\R, \C}$.
Let $\struct {\HH_1, \innerprod \cdot \cdot_1}$ and $\struct {\HH_2, \innerprod \cdot \cdot_2}$ be Hilbert spaces over $\GF$.
Let $\KK_1$ and $\KK_2$ be closed linear subspaces of $\HH_1$ and $\HH_2$ respectively.
Let $T_1 : \KK_1 \to \KK_2$ be a bounded linear transformation.
Let $\KK_1^\bot$ of $\KK_2^\bot$ be the orthocomplements of $\KK_1$ and $\KK_2$ respectively.
Let $T_2 : \KK_1^\bot \to \KK_2^\bot$ be a bounded linear transformation.
Define $T : \HH_1 \to \HH_2$ by:
:$\map T {u + v} = T_1 u + T_2 v$
for each $u \in \KK_1$ and $v \in \KK_1^\bot$. 
Then $T$ is a bounded linear transformation extending $T_1$.

Proof:
We first show that $T$ is well-defined. 
Let $u_1, u_2 \in \KK_1$ and $v_1, v_2 \in \KK_2$.
From Direct Sum of Subspace and Orthocomplement, we have $\KK_1 \oplus \KK_1^\bot = \HH_1$ as an internal direct sum.
Hence $\KK_1 \cap \KK_1^\bot = \set { {\mathbf 0}_\HH}$, and if $u_1 + v_1 = u_2 + v_2$, then $u_1 = u_2$ and $v_1 = v_2$.
Hence $T$ is well-defined.
We show that $T$ is linear.
Let $x, y \in \HH$ and $\lambda \in \GF$. 
Since $\KK_1 \oplus \KK_1^\bot = \HH_1$, there exists $u_1, u_2 \in \KK_1$ and $v_1, v_2 \in \KK_1^\bot$ such that:
:$x = u_1 + v_1$
and:
:$y = u_2 + v_2$
We then have:
:$x + \lambda y = \paren {u_1 + \lambda u_2} + \paren {v_1 + \lambda v_2}$
where $u_1 + \lambda u_2 \in \KK_1$ and $v_1 + \lambda v_2 \in \KK_1^\bot$.
Hence:
{{begin-eqn}}
{{eqn	| l = \map T {x + \lambda y}
		| r = \map {T_1} {u_1 + \lambda v_1} + \map {T_2} {u_2 + \lambda v_2}
}}
{{eqn	| r = T_1 u_1 + T_2 u_2 + \lambda \paren {T_1 v_1 + T_2 v_2}
		| c = $T_1$, $T_2$ are linear 
}}
{{eqn	| r = \map T {u_1 + u_2} + \lambda \map T {v_1 + v_2}
		| c = construction of $T$ 
}}
{{eqn	| r = T x + \lambda T y
}}
{{end-eqn}}
So $T$ is linear.
We show that $T$ is bounded.
Let $x \in \HH$ and take $u \in \KK_1$, $v \in \KK_1^\bot$ such that $x = u + v$.
We then have:
{{begin-eqn}}
{{eqn	| l = \norm {T x}^2_2
		| r = \norm {T_1 u + T_2 v}^2_2
}}
{{eqn	| r = \norm {T_1 u}^2_2 + \norm {T_2 v}^2_2
		| c = from Pythagoras's Theorem (Inner Product Space) since $T_1 u \in K_1$ and $T_2 v \in K_1^\bot$, so $T_1 u \perp T_2 v$
}}
{{eqn	| o = \le 
		| r = M_1 \norm u^2_1 + M_2 \norm v^2_1
		| c = {{Defof|Bounded Linear Transformation}}
}}
{{eqn	| o = \le 
		| r = \max \set {M_1, M_2} \paren {\norm u^2_1 + \norm v^2_1} 
}}
{{eqn	| r = \max \set {M_1, M_2} \norm {u + v}^2_1
		| c = from Pythagoras's Theorem (Inner Product Space) since $u \perp v$
}}
{{eqn	| r = \max \set {M_1, M_2} \norm x_1^2 
}}
{{end-eqn}}
We conclude that:
:$\norm {T x}_2 \le \sqrt {\max \set {M_1, M_2} } \norm x_1$ 
for each $x \in \HH$.
So $T$ is a bounded transformation.
Finally, for $x \in \KK_1$ we have:
:$T x = \map T {x + {\mathbf 0}_\HH} = T_1 x + \map {T_2} { {\mathbf 0}_\HH} = T_1 x$
since $T_2$ is linear.
Hence $T$ extends $T_1$.
{{qed}}
Category:Bounded Linear Transformations
Category:Hilbert Spaces
5pzj0lxkbwb5v0pufa6yu54btfy0wz6
Theorem: Orthocomplement of Closure

Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space.
Let $S \subseteq V$ be non-empty.
Then:
:$S^\bot = \map \cl S^\bot$
where $\bot$ denotes orthocomplementation.

Proof:
From Orthocomplement Reverses Subset, we have:
:$\map \cl S^\bot \subseteq S^\bot$
Conversely, let $y \in S^\bot$.
Let $x \in \map \cl S$.
Then there exists a sequence $\sequence {x_n}_{n \mathop \in \N}$ in $S$ such that $x_n \to x$.
Since $y \in S^\bot$, we have $\innerprod {x_n} y = 0$ for each $n \in \N$.
From Inner Product is Continuous, we have $\innerprod x y = 0$ taking $n \to \infty$.
Since $x \in \map \cl S$ was arbitrary we have $y \in \map \cl S^\bot$.
{{qed}}
Category:Orthocomplements
1d95mok7tljc5zy91lw3yeqaucqfow5
Theorem: *-Algebra Homomorphism between C*-Algebras is Norm-Decreasing

Let $\struct {A, \ast, \norm {\, \cdot \,}_A}$ and $\struct {B, \dagger, \norm {\, \cdot \,}_B}$ be $\text C^\ast$-algebras.
Let $\phi : A \to B$ be a $\ast$-algebra homomorphism.
Then:
:$\norm {\map \phi x}_B \le \norm x_A$ for each $x \in A$.

Proof:
Let $x \in A$.
Then:
{{begin-eqn}}
{{eqn	| l = \norm {\map \phi x}^2_B
		| r = \norm {\map \phi x \paren {\map \phi x}^\dagger}_B 
		| c = {{Defof|C*-Algebra}}
}}
{{eqn	| r = \map {r_B} {\map \phi x \paren {\map \phi x}^\dagger}
		| c = Spectral Radius of Normal Element of C*-Algebra Equal to Norm
}}
{{eqn	| r = \map {r_B} {\map \phi {x x^\ast} }
		| c = {{Defof|*-Algebra Homomorphism}}
}}
{{end-eqn}}
From Spectrum of Image of Element of Unital Algebra under Unital Algebra Homomorphism: Corollary, we have:
:$\map {\sigma_B} {\map \phi {x x^\ast} } \cup \set 0 \subseteq \map {\sigma_A} {x x^\ast} \cup \set 0$ 
Hence we have:
{{begin-eqn}}
{{eqn	| l = \map {r_B} {\map \phi {x x^\ast} }
		| r = \sup \set {\cmod z : z \in \map {\sigma_B} {\map \phi {x x^\ast} } }
		| c = {{Defof|Spectral Radius}}
}}
{{eqn	| r = \sup \set {\cmod z : z \in \map {\sigma_B} {\map \phi {x x^\ast} } \cup \set 0}
}}
{{eqn	| o = \le
		| r = \sup \set {\cmod z : z \in \map {\sigma_A} {x x^\ast} \cup \set 0}
		| c = since $\map {\sigma_B} {\map \phi {x x^\ast} } \cup \set 0 \subseteq \map {\sigma_A} {x x^\ast} \cup \set 0$
}}
{{eqn	| r = \sup \set {\cmod z : z \in \map {\sigma_A} {x x^\ast} }
}}
{{eqn	| r = \map {r_A} {x x^\ast}
		| c = {{Defof|Spectral Radius}}
}}
{{eqn	| r = \norm {x x^\ast}_A
		| c = Spectral Radius of Normal Element of C*-Algebra Equal to Norm
}}
{{eqn	| r = \norm x^2_A
		| c = {{Defof|C*-Algebra}}
}}
{{end-eqn}}
Hence we obtain:
:$\norm {\map \phi x}_B^2 \le \norm x^2_A$
So:
:$\norm {\map \phi x}_B \le \norm x_A$ for each $x \in A$. 
{{qed}}
Category:C*-Algebras
thafnrvwopjq2bxzk6euwn55ktmny6m
Theorem: Linear Functional on *-Algebra Real-Valued at Hermitian Elements preserves Star

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $f : A \to \C$ be a linear functional such that:
:for each $x \in A$ Hermitian, we have $\map \phi x \in \R$.
Then:
:$\overline {\map \phi x} = \map \phi {x^\ast}$ for each $x \in A$.

Proof:
Let $x \in A$.
From Element of *-Algebra Uniquely Decomposes into Hermitian Elements, there exists Hermitian $b, c \in A$ such that:
:$x = b + i c$
Then:
:$x^\ast = b - i c$
by $(\text C^\ast 2)$ and $(\text C^\ast 4)$ in the definition of an involution.
By hypothesis we have $\map \phi b, \map \phi c \in \R$.
Then we have:
{{begin-eqn}}
{{eqn	| l = \overline {\map \phi x}
		| r = \overline {\map \phi {b + i c} }
}}
{{eqn	| r = \overline {\map \phi b + i \map \phi c}
		| c = $\phi$ is linear
}}
{{eqn	| r = \map \phi b - i \map \phi c
		| c = $\map \phi b, \map \phi c \in \R$ 
}}
{{eqn	| r = \map \phi {b - i c}
		| c = $\phi$ is linear
}}
{{eqn	| r = \map \phi {x^\ast} 
}}
{{end-eqn}}
{{qed}}
Category:*-Algebras
es04cq6bj1unlglkhve4k6az1loob9o
Theorem: Positive Linear Functional on C*-Algebra preserves Star

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\phi : A \to \C$ be a positive linear functional.
Then:
:$\overline {\map \phi x} = \map \phi {x^\ast}$

Proof:
From Linear Functional on *-Algebra Real-Valued at Hermitian Elements preserves Star, it is enough to show that:
:$\map \phi x \in \R$ whenever $x \in A$ is Hermitian.
This is precisely Positive Linear Functional on C*-Algebra is Real on Hermitian Elements.
{{qed}}
Category:Positive Linear Functionals
Category:C*-Algebras
e3brlblvw3fna546nerp8fopk2ovgdi
Theorem: Bound on Norm of Real and Imaginary Parts of Element of Banach *-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a Banach $\ast$-algebra.
Let $x \in A$.
Let $\map \Re x$ and $\map \Im x$ be the real and imaginary parts of $x$ respectively.
Then:
:$\norm {\map \Re x} \le \norm x$
and:
:$\norm {\map \Im x} \le \norm x$
for each $x \in A$.

Proof:
Let $x \in A$.
Then we have:
{{begin-eqn}}
{{eqn	| l = \norm {\frac 1 2 \paren {x + x^\ast} }
		| r = \frac 1 2 \norm {x + x^\ast} 
		| c = {{NormAxiomVector|2}}
}}
{{eqn	| o = \le
		| r = \frac 1 2 \paren {\norm x + \norm {x^\ast} }
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| r = \frac 1 2 \paren {\norm x + \norm x}
		| c = {{Defof|Banach *-Algebra}}
}}
{{eqn	| r = \norm x
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \norm {\frac 1 {2 i} \paren {x - x^\ast} }
		| r = \frac 1 2 \norm {x - x^\ast} 
		| c = {{NormAxiomVector|2}}
}}
{{eqn	| o = \le
		| r = \frac 1 2 \paren {\norm x + \norm {x^\ast} }
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| r = \frac 1 2 \paren {\norm x + \norm x}
		| c = {{Defof|Banach *-Algebra}}
}}
{{eqn	| r = \norm x
}}
{{end-eqn}}
{{qed}}
Category:Banach *-Algebras
qk8igj5bpw3hjlsypkj1alnxmgd0hh9
Theorem: Linear Transformation from Banach *-Algebra is Bounded if Bounded on Hermitian Elements

Let $\struct {A, \ast, \norm {\, \cdot \,}_A}$ be a Banach $\ast$-algebra.
Let $\struct {B, \norm {\, \cdot \,}_B}$ be a normed vector space over $\C$.
Let $T : A \to B$ be a linear transformation such that there exists $M > 0$ with:
:$\norm {T x}_B \le M \norm x_A$ for each $x \in A$ Hermitian.
Then $T$ is bounded.

Proof:
Let $x \in A$.
From Element of *-Algebra Uniquely Decomposes into Hermitian Elements, we have:
:$x = \map \Re x + i \map \Im x$
where $\map \Re x$ and $\map \Im x$ are Hermitian.
Then we have:
{{begin-eqn}}
{{eqn	| l = \norm {T x}_B
		| r = \norm {\map T {\map \Re x} + i \map T {\map \Im x} }_B
		| c = {{Defof|Linear Transformation}}
}}
{{eqn	| o = \le
		| r = \norm {\map T {\map \Re x} } + \norm {\map T {\map \Im x} }_B
		| c = {{NormAxiomVector|2}}, {{NormAxiomVector|3}}
}}
{{eqn	| o = \le
		| r = M \norm {\map \Re x}_A + M \norm {\map \Im x}_A 
}}
{{eqn	| o = \le
		| r = M \norm x_A + M \norm x_A 
		| c = Bound on Norm of Real and Imaginary Parts of Element of Banach *-Algebra
}}
{{eqn	| r = 2 M \norm x_A 
}}
{{end-eqn}}
Hence $T$ is bounded.
{{qed}}
Category:Banach *-Algebras
4obrjwrx1kcmzvugnxhqhmzs4ce8tc3
Theorem: Sum of Two Positive Elements of C*-Algebra is Positive/Corollary

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $a_1, a_2, \ldots, a_n \in A$ be positive.
Then:
:$\ds \sum_{j \mathop = 1}^n a_j$ is positive.

Proof:
Proof by induction:
For all $n \in \N$, let $\map P n$ be the proposition:
:for all $a_1, a_2, \ldots, a_n \in A$ positive, $\ds \sum_{j \mathop = 1}^n a_j$ is positive.
Theorem: Positive Linear Functional on C*-Algebra is Bounded

Let $\struct {A, \ast, \norm {\, \cdot \,}_A}$ be a $\text C^\ast$-algebra.
Let $f : A \to \C$ be a positive linear functional.
Then $f$ is bounded.

Proof:
From Linear Transformation from C*-Algebra is Bounded if Bounded on Positive Elements, it is enough to show that:
:there exists $c > 0$ such that for all positive $x \in A$ we have $\cmod {\map f x} \le c \norm x$.
{{AimForCont}} suppose that:
:there does not exist $c > 0$ such that for all positive $x \in A$ we have $\cmod {\map f x} \le c \norm x$.
Then for each $n \in \N$ there exists $y_n \in A$ positive such that:
:$\cmod {\map f {y_n} } > 2^n \norm {y_n}$ 
Since $y_n \ne {\mathbf 0}_A$, setting:
:$\ds x_n = \frac {y_n} {\norm {y_n} }$
we have:
:$\ds \cmod {\map f {x_n} } > 2^n$
with $\norm {x_n} = 1$.
Further, $x_n$ is positive for each $n \in \N$ by Non-Negative Multiple of Positive Element of C*-Algebra is Positive.
Hence $\map f {x_n} \ge 0$ for each $n \in \N$, and we have:
:$\map f {x_n} > 2^n$
Hence we have, for each $n \in \N$:
:$\ds \map f {\frac {x_n} {2^n} } > 1$
and hence:
:$\ds \map f {\sum_{k \mathop = 1}^n \frac {x_k} {2^k} } > n$
by linearity.
We have:
:$\ds \sum_{k \mathop = 1}^\infty \norm {\frac {x_k} {2^k} } = \sum_{k \mathop = 1}^\infty \frac 1 {2^k} < \infty$
from Sum of Infinite Geometric Sequence.
Hence from Absolutely Convergent Series in Normed Vector Space is Convergent iff Space is Banach, we have that:
:$\ds \sum_{k \mathop = 1}^n \frac {x_k} {2^k} \to x$ as $n \to \infty$
for some $x \in A$.
From Convergent Series of Positive Elements of C*-Algebra is Positive, we have:
:$\ds x - \sum_{k \mathop = 1}^n \frac {x_k} {2^k} = \sum_{k \mathop = n + 1}^\infty \frac {x_n} {2^n}$ is positive. 
Since $f$ is a positive linear functional, we have:
:$\ds \map f {x - \sum_{k \mathop = 1}^n \frac {x_k} {2^k} } \ge 0$
Since $x$ and $\ds \sum_{k \mathop = 1}^n \frac {x_k} {2^k}$ are both positive, we have:
:$\map f x \in \R_{\ge 0}$
and:
:$\map f {\sum_{k \mathop = 1}^n \frac {x_k} {2^k} } \in \R_{\ge 0}$
since $f$ is positive.
Hence by linearity:
:$\ds \map f x \ge \map f {\sum_{k \mathop = 1}^n \frac {x_k} {2^k} } > n$
Since $\map f x < \infty$, by taking $n > \map f x$ we obtain a contradiction.
Hence:
:there exists $c > 0$ such that for all positive $x \in A$ we have $\cmod {\map f x} \le c \norm x$.
Hence $f$ is bounded by Linear Transformation from C*-Algebra is Bounded if Bounded on Positive Elements.
{{qed}}
Theorem: Norm of Positive Linear Functional on Unital C*-Algebra

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra with identity element ${\mathbf 1}_A$. 
Let $f : A \to \C$ be a positive linear functional.
Let $\norm {\, \cdot \,}_{A^\ast}$ be the norm of a bounded linear functional.
Then $f$ is bounded and:
:$\norm f_{A^\ast} = \map f { {\mathbf 1}_A}$

Proof:
From Positive Linear Functional on C*-Algebra is Bounded, $f$ is bounded.
We show that:
:$\cmod {\map f x} \le \map f { {\mathbf 1}_A}$
for each $x \in A$ with $\norm x \le 1$. 
Since equality is attained for $x = {\mathbf 1}_A$, we will then have $\norm f_{A^\ast} = \map f { {\mathbf 1}_A}$.
We have, for all $u \in A$:
{{begin-eqn}}
{{eqn	| l = \map \Re {\map f u}
		| r = \frac 1 2 \paren {\map f u + \overline {\map f u} }
}}
{{eqn	| r = \frac 1 2 \paren {\map f u + \map f {u^\ast} }
		| c = Positive Linear Functional on C*-Algebra preserves Star
}}
{{eqn	| r = \map f {\frac 1 2 \paren {u + u^\ast} }
		| c = $f$ is linear
}}
{{eqn	| r = \map f {\map \Re u}
		| c = {{Defof|Real Part of Element of *-Algebra}}
}}
{{end-eqn}}
Let $x \in A$ have $\norm x \le 1$.
Take $\theta \in \R$ such that:
:$\cmod {\map \phi x} = e^{i \theta} \map \phi x$ 
Then we have:
{{begin-eqn}}
{{eqn	| l = \cmod {\map f x}
		| r = \map \Re {\cmod {\map f x} }
}}
{{eqn	| r = \map \Re {\map f {e^{i \theta} x} }
		| c = {{Defof|Linear Functional}}
}}
{{eqn	| r = \map f {\map \Re {e^{i \theta} x} }
}}
{{end-eqn}}
From Element of *-Algebra Uniquely Decomposes into Hermitian Elements, $\map \Re {e^{i \theta} x}$ is Hermitian.
From Bounds on Hermitian Element of Unital C*-Algebra in terms of Bounds on Spectrum, we have:
:$\map \Re {e^{i \theta} x} \le_A \norm {e^{i \theta} x} {\mathbf 1}_A$
where $\le_A$ is the canonical preordering of $A$.
From {{NormAxiomVector|1}}, we have:
:$\map \Re {e^{i \theta} x} \le_A \norm x {\mathbf 1}_A = {\mathbf 1}_A$
From Positive Linear Functional on C*-Algebra is Increasing on Hermitian Elements, we have:
:$\map f {\map \Re {e^{i \theta} x} } \le \map f { {\mathbf 1}_A}$
Hence:
:$\cmod {\map f x} \le \map f { {\mathbf 1}_A}$
{{qed}}
Category:Positive Linear Functionals
Category:C*-Algebras
24k84ru7v6xtab8yqhv15rm6zskfye7
Theorem: Positive Linear Functional on C*-Algebra is Real on Hermitian Elements

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $\phi : A \to \C$ be a positive linear functional.
Let $x \in A$ be Hermitian.
Then $\map \phi x \in \R$.

Proof:
From Hermitian Element of C*-Algebra Decomposes into Positive Elements, there exists positive elements $x^+, x^- \in A$ such that:
:$x = x^+ - x^-$
Since $f$ is positive, we have $\map \phi {x^+} \ge 0$ and $\map \phi {x^-} \ge 0$. 
Hence from linearity:
:$\map \phi x = \map \phi {x^+} - \map \phi {x^-} \in \R$ 
{{qed}}
Category:Positive Linear Functionals
Category:C*-Algebras
jbzpeam4w14b2gybeokoqv664e5i5sb
Theorem: Positive Linear Functional on C*-Algebra is Increasing on Hermitian Elements

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra with identity element ${\mathbf 1}_A$. 
Let $f : A \to \C$ be a positive linear functional.
Let $\le_A$ be the canonical preordering of $A$. 
Let $x, y \in A$ be Hermitian such that $x \le_A y$.
Then $\map f x \le \map f y$.

Proof:
From the definition of the canonical preordering, we have:
:$y - x$ is positive.
From the definition of a positive linear functional we have:
:$\map f {y - x} \ge 0$
Since $f$ is linear, we have:
:$\map f y - \map f x \ge 0$ 
From Positive Linear Functional on C*-Algebra is Real on Hermitian Elements, we have $\map f x \in \R$ and $\map f y \in \R$.
Hence:
:$\map f x \le \map f y$
{{qed}}
Category:Positive Linear Functionals
Category:C*-Algebras
tfvhcqhsehm8yj2raofdxd8eniwsaml
Theorem: Positive Linear Functional on C*-Algebra induces Semi-Inner Product

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $f : A \to \C$ be a positive linear functional. 
Define $\innerprod \cdot \cdot : A^2 \to A$ by:
:$\innerprod x y = \map f {y^\ast x}$
for each $x, y \in A$. 
Then $\innerprod \cdot \cdot$ is a semi-inner product on $A$.

Proof:
=== Proof of Conjugate Symmetry ===
Let $x, y \in A$ we have:
{{begin-eqn}}
{{eqn	| l = \overline {\innerprod x y}
		| r = \overline {\map f {y^\ast x} }
}}
{{eqn	| r = \map f {\paren {y^\ast x}^\ast}
		| c = Positive Linear Functional on C*-Algebra preserves Star
}}
{{eqn	| r = \map f {x^\ast y}
		| c = $(\text C^\ast 4)$ and $(\text C^\ast 1)$ in {{Defof|Involution on Algebra}}
}}
{{eqn	| r = \innerprod y x
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Positive Linear Functional on C*-Algebra induces Semi-Inner Product/Corollary

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $f : A \to \C$ be a positive linear functional. 
Let $x, y \in A$.
Then:
:$\cmod {\map f {y^\ast x} }^2 \le \map f {y^\ast y} \map f {x^\ast x}$

Proof:
Define $\innerprod \cdot \cdot : A^2 \to A$ by:
:$\innerprod x y = \map f {y^\ast x}$
for each $x, y \in A$. 
By Positive Linear Functional on C*-Algebra induces Semi-Inner Product, $\innerprod \cdot \cdot$ is a semi-inner product.
Hence from Cauchy-Bunyakovsky-Schwarz Inequality: Inner Product Spaces, we have:
:$\cmod {\innerprod x y}^2 \le \innerprod x x \innerprod y y$
so that:
:$\cmod {\map f {y^\ast x} }^2 \le \map f {y^\ast y} \map f {x^\ast x}$
{{qed}}
Theorem: Canonical Mapping of Locale to Powerset of Points is Frame Homomorphism

Let $\struct{L, \preceq}$ be a locale.
Let $\map {\operatorname{pt}} L$ denote the points of $L$ as completely prime filters.
For each $a \in L$, let:
:$\Sigma_a = \set{p \in \map {\operatorname{pt}} L : a \in p}$
Let $\Sigma : L \to \powerset {\map {\operatorname{pt}} L}$ be the mapping defined by:
:$\forall a \in L : \map \Sigma a = \Sigma_a$
where $\powerset {\map {\operatorname{pt}} L}$ denotes  the powerset of $\map {\operatorname{pt}} L$.
Then:
:$\Sigma: \struct{L, \preceq} \to \struct{\powerset {\map {\operatorname{pt}} L}, \subseteq}$ is a frame homomorphism.

Proof:
=== $\Sigma$ Preserves Arbitrary Supremums ===
Let $\set{a_i : i \in I}$ be an indexed family of elements of $L$.
Let $\ds \bigvee_{i \in I} a_i$ denote the supremum of $\set{a_i : i \in I}$.
We have:
{{begin-eqn}}
{{eqn | q = \forall p \in \map {\operatorname{pt} } L
      | l = p 
      | o = \in
      | r = \map \Sigma {\bigvee_{i \in I} a_i}
}}
{{eqn | ll = \leadstoandfrom 
      | l = \bigvee_{i \in I} a_i 
      | o = \in
      | r = p
      | c = Definition of $\map \Sigma {\bigvee_{i \in I} a_i}$
}}
{{eqn | ll = \leadstoandfrom 
      | l = \exists i \in I : a_i 
      | o = \in
      | r = p
      | c = Characterization of Completely Prime Filter in Complete Lattice
}}
{{eqn | ll = \leadstoandfrom 
      | l = \exists i \in I : p 
      | o = \in
      | r = \map \Sigma {a_i}
      | c = Definition of $\Sigma$
}}
{{eqn | ll = \leadstoandfrom 
      | l = p 
      | o = \in
      | r = \bigcup_{i \in I} \map \Sigma {a_i}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
By definition of set Equlity:
:$\ds \map \Sigma {\bigvee_{i \in I} a_i} = \bigcup_{i \in I} \map \Sigma {a_i}$
It follows that $\Sigma$ is arbitrary join preserving by definition. 
{{qed|lemma}}
Theorem: Frame Homomorphism Preserves Greatest Element

Let $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ be frames.
Let $\phi: L_1 \to L_2$ be a frame homomophism.
Let $\top_1$ and $\top_2$ denote the greatest elelment of $L_1$ and $L_2$ respectively.
Then:
:$\map \phi \top_1 = \top_2$

Proof:
we have:
{{begin-eqn}}
{{eqn | l = \map \phi \top_1
      | r = \map \phi {\bigwedge \O}
      | c = {{Defof|Frame}} and Infimum of Empty Set is Greatest Element
}}
{{eqn | r = \bigwedge \set{\map \phi x : x \in \O}
      | c = Frame homomorphism is finite meet preserving
}}
{{eqn | r = \bigwedge \O
      | c = {{Defof|Empty Set}}
}}
{{eqn | r = \top_2
      | c = {{Defof|Frame}} and Infimum of Empty Set is Greatest Element
}}
{{end-eqn}}
{{qed}}