avewright/proofwiki-math huggingface dataset:
Theorem: Equidistance is Independent of Betweenness

Let $\GG$ be a formal systematic treatment of geometry containing only:
:The language and axioms of first-order logic, and the disciplines preceding it
:The undefined terms of Tarski's Geometry (excluding equidistance) 
:Some or all of Tarski's Axioms of Geometry.
In $\GG$, equidistance $\equiv$ is necessarily an undefined term with respect to betweenness $\mathsf B$.

Proof:
Our assertion is that $\equiv$ cannot be defined in terms of $\mathsf B$.
{{AimForCont}} that it can.
Call this assumption $\paren A$.
If $\paren A$ holds, it must hold in all systems.
Let one such system be $\tuple {\R^2, \mathsf B_1, \equiv_1}$ where:
:$\R^2$ is the cartesian product of the set of real numbers with itself
:$\mathsf B_1$ is a ternary relation of betweenness
:$\equiv_1$ is a quaternary relation of equidistance
Let $\GG$ be the discipline preceding the given discipline, where $\GG$ is as defined above (excluding both $\equiv$ and $\mathsf B$).
{{questionable|if $\GG$ isn't strong enough to create $\R^2$, how can we use it? There is something incorrect in my presentation, particularly since we're going to use $\cdot$ and $\le$ -- GFP.}}
Define $\mathsf B_1$ as follows:
{{:Definition:Between (Geometry)}}
Define $\equiv_1$ as follows:
{{:Definition:Equidistance}}
Now, define the isomorphism $\phi$ on $\struct {\R^2, \mathsf B_2, \equiv_2}$ as:
:$\phi: \R^2 \to \R^2$ on $\struct {\R^2, \mathsf B_1, \equiv_1}, \tuple {x_1, x_2} \mapsto \tuple {x_1, 2 x_2}$
{{finish|prove that $\phi$ is an isomorphism}}
Now consider the system:
:$\struct {\R^2, \mathsf B_2, \equiv_2}$
where $\mathsf B_2$ and $\equiv_2$ are the relations defined as above, but on the elements in the images of $\mathsf B_1$ and $\equiv_1$, respectively.
Observe that $\mathsf B_1$ and $\mathsf B_2$ coincide, because in:
:$\paren {x_1 - y_1} \cdot \paren {2 y_2 - 2 z_2} = \paren {2 x_2 - 2 y_2} \cdot \paren {y_1 - z_1} \land$
:$\paren {0 \le \paren {x_1 - y_1} \cdot \paren {y_1 - z_1} } \land \paren {0 \le \paren {2 x_2 - 2 y_2} \cdot \paren {2 y_2 - 2 z_2} }$
we can simply factor out the $2$ and divide both sides of the equality of inequality by $2$.
But consider the elements:
:$p_1 = \tuple {0, 0}$
:$p_2 = \tuple {0, 1}$
:$p_3 = \tuple {1, 0}$
Observe that $p_1 p_2 \equiv_1 p_1 p_3$:
:$\paren {0 - 0}^2 + \paren {0 - 1}^2 = \paren {0 - 1}^2 + \paren {0 - 0}^2$
But $\map \neg {p_1 p_2 \equiv_2 p_1 p_3}$:
:$\paren {0 - 0}^2 + \paren {0 - 2}^2 \ne \paren {0 - 1}^2 + \paren {0 - 0}^2$
But both $\struct {\R^2, \mathsf B_1, \equiv_1}$ and $\struct {\R^2, \mathsf B_2, \equiv_2}$ are both models of $\GG$.
{{explain|prove it}}
Recall that if $\paren A$ holds, it must hold in all systems.
But it does not.
Hence $\paren A$ is false, from Proof by Contradiction.
{{qed}}
{{proofread}}
{{help}}
Theorem: Existence and Uniqueness of Adjoint

Let $\mathbb F \in \set {\R, \C}$.
{{explain|How sure are we that this does not hold for ALL subfields of $\C$, not just these ones? <br>At least, the Hilbert assumptions forces $\mathbb F$ to be complete.}}
Let $\struct {\HH, \innerprod \cdot \cdot_\HH}$ and $\struct {\KK, \innerprod \cdot \cdot_\KK}$ be Hilbert spaces over $\mathbb F$.
Let $A: \HH \to \KK$ be a bounded linear transformation. 
Then there exists a unique bounded linear transformation $B: \KK \to \HH$ such that: 
:$\innerprod {\map A x} y_\KK = \innerprod x {\map B y}_\HH$
for all $x \in \HH$ and $y \in \KK$. 
That is:
:each bounded linear transformation between Hilbert spaces has a unique adjoint.

Proof:
We first show that such a unique mapping $B$ exists, without first insisting on a bounded linear transformation.
Theorem: Linear Transformation is Isomorphism iff Inverse Equals Adjoint

Let $\struct {\HH, \innerprod \cdot \cdot_\HH}$ and $\struct {\KK, \innerprod \cdot \cdot_\KK}$ be Hilbert spaces.
Let $U : \HH \to \KK$ be a bounded linear transformation.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$U$ is an isomorphism}}
{{item|(2):|$U$ is invertible and $U^{-1} {{=}} U^*$, where $U^*$ denotes the adjoint of $U$}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Suppose that:
:$U$ is an isomorphism.
That is:
:$\innerprod {U g} {U h}_\KK = \innerprod g h_\HH$
for each $g, h \in \HH$.
Let $g, h \in \HH$.
From the definition of the adjoint, we have: 
:$\innerprod g h_\HH = \innerprod g {U^* U h}_\KK$
So, from Inner Product is Sesquilinear, we have: 
:$\innerprod g {h - U^* U h}_\HH = 0$
Setting $g = h - U^* U h$, we have: 
:$\innerprod {h - U^* U h} {h - U^* U h}_\HH = 0$
So from the positiveness of the inner product, we have: 
:$h - U^* U h = 0$
so:
:$h = U^* U h$
for all $h \in \HH$.
So: 
:$U^* U = I_\HH$
where $I_\HH$ is the identity map on $\HH$. 
From Hilbert Space Isomorphism is Bijection, we have that: 
:$U$ is a bijection. 
So: 
:$U$ is invertible.
Let $U^{-1} : \KK \to \HH$ be the inverse of $U$. 
Then, we have: 
{{begin-eqn}}
{{eqn	| l = U^{-1}
	| r = I_\HH U^{-1}
}}
{{eqn	| r = \paren {U^* U} U^{-1}
}}
{{eqn	| r = U^* \paren {U U^{-1} }
}}
{{eqn	| r = U^*
}}
{{end-eqn}}
So:
:$U$ is invertible with $U^{-1} = U^*$.
{{qed|lemma}}
Theorem: Limit of Sequence is Limit of Real Function

Let $\sequence {a_n}$ be a real sequence.
Let $f: x \mapsto \map f x$ be a real function.
Suppose the limit:
:$\ds \lim_{x \mathop \to +\infty} \map f x$
exists.
If for every $n$ in the domain of $\sequence {a_n}$:
:$\map f n = a_n$
then:
:$\ds \lim_{n \mathop \to +\infty} \ a_n = \ds \lim_{x \mathop \to +\infty} \map f x$

Proof:
This is an instance of Limit of Function by Convergent Sequences, as the reals form a metric space.
{{qed}}
Theorem: Equality of Cartesian Products

Let $A, B, C, D$ be nonempty sets.
Then:
:$A \times B = C \times D \iff A = C \land B = D$
where $\times$ denotes cartesian product.

Proof:
If $A = C$ and $B = D$, it is immediate that $A \times B = C \times D$.
Now suppose that $A \times B = C \times D$.
By definition of Cartesian product:
{{begin-eqn}}
{{eqn | l = x \in A, y \in B
      | o = \leadstoandfrom
      | r = \tuple {x, y} \in A \times B
}}
{{eqn | o = \leadstoandfrom
      | r = \tuple {x, y} \in C \times D
      | c = {{Defof|Set Equality}}
}}
{{eqn | o = \leadstoandfrom
      | r = x \in C, y \in D
}}
{{end-eqn}}
It follows that $x \in A$ {{iff}} $x \in C$, and so $A = C$.
Similarly, $y \in B$ {{iff}} $y \in D$, hence $B = D$.
The result follows.
{{qed}}
Theorem: Adjoint of Composition of Linear Transformations is Composition of Adjoints

:$\paren {A B}^* = B^* A^*$

Proof:
Let ${\innerprod \cdot \cdot}_\HH$, ${\innerprod \cdot \cdot}_\KK$ and ${\innerprod \cdot \cdot}_\LL$ denote inner products over $\HH$, $\KK$ and $\LL$ respectively.
Let $h \in \HH$ and $l \in \LL$.
Then:
{{begin-eqn}}
{{eqn | l = \innerprod {\map {\paren {A B} } h} l_\LL
      | r = \innerprod {\map B h} {\map {A^*} l}_\KK
      | c = {{Defof|Adjoint Linear Transformation}} of $A$
}}
{{eqn | r = \innerprod h {\map {B^* A^*} l}_\HH
      | c = {{Defof|Adjoint Linear Transformation}} of $B$
}}
{{end-eqn}}
We also have, by the definition of the adjoint:
:$\innerprod {\map {\paren {A B} } h} l_\LL = \innerprod h {\map {\paren {A B}^*} l}_\LL$
So, by the uniqueness part of Existence and Uniqueness of Adjoint:
:$\paren {A B}^* = B^* A^*$
{{qed}}
Theorem: Adjoint is Involutive

:$A^{**} = A$

Proof:
Let $x \in \HH$ and $y \in \KK$ be vectors. 
By the definition of the adjoint, we have: 
:$\innerprod {A x} y_\KK = \innerprod x {A^* y}_\HH$
Taking complex conjugates, we have: 
:$\overline {\innerprod {A x} y_\KK} = \overline {\innerprod x {A^* y}_\HH}$
Using the conjugate symmetry of the inner product, we have: 
:$\innerprod y {A x}_\KK = \innerprod {A^* y} x_\HH$
So, by the definition of the adjoint:
:$\innerprod y {A x}_\KK = \innerprod y {\paren {A^*}^* x}_\HH$
From the uniqueness of the adjoint, we obtain: 
:$\paren {A^*}^* = A$
{{qed}}
Theorem: Adjoining Commutes with Inverting

Let $\HH$ and $\KK$ be Hilbert spaces.
Let $\map \BB {\HH, \KK}$ be the set of bounded linear transformations from $\HH$ to $\KK$.
Let $A \in \map \BB {\HH, \KK}$ be a bounded linear transformation on $\HH$.
Let $A^{-1} \in \map \BB {\KK, \HH}$ be an inverse for $A$.
Let $A^*$ denote the adjoint of $A$.
Then $A^*$, is invertible, and:
:$\paren {A^*}^{-1} = \paren {A^{-1} }^*$

Proof:
By definition of inverse, one has $A A^{-1} = I_\KK$, where $I_\KK$ is the identity operator on $\KK$.
From Adjoint of Composition of Linear Transformations is Composition of Adjoints and Adjoint of Identity Transformation:
:$I_\KK = {I_\KK}^* = \paren {A A^{-1} }^* = \paren {A^{-1} }^*A^*$
Similarly:
:$I_\HH = {I_\HH}^* = \paren {A^{-1} A}^* = A^* \paren {A^{-1} }^*$
Hence, by definition of inverse:
:$\paren {A^*}^{-1} = \paren {A^{-1} }^*$
Hence, by definition, $A^*$ is invertible.
{{qed}}
Theorem: Identity of Points

Two points share the same position {{iff}} they are the same points.

Proof:
Let $a$ be a point with position $P_1$.
Let $b$ be a point with position $P_2$.
By hypothesis, $P_1 = P_2$.
By Leibniz's Law, two objects are the same object {{iff}} they share every property in common.
By the definition of point, the ''only'' property possessed by a point is position.
We have:
:$P_1 = P_2 \dashv \vdash a = b$
Hence the result.
{{qed}}
Theorem: Successor of Omega

:$\omega + 1 = \set {0, 1, 2, \ldots; \omega}$
where $\omega$ is the minimally inductive set and $\omega + 1$ is the successor of $\omega$.
Note the use of the semicolon; this is the notation for multipart infinite sets.

Proof:
{{begin-eqn}}
{{eqn | l = \omega + 1
      | r = \omega \cup \set {\omega}
      | c = {{Defof|Successor Set}}
}}
{{eqn | r = \set {0, 1, 2, \ldots} \cup \set \omega
      | c = {{Defof|Von Neumann Construction of Natural Numbers}}
}}
{{eqn | r = \set {0, 1, 2, \ldots; \omega}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Formulations of Axiom of Choice

The following formulations of the Axiom of Choice are equivalent:
=== Formulation 1 ===
{{:Axiom:Axiom of Choice/Formulation 1}}
=== Formulation 2 ===
{{:Axiom:Axiom of Choice/Formulation 2}}
=== Formulation 3 ===
{{:Axiom:Axiom of Choice/Formulation 3}}
=== Formulation 4 ===
{{:Axiom:Axiom of Choice/Formulation 4}}

Proof:
=== Formulation 1 implies Formulation 2 ===
{{:Equivalence of Formulations of Axiom of Choice/Formulation 1 implies Formulation 2}}{{qed|lemma}}
Theorem: Norm of Adjoint

Let $H, K$ be Hilbert spaces.
Let $A \in \map B {H, K}$ be a bounded linear transformation.
Let $A^* \in \map B {K, H}$ be the adjoint of $A$.
Then $A$ and $A^*$ satisfy:
:$\norm A_{\map B {H, K} }^2 = \norm {A^*}_{\map B {K, H} }^2 = \norm {A^* A}_{\map B {H, H} }$
where:
:$\norm \cdot_{\map B {H, K} }$ denotes the operator norm on $\map B {H, K}$
:$\norm \cdot_{\map B {K, H} }$ denotes the operator norm on $\map B {K, H}$
:$\norm \cdot_{\map B {H, H} }$ denotes the operator norm on $\map B {H, H}$

Proof:
Let $h \in H$ such that $\norm h_H \le 1$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {A h}_K^2
      | r = \innerprod {A h} {A h}_K
      | c = {{Defof|Inner Product Norm}}
}}
{{eqn | r = \innerprod {A^* A h} h_H
      | c = {{Defof|Adjoint Linear Transformation}}
}}
{{eqn | o = \le
      | r = \norm {A^*A h}_H \norm h_H
      | c = Cauchy-Bunyakovsky-Schwarz Inequality
}}
{{eqn | o = \le
      | r = \norm {A^* A} \norm h_H^2
      | c = Fundamental Property of Norm on Bounded Linear Transformation
}}
{{eqn | o = \le
      | r = \norm {A^* A}
      | c = Assumption on $h$
}}
{{eqn | o = \le
      | r = \norm {A^*} \norm A
      | c = Norm on Bounded Linear Transformation is Submultiplicative
}}
{{end-eqn}}
By definition $(1)$ for $\norm A$, it follows that:
:$\norm A^2 \le \norm {A^* A} \le \norm {A^*} \norm A$
That is:
:$\norm A \le \norm {A^*}$.
By substituting $A^*$ for $A$, and using $A^{**} = A$ from Adjoint is Involutive, the reverse inequality is obtained.
Hence $\norm A^2 = \norm {A^* A} = \norm {A^*}^2$.
{{qed}}
Theorem: Operator is Hermitian iff Numerical Range is Real

Let $\struct {\HH, \innerprod \cdot \cdot_\HH}$ be a Hilbert space over $\C$. 
Let $A : \HH \to \HH$ be a bounded linear operator.
Let $\map W A$ be the numerical range of $A$.
Then $A$ is Hermitian {{iff}}:
:$\map W A \subseteq \R$
That is:
:$\forall h \in \HH: \innerprod {A h} h_\HH \mathop \in \R$

Proof:
=== Necessary Condition ===
Suppose that $A$ is Hermitian. 
Then: 
:$A^* = A$
where $A^*$ denotes the adjoint of $A$.
Let $x \in \HH$. 
Then, by the definition of the adjoint, we have: 
:$\innerprod {A x} x_\HH = \innerprod x {A x}_\HH$
From the conjugate symmetry of the inner product, we have: 
:$\innerprod x {A x}_\HH = \overline {\innerprod {A x} x_\HH}$
So:
:$\innerprod {A x} x_\HH = \overline {\innerprod {A x} x_\HH}$
So, from Complex Number equals Conjugate iff Wholly Real:
:$\innerprod {A x} x_\HH$ is a real number.
{{qed|lemma}}
Theorem: Operator Zero iff Inner Product Zero

Let $\HH$ be a Hilbert space over $\C$.
Let $A: \HH \to \HH$ be a bounded linear operator.
Then:
:$\forall h \in \HH: \innerprod {A h} h_\HH = 0$
{{Iff}}
:$A$ is the zero operator.

Proof:
=== Necessary Case ===
We have that $A$ is the zero operator.
Then:
:$\innerprod {A h} h = \innerprod 0 h = 0$
{{qed|lemma}}
Theorem: Linear Operator is Sum of Real and Imaginary Parts

Let $\HH$ be a Hilbert space over $\C$.
Let $A \in \map B \HH$ be a bounded linear operator.
Let $B$ and $C$ be the real and imaginary parts of $A$, respectively.
Then $A = B + i C$.

Proof:
{{begin-eqn}}
{{eqn|l = B + i C
     |r = \frac 1 2 \paren {A + A^*} + i \frac 1 {2i} \paren {A - A^*}
     |c = Definitions of $B, C$
}}
{{eqn|r = \frac 1 2 A + \frac 1 2 A^* + \frac 1 2 A - \frac 1 2 A^*
}}
{{eqn|r = A
}}
{{end-eqn}}
{{qed}}
Theorem: Characterization of Normal Operators

Let $\GF \in \set {\R, \C}$.
Let $\HH$ be a Hilbert space over $\GF$.
Let $A$ be a bounded linear operator on $\HH$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$A A^* {{=}} A^* A$, that is, $A$ is normal}}
{{item|(2):|$\forall h \in \HH: \norm {A h}_\HH {{=}} \norm {A^*h}_\HH$}}
{{end-itemize}}
where:
:$A^*$ denotes the adjoint of $A$
:$\norm {\, \cdot\,}_\HH$ denotes the inner product norm of $\HH$
If $\GF = \C$, these are also equivalent to:
:$(3): \quad \map \Re A \map \Im A = \map \Im A \map \Re A$, that is, the real and imaginary parts of $A$ commute.

Proof:
=== $(3)$ equivalent to $(1)$ ===
Suppose $\GF = \C$. 
We have: 
{{begin-eqn}}
{{eqn	| l = \map \Re A \map \Im A
		| r = \paren {\frac 1 2 \paren {A + A^\ast} } \paren {\frac 1 {2 i} \paren {A - A^\ast} }
}}
{{eqn	| r = \frac 1 {4 i} \paren {A + A^\ast} \paren {A - A^\ast} 
}}
{{eqn	| r = \frac 1 {4 i} \paren {A^2 + A^\ast A - A A^\ast - \paren {A^\ast}^2}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \map \Im A \map \Re A
		| r = \paren {\frac 1 {2 i} \paren {A - A^\ast} } \paren {\frac 1 2 \paren {A + A^\ast} }
}}
{{eqn	| r = \frac 1 {4 i} \paren {A - A^\ast} \paren {A + A^\ast}
}}
{{eqn	| r = \frac 1 {4 i} \paren {A^2 - A^\ast A + A A^\ast - \paren {A^\ast}^2}
}}
{{end-eqn}}
So $\map \Re A \map \Im A = \map \Im A \map \Re A$ {{iff}}:
:$A^\ast A - A A^\ast = -A^\ast A + A A^\ast$
This is equivalent to: 
:$A^\ast A = A A^\ast$
{{qed|lemma}}
Theorem: Bounded Linear Transformation is Isometry iff Adjoint is Left-Inverse

Let $\HH, \KK$ be Hilbert spaces.
Let $A \in \map B{\HH, \KK}$ be a bounded linear transformation.
Then $A$ is an isometry {{iff}}:
:$A^*A = I_\HH$
where $A^*$ denotes the adjoint of $A$, and $I_\HH$ the identity operator on $\HH$.

Proof:
Let $g, h \in \HH$. Then by the definition of adjoint:
:${\innerprod {A g} {A h} }_\KK = {\innerprod {A^* A g} h}_\HH$
From the uniqueness of the adjoint, it follows that:
:${\innerprod {A g} {A h} }_\KK = {\innerprod g h}_\HH$
holds {{iff}} $A^*A = I_\HH$.
Hence the result by definition of isometry.
{{qed}}
Theorem: Characterization of Unitary Operators

Let $\HH$ be a Hilbert space.
Let $A$ be a bounded linear operator on $\HH$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$A$ is a unitary operator}}
{{item|(2):|$A^* A {{=}} A A^* {{=}} I$, where $A^*$ denotes the adjoint of $A$, and $I$ denotes the identity operator}}
{{item|(3):|$A$ is a normal isometry}}
{{end-itemize}}

Proof:
=== $(3)$ implies $(2)$ ===
Suppose that $A$ is a normal isometry.
Then:
:$\innerprod {A x} {A x} = \innerprod x x$ for each $x \in \HH$.
From Adjoint is Involutive, we have:
:$\innerprod {A x} {\paren {A^\ast}^\ast x} = \innerprod x x$ 
So, from the definition of the adjoint, we have:
:$\innerprod {A^\ast A x} x = \innerprod {I x} x$ for all $x \in \HH$.
Hence from Operator with Zero Numerical Range is Zero Operator: Corollary, we have:
:$A^\ast A = I$ 
Since $A$ is normal, we also have:
:$A A^\ast = I$
{{qed|lemma}}
Theorem: Kernel of Linear Transformation is Orthocomplement of Image of Adjoint

Let $\struct {\HH, \innerprod \cdot \cdot_\HH}$ and $\struct {\KK, \innerprod \cdot \cdot_\KK}$ be Hilbert spaces.
Let $\map \BB {\HH, \KK}$ denote the set of bounded linear transformations from $\HH$ to $\KK$.
Let $A \in \map \BB {\HH, \KK}$ be a bounded linear transformation.
Then $\ker A = \paren {\Img {A^*} }^\perp$, where:
:$A^*$ denotes the adjoint of $A$
:$\ker A$ is the kernel of $A$
:$\Img {A^*}$ is the image of $A^*$
:$\perp$ signifies orthocomplementation

Proof:
Let $x \in \HH$ be arbitrary.
First fix $x \in \map \ker A$ and let $y \in \Img {A^\ast}$ be arbitrary.
We then have: 
:$y = A^\ast u$
for some $u \in \KK$. 
We have: 
:$\innerprod x y_\HH = \innerprod x {A^\ast u}_\HH$
By the definition of the adjoint, we have: 
:$\innerprod x y_\HH = \innerprod {A x} u_\KK$
But $x \in \map \ker A$, so:
:$\innerprod {A x} u_\KK = 0$ 
So: 
:$\innerprod x y_\HH = 0$ for any $y \in \Img {A^\ast}$.
So:
:$x \in \paren {\Img {A^\ast} }^\bot$
So from the definition of set inclusion, we have: 
:$\map \ker A \subseteq \paren {\Img {A^\ast} }^\bot$
Now let $x \in \paren {\Img {A^\ast} }^\bot$. 
Then for each $y \in \Img {A^\ast}$ we have: 
:$\innerprod x y_\HH = 0$
For each $y \in \Img {A^\ast}$ we can write $y = A^\ast u$ for some $u \in \KK$. 
Then we have: 
:$\innerprod x {A^\ast u}_\HH = 0$
for each $u \in \KK$, and so:
:$\innerprod {A x} u_\KK = 0$
for each $u \in \KK$ from the definition of the adjoint. 
In particular, we are free to pick $u = A x$.
Then:
:$\innerprod {A x} {A x}_\KK = 0$
So $A x = 0$ from the definition of the inner product.
So:
:$x \in \ker A$
So, from the definition of set inclusion, we have: 
:$\paren {\Img {A^\ast} }^\bot \subseteq \ker A$
Hence by definition of set equality:
:$\ker A = \paren {\Img {A^*} }^\perp$
{{qed}}
Theorem: Relation Contains Mapping is Equivalent to AoC

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation on $S \times T$.
Then:
:there exists a mapping $f \subseteq \RR$ whose domain is the same as the preimage of $\RR$
{{iff}}
:the axiom of choice holds.

Proof:
{{ProofWanted}}
{{AoC}}
Theorem: Existence of Set with Singleton Intersections with Disjoint Collection

Let $\CC$ be a set of sets all of which are pairwise disjoint.
Then:
:there exists a set $A$ such that $\forall S \in \CC: A \cap S$ is a singleton
{{iff}}
:the axiom of choice holds.

Proof:
{{proof wanted}}
{{AoC}}
Theorem: Complementary Idempotent is Idempotent

Let $\HH$ be a Hilbert space.
Let $I$ be an identity operator on $\HH$.
Let $A$ be an idempotent operator.
Then the complementary idempotent $I - A$ is also idempotent.

Proof:
{{begin-eqn}}
{{eqn|l = \paren {I - A}^2
     |r = I^2 - I A - A I + A^2
}}
{{eqn|r = I^2 - 2 A + A^2
     |c = {{Defof|Identity Operator}}
}}
{{eqn|r = I - A
     |c = {{Defof|Idempotent Operator}}
}}
{{end-eqn}}
That is, $I - A$ is idempotent.
{{qed}}
Theorem: Range of Idempotent is Kernel of Complementary Idempotent

Let $\struct {\HH, \innerprod \cdot \cdot}$ be a Hilbert space.
Let $A$ be an idempotent operator.
Then:
:$\Rng A = \map \ker {I - A}$

Proof:
If $h \in \map \ker {I - A}$, we have:
:$\map {\paren {I - A} } h = {\mathbf 0}_\HH$
That is:
:$h - A h = {\mathbf 0}_\HH$ 
so that:
:$A h = h$ 
and so:
:$h \in \Rng A$ 
So we have:
:$\map \ker {I - A} \subseteq \Rng A$ 
Now let $h \in \Rng A$.
Then there exists $k \in \HH$ such that $h = A k$. 
Then we have $h - A h = h - A^2 k$.
Since $A$ is an idempotent operator, we have:
:$A^2 k = A k = h$
Hence:
:$h - A h = {\mathbf 0}_\HH$
So:
:$h \in \map \ker {I - A}$
We therefore obtain:
:$\Rng A \subseteq \map \ker {I - A}$
So:
:$\Rng A = \map \ker {I - A}$
{{qed}}
Theorem: Real Natural Logarithm Function is Continuous

The real natural logarithm function is continuous.

Proof:
We have that the Natural Logarithm Function is Differentiable.
The result follows from Differentiable Function is Continuous.
{{qed}}
Theorem: Real Natural Logarithm Function is Continuous

The real natural logarithm function is continuous.

Proof:
From Bounds of Natural Logarithm:
:$\dfrac 1 2 < \map \ln 2 < 1$
Fix $x \in \R$.
Consider $\dfrac x {\map \ln 2}$.
From Rationals are Everywhere Dense in Topological Space of Reals:
:$\forall \epsilon \in \R_{>0} \exists r \in \Q : \size {r - \dfrac x {\map \ln 2} } < \epsilon$
Thus:
{{begin-eqn}}
{{eqn | l = \size {r - \dfrac x {\map \ln 2} }
      | o = <
      | r = \epsilon
}}
{{eqn | ll= \leadsto
      | l = \map \ln 2 \size {r - \dfrac x {\map \ln 2} }
      | r = \size {\map \ln {2^r} - x }
      | c = Natural Logarithm of Rational Power
}}
{{eqn | o = < 
      | r = \epsilon \, \map \ln 2
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | o = < 
      | r = \epsilon
      | c = as $\map \ln 2 < 1$
}}
{{eqn | ll= \leadsto
      | l = \size {\map \ln t - x}
      | o = <
      | r = \epsilon
      | c = substituting $t = 2^r$
}}
{{end-eqn}}
Thus:
:$\forall \epsilon \in \R_{>0}: \exists t \in \R_{>0}: \size {\map \ln t - x} < \epsilon$
Thus, the image of $\R_{>0}$ under $\ln$ is everywhere dense in $\R$.
From Monotone Real Function with Everywhere Dense Image is Continuous, $\ln$ is continuous on $\R_{>0}$.
Hence the result.
{{qed}}
Theorem: Characterization of Projections

Let $\HH$ be a Hilbert space.
Let $A \in \map B \HH$ be an idempotent operator.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$A$ is a projection in the Hilbert space sense}}
{{item|(2):|$A$ is the orthogonal projection onto $\Img A$}}
{{item|(3):|$\norm A {{=}} 1$, where $\norm {\, \cdot \,}$ is the norm on bounded linear operators}}
{{item|(4):|$A$ is Hermitian}}
{{item|(5):|$A$ is normal}}
{{item|(6):|$\forall h \in \HH: \innerprod {A h} h_\HH \ge 0$}}
{{item|(7):|$\forall h \in \HH: \innerprod {A h} h_\HH {{=}} \norm {A h}^2$}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Let $K = \Img A$.
From {{Corollary|Range of Idempotent is Kernel of Complementary Idempotent|2}}, $K$ is a closed linear subspace of $\HH$. 
Hence we can define the orthogonal projection $P_K$. 
We just need to show that:
:$A = P_K$
From Unique Point of Minimal Distance to Closed Linear Subspace of Hilbert Space iff Orthogonal, for each $h \in \HH$:
:$P_K h$ is the unique element of $K$ such that $h - P_K h \perp K$
In other words:
:$P_K h$ is the unique element of $K$ such that $h - P_K h \in K^\bot$, where $K^\bot$ is the orthocomplement of $K$. 
Since $A$ is a projection, we have:
:$K^\bot = \paren {\Img A}^\perp = \map \ker A$ 
Now note that we have:
:$\map A {h - A h} = A h - A^2 h = A h - A h = {\mathbf 0}_\HH$
Since $P_K h$ is unique, we have $A h = P_K h$. 
Hence $A = P_K$.
{{qed|lemma}}
Theorem: Set of Linear Subspaces is Closed under Intersection

Let $\struct {V, +, \circ}_K$ be a $K$-vector space.
Let $\family {M_i}_{i \mathop \in I}$ be an $I$-indexed family of subspaces of $V$.
Then $M := \ds \bigcap_{i \mathop \in I} M_i$ is also a subspace of $V$.

Proof:
It needs to be demonstrated that $M$ is:
:$(1): \quad$ a closed algebraic structure under $+$
:$(2): \quad$ closed for scalar product $\circ$.
So let $a, b \in M$.
By definition of intersection, $a, b \in M_i$ for all $i \in I$.
As the $M_i$ are subspaces of $V$, $a + b \in M_i$ for all $i \in I$.
That is, by definition of intersection, $a + b \in M$.
It follows that $M$ is closed under $+$.
Now let $\lambda \in K, a \in M$.
By definition of intersection, $a \in M_i$ for all $i \in I$.
As the $M_i$ are subspaces of $V$, $\lambda \circ a \in M_i$ for all $i \in I$.
That is, by definition of intersection, $\lambda \circ a \in M$.
It follows that $M$ is closed under $\circ$.
Hence the result, by definition of subspace.
{{qed}}
Category:Vector Subspaces
n61jxciytzxpoqcg6jss1ihrwb7gbgb