avewright/proofwiki-math huggingface dataset:
Theorem: Normed Division Ring is Dense Subring of Completion

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:
:$\struct {R, \norm {\, \cdot \,} }$ is isometrically isomorphic to a dense normed division subring of $\struct {R', \norm {\, \cdot \,}' }$.

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 \phi \sqbrk R$ 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.
By Epimorphism from Division Ring to Ring then $\phi \sqbrk R$ is a division subring of $R'$.
By Division Subring of Normed Division Ring then $\struct {\phi \sqbrk R, \norm {\, \cdot \,}' }$ is a normed division subring of $\struct {R', \norm {\, \cdot \,}' }$.
By Distance-Preserving Surjection is Isometry of Metric Spaces then $\phi: R \to \phi \sqbrk R$ is an isometry.
The result follows.
{{qed}}
Category:Normed Division Rings
Category:Complete Metric Spaces
Category:Completion of Normed Division Ring
epm1gys3mg563yr9k2591azsf5yqmiz
Theorem: Inverse of Isometric Isomorphism

Let $\struct {R, \norm {\,\cdot\,}_R}$ and $\struct {S, \norm {\,\cdot\,}_S}$ be normed division rings.
Let $\phi:R \to S$ be a mapping.
Then $\phi:R \to S$ is an isometric isomorphism {{iff}} $\phi^{-1}: S \to R$ is also an isometric isomorphism.

Proof:
By Inverse of Algebraic Structure Isomorphism is Isomorphism then:
:$\phi: R \to S$ is an ring isomorphism {{iff}} $\phi^{-1}: S \to R$ is also an ring isomorphism.
Let $d_R$ and $d_S$ be the metric induced by the norms $\norm {\,\cdot\,}_R$ and $\norm {\,\cdot\,}_S$ respectively.
By Inverse of Isometry of Metric Spaces is Isometry then:
:$\phi: \struct {R, d_R} \to \struct {S, d_S}$ is an isometry {{iff}} $\phi^{-1}: \struct {S, d_S} \to \struct {R, d_R}$ is also an isometry.
The result follows.
{{qed}}
Category:Normed Division Rings
Category:Isometric Isomorphisms (Normed Division Rings)
ic4m58fw85zup1pyqlxjrdztmvcihg9
Theorem: Isometric Isomorphism is Norm-Preserving

Let $\struct {R, \norm {\,\cdot\,}_R}$ and $\struct {S, \norm {\,\cdot\,}_S}$ be normed division rings.
Let $\phi: R \to S$ be a ring isomorphism.
Then $\phi: R \to S$ is an isometric isomorphism {{iff}} $\phi$ satisfies:
:$\forall x \in R: \norm {\map \phi x}_S = \norm x_R $

Proof:
Let $d_R$ and $d_S$ be the metric induced by the norms $\norm {\,\cdot\,}_R$ and $\norm {\,\cdot\,}_S$ respectively.
Theorem: Taylor Series of Holomorphic Function

:$\ds \map f z = \sum_{n \mathop = 0}^\infty \frac {\map {f^{\paren n} } a} {n!} \paren {z - a}^n$

Proof:
In Holomorphic Function is Analytic, it is shown that: 
:$\ds \map f z = \sum_{n \mathop = 0}^\infty \paren {\frac 1 {2 \pi i} \int_{\partial D} \frac {\map f t} {\paren {t - a}^{n + 1} } \rd t} \paren {z - a}^n$ 
for all $z \in D$.
From Cauchy's Integral Formula for Derivatives, we have: 
:$\ds \frac 1 {2 \pi i} \int_{\partial D} \frac {\map f t} {\paren {t - a}^{n + 1} } \rd t = \frac {\map {f^{\paren n} } a} {n!}$
Hence the result. 
{{qed}}
Category:Holomorphic Functions
Category:Taylor Series
nkodsog7h7k61p3ivpydfzmrrrpqsi9
Theorem: Equivalence of Definitions of Square Function

Let $\F$ denote one of the standard classes of numbers: $\N$, $\Z$, $\Q$, $\R$, $\C$.
{{TFAE|def = Square Function}}

Proof:
By definition of $n$th power (for positive $n$):
:$x^n = \begin {cases} 1 & : n = 0 \\ x \times x^{n - 1} & : n > 0 \end {cases}$
Thus:
{{begin-eqn}}
{{eqn | l = x^2
      | r = x \times x^1
      | c = 
}}
{{eqn | r = x \times x \times x^0
      | c = 
}}
{{eqn | r = x \times x \times 1
      | c = 
}}
{{eqn | r = x \times x
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Square Function
4ldmzfwuvdakhwp4s2i56933sj67710
Theorem: Subring of Non-Archimedean Division Ring

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring with non-archimedean norm $\norm {\, \cdot \,}$.
Let $\struct {S, \norm {\, \cdot \,}_S }$ be a normed division subring of $R$.
Then:
:$\norm {\, \cdot \,}_S$ is a non-archimedean norm.

Proof:
$\forall x, y \in S$:
{{begin-eqn}}
{{eqn | l = \norm {x + y}_S
      | r = \norm {x + y}
      | c = Definition of $\norm {\,\cdot\,}_S$
}}
{{eqn | o = \le
      | r = \max \set {\norm x, \norm y}
      | c = $(\text N 4)$: Ultrametric Inequality
}}
{{eqn | r = \max \set {\norm x_S, \norm y_S}
      | c = Definition of $\norm {\, \cdot \,}_S$
}}
{{end-eqn}}
{{qed}}
Category:Normed Division Rings
mnmsno5i821o90pknrspo4twwhbguqt
Theorem: Isometrically Isomorphic Non-Archimedean Division Rings

Let $\struct {R, \norm {\,\cdot\,}_R}$ and $\struct {S, \norm {\,\cdot\,}_S}$ be normed division rings.
Let $\phi:R \to S$ be an isometric isomorphism.
Then:
:$\norm {\,\cdot\,}_R$ is a non-archimedean norm {{iff}} $\norm {\,\cdot\,}_S$ is a non-archimedean norm.

Proof:
=== Necessary Condition ===
Let $\norm {\,\cdot\,}_R$ be a non-archimedean norm.
Then for all $x,y \in R$:
{{begin-eqn}}
{{eqn | l = \norm {x + y}_S
      | r = \norm {\map \phi {\map {\phi^{-1} } x} + \map \phi {\map {\phi^{-1} } y} }_S
      | c = $\phi$ is a bijection
}}
{{eqn | r = \norm {\map {\phi^{-1} } x  + \map {\phi^{-1} } y}_R
      | c = $\phi$ is an isometry.
}}
{{eqn | o = \le
      | r = \max \set {\norm {\map {\phi^{-1} } x}_R, \norm {\map {\phi^{-1} } y}_R}
      | c = $\norm {\,\cdot\,}_R$ is non-archimedean.
}}
{{eqn | r = \max \set {\norm {\map \phi {\map {\phi^{-1} } x} }_S, \norm {\map \phi {\map {\phi^{-1} } y} }_S}
      | c = $\phi$ is an isometry.
}}
{{eqn | r = \max \set {\norm x_S, \norm y_S}
      | c = $\phi$ is a bijection.
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Non-Archimedean Division Ring iff Non-Archimedean Completion

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:
:$\norm {\, \cdot \,}$ is non-archimedean {{iff}} $\norm {\, \cdot \,}'$ is non-archimedean.

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 \phi \sqbrk R$ is a dense subspace in $\struct {R', \norm {\, \cdot \,}' }$.
By Normed Division Ring is Dense Subring of Completion, $\phi \sqbrk R$ is a dense normed division subring of $R'$ and $\phi: R \to \map \phi R$ is an isometric isomorphism.
By Isometrically Isomorphic Non-Archimedean Division Rings, $\struct {R, \norm {\, \cdot \,} }$ is non-archimedean {{iff}} $\struct {\phi \sqbrk R, \norm {\, \cdot \,}' }$ is.
So it remains to show that $\struct {\phi \sqbrk R, \norm {\, \cdot \,}' }$ non-archimedean {{iff}} $\struct {R', \norm {\, \cdot \,}' }$ is.
Theorem: Domain of Integer Square Function

The domain of the integer square function is the entire set of integers $\Z$.

Proof:
The operation of integer multiplication is defined on all integers.
Thus:
:$\forall x \in \Z: \exists y \in \Z: x^2 = y$
Hence the result by definition of domain.
{{qed}}
Category:Square Function
thaqmabzebfpu0jntuszq9f2o226uxb
Theorem: Image of Integer Square Function

The image of the integer square function is the set of square numbers.

Proof:
Follows directly by definition of the integer square function.
{{qed}}
Category:Square Function
crigqa9nrja5iymme5m6dh111j0ao06
Theorem: Restriction of Real Square Mapping to Positive Reals is Bijection

Let $f: \R \to \R$ be the real square function:
:$\forall x \in \R: \map f x = x^2$
Let $g: \R_{\ge 0} \to R_{\ge 0} := f {\restriction_{\R_{\ge 0} \times R_{\ge 0} } }$ be the restriction of $f$ to the positive real numbers $\R_{\ge 0}$.
Then $g$ is a bijective restriction of $f$.

Proof:
From Order is Preserved on Positive Reals by Squaring, $f$ is strictly increasing on $\R_{\ge 0}$.
By definition, a strictly increasing real function is strictly monotone.
The result follows from Strictly Monotone Real Function is Bijective.
{{qed}}
Theorem: Inverse of Real Square Function on Positive Reals

Let $f: \R_{\ge 0} \to R_{\ge 0}$ be the restriction of the real square function to the positive real numbers $\R_{\ge 0}$.
The inverse of $f$ is $f^{-1}: \R_{\ge 0} \times R_{\ge 0}$ defined as:
:$\forall x \in \R_{\ge 0}: \map {f^{-1} } x = \sqrt x$
where $\sqrt x$ is the positive square root of $x$.

Proof:
From Restriction of Real Square Mapping to Positive Reals is Bijection, $f$ is a bijection.
By definition of the positive square root:
:$y = \sqrt x \iff x = y^2$
for $x, y \in \R_{\ge 0}$.
Hence the result.
{{qed}}
Theorem: Real Square Function is not Bijective

Let $f: \R \to \R$ be the real square function:
:$\forall x \in \R: \map f x = x^2$
Then $f$ is not a bijection.

Proof:
From Real Square Function is not Injective, $f$ is not an injection.
From Real Square Function is not Surjective, $f$ is not a surjection.
The result follows by definition of bijection.
{{qed}}
Theorem: Inverse of Linear Function on Real Numbers

Let $a, b \in \R$ be real numbers such that $a \ne 0$.
Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = a x + b$
Then the inverse of $f$ is given by:
:$\forall y \in \R: \map {f^{-1} } y = \dfrac {y - b} a$

Proof:
We have that Linear Function on Real Numbers is Bijection.
Let $y = \map f x$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | r = \map f x
      | c = 
}}
{{eqn | r = a x + b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \dfrac {y - b} a
      | c = 
}}
{{end-eqn}}
and so:
:$\forall y \in \R: \map {f^{-1} } y = \dfrac {y - b} a$
{{qed}}
Theorem: Linear Function on Real Numbers is Bijection

Let $a, b \in \R$ be real numbers.
Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = a x + b$
Then $f$ is a bijection {{iff}} $a \ne 0$.

Proof:
Let $a \ne 0$.
Let $y = \map f x$.
{{begin-eqn}}
{{eqn | l = y
      | r = \map f x
      | c = 
}}
{{eqn | r = a x + b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \dfrac {y - b} a
      | c = 
}}
{{end-eqn}}
and so:
:$\forall y \in \R: \exists x \in \R; y = \map f x$
demonstrating that $f$ is surjective.
Then:
{{begin-eqn}}
{{eqn | l = \map f {x_1}
      | r = \map f {x_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a x_1 + b
      | r = a x_2 + b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a x_1
      | r = a x_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1
      | r = x_2
      | c = as $a \ne 0$
}}
{{end-eqn}}
demonstrating that $f$ is injective.
Thus $f$ is a bijection by definition.
{{qed|lemma}}
Let $a = 0$.
Then:
:$\forall x \in \R: \map f x = b$
Thus for example:
:$\map f 1 = \map f 2$
and $f$ is trivially not injective.
Also:
:$\forall y \in \R: y \ne b \implies \nexists x \in \R: \map f x = y$
and $f$ is equally trivially not surjective either.
Thus $f$ is not a bijection by definition.
{{qed}}
Theorem: Composition of Linear Real Functions

Let $a, b, c, d \in \R$ be real numbers.
Let $\theta_{a, b}: \R \to \R$  be the real function defined as:
:$\forall x \in \R: \map {\theta_{a, b} } x = a x + b$
Let $\theta_{c, d} \circ \theta_{a, b}$ denote the composition of $\theta_{c, d}$ with $\theta_{a, b}$.
Then:
:$\theta_{c, d} \circ \theta_{a, b} = \theta_{a c, b c + d}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\paren {\theta_{c, d} \circ \theta_{a, b} } } x
      | r = \map {\theta_{c, d} } {\map {\theta_{a, b} } x}
      | c = 
}}
{{eqn | r = \map {\theta_{c, d} } {a x + b}
      | c = 
}}
{{eqn | r = c \paren {a x + b} + d
      | c = 
}}
{{eqn | r = \paren {a c} x + \paren {b c + d}
      | c = 
}}
{{eqn | r =  \theta_{a c, b c + d}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Condition for Composition of Linear Real Functions to be Commutative

Let $a, b, c, d \in \R$ be real numbers.
Let $\theta_{a, b}: \R \to \R$  be the real function defined as:
:$\forall x \in \R: \map {\theta_{a, b} } x = a x + b$
Let $\theta_{c, d} \circ \theta_{a, b}$ denote the composition of $\theta_{c, d}$ with $\theta_{a, b}$.
Then:
:$\theta_{c, d} \circ \theta_{a, b} = \theta_{a, b} \circ \theta_{c, d}$
{{iff}}:
:$b c + d = a d + b$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\theta_{c, d} \circ \theta_{a, b} } x
      | r = \map {\theta_{a, b} \circ \theta_{c, d} } x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \theta_{a c, b c + d}
      | r = \theta_{c a, a d + b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b c + d
      | r = a d + b
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Composition of Right Inverse with Mapping is Idempotent

Let $f: S \to T$ be a mapping.
Let $g: T \to S$ be a right inverse mapping of $f$.
Then:
:$\paren {g \circ f} \circ \paren {g \circ f} = g \circ f$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {g \circ f} \circ \paren {g \circ f}
      | r = g \circ \paren {f \circ g} \circ f
      | c = Composition of Mappings is Associative
}}
{{eqn | r = g \circ I_T \circ f
      | c = {{Defof|Right Inverse Mapping}}
}}
{{eqn | r = g \circ f
      | c = {{Defof|Identity Mapping}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set of Even Integers is Equivalent to Set of Integers

Let $\Z$ denote the set of integers.
Let $2 \Z$ denote the set of even integers.
Then:
:$2 \Z \sim \Z$
where $\sim$ denotes set equivalence.

Proof:
To demonstrate set equivalence, it is sufficient to construct a bijection between the two sets.
Let $f: \Z \to 2 \Z$ defined as:
:$\forall x \in \Z: \map f x = 2 x$
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 x
      | r = 2 y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = 
}}
{{end-eqn}}
demonstrating injectivity.
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = 2 \Z
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x \in \Z
      | l = y
      | r = 2 x
      | c = {{Defof|Even Integer}}
}}
{{eqn | ll= \leadsto
      | l = y
      | o = \in
      | r = f \sqbrk \Z
      | c = 
}}
{{end-eqn}}
demonstrating surjectivity.
Hence by definition $f$ is a bijection.
{{qed}}
Theorem: Sets of Permutations of Equivalent Sets are Equivalent

Let $A$ and $B$ be sets such that:
:$A \sim B$
where $\sim$ denotes set equivalence.
Let $\map \Gamma A$ denote the set of permutations on $A$.
Then:
:$\map \Gamma A \sim \map \Gamma B$

Proof:
By definition of set equivalence, let $f: A \to B$ be a bijection.
Define $\Phi : \map \Gamma A \to \map \Gamma B$ by:
:$\map \Phi \gamma := f \circ \gamma \circ f^{-1}$
By definition of permutation, each $\gamma \in \map \Gamma A$ is a bijection.
By Composite of Bijections is Bijection, each $f \circ \gamma$ is a bijection.
By Inverse of Bijection is Bijection, the inverse mapping $f^{-1}$ is a bijection.
Then by Composite of Bijections is Bijection, each $\map \Phi \gamma = f \circ \gamma \circ f^{-1}$ is a bijection.
Thus each $\map \Phi \gamma$ is a permutation of $B$, so $\Phi$ is well-defined.
Define $\Psi : \map \Gamma B \to \map \Gamma A$ by:
:$\map \Psi \delta := f^{-1} \circ \delta \circ f$
$\Psi$ is a well-defined mapping by the same reasoning as for $\Phi$.
Then for each $\gamma \in \map \Gamma A$:
{{begin-eqn}}
{{eqn | l = \map {\paren {\Psi \circ \Phi} } \gamma
      | r = \map \Psi {\map \Phi \gamma}
}}
{{eqn | r = \map \Psi {f \circ \gamma \circ f^{-1} }
}}
{{eqn | r = f^{-1} \circ \paren {f \circ \gamma \circ f^{-1} } \circ f
}}
{{eqn | r = \paren {f \circ f^{-1} } \circ \gamma \circ \paren {f^{-1} \circ f}
      | c = Composition of Mappings is Associative
}}
{{eqn | r = I_B \circ \gamma \circ I_A
      | c = Composite of Bijection with Inverse is Identity Mapping
}}
{{eqn | r = \gamma \circ I_A
      | c = Identity Mapping is Left Identity
}}
{{eqn | r = \gamma
      | c = Identity Mapping is Right Identity
}}
{{end-eqn}}
Thus $\Psi \circ \Phi = I_{\map \Gamma A}$.
Similarly, for each $\delta \in \map \Gamma B$:
{{begin-eqn}}
{{eqn | l = \map {\Phi \circ \Psi} {\delta}
      | r = \map \Phi {\map \Psi \delta}
}}
{{eqn | r = \map \Phi {f^{-1} \circ \delta \circ f}
}}
{{eqn | r = f \circ \paren {f^{-1} \circ \delta \circ f} \circ f^{-1}
}}
{{eqn | r = \paren {f^{-1} \circ f} \circ \delta \circ \paren {f \circ f^{-1} }
      | c = Composition of Mappings is Associative
}}
{{eqn | r = I_A \circ \delta \circ I_B
      | c = Composite of Bijection with Inverse is Identity Mapping
}}
{{eqn | r = \delta \circ I_B
      | c = Identity Mapping is Left Identity
}}
{{eqn | r = \delta
      | c = Identity Mapping is Right Identity
}}
{{end-eqn}}
Thus $\Phi \circ \Psi = I_{\map \Gamma B}$.
By Bijection iff Left and Right Inverse, both $\Phi$ and $\Psi$ are bijections.
In particular:
:$\map \Gamma A \sim \map \Gamma B$
{{qed}}
Theorem: Composition of Permutations is not Commutative

Let $S$ be a set.
Let $\map \Gamma S$ denote the set of permutations on $S$.
Let $\pi, \rho$ be elements of $\map \Gamma S$
Then it is not necessarily the case that:
:$\pi \circ \rho = \rho \circ \pi$
where $\circ$ denotes composition.

Proof:
Proof by Counterexample:
Let $S := \set {1, 2, 3}$.
Let:
{{begin-eqn}}
{{eqn | l = \pi
      | o = :=
      | r = \dbinom {1 \ 2 \ 3} {2 \ 3 \ 1}
}}
{{eqn | l = \rho
      | o = :=
      | r = \dbinom {1 \ 2 \ 3} {1 \ 3 \ 2}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \pi \circ \rho
      | r = \dbinom {1 \ 2 \ 3} {2 \ 3 \ 1} \circ \dbinom {1 \ 2 \ 3} {1 \ 3 \ 2} 
}}
{{eqn | r = \dbinom {1 \ 2 \ 3} {3 \ 2 \ 1}
}}
{{end-eqn}}
while:
{{begin-eqn}}
{{eqn | l = \rho \circ \pi
      | r = \dbinom {1 \ 2 \ 3} {1 \ 3 \ 2} \circ \dbinom {1 \ 2 \ 3} {2 \ 3 \ 1}
}}
{{eqn | r = \dbinom {1 \ 2 \ 3} {2 \ 1 \ 3}
}}
{{eqn | o = \ne
      | r = \pi \circ \rho
}}
{{end-eqn}}
{{qed}}
Theorem: Three Points in Ultrametric Space have Two Equal Distances/Corollary 2

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring with non-Archimedean norm $\norm{\,\cdot\,}$,
Let $x, y \in R$ and $\norm x \ne \norm y$.
Then:
:$\norm {x + y} = \norm {x - y} = \norm {y - x} = \max \set {\norm x, \norm y}$

Proof:
Let $d$ be the metric induced by the norm $\norm {\,\cdot\,}$.
By Non-Archimedean Norm iff Non-Archimedean Metric then $d$ is a non-Archimedean metric and $\struct {R, d}$ is an ultrametric space.
Let $x, y \in R$ and $\norm x \ne \norm y$.
By the definition of the non-Archimedean metric $d$ then:
:$\norm x = \norm {x - 0} = \map d {x, 0}$
and similarly:
:$\norm y = \map d {y, 0}$
By assumption then:
:$\map d {x, 0} \ne \map d {y, 0}$
By Three Points in Ultrametric Space have Two Equal Distances then:
:$\norm {x - y} = \map d {x, y} = \max \set {\map d {x, 0}, \map d {y, 0} } = \max \set {\norm x, \norm y}$
By Norm of Negative then:
:$\norm {y - x} = \norm {x - y} = \max \set {\norm x, \norm y}$
By the definition of the non-Archimedean metric $d$ then:
:$\norm y = \norm {0 - \paren {-y} } = \map d {0, -y} = \map d {-y, 0}$
By assumption then:
:$\map d {x, 0} \ne \map d {-y, 0}$
By Three Points in Ultrametric Space have Two Equal Distances then:
:$\map d {x, -y} = \max \set {\map d {x, 0}, \map d {-y, 0} } = \max \set {\norm x, \norm y}$
By the definition of the non-Archimedean metric $d$ then:
:$\map d {x, -y} = \norm {x - \paren {-y} } = \norm {x + y}$
So $\norm {x + y} = \max \set {\norm x, \norm y}$.
The result follows.
{{qed}}
Theorem: Topological Properties of Non-Archimedean Division Rings/Centers of Open Balls

:$y \in \map {B_r} x \implies \map {B_r} y = \map {B_r} x$

Proof:
Let $y \in \map {B_r} x$.
Let $a \in \map {B_r} y$.
By the definition of an open ball, then:
:$\norm {a - y} < r$
:$\norm {y - x} < r$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {a - x}
      | r = \norm {a - y + y - x}
}}
{{eqn | o = \le
      | r = \max \set {\norm {a - y}, \norm{y - x} } 
      | c = {{Defof|Non-Archimedean Division Ring Norm}}
}}
{{eqn | o = <
      | r = r
      | c = 
}}
{{end-eqn}}
By the definition of an open ball: 
:$a \in \map {B_r} x$
Hence:
:$\map {B_r} y \subseteq \map {B_r} x$
By Norm of Negative:
:$\norm {x - y} < r$
By the definition of an open ball:
:$x \in \map {B_r} y$
Similarly it follows that:
:$\map {B_r} x \subseteq \map {B_r} y$
By set equality:
:$\map {B_r} y = \map {B_r} x$
{{qed}}
Theorem: Topological Properties of Non-Archimedean Division Rings/Centers of Closed Balls

