avewright/proofwiki-math huggingface dataset:
Theorem: Characteristic Function of Normal Distribution

The characteristic function of the normal distribution with mean $\mu$ and variance $\sigma^2$ is given by:
:$\map \phi t = e^{i t \mu - \frac 1 2 t^2 \sigma^2}$

Proof:
=== {{Lemma|Characteristic Function of Normal Distribution|1}} ===
{{:Characteristic Function of Normal Distribution/Lemma 1}}{{qed|lemma}}
Theorem: Product of Subset with Intersection/Equality does not Hold

While it is the case that:
:$X \circ \paren {Y \cap Z} \subseteq \paren {X \circ Y} \cap \paren {X \circ Z}$
it is not necessarily the case that:
:$X \circ \paren {Y \cap Z} = \paren {X \circ Y} \cap \paren {X \circ Z}$

Proof:
Proof by Counterexample:
Let $a \in G$ such that $a \ne a^{-1}$.
Let $X = \set {a, a^{-1} }, Y = \set a, Z = \set {a^{-1} }$.
Then:
:$X \circ \paren {Y \cap Z} = X \circ \O = \O$
:$\paren {X \circ Y} \cap \paren {X \circ Z} = \set {a^2, e} \cap \set {e, a^{-2} } \ne \O$
so:
:$X \circ \paren {Y \cap Z} \ne \paren {X \circ Y} \cap \paren {X \circ Z}$
{{qed}}
Theorem: Coset of Subgroup of Subgroup

Let $G$ be a group.
Let $H, K \le G$ be subgroups of $G$.
Let $K \subseteq H$.
Let $x \in G$.
Then either:
:$x K \subseteq H$
or:
:$x K \cap H = \O$
where $x K$ denotes the left coset of $K$ by $x$.

Proof:
Suppose $x K \cap H \ne \O$.
Then:
{{begin-eqn}}
{{eqn | l = x K \cap H
      | o = \ne
      | r = \O
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists y \in G
      | l = y
      | o = \in
      | r = x K \cap H
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = x K
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x K
      | r = y K
      | c = Left Cosets are Equal iff Element in Other Left Coset
}}
{{end-eqn}}
We have that:
:$y \in H$
and:
:$K \subseteq H$
As $H$ is a group, it is closed.
Hence:
:$\forall x \in K: y x \in H$
which means, by definition of subset product:
:$y K \subseteq H$
Hence the result.
{{qed}}
Theorem: Intersection of Left Cosets of Subgroups is Left Coset of Intersection

Let $G$ be a group.
Let $H, K \le G$ be subgroups of $G$.
Let $a, b \in G$.
Let:
:$a H \cap b K \ne \O$
where $a H$ denotes the left coset of $H$ by $a$.
Then $a H \cap b K$ is a left coset of $H \cap K$.

Proof:
Let $x \in a H \cap b K$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = a H
}}
{{eqn | ll= \leadsto
      | l = x H
      | r = a H
      | c = Left Cosets are Equal iff Element in Other Left Coset
}}
{{end-eqn}}
and similarly:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = b K
}}
{{eqn | ll= \leadsto
      | l = x K
      | r = b K
      | c = Left Cosets are Equal iff Element in Other Left Coset
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = a H \cap b K
      | r = x H \cap x K
}}
{{eqn | r = x \paren {H \cap K}
      | c = {{Corollary|Product of Subset with Intersection}}
}}
{{end-eqn}}
Hence the result by definition of left coset.
{{qed}}
Theorem: Right Cosets are Equal iff Element in Other Right Coset

Let $H x$ denote the right coset of $H$ by $x$.
Then:
:$H x = H y \iff x \in H y$

Proof:
{{begin-eqn}}
{{eqn | l = H x
      | r = H y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x y^{-1}
      | o = \in
      | r = H
      | c = Right Cosets are Equal iff Product with Inverse in Subgroup
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = H y
      | c = Element in Right Coset iff Product with Inverse in Subgroup
}}
{{end-eqn}}
{{Qed}}
Theorem: Subgroup of Subgroup with Prime Index/Corollary

Let $\struct {G, \circ}$ be a group.
Let $H$ and $K$ be subgroups of $G$.
Let $K \subsetneq H$.
Let:
:$\index G K = p$
where:
:$p$ denotes a prime number
:$\index G K$ denotes the index of $K$ in $G$.
Then:
:$H = G$

Proof:
As $K \subsetneq H$ and $K$ is a subgroups of $G$, it follows that $K$ is a proper subgroup of $H$.
That is, $K \ne H$
Hence from Subgroup of Subgroup with Prime Index:
:$H = G$
{{qed}}
Theorem: Order of Element divides Order of Centralizer

Let $G$ be a finite group.
Let $x \in G$ be an element of $G$.
Let $\map {C_G} x$ denote the centralizer of $x$.
Then:
:$\order x \divides \order {\map {C_G} x}$
where:
:$\order x$ denotes the order of $x$ in $G$
:$\divides$ denotes divisibility
:$\order {\map {C_G} x}$ denotes the order of $\map {C_G} x$.

Proof:
From Order of Cyclic Group equals Order of Generator:
:$\order x = \order {\gen x}$
where $\gen x$ denotes the subgroup of $G$ generated  by $x$.
By definition, $\gen x$ is a cyclic group.
By Cyclic Group is Abelian, all elements of $\gen x$ commute with $x$.
Thus by definition of centralizer:
:$\gen x \subseteq \map {C_G} x$
From Centralizer of Group Element is Subgroup, $\map {C_G} x$ is a subgroup of $G$.
So $\gen x$ is a subgroup of $\map {C_G} x$.
The result follows from Lagrange's theorem.
{{qed}}
Theorem: Left Coset of Stabilizer in Group of Transformations

Let $S$ be a non-empty set.
Let $G$ be a group of permutations of $S$.
Let $t \in G$.
Let $G_t$ be the set defined as:
:$G_t = \set {g \in G: \map g t = t}$
Then each left coset of $G_t$ in $G$ consists of the elements of $G$ that map $t$ to some element of $S$.
{{explain|The source work does not discuss group actions, but still defines $G_t$ as the stabilizer of $t$ in $G$. This needs to be reviewed and put into the language of group actions as a result related to transformation group action -- but this area of group theory is not as well covered in {{ProofWiki}} as it ought to be. I need to dig out my college notes on group actions, which were more comprehensive and understandable than any of the other works I have on my shelf, which will also need to be exploited properly.<br>Hence the second part of this question in Whitelaw is not covered yet.}}

Proof:
Let $x \in G$.
Consider the left coset $x G_t$.
Let $\map x t = s$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = x G_t
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y^{-1} x
      | o = \in
      | r = G_t
      | c = Element in Left Coset iff Product with Inverse in Subgroup
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {y^{-1} } {\map x t}
      | r = t
      | c = Definition of $G_t$
}}
{{eqn | ll= \leadstoandfrom
      | l = \map {y^{-1} } s
      | r = t
      | c = Definition of $s$
}}
{{eqn | ll= \leadstoandfrom
      | l = \map y t
      | r = s
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Coprime Cyclic Subgroups is Trivial

Let $G$ be a group whose identity is $e$.
Let $x, y \in G$ such that:
:$\order x \perp \order y$
where:
:$\order x, \order y$ denotes the orders of $x$ and $y$ in $G$ respectively
:$\perp$ denotes the coprimality relation.
Then:
:$\gen x \cap \gen y = \set e$
where $\gen x, \gen y$ denotes the subgroup of $G$ generated by $x$ and $y$ in $G$ respectively.

Proof:
From Order of Cyclic Group equals Order of Generator:
:$\order x = \order {\gen x}$
and:
:$\order y = \order {\gen y}$
where $\order {\gen x}, \order {\gen y}$ denote the orders of $\gen x$ and $\gen y$ respectively.
From Intersection of Subgroups is Subgroup:
:$\gen x \cap \gen y$ is a subgroup of both $\gen x$ and $\gen y$.
From Lagrange's Theorem:
:$\order {\gen x \cap \gen y} \divides \order {\gen x}$
and:
:$\order {\gen x \cap \gen y} \divides \order {\gen y}$
But as  $\order {\gen x} \perp \order {\gen y}$:
:$\order {\gen x \cap \gen y} = 1$
Hence the result by definition of trivial subgroup.
{{qed}}
Theorem: Normed Division Ring is Field iff Completion is Field

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\struct {R', \norm {\, \cdot \,}' }$ be a normed division ring completion of $\struct {R, \norm {\, \cdot \,} }$
Then:
:$R$ is a field {{iff}} $R'$ is a field.

Proof:
By the definition of a normed division ring completion then:
:$(1): \quad$ there exists a distance-preserving ring monomorphism $\phi: R \to R'$.
:$(2): \quad$ $\struct {R', \norm {\, \cdot \,}' }$ is a complete metric space.
:$(3): \quad$ The image $\phi \sqbrk R$ of $\phi$ is a dense subspace in $\struct {R', \norm {\, \cdot \,}' }$.
By image of a ring homomorphism is a subring then $\phi \sqbrk R$ is a subring of $R'$ and $\phi: R \to \phi \sqbrk R$ is an isomorphism.
Theorem: Non-Abelian Order 8 Group has Order 4 Element

Let $G$ be a non-abelian group of order $8$.
Then $G$ has at least one element of order $4$.

Proof:
Let $e \in G$ be the identity of $G$.
Let $g \in G$ be an arbitrary element of $G$ such that $g \ne e$.
From Identity is Only Group Element of Order 1, only $e$ has order $1$.
Thus from Order of Element Divides Order of Finite Group:
:$\order g \in \set {2, 4, 8}$
Suppose $\order g = 8$.
Then $G$ is cyclic.
So by Cyclic Group is Abelian, $G$ would be abelian.
So $g$ cannot be of order $8$.
Suppose all elements of $G \setminus \set e$ are of order $2$.
Then by definition $G$ is a Boolean group.
By Boolean Group is Abelian, $G$ would be abelian. 
So the only option left is for at least one element of $G$ to be of order $4$.
{{qed}}
Theorem: Group of Prime Order p has p-1 Elements of Order p

Let $p$ be a prime number.
Let $G$ be a group with identity $e$ whose order is $p$.
Then $G$ has $p - 1$ elements of order $p$.

Proof:
Let $\order g$ denote the order of an element $g$ of $G$.
From Order of Element Divides Order of Finite Group:
:$\order g \divides p$
where $\divides$ denotes divisibility.
By definition of prime number, the only divisors of $p$ are $1$ and $p$.
From Identity is Only Group Element of Order 1, only $e$ has order $1$ in $G$.
That leaves $p - 1$ elements of order $p$.
{{qed}}
Theorem: Number of Order p Elements in Group with m Order p Subgroups

Let $G$ be a group whose identity is $e$.
Let $G$ have $m$ subgroups of order $p$.
The total number of elements of $G$ of order $p$ is $m \paren {p - 1}$.

Proof:
Let $H \le G$ be a subgroup of $G$ of order $p$.
From Prime Group is Cyclic, $H$ is a cyclic group.
From Group of Prime Order p has p-1 Elements of Order p, $H$ has $p - 1$ elements of order $p$.
From Intersection of Subgroups of Prime Order, each of the $m$ sets of $p - 1$ non-identity elements of the $m$ subgroups of order $p$ are pairwise disjoint.
Each elements of $G$ order $p$ is the generator of a cyclic group of order $p$.
Therefore there are no elements of order $p$ apart from the $m \paren {p - 1}$ such elements of the $m$ subgroups of order $p$.
Hence the result.
{{qed}}
Theorem: Non-Cyclic Group of Order p^2 has p+3 Subgroups

Let $p$ be a prime number.
Let $G$ be a non-cyclic group whose order is $p^2$.
Then $G$ has exactly $p + 3$ subgroups.

Proof:
By Order of Element Divides Order of Finite Group, all elements of $G$ have order in $\set {1, p, p^2}$.
But as $G$ is non-cyclic, it can have no element of order $p^2$.
By Identity is Only Group Element of Order 1, $G$ has $p^2 - 1$ elements of order $p$.
Let $m$ denote the number of subgroups of $G$ of order $p$.
From Number of Order p Elements in Group with m Order p Subgroups, $G$ has $m \paren {p - 1}$ elements of order $p$.
Then:
{{begin-eqn}}
{{eqn | l = m \paren {p - 1}
      | r = p^2 - 1
      | c = 
}}
{{eqn | r = \paren {p + 1} \paren {p - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m
      | r = p + 1
      | c = 
}}
{{end-eqn}}
Together with the trivial subgroup and $G$ itself, that makes $p + 3$ subgroups.
{{qed}}
Theorem: Order of Finite Abelian Group with p+ Order p Elements is Divisible by p^2

Let $p$ be a prime number.
Let $G$ be a finite abelian group whose identity is $e$.
Let $G$ have at least $p$ elements of order $p$.
Then:
: $p^2 \divides \order G$
where:
:$\divides$ denotes divisibility
:$\order G$ denotes the order of $G$.

Proof:
Let $x \in G$ be of order $p$.
Consider $\gen x$, the subgroup generated by $x$.
By Group of Prime Order p has p-1 Elements of Order p, the elements of $\gen x$ are all of order $p$ except $e$.
Thus, by hypothesis, there must exist another $y \in G$ of order $p$.
Consider the subset of $G$:
:$S := \set {x^i y^j: 0 \le i, j < p}$
By the Finite Subgroup Test, $S$ is a subgroup of $G$ which has $p^2$ elements.
By Lagrange's theorem:
:$\order S \divides \order G$
But $\order S = p^2$ and so $p^2 \divides \order G$.
{{qed}}
Theorem: Order of Finite Abelian Group with p+ Order p Elements is Divisible by p^2

Let $p$ be a prime number.
Let $G$ be a finite abelian group whose identity is $e$.
Let $G$ have at least $p$ elements of order $p$.
Then:
: $p^2 \divides \order G$
where:
:$\divides$ denotes divisibility
:$\order G$ denotes the order of $G$.

Proof:
By hypothesis there are elements $x, y$ of order $3$ in $G$ such that $x, y, x^2$ are all different.
Consider the subset of $G$:
:$S := \set {x^i y^j: 0 \le i, j \le 2}$
By the Finite Subgroup Test, $S$ is a subgroup of $G$ which has $9$ elements.
By Lagrange's theorem:
:$\order S \divides \order G$
But $\order S = 9$ and so $9 \divides \order G$.
{{qed}}
Theorem: Order of Finite Abelian Group with p+ Order p Elements is Divisible by p^2

Let $p$ be a prime number.
Let $G$ be a finite abelian group whose identity is $e$.
Let $G$ have at least $p$ elements of order $p$.
Then:
: $p^2 \divides \order G$
where:
:$\divides$ denotes divisibility
:$\order G$ denotes the order of $G$.

Proof:
An example of Order of Finite Abelian Group with $p+$ Order $p$ Elements is Divisible by $p^2$, setting $p = 3$.
{{qed}}
Theorem: Abelian Group of Semiprime Order is Cyclic

Let $p$ and $q$ be distinct prime numbers.
Let $G$ be an abelian group such that:
:$\order G = p q$
where $\order G$ denotes the order of $G$.
Then $G$ is cyclic.

Proof:
By Order of Element Divides Order of Finite Group, the order of elements of $G$ are all in $\set {1, p, q, p q}$.
We have that Identity is Only Group Element of Order 1.
Suppose $G$ were to contain more than $p - 1$ elements of order $p$.
Then by Order of Finite Abelian Group with $p+$ Order $p$ Elements is Divisible by $p^2$:
:$p^2 \divides \order G$
where $\divides$ denotes divisibility.
As $p^2 \nmid p q$ it follows that $G$ contains no more than $p - 1$ elements of order $p$.
Similarly it follows that $G$ contains no more than $q - 1$ elements of order $q$.
These, along with $e$, account for $\paren {p - 1} + \paren {q - 1} + 1 = p + q - 1$ elements.
Thus the number of elements of order $p q$ is:
:$p q - \paren {p + q - 1} = \paren {p - 1} \paren {q - 1}$
which is strictly positive.
The result follows from Group whose Order equals Order of Element is Cyclic.
{{qed}}
Theorem: General Morphism Property for Groups

Let $\struct {G, \circ}$ and $\struct {H, *}$ be groups.
Let $\phi: G \to H$ be a group homomorphism.
Then:
:$\forall g_k \in H: \map \phi {g_1 \circ g_2 \circ \cdots \circ g_n} = \map \phi {g_1} * \map \phi {g_2} * \cdots * \map \phi {g_n}$

Proof:
A group is a semigroup.
The result then follows from the General Morphism Property for Semigroups.
{{Qed}}
Theorem: General Linear Group to Determinant is Homomorphism/Corollary

The kernel of the $\det$ mapping is the special linear group $\SL {n, \R}$.

Proof:
From General Linear Group to Determinant is Homomorphism:
:$\det$ is a group homomorphism.
The special linear group $\SL {n, \R}$ is the subset of $\GL {n, \R}$ such that:
:$\forall \mathbf A \in \SL {n, \R}: \map \det {\mathbf A} = 1$
From Real Multiplication Identity is One:
: $1$ is the identity of the multiplicative group of real numbers.
It follows by definition that $\SL {n, \R}$ is the kernel of the $\det$ mapping.
{{qed}}
Theorem: Quotient Group of General Linear Group by Special Linear Group

Let $\GL {n, \R}$ denote the general linear group of degree $n$ over $\R$.
Let $\SL {n, \R}$ denote the special linear group of degree $n$ over $\R$.
Then the quotient group $\GL {n, \R} / \SL {n, \R}$ is the multiplicative group of real numbers $\struct {\R_{\ne 0}, \times}$.

Proof:
Let $\det: \GL {n, \R} \to \struct {\R_{\ne 0}, \times}$ be the group homomorphism:
:$\mathbf A \mapsto \map \det {\mathbf A}$
where $\map \det {\mathbf A}$ is the determinant of $\mathbf A$.
This is demonstrated to be a homomorphism in General Linear Group to Determinant is Homomorphism
From {{Corollary|General Linear Group to Determinant is Homomorphism}}, the kernel of $\phi$ is $\SL {n, \R}$.
Thus from Kernel is Normal Subgroup of Domain, $\SL {n, \R}$ is normal in $\GL {n, \R}$.
From the First Isomorphism Theorem for Groups:
:$\Img \phi \cong \GL {n, \R} / \SL {n, \R}$
By definition, the image of $\phi$ is the multiplicative group of real numbers.
Hence the result.
{{qed}}
Theorem: Normed Division Ring Completions are Isometric and Isomorphic/Lemma 1

Let $\psi' = \phi_2 \circ \phi_1^{-1}:\phi_1 \paren R \to \phi_2 \paren R$ be the composition of $\phi_1^{-1}$ with $\phi_2$. 
Then $\psi': \struct {\map {\phi_1} R, \norm {\, \cdot \,}_1 } \to \struct {\map {\phi_2} R, \norm {\, \cdot \,}_2 }$ is an isometric ring isomorphism.

Proof:
By Monomorphism Image is Isomorphic to Domain, $\phi_1:R \to \map {\phi_1} R$ and $\phi_2:R \to \map {\phi_2} R$ are ring isomorphisms.
By Distance-Preserving Image Isometric to Domain for Metric Spaces, $\phi_1:R \to \map {\phi_1} R$ and $\phi_2:R \to \map {\phi_2} R$ are isometries.
By Inverse of Algebraic Structure Isomorphism is Isomorphism, $\phi_1^{-1}:\map {\phi_1} R \to R$ is a ring isomorphism.
By Inverse of Isometry of Metric Spaces is Isometry, $\phi_1^{-1}:\map {\phi_1} R \to R$ is a ring isomorphism is an isometry.
By Composition of Ring Isomorphisms is Ring Isomorphism, $\psi'$ is a ring isomorphism.
By Composition of Isometries is Isometry, $\psi'$ is an isometry.
{{qed}}
Category:Normed Division Ring Completions are Isometric and Isomorphic
qn8vxi6qv1dlov06qjasvk6b1j25lad
Theorem: Normed Division Ring Completions are Isometric and Isomorphic/Lemma 2

Let $\psi: S_1 \to S_2$ be defined by:
:$\forall x \in S_1: \map \psi x = \ds \lim_{n \mathop \to \infty} \map {\psi'} {x_n}$
where $\ds x = \lim_{n \mathop \to \infty} x_n$ for some sequence $\sequence {x_n} \subseteq R_1$
Then $\psi$ is a well-defined mapping.

Proof:
Let $x \in S_1$.
By the definition of dense subset:
:$\map \cl {R_1} = S_1$
By Closure of Subset of Metric Space by Convergent Sequence, there exists a sequence $\sequence {x_n} \subseteq R_1 $ that converges to $x$, that is:
:$\ds \lim_{n \mathop \to \infty} x_n = x$
By Isometric Image of Cauchy Sequence is Cauchy Sequence, $\sequence {\map {\psi'} {x_n} }$ is a Cauchy sequence in $R_2 \subseteq S_2$.
Since $S_2$ is complete then the sequence $\sequence {\map {\psi'} {x_n} }$ has a limit, say $y$.
Let $\sequence {x_n}$ and $\sequence {x'_n}$ be sequences in $\map {\phi_1} R$ such that:
:$\ds \lim_{n \mathop \to \infty} x_n = \lim_{n \mathop \to \infty} x'_n = x$
Then:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} x_n - x'_n
      | r = \paren {\lim_{n \mathop \to \infty} x_n} - \paren {\lim_{n \mathop \to \infty} x'_n}
      | c = Difference Rule for Sequences in Normed Division Ring
}}
{{eqn | r = x - x
}}
{{eqn | r = 0_{S_1}
}}
{{eqn | o =
}}
{{eqn | ll= \leadsto
      | r = \lim_{n \mathop \to \infty} \norm {x_n - x'_n}_1
      | l = 0
      | c = {{Defof|Convergent Sequence in Normed Division Ring}}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \norm {\map {\psi'} {x_n} - \map {\psi'} {x'_n} }_2
      | c = {{Defof|Isometric Metric Spaces}}
}}
{{eqn | o =
}}
{{eqn | ll= \leadsto
      | r = \lim_{n \mathop \to \infty} \map {\psi'} {x_n} - \map {\psi'} {x'_n}
      | l = 0_{S_2}
      | c = {{Defof|Convergent Sequence in Normed Division Ring}}
}}
{{eqn | r = \paren {\lim_{n \mathop \to \infty} \map {\psi'} {x_n} } - \paren {\lim_{n \mathop \to \infty} \map {\psi'} {x'_n} }
      | c = Difference Rule for Sequences in Normed Division Ring
}}
{{eqn | o =
}}
{{eqn | ll= \leadsto
      | l = \lim_{n \mathop \to \infty} \map {\psi'} {x_n}
      | r = \lim_{n \mathop \to \infty} \map {\psi'} {x'_n}
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Normed Division Ring Completions are Isometric and Isomorphic
4beftu2jycnxuqj9do597ln6qpa0cis
Theorem: Normed Division Ring Completions are Isometric and Isomorphic/Lemma 3

:$\psi$ is a surjective mapping.

Proof:
Let $y \in S_2$.
By the definition of dense subset:
:$\map \cl {R_2} = S_2$
By Closure of Subset of Metric Space by Convergent Sequence:
:there exists a sequence $\sequence {y_n} \subseteq R_2 $ that converges to $y$, that is, $\ds \lim_{n \mathop \to \infty} y_n = y$
By Isometric Image of Cauchy Sequence is Cauchy Sequence, $\sequence {\map {\psi'^{-1} } {y_n} }$ is a Cauchy sequence in $R_1 \subseteq S_1$.
Because $S_1$ is complete, the sequence $\sequence {\map {\psi’^{-1} } {y_n} }$ has a limit, say $x$.
By the definition of $\psi$:
{{begin-eqn}}
{{eqn | l = \map \psi x
      | r = \lim_{n \mathop \to \infty} \map {\psi'} {\map {\psi'^{-1} } {y_n} }
}}
{{eqn | r = \lim_{n \mathop \to \infty} y_n
}}
{{eqn | r = y
}}
{{end-eqn}}
{{qed}}
Category:Normed Division Ring Completions are Isometric and Isomorphic
payln0ckpf9y9bwoo675qocyxcmncra
Theorem: Normed Division Ring Completions are Isometric and Isomorphic/Lemma 4

:$\psi$ is an isometry.

Proof:
Let $x, y \in S_1$.
Let $\sequence {x_n}$ and $\sequence {y_n}$ be sequences in $R_1$ such that $\ds \lim_{n \mathop \to \infty} x_n = x, \lim_{n \mathop \to \infty} y_n = y$.
Then:
{{begin-eqn}}
{{eqn | l = x - y
      | r = \lim_{n \mathop \to \infty} x_n - y_n
      | c = Difference Rule for Sequences in Normed Division Ring
}}
{{eqn | o =
}}
{{eqn | ll= \leadsto
      | l = \norm {x - y}
      | r = \lim_{n \mathop \to \infty} \norm {x_n - y_n}
      | c = Modulus of Limit
}}
{{eqn | r = \lim_{n \mathop \to \infty} \norm {\map {\psi'} {x_n} - \map {\psi'} {y_n} }
      | c = {{Defof|Isometry (Metric Spaces)}}
}}
{{end-eqn}}
On the other hand:
{{begin-eqn}}
{{eqn | l = \map \psi x - \map \psi y
      | r = \paren {\lim_{n \mathop \to \infty} \map {\psi'} {x_n} } - \paren {\lim_{n \mathop \to \infty} \map {\psi'} {y_n} }
      | c = Definition of $\psi$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map {\psi'} {x_n} - \map {\psi'} {y_n}
      | c = Difference Rule for Sequences in Normed Division Ring
}}
{{eqn | o =
}}
{{eqn | ll= \leadsto
      | l = \norm {\map \psi x - \map \psi y}
      | r = \lim_{n \mathop \to \infty} \norm {\map {\psi'} {x_n} - \map {\psi'} {y_n} }
      | c = Modulus of Limit
}}
{{end-eqn}}
By Convergent Sequence in Metric Space has Unique Limit:
:$\norm {x - y} = \norm {\map \psi x - \map \psi y}$
It follows that $\psi$ is distance-preserving.
By Distance-Preserving Surjection is Isometry of Metric Spaces then $\psi$ is an isometry.
{{qed}}
Category:Normed Division Ring Completions are Isometric and Isomorphic
kxb5zt2vj17fe86nce6vw7i9y8avchm