avewright/proofwiki-math huggingface dataset:
Theorem: Frame Homomorphism Preserves Smallest 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 $\bot_1$ and $\bot_2$ denote the smallest elelment of $L_1$ and $L_2$ respectively.
Then:
:$\map \phi \bot_1 = \bot_2$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map \phi \bot_1
      | r = \map \phi {\bigvee \O}
      | c = {{Defof|Frame}} and Supremum of Empty Set is Smallest Element
}}
{{eqn | r = \bigvee \set{\map \phi x : x \in \O}
      | c = Frame homomorphism is arbitrary join preserving
}}
{{eqn | r = \bigvee \O
      | c = {{Defof|Empty Set}}
}}
{{eqn | r = \bot_2
      | c = {{Defof|Frame}} and Supremum of Empty Set is Smallest Element
}}
{{end-eqn}}
{{qed}}
Theorem: Zero Set of Semi-Inner Product is Vector Subspace

Let $\GF \in \set {\R, \C}$. 
Let $\struct {V, \innerprod \cdot \cdot}$ be a semi-inner product space over $\GF$.
Let:
:$N = \set {x \in V : \innerprod x x = 0}$
Then $N$ is a vector subspace of $V$.

Proof:
Let $x, y \in N$ and 
Then by Cauchy-Bunyakovsky-Schwarz Inequality: Inner Product Spaces we have:
:$\cmod {\innerprod x y}^2 \le \innerprod x x \innerprod y y = 0$
and:
:$\cmod {\innerprod y x}^2 \le \innerprod x x \innerprod y y = 0$ 
Hence $\innerprod x y = \innerprod y x = 0$.
Then we have:
{{begin-eqn}}
{{eqn	| l = \innerprod {x + \lambda y} {x + \lambda y}
		| r = \innerprod x x + \lambda \innerprod y x + \overline \lambda \innerprod x y + \lambda \overline \lambda \innerprod y y
		| c = using sesquilinearity
}}
{{eqn	| r = \innerprod x x + \lambda \overline \lambda \innerprod y y
		| c = since $\innerprod x y = \innerprod y x = 0$
}}
{{eqn	| r = 0
		| c = since $x, y \in N
}}
{{end-eqn}}
{{qed}}
Category:Semi-Inner Product Spaces
0uonbuzsnec0zt03pquxwowogojb7v1
Theorem: Semi-Inner Product induces Inner Product on Quotient

Let $\GF \in \set {\R, \C}$. 
Let $\struct {V, \innerprod \cdot \cdot}$ be a semi-inner product space over $\GF$.
Let:
:$N = \set {x \in V : \innerprod x x = 0}$
Let $X/N$ be the quotient vector space of $X$ modulo $N$. 
Define:
:$\innerprod {x + N} {y + N}_{X/N} = \innerprod x y$
for each $x, y \in X$. 
Then $\innerprod \cdot \cdot_{X/N}$ is an inner product on $X/N$.

Proof:
First note that Zero Set of Semi-Inner Product is Vector Subspace shows that $N$ is a vector subspace and hence $X/N$ is well-defined.
We show that $\innerprod \cdot \cdot_{X/N}$ is well-defined. 
We need to show that if $x, y, x', y' \in X$ are such that $x - x' \in N$ and $y - y' \in N$, then $\innerprod x y = \innerprod {x'} {y'}$. 
We have:
{{begin-eqn}}
{{eqn	| l = \innerprod x y
		| r = \innerprod {x - x' + x'} {y - y' + y'}
}}
{{eqn	| r = \innerprod {x - x'} {y - y' + y'} + \innerprod {x'} {y - y' + y'}
}}
{{eqn	| r = \innerprod {x - x'} {y - y'} + \innerprod {x - x'} {y'} + \innerprod {x'} {y - y'} + \innerprod {x'} {y'}
}}
{{end-eqn}}
From Cauchy-Bunyakovsky-Schwarz Inequality: Inner Product Spaces, we have:
:$\cmod {\innerprod {x - x'} {y - y'} }^2 \le \innerprod {x - x'} {x - x'} \innerprod {y - y'} {y - y'} = 0$
since $x - x' \in N$ and $y - y' \in N$.
We also have:
:$\cmod {\innerprod {x - x'} {y'} }^2 \le \innerprod {x - x'} {x - x'} \innerprod {y'} {y'} = 0$
since $x - x' \in N$.
Finally:
:$\cmod {\innerprod {x'} {y - y'} }^2 \le \innerprod {x'} {x'} \innerprod {y - y'} {y - y'} = 0$ 
since $y - y' \in N$. 
So we have $\innerprod {x - x'} {y - y'} + \innerprod {x - x'} {y'} + \innerprod {x'} {y - y'} = 0$ and we obtain:
:$\innerprod x y = \innerprod {x'} {y'}$
Hence $\innerprod \cdot \cdot_{X/N}$ is well-defined.
We just need to verify that $\innerprod \cdot \cdot_{X/N}$ is an inner product on $X/N$.
Theorem: Generalized Sum Commutes with Inner Product

Let $\struct {\HH, \innerprod \cdot \cdot}$ be an inner product space.
Let $\Lambda$ be a set. 
Let $\sequence {x_\lambda}_{\lambda \mathop \in \Lambda}$ be a $\Lambda$-indexed family in $\HH$ such that the generalized sum $\ds \sum \set {x_\lambda : \lambda \in \Lambda}$ converges.
Let $y \in \HH$.
Then:
:$\ds \sum \set {\innerprod {x_\lambda} y : \lambda \in \Lambda}$ converges 
and further:
:$\ds \sum \set {\innerprod {x_\lambda} y : \lambda \in \Lambda} = \innerprod {\sum \set {x_\lambda : \lambda \in \Lambda} } y $

Proof:
Let $\struct {\FF, \subseteq}$ be the set of finite subsets of $\Lambda$ ordered by inclusion.
Define, for $F \in \FF$:
:$\ds \map {s_1} F = \sum \set {\innerprod {x_\lambda} y : \lambda \in \Lambda}$
and:
:$\ds \map {s_2} F = \innerprod {\sum \set {x_\lambda : \lambda \in \Lambda} } y$
Noting that $\ds \family {\sum_{\lambda \mathop \in F} x_\lambda}_{F \in \FF}$ converges to $\ds \sum \set {x_\lambda : \lambda \in \Lambda}$, we have that:
:$\family {\map {s_2} F}_{\lambda \in \Lambda}$ converges to $\ds \innerprod {\sum \set {x_\lambda : \lambda \in \Lambda} } y$
by Characterization of Continuity in terms of Nets.
From the linearity of $\innerprod \cdot \cdot$ in the first argument we have:
:$\map {s_1} F = \map {s_2} F$
Hence since $\family {\map {s_2} F}_{F \in \FF}$ converges to $\ds \innerprod {\sum \set {x_\lambda : \lambda \in \Lambda} } y$, so does $\family {\map {s_1} F}_{F \in \FF}$.
Hence we obtain the convergence of:
:$\ds \sum \set {\innerprod {x_\lambda} y : \lambda \in \Lambda}$
and obtain:
:$\ds \sum \set {\innerprod {x_\lambda} y : \lambda \in \Lambda} = \innerprod {\sum \set {x_\lambda : \lambda \in \Lambda} } y $ 
{{qed}}
Category:Generalized Sums
k00j9jc774ba1u0q17jwoz95i4m60bx
Theorem: Equivalence of Definitions of Positive Definite Matrix

Let $\mathbf A$ be a symmetric square matrix of order $n$.
{{TFAE|def = Positive Definite Matrix}}

Proof:
{{MissingLinks}}
Theorem: Orthocomplement equal to Orthocomplement of Linear Span

Let $\GF \in \set {\R, \C}$. 
Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space over $\GF$. 
Let $S \subseteq V$ be non-empty.
Then:
:$S^\bot = \paren {\map \span S}^\bot$
where $\bot$ denotes orthocomplement.

Proof:
From Orthocomplement Reverses Subset, we have:
:$\paren {\map \span S}^\bot \subseteq S^\bot$ 
Conversely let $y \in S^\bot$. 
Let $x \in \map \span S$.
From the definition of the linear span there exists $x_1, \ldots, x_n \in S$ and $\alpha_1, \ldots, \alpha_n \in \GF$ such that:
:$\ds x = \sum_{j \mathop = 1}^n \alpha_j x_j$
We then have:
{{begin-eqn}}
{{eqn	| l = \innerprod x y
		| r = \innerprod {\sum_{j \mathop = 1}^n \alpha_j x_j} y
}}
{{eqn	| r = \sum_{j \mathop = 1}^n \alpha_j \innerprod {x_j} y
		| c = linearity in first argument 
}}
{{eqn	| r = 0
		| c = since $x_j \in S$ for each $j$, we have $\innerprod {x_j} y = 0$ 
}}
{{end-eqn}}
So $\innerprod x y = 0$ for all $x \in \map \span S$.
So $y \in \paren {\map \span S}^\bot$.
Hence we have $S^\bot \subseteq \paren {\map \span S}^\bot$.
We conclude:
:$S^\bot = \paren {\map \span S}^\bot$
{{qed}}
Category:Orthocomplements
shpfro7afsm9wdr3v9hqohovdmp0mn0
Theorem: Adjoint of Direct Sum of Bounded Linear Operators on Hilbert Space

Let $\GF \in \set {\R, \C}$. 
Let $\sequence {\family {\HH_i, \innerprod \cdot \cdot_i} }_{i \mathop \in I}$ be a $I$-indexed family of Hilbert spaces over $\GF$.
For each $i \in I$, let $T_i : \HH_i \to \HH_i$ be a bounded linear operator.
Suppose that:
:$\ds \sup_{i \mathop \in I} \norm {T_i}_{\map B {\HH_i} } < \infty$
where $\norm {\, \cdot \,}_{\map B {\HH_i} }$ is the norm of a bounded linear operator on $\HH_i$.
Let:
:$\ds \HH = \bigoplus_{i \mathop \in I} \HH_i$
be the Hilbert space direct sum of $\sequence {\family {\HH_i, \innerprod \cdot \cdot_i} }_{i \mathop \in I}$ with inner product $\innerprod \cdot \cdot$ and norm $\norm {\, \cdot \,}$.
Let:
:$\ds T = \bigoplus_{i \mathop \in I} T_i$
and:
:$\ds \bigoplus_{i \mathop \in I} T_i^\ast$ 
be the direct sum of $\family {T_i}_{i \mathop \in I}$ and $\family {T_i^\ast}_{i \mathop \in I}$ respectively.
Then:
:$\ds T^\ast = \bigoplus_{i \mathop \in I} T_i^\ast$
That is:
:$\ds \paren {\bigoplus_{i \mathop \in I} T_i}^\ast = \bigoplus_{i \mathop \in I} T_i^\ast$

Proof:
From Norm of Adjoint, we have:
:$\norm {T_i}_{\map B {\HH_i} } = \norm {T_i^\ast}_{\map B {\HH_i} }$
and hence:
:$\ds \sup_{i \mathop \in I} \norm {T_i^\ast}_{\map B {\HH_i} } < \infty$
so we can indeed define $\ds \bigoplus_{i \mathop \in I} T_i^\ast$.
Let $f, g \in \HH$. 
We then have:
{{begin-eqn}}
{{eqn	| l = \innerprod {T f} g
		| r = \sum \set {\innerprod {T_i \map f i} {\map g i}_i : i \in I} 
}}
{{eqn	| r = \sum \set {\innerprod {\map f i} {T_i^\ast \map g i}_i : i \in I}
		| c = {{Defof|Adjoint Linear Transformation}}
}}
{{eqn	| r = \innerprod f {\paren {\bigoplus_{i \mathop \in I} T_i^\ast} g}
		| c = {{Defof|Direct Sum of Bounded Linear Operators on Hilbert Space}}
}}
{{end-eqn}}
and hence conclude:
:$\ds T^\ast = \bigoplus_{i \mathop \in I} T_i^\ast$
{{qed}}
Category:Direct Sums of Hilbert Spaces
9cqszzzswz8s9cx6q5z4kaz12ggnbj1
Theorem: Composition of Direct Sums of Bounded Linear Operators on Hilbert Space

Let $\GF \in \set {\R, \C}$. 
Let $\sequence {\family {\HH_i, \innerprod \cdot \cdot_i} }_{i \mathop \in I}$ be a $I$-indexed family of Hilbert spaces over $\GF$.
For each $i \in I$, let $T_i : \HH_i \to \HH_i$ and $S_i : \HH_i \to \HH_i$ be bounded linear operators.
Suppose that:
:$\ds \sup_{i \mathop \in I} \norm {T_i}_{\map B {\HH_i} } < \infty$
and:
:$\ds \sup_{i \mathop \in I} \norm {S_i}_{\map B {\HH_i} } < \infty$
where $\norm {\, \cdot \,}_{\map B {\HH_i} }$ is the norm of a bounded linear operator on $\HH_i$.
Let:
:$\ds \HH = \bigoplus_{i \mathop \in I} \HH_i$
be the Hilbert space direct sum of $\sequence {\family {\HH_i, \innerprod \cdot \cdot_i} }_{i \mathop \in I}$ with inner product $\innerprod \cdot \cdot$ and norm $\norm {\, \cdot \,}$.
Let:
:$\ds T = \bigoplus_{i \mathop \in I} T_i$
:$\ds S = \bigoplus_{i \mathop \in I} S_i$
:$\ds \bigoplus_{i \mathop \in I} T_i S_i$ 
be the direct sum of $\family {T_i}_{i \mathop \in I}$, $\family {S_i}_{i \mathop \in I}$ and $\family {T_i S_i}_{i \mathop \in I}$ respectively.
Then we have:
:$\ds T S = \bigoplus_{i \mathop \in I} T_i S_i$ 
That is:
:$\ds \paren {\bigoplus_{i \mathop \in I} T_i} \paren {\bigoplus_{i \mathop \in I} S_i} = \bigoplus_{i \mathop \in I} T_i S_i$

Proof:
From Norm on Bounded Linear Transformation is Submultiplicative we have:
{{begin-eqn}}
{{eqn	| l = \norm {T_i S_i}_{\map B {\HH_i} }
		| o = \le
		| r = \norm {T_i}_{\map B {\HH_i} } \norm {S_i}_{\map B {\HH_i} }
}}
{{eqn	| o = \le
		| r = \paren {\sup_{i \mathop \in I} \norm {T_i}_{\map B {\HH_i} } } \paren {\sup_{i \mathop \in I} \norm {S_i}_{\map B {\HH_i} } }
}}
{{end-eqn}}
Hence we have:
:$\ds \sup_{i \mathop \in I} \norm {T_i S_i}_{\map B {\HH_i} } \le \paren {\sup_{i \mathop \in I} \norm {T_i}_{\map B {\HH_i} } } \paren {\sup_{i \mathop \in I} \norm {S_i}_{\map B {\HH_i} } } < \infty$
Hence:
:$\ds \bigoplus_{i \mathop \in I} T_i S_i$ is well-defined.
Let $f \in \HH$ and $i \in I$.
Then we have:
:$\ds \map {\paren {\paren {\bigoplus_{i \mathop \in I} T_i} \paren {\bigoplus_{i \mathop \in I} S_i} f} } i = T_i \map {\paren {\paren {\bigoplus_{i \mathop \in I} S_i} f} } i = T_i S_i \map f i = \map {\paren {\paren {\bigoplus_{i \mathop \in I} T_i S_i} f} } i$
by the definition of the direct sum.
Hence we have:
:$\ds \paren {\bigoplus_{i \mathop \in I} T_i} \paren {\bigoplus_{i \mathop \in I} S_i} f = \paren {\bigoplus_{i \mathop \in I} T_i S_i} f$
for each $f \in \HH$.
Hence:
:$\ds \paren {\bigoplus_{i \mathop \in I} T_i} \paren {\bigoplus_{i \mathop \in I} S_i} = \bigoplus_{i \mathop \in I} T_i S_i$
{{qed}}
Category:Hilbert Space Direct Sums
th8udf1dgawvbnpxfc9rmnmtnfls665
Theorem: Linear Combination of Direct Sums of Bounded Linear Operators on Hilbert Space

Let $\GF \in \set {\R, \C}$. 
Let $\sequence {\family {\HH_i, \innerprod \cdot \cdot_i} }_{i \mathop \in I}$ be a $I$-indexed family of Hilbert spaces over $\GF$.
For each $i \in I$, let $T_i : \HH_i \to \HH_i$ and $S_i : \HH_i \to \HH_i$ be bounded linear operators.
Let $\lambda \in \GF$.
Suppose that:
:$\ds \sup_{i \mathop \in I} \norm {T_i}_{\map B {\HH_i} } < \infty$
and:
:$\ds \sup_{i \mathop \in I} \norm {S_i}_{\map B {\HH_i} } < \infty$
where $\norm {\, \cdot \,}_{\map B {\HH_i} }$ is the norm of a bounded linear operator on $\HH_i$.
Let:
:$\ds \HH = \bigoplus_{i \mathop \in I} \HH_i$
be the Hilbert space direct sum of $\sequence {\family {\HH_i, \innerprod \cdot \cdot_i} }_{i \mathop \in I}$ with inner product $\innerprod \cdot \cdot$ and norm $\norm {\, \cdot \,}$.
Let:
:$\ds T = \bigoplus_{i \mathop \in I} T_i$
:$\ds S = \bigoplus_{i \mathop \in I} S_i$
:$\ds \bigoplus_{i \mathop \in I} \paren {T_i + \lambda S_i}$ 
be the direct sum of $\family {T_i}_{i \mathop \in I}$, $\family {S_i}_{i \mathop \in I}$ and $\family {T_i + \lambda S_i}_{i \mathop \in I}$ respectively.
Then we have:
:$\ds T + \lambda S = \bigoplus_{i \mathop \in I} \paren {T_i + \lambda S_i}$ 
That is:
:$\ds \bigoplus_{i \mathop \in I} T_i + \lambda \bigoplus_{i \mathop \in I} S_i = \bigoplus_{i \mathop \in I} \paren {T_i + \lambda S_i}$

Proof:
First, from {{NormAxiomVector|3}} and {{NormAxiomVector|2}}, we have:
{{begin-eqn}}
{{eqn	| l = \norm {T_i + \lambda S_i}_{\map B {\HH_i} }
		| o = \le
		| r = \norm {T_i}_{\map B {\HH_i} } + \cmod \lambda \norm {S_i}_{\map B {\HH_i} }
}}
{{eqn	| o = \le
		| r = \sup_{i \mathop \in I} \norm {T_i}_{\map B {\HH_i} } + \cmod \lambda \sup_{i \mathop \in I} \norm {S_i}_{\map B {\HH_i} }
}}
{{end-eqn}}
Hence:
:$\ds \sup_{i \mathop \in I} \norm {T_i + \lambda S_i}_{\map B {\HH_i} } \le \sup_{i \mathop \in I} \norm {T_i}_{\map B {\HH_i} } + \cmod \lambda \sup_{i \mathop \in I} \norm {S_i}_{\map B {\HH_i} } < \infty$
Hence the direct sum:
:$\ds \bigoplus_{i \mathop \in I} \paren {T_i + \lambda S_i}$ is well-defined.
Let $f \in \HH$ and $i \in I$.
We have:
{{begin-eqn}}
{{eqn	| l = \map {\paren {\paren {\bigoplus_{i \mathop \in I} T_i} f} } i + \lambda \map {\paren {\paren {\bigoplus_{i \mathop \in I} S_i} f} } i
		| r = T_i \map f i + \lambda S_i \map g i 
}}
{{eqn	| r = \map {\paren {\paren {\bigoplus_{i \mathop \in I} \paren {T_i + \lambda S_i} } f} } i
}}
{{end-eqn}}
Hence we have:
:$\ds \paren {\bigoplus_{i \mathop \in I} T_i} f + \lambda \paren {\bigoplus_{i \mathop \in I} S_i} f = \paren {\bigoplus_{i \mathop \in I} \paren {T_i + \lambda S_i} } f$
for each $f \in \HH$.
Hence:
:$\ds \bigoplus_{i \mathop \in I} T_i + \lambda \bigoplus_{i \mathop \in I} S_i = \bigoplus_{i \mathop \in I} \paren {T_i + \lambda S_i}$ 
{{qed}}
Category:Hilbert Space Direct Sums
14h3q1cbcvspbvv0x3v9ax6prm4rxh4
Theorem: Hermitian Elements of *-Algebra form Real Vector Subspace

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $A_{\mathbf{SA} }$ be the set of Hermitian elements of $A$.
Then $A_{\mathbf{SA} }$ is a $\R$-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 \in A_{\mathbf{SA} }$.
In particular $A_{\mathbf{SA} } \ne \O$.
Let $a, b \in A_{\mathbf{SA} }$ and $\lambda \in \R$.
We have, from $(\text C^\ast 2)$ and $(\text C^\ast 4)$ in the definition of an involution:
:$\paren {a + \lambda b}^\ast = a^\ast + \lambda b^\ast = a + \lambda b$
Hence $a + \lambda b$ is Hermitian and $a + \lambda b \in A_{\mathbf{SA} }$.
So by the One-Step Vector Subspace Test, we have that $A_{\mathbf{SA} }$ is a $\R$-vector subspace of $A$.
{{qed}}
Category:*-Algebras
8qza0nzprr1evtwopyod8lwzm01ulii
Theorem: State Space of C*-Algebra is Weak-* Compact

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a $\text C^\ast$-algebra.
Let $S_A$ be the set of states on $A$.
Let $w^\ast$ be the weak-$\ast$ topology. 
Then $\struct {S_A, w^\ast}$ is compact.

Proof:
By definition, we have:
:$S_A \subseteq B_{A^\ast}$
where $B_{A^\ast}$ is the closed unit ball of $A^\ast$.
From Banach-Alaoglu Theorem, $\struct {B_{A^\ast}, w^\ast}$ is compact.
From Closed Subspace of Compact Space is Compact, it is enough to show that $S_A$ is closed in $\struct {B_{A^\ast}, w^\ast}$.
Let $\family {f_\lambda}_{\lambda \mathop \in \Lambda}$ be a net in $S_A$ converging to $f$ in $B_{A^\ast}$.
From Characterization of Convergent Net in Weak-* Topology, we have:
:$\family {\map {f_\lambda} a}_{\lambda \mathop \in \Lambda}$ converges to $f$ for each $x \in A$. 
Let $a \in A$ be positive.
Then:
:$\map {f_\lambda} a \ge 0$ for each $\lambda \in \Lambda$. 
Hence from Inequality Rule for Real Convergent Nets, we have:
:$\map f a \ge 0$ 
So $f$ is a positive linear functional. 
Further, we have:
:$\norm {f_\lambda}_{A^\ast} = 1$ for each $\lambda \in \Lambda$.
From Norm is Continuous and Characterization of Continuity in terms of Nets, we have:
:$\norm f_{A^\ast} = 1$ 
So $f \in S_A$.
Hence whenever $\family {f_\lambda}_{\lambda \mathop \in \Lambda}$ be a net in $S_A$ converging to $f$ in $B_{A^\ast}$, we have $f \in S_A$.
Hence from Characterization of Closedness in terms of Nets, $S_A$ is closed in $\struct {B_{A^\ast}, w^\ast}$. 
Hence from Closed Subspace of Compact Space is Compact, $\struct {S_A, w^\ast}$ is compact.
{{qed}}
Theorem: State Space of Unital C*-Algebra is Convex

Let $\struct {A, \ast, \norm {\, \cdot \,} }$ be a unital $\text C^\ast$-algebra.
Let $S_A$ be the set of states on $A$.
Then $S_A$ is convex.

Proof:
Let $t \in \closedint 0 1$ and $f, g \in S_A$.
Then $t f + \paren {1 - t} g$ is a linear functional.
Further, for each $a \in A$ positive, we have:
:$\map f a \ge 0$
and:
:$\map g a \ge 0$
Hence:
:$t \map f a + \paren {1 - t} \map g a \ge 0$
Hence $t f + \paren {1 - t} g$ is a positive linear functional.
From Norm of Positive Linear Functional on Unital C*-Algebra, we have:
:$\norm {t f + \paren {1 - t} g}_{A^\ast} = \map {\paren {t f + \paren {1 - t} g} } { {\mathbf 1}_A}$
We have:
:$\map f { {\mathbf 1}_A} = 1$
and:
:$\map g { {\mathbf 1}_A} = 1$
Hence:
:$t \map f { {\mathbf 1}_A} + \paren {1 - t} \map g { {\mathbf 1}_A} = t + \paren {1 - t} = 1$
So:
:$\norm {t f + \paren {1 - t} g}_{A^\ast} = 1$
Hence $S_A$ is convex.
{{qed}}
Theorem: Real Part of Imaginary Unit times Element of *-Algebra

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $x \in A$.
Then:
:$\map \Re {i x} = -\map \Im x$
where $\Re$ and $\Im$ denote the real and imaginary parts of $A$.

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \map \Re {i x}
		| r = \frac {\paren {i x} + \paren {i x}^\ast} 2
		| c = {{Defof|Real Part of Element of *-Algebra}}
}}
{{eqn	| r = \frac {i x - i x^\ast} 2
		| c = $(\text C^\ast 4)$ from {{Defof|Involution on Algebra}}
}}
{{eqn	| r = i^2 \frac {x - x^\ast} {2 i}
}}
{{eqn	| r = -\frac {x - x^\ast} {2 i}
}}
{{eqn	| r = -\map \Im x
		| c = {{Defof|Imaginary Part of Element of *-Algebra}}
}}
{{end-eqn}}
{{qed}}
Category:*-Algebras
0lbjdczbabtzb8spxplrx33lpjeji9a
Theorem: Imaginary Part of Imaginary Unit times Element of *-Algebra

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $x \in A$.
Then:
:$\map \Im {i x} = \map \Re x$
where $\Re$ and $\Im$ denote the real and imaginary parts of $A$.

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \map \Im {i x}
		| r = \frac {i x - \paren {i x}^\ast} {2 i}
		| c = {{Defof|Imaginary Part of Element of *-Algebra}}
}}
{{eqn	| r = \frac {i x + i x^\ast} {2 i}
		| c = $(\text C^\ast 4)$ from {{Defof|Involution on Algebra}}
}}
{{eqn	| r = \frac {x + x^\ast} 2
}}
{{eqn	| r = \map \Re x
		| c = {{Defof|Imaginary Part of Element of *-Algebra}}
}}
{{end-eqn}}
{{qed}}
Category:*-Algebras
3lowywhi62hc8dequocytbrzle7xhpz
Theorem: Real Part of Element of *-Algebra is Real Linear

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $x, y \in A$ and $\lambda \in \R$.
Then we have:
:$\map \Re {x + \lambda y} = \map \Re x + \lambda \map \Re y$
where $\Re$ denotes real part.

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \map \Re {x + \lambda y}
		| r = \frac {x + \lambda y + \paren {x + \lambda y}^\ast} 2
		| c = {{Defof|Real Part of Element of *-Algebra}}
}}
{{eqn	| r = \frac {x + \lambda y + x^\ast + \lambda y^\ast} 2
		| c = $(\text C^\ast 2)$ and $(\text C^\ast 4)$ in {{Defof|Involution on Algebra}}, Complex Number equals Conjugate iff Wholly Real
}}
{{eqn	| r = \frac {x + x^\ast} 2 + \lambda \frac {y + y^\ast} 2
}}
{{eqn	| r = \map \Re x + \lambda \map \Re y
		| c = {{Defof|Real Part of Element of *-Algebra}}
}}
{{end-eqn}}
{{qed}}
Category:*-Algebras
66fm9mi0xl6j5u98am7lfvz91c3vzit
Theorem: Imaginary Part of Element of *-Algebra is Real Linear

Let $\struct {A, \ast}$ be a $\ast$-algebra over $\C$.
Let $x, y \in A$ and $\lambda \in \R$.
Then we have:
:$\map \Im {x + \lambda y} = \map \Im x + \lambda \map \Im y$
where $\Im$ denotes real part.

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \map \Im {x + \lambda y}
		| r = \frac {x + \lambda y - \paren {x + \lambda y}^\ast} {2 i}
		| c = {{Defof|Real Part of Element of *-Algebra}}
}}
{{eqn	| r = \frac {x + \lambda y - x^\ast - \lambda y^\ast} {2 i}
		| c = $(\text C^\ast 2)$ and $(\text C^\ast 4)$ in {{Defof|Involution on Algebra}}, Complex Number equals Conjugate iff Wholly Real
}}
{{eqn	| r = \frac {x - x^\ast} 2 + \lambda \frac {y - y^\ast} 2
}}
{{eqn	| r = \map \Im x + \lambda \map \Im y
		| c = {{Defof|Real Part of Element of *-Algebra}}
}}
{{end-eqn}}
{{qed}}
Category:*-Algebras
btgfi4jrut2ff8vdqt447ejo7njzywp
Theorem: Canonical Bijection from Completely Prime Filters to Frame Homomorphisms

Let $\struct{L, \preceq}$ be a locale.
Let $\map {\operatorname{Sp}} L = \struct{\map {\operatorname{pt}} L, \set{\Sigma_a : a \in L}}$ be the spectrum of $L$ as completely prime filters where:
:*$\quad\map {\operatorname{pt}} L$ denotes the set of points as completely prime filters of $L$.
:*$\quad$for each $a \in L$, $\Sigma_a = \set{p \in \map {\operatorname{pt}} L : a \in p}$
Let $\Sigma_L = \set{\Sigma_a : a \in L}$
Let $\map {\operatorname{Sp}'} L = \struct{\map {\operatorname{pt}'} L, \set{\Sigma'_a : a \in L}}$ be the spectrum of $L$ as frame homomorphisms where:
:*$\quad\map {\operatorname{pt}'} L$ denotes the set of points as frame homomorphisms of $L$.
:*$\quad$for each $a \in L$, $\Sigma'_a = \set{\phi \in \map {\operatorname{pt}'} L : \map \phi a = \top}$
Let $\Sigma'_L = \set{\Sigma'_a : a \in L}$
Let $f : \map {\operatorname{pt}} L \to \map {\operatorname{pt}'} L$ be the mapping defined by:
:$\forall p \in \map {\operatorname{pt}} L : \map f p$ is the frame homomorphim defined by:
::<nowiki>$\forall a \in L : \map {\map f p} a = \begin{cases}
\top & : a \in p\\
\bot & : a \notin p 
\end{cases}$</nowiki>
Then:
:$f$ is a bijection
:$f^\to \restriction_{\Sigma_L}$ is a surjection from $\Sigma_L$ to $\Sigma'_L$

Proof:
=== $f$ is a Bijection ===
From Frame Homomorphism Onto Two Induced by Completely Prime Filter:
:$f$ is a well-defined mapping
Let $g : \map {\operatorname{pt}'} L \to \map {\operatorname{pt}} L$ be the mapping defined by:
:$\forall \phi \in \map {\operatorname{pt}'} L : \map g \phi = \map {\phi^{-1}} \top$
where:
:$\map {\phi^{-1}} \top$ denotes the preimage of $\top \in \mathbf 2$ under the mapping $\phi$
From Completely Prime Filter Induced by Frame Homomorphism Onto Two:
:$g$ is a well-defined mapping
From Completely Prime Filter Induced by Frame Homomorphism Induced by Completely Prime Filter:
:$g \circ f = \operatorname {id}_{\map {\operatorname{pt}} L}$
where $\operatorname {id}_{\map {\operatorname{pt}} L}$ is the identity mapping on $\map {\operatorname{pt}} L$
From Frame Homomorphism Induced by Completely Prime Filter Induced by Frame Homomorphism:
:$f \circ g = \operatorname {id}_{\map {\operatorname{pt}'} L}$
where $\operatorname {id}_{\map {\operatorname{pt}} L}$ is the identity mapping on $\map {\operatorname{pt}'} L$
Hence $f$ is a bijection by definition.
{{qed|lemma}}