:$y \in \map { {B_r}^-} x \implies \map { {B_r}^-} y = \map { {B_r}^-} x$

Proof:
Let $y \in \map { {B_r}^-} x$.
Let $a \in \map { {B_r}^-} y$.
By the definition of an closed ball, then:
:$\norm {a - y} \le r$
:$\norm {y - x} \le r$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {a - x}
      | r = \norm {a - y + y - x}
}}
{{eqn | r = \max \set {\norm {a - y}, \norm {y - x} } 
      | o = \le
      | c = {{Defof|Non-Archimedean Division Ring Norm}}
}}
{{eqn | r = r
      | o = \le
      | c = 
}}
{{end-eqn}}
By the definition of a closed ball, then: 
:$a \in \map { {B_r}^-} x$.
Hence:
:$\map { {B_r}^-} y \subseteq \map { {B_r}^-} x$
By Norm of Negative then:
:$\norm {x - y} \le r$
By the definition of a closed ball, then:
:$x \in \map { {B_r}^-} y$
Similarly it follows that:
:$\map { {B_r}^-} x \subseteq \map { {B_r}^-} y$
By set equality:
:$\map { {B_r}^-} x = \map { {B_r}^-} y$
{{qed}}
Theorem: Topological Properties of Non-Archimedean Division Rings/Open Balls are Clopen

:The open $r$-ball of $x$, $\map {B_r} x$, is both open and closed in the metric induced by $\norm {\,\cdot\,}$.

Proof:
Let $d$ be the metric induced by the norm $\norm {\,\cdot\,}$.
By the definition of an open ball in $\norm {\,\cdot\,}$:
:$\map {B_r} x$ is an open ball in the metric space $\struct {R, d}$.
By Open Ball of Metric Space is Open Set then $\map {B_r} x$ is open in $\struct {R, d}$.
So it remains to show that $\map {B_r} x$ is closed in $\struct {R, d}$.
Let $\map \cl {\map {B_r} x}$ denote the closure of $\map {B_r} x$.
Let $y \in \map \cl {\map {B_r} x}$.
By the definition of the closure of $\map {B_r} x$ then:
:$\forall s > 0: \map {B_s} y \cap \map {B_r} x \ne \O$
In particular:
:$\map {B_r} y \cap \map {B_r} x \ne \O$
Let $z \in \map {B_r} y \cap \map {B_r} x$.
By Centers of Open Balls:
:$\map {B_r} y = B_r \paren{z} = \map {B_r} x$
By the definition of an open ball:
:$y \in \map {B_r} y = \map {B_r} x$.
Hence:
:$\map \cl {\map {B_r} x} \subseteq \map {B_r} x$
By Subset of Metric Space is Subset of its Closure then:
:$\map {B_r} x \subseteq \map \cl {\map {B_r} x}$
So by definition of set equality:
:$\map \cl {\map {B_r} x} = \map {B_r} x$
By Set is Closed iff Equals Topological Closure then $\map {B_r} x$ is closed.
{{qed}}
Theorem: Topological Properties of Non-Archimedean Division Rings/Closed Balls are Clopen

:The closed $r$-ball of $x$, $\map { {B_r}^-} x$, is both open and closed in the metric induced by $\norm {\,\cdot\,}$.

Proof:
Let $d$ be the metric induced by the norm $\norm {\,\cdot\,}$.
By the definition of a closed ball in $\norm {\,\cdot\,}$ then:
:$\map { {B_r}^-} x$ is a closed ball in the metric space $\struct {R, d}$.
By Closed Ball is Closed in Metric Space then $\map { {B_r}^-} c$ is closed in $d$.
So it remains to show that $\map { {B_r}^-} x$ is open in $d$.
Let $y \in \map { {B_r}^-} x$.
By Centers of Closed Balls then:
:$\map { {B_r}^-} y = \map { {B_r}^-} x$
By the definition of an open ball then:
:$y \in \map {B_r} y \subseteq \map { {B_r}^-} y = \map { {B_r}^-} x$
By the definition of an open set in a metric space, $\map { {B_r}^-} x$ is open.
{{qed}}
Theorem: Topological Properties of Non-Archimedean Division Rings/Intersection of Open Balls

:$\map {B_r} x \cap \map {B_s} y \ne \O \iff \map {B_r} x \subseteq \map {B_s} y$ or $\map {B_s} y \subseteq \map {B_r} x$

Proof:
=== Necessary Condition ===
Let $z \in \map {B_r} x \cap \map {B_s} y$.
If $r \le s$ then:
{{begin-eqn}}
{{eqn| l = \map {B_r} x
     | r = \map {B_r} z
     | c = Every element in an open ball is the center
}}
{{eqn| o = \subseteq 
     | r = \map {B_s} z
     | c = as $r \le s$
}}
{{eqn| r = \map {B_s} y
     | c = Every element in an open ball is the center
}}
{{end-eqn}}
Similarly, if $s \le r$ then:
{{begin-eqn}}
{{eqn| l = \map {B_s} y 
     | o = \subseteq 
     | r = \map {B_r} x
}}
{{end-eqn}}
{{qed|lemma}}