avewright/proofwiki-math huggingface dataset:
Theorem: Equivalence Relation on Natural Numbers such that Quotient is Power of Two/Smallest Equivalence Class with no Prime

Let $\eqclass x \alpha$ denote the $\alpha$-equivalence class of a natural number $x$.
Let $r$ be the smallest natural number such that $\eqclass r \alpha$ contains no prime number.
Then $r = 9$.

Proof:
That $\alpha$ is an equivalence relation is proved in Equivalence Relation on Natural Numbers such that Quotient is Power of Two.
{{AimForCont}} $r$ is even.
Then $r = 2 s$ for some $s \in \N$.
Thus $s \in \eqclass r \alpha$ such that $s < r$.
This contradicts the supposition that $r$ is the smallest such natural number.
Thus $r$ has to be the smallest odd composite number, and so:
:$r = 3^2 = 9$
{{qed}}
Theorem: Equivalence Relation on Square Matrices induced by Positive Integer Powers

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $S$ be the set of all square matrices of order $n$.
Let $\alpha$ denote the relation defined on $S$ by:
:$\forall \mathbf A, \mathbf B \in S: \mathbf A \mathrel \alpha \mathbf B \iff \exists r, s \in \N: \mathbf A^r = \mathbf B^s$
Then $\alpha$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Equivalence Relation on Integers Modulo 5 induced by Squaring

Let $\beta$ denote the relation defined on the integers $\Z$ by:
:$\forall x, y \in \Z: x \mathrel \beta y \iff x^2 \equiv y^2 \pmod 5$
Then $\beta$ is an equivalence relation.
=== Number of $\beta$-Equivalence Classes ===
{{:Equivalence Relation on Integers Modulo 5 induced by Squaring/Number of Equivalence Classes}}
=== Addition Modulo $\beta$ is not Well-Defined ===
{{:Equivalence Relation on Integers Modulo 5 induced by Squaring/Addition Modulo Beta is not Well-Defined}}
=== Multiplication Modulo $\beta$ is Well-Defined ===
{{:Equivalence Relation on Integers Modulo 5 induced by Squaring/Multiplication Modulo Beta is Well-Defined}}

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Equivalence Relation on Integers Modulo 5 induced by Squaring/Number of Equivalence Classes

The number of distinct $\beta$-equivalence classes is $3$:
{{begin-eqn}}
{{eqn | l = \eqclass 0 \beta
      | o = 
}}
{{eqn | l = \eqclass 1 \beta
      | r = \eqclass 4 \beta
      | c = 
}}
{{eqn | l = \eqclass 2 \beta
      | r = \eqclass 3 \beta
      | c = 
}}
{{end-eqn}}

Proof:
That $\beta$ is an equivalence relation is proved in Equivalence Relation on Integers Modulo 5 induced by Squaring.
The set of residue classes modulo $5$ is:
:$\set {\eqclass 0 5, \eqclass 1 5, \eqclass 2 5, \eqclass 3 5, \eqclass 4 5}$
Then:
{{begin-eqn}}
{{eqn | l = 0 \times 0
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass 0 5 \times_5 \eqclass 0 5
      | r = \eqclass 0 5
      | c = 
}}
{{eqn | l = 1 \times 1
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass 1 5 \times_5 \eqclass 1 5
      | r = \eqclass 1 5
      | c = 
}}
{{eqn | l = 2 \times 2
      | r = 4
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass 2 5 \times_5 \eqclass 2 5
      | r = \eqclass 4 5
      | c = 
}}
{{eqn | l = 3 \times 3
      | r = 9
      | c = 
}}
{{eqn | o = \equiv
      | r = 4
      | rr= \pmod 5
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass 3 5 \times_5 \eqclass 3 5
      | r = \eqclass 4 5
      | c = 
}}
{{eqn | l = 4 \times 4
      | r = 16
      | c = 
}}
{{eqn | o = \equiv
      | r = 1
      | rr= \pmod 5
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass 4 5 \times_5 \eqclass 4 5
      | r = \eqclass 1 5
      | c = 
}}
{{end-eqn}}
Thus we have that:
:${\eqclass 1 5}^2 = {\eqclass 4 5}^2 = \eqclass 1 \beta$
:${\eqclass 2 5}^2 = {\eqclass 3 5}^2 = \eqclass 2 \beta$
Hence the result.
{{qed}}
Theorem: Equivalence Relation on Integers Modulo 5 induced by Squaring/Addition Modulo Beta is not Well-Defined

Let the $+_\beta$ operator ("addition") on the $\beta$-equivalence classes be defined as:
:$\eqclass a \beta +_\beta \eqclass b \beta := \eqclass {a + b} \beta$
Then such an operation is not well-defined.

Proof:
That $\beta$ is an equivalence relation is proved in Equivalence Relation on Integers Modulo 5 induced by Squaring.
From Number of Equivalence Classes we have:
We have:
{{begin-eqn}}
{{eqn | l = \eqclass 1 \beta
      | r = \eqclass 4 \beta
      | c = 
}}
{{eqn | l = \eqclass 2 \beta
      | r = \eqclass 3 \beta
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \eqclass 0 \beta
      | r = \eqclass 5 \beta
      | c = 
}}
{{eqn | r = \eqclass {1 + 4} \beta
      | c = 
}}
{{eqn | r = \eqclass 1 \beta + \eqclass 4 \beta
      | c = 
}}
{{eqn | r = \eqclass 1 \beta + \eqclass 1 \beta
      | c = 
}}
{{eqn | r = \eqclass 2 \beta
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Equivalence Relation on Integers Modulo 5 induced by Squaring/Multiplication Modulo Beta is Well-Defined

Let the $\times_\beta$ operator ("multiplication") on the $\beta$-equivalence classes be defined as:
:$\eqclass a \beta \times_\beta \eqclass b \beta := \eqclass {a \times b} \beta$
Then such an operation is well-defined.

Proof:
That $\beta$ is an equivalence relation is proved in Equivalence Relation on Integers Modulo 5 induced by Squaring.
Let:
{{begin-eqn}}
{{eqn | l = x, x'
      | o = \in
      | r = \eqclass x \beta
}}
{{eqn | l = y, y'
      | o = \in
      | r = \eqclass y \beta
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = x^2
      | o = \equiv
      | r = \paren {x'}^2
      | rr= \pmod 5
      | c = 
}}
{{eqn | l = y^2
      | o = \equiv
      | r = \paren {y'}^2
      | rr= \pmod 5
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x y}^2
      | o = \equiv
      | r = \paren {x' y'}^2
      | rr= \pmod 5
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Constant Sequence Converges to Constant in Normed Division Ring

:the constant sequence $\tuple {\lambda, \lambda, \lambda, \dots}$ is convergent and $\ds \lim_{n \mathop \to \infty} \lambda = \lambda$

Proof:
Let $\sequence {x_n}$ be the constant sequence: 
:$\forall n \in \N: x_n = \lambda$
Given $\epsilon \in \R_{>0}$:
:$\forall n \ge 1: \norm {x_n - \lambda} = \norm {\lambda - \lambda} = \norm 0 = 0 < \epsilon$
The result follows.
{{qed}}
Category:Sequences
Category:Normed Division Rings
h73emd7nlxa5xjkduobvr6lacofekfi
Theorem: Product of Sequence Converges to Zero with Cauchy Sequence Converges to Zero

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring with zero $0$.
Let $\sequence {x_n}$ and $\sequence {y_n} $ be sequences in $R$.
Let $\sequence {x_n}$ converge to $0$.
Let $\sequence {y_n}$ be a Cauchy sequence.
Then:
:$\sequence {x_n y_n}$ and $\sequence {y_n x_n}$ converge to $0$.

Proof:
By Cauchy Sequence in Normed Division Ring is Bounded:
:$\exists M \in \R_{>0}: \forall n, \norm {x_n} \le M$
Given $\epsilon > 0$.
Since $\sequence {x_n}$ converges to $0$ then: 
:$\exists N \in \N: \forall n > N, \norm {x_n} < \dfrac \epsilon M$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {x_n y_n - 0}
      | r = \norm {x_n y_n}
}}
{{eqn | r = \norm {x_n} \norm {y_n}
      | c = {{Norm-axiom-mult|2}}
}}
{{eqn | o = <
      | r = \norm {x_n} M
      | c = $\sequence {y_n}$ is bounded by $M$
}}
{{eqn | o = <
      | r = \paren { \dfrac \epsilon M } M
      | c = $\sequence {x_n}$ converges to $0$
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
Similarly, $\norm {y_n x_n - 0} < \epsilon$
The result follows by definition of convergence in normed division rings.
{{qed}}
Theorem: Cauchy Sequence is Bounded/Normed Division Ring

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring.
Every Cauchy sequence in $R$ is bounded.

Proof:
Let $\sequence {x_n} $ be a Cauchy sequence in $R$.
Then by definition:
:$\forall \epsilon \in \R_{\gt 0}: \exists N \in \N : \forall n, m \ge N: \norm {x_n - x_m} < \epsilon$
Let $n_1$ satisfy:
:$\forall n, m \ge n_1: \norm {x_n - x_m} < 1$
Then $\forall n \ge n_1$:
{{begin-eqn}}
{{eqn | l = \norm {x_n}
      | r = \norm {x_n - x_{n_1} + x_{n_1} }
}}
{{eqn | o = \le
      | r = \norm {x_n - x_{n_1} } + \norm {x_{n_1} }
      | c = {{Norm-axiom-mult|3}}
}}
{{eqn | o = \le
      | r = 1 + \norm {x_{n_1} }
      | c = as $n, n_1 \ge n_1$
}}
{{end-eqn}}
Let $K = \max \set {\norm {x_1}, \norm {x_2}, \dots, \norm {x_{n_1 - 1} }, 1 + \norm {x_{n_1} } }$.
Then:
:$\forall n < n_1: \norm {x_n} \le K$
:$\forall n \ge n_1: \norm {x_n} \le 1 + \norm {x_{n_1} } \le K$
It follows by definition that $\sequence {x_n}$ is bounded.
{{qed}}
Theorem: Cauchy Sequence is Bounded/Normed Division Ring

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring.
Every Cauchy sequence in $R$ is bounded.

Proof:
Let $d$ be the metric induced on $R$ be the norm $\norm {\,\cdot\,}$.
Let $\sequence {x_n} $ be a Cauchy sequence in $\struct {R, \norm {\,\cdot\,}}$.
By the definition of a Cauchy sequence in a normed division ring, $\sequence {x_n} $ is a Cauchy sequence in $\struct {R, d}$.
By Cauchy Sequence in Metric Space is Bounded, $\sequence {x_n} $ is a bounded sequence in $\struct {R, d}$.
By Sequence is Bounded in Norm iff Bounded in Metric then $\sequence {x_n} $ is a bounded sequence in $\struct {R, \norm {\,\cdot\,} }$.
{{qed}}
Theorem: Cauchy Sequence is Bounded/Normed Division Ring

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring.
Every Cauchy sequence in $R$ is bounded.

Proof:
Let $\sequence {x_n} $ be a Cauchy sequence in $R$.
By Norm Sequence of Cauchy Sequence has Limit, $\sequence {\norm {x_n} }$ is a convergent sequence in $\R$.
By Convergent Real Sequence is Bounded, $\sequence {\norm {x_n} }$ is bounded.
That is:
:$\exists M \in \R_{\gt 0}: \forall n \in \N: \norm {x_n} = \size {\norm {x_n} } \le M$
Thus, by definition, $\sequence {x_n}$ is bounded.
{{qed}}
Theorem: Cauchy Sequence with Finite Elements Prepended is Cauchy Sequence

Let $\struct {R, \norm {\, \cdot \,} }$ be a normed division ring.
Let $\sequence {x_n}$ be a sequence in $R$.
Let $N \in \N$
Let $\sequence {y_n}$ be the sequence defined by:
:$\forall n, y_n = x_{N + n}$
Let $\sequence {y_n}$ be a Cauchy sequence in $R$.
Then:
:$\sequence {x_n}$ is a Cauchy sequence in $R$.

Proof:
Given $\epsilon > 0$:
By the definition of a Cauchy sequence then:
:$\exists N': \forall n, m > N', \norm {y_n - y_m} < \epsilon$
Hence $\forall n, m > \paren {N' + N}$:
{{begin-eqn}}
{{eqn | l = \norm {x_n - x_m }
      | r = \norm {y_{n - N} - y_{m - N} }
      | c = $n, m > N$
}}
{{eqn | o = <
      | r = \epsilon
      | c = $n - N, m - N > N'$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Convergent Sequence with Finite Elements Prepended is Convergent Sequence

Let $\struct {R, \norm { \, \cdot \, } }$ be a normed division ring.
Let $\sequence {x_n}$ be a sequence in $R$.
Let $N \in \N$.
Let $\sequence {y_n}$ be the sequence defined by:
:$\forall n \in \N: y_n = x_{N + n}$
Let $\sequence {y_n}$ be a convergent sequence in $R$ with limit $l$.
Then:
:$\sequence {x_n}$ is a convergent sequence in $R$ with limit $l$.

Proof:
Let $\epsilon \in \R_{>0}$ be given.
By the definition of a convergent sequence in $R$ with limit $l$:
:$\exists N' \in \R_{>0}: \forall n \in \N: n > N' \implies \norm {y_n - l} < \epsilon$
Hence:
{{begin-eqn}}
{{eqn | q = \forall n > \paren {N' + N}
      | l = \norm {x_n - l}
      | r = \norm {y_{n - N} - l}
      | c = for $n > N$
}}
{{eqn | o = <
      | r = \epsilon
      | c = for $n - N > N'$
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Maximal Left and Right Ideal iff Quotient Ring is Division Ring

Let $R$ be a ring with unity.
Let $J$ be an ideal of $R$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$J$ is a maximal left ideal}}
{{item|(2):|$J$ is a maximal right ideal}}
{{item|(3):|the quotient ring $R / J$ is a division ring}}
{{end-itemize}}

Proof:
=== Maximal Left Ideal implies Quotient Ring is Division Ring ===
{{:Maximal Left and Right Ideal iff Quotient Ring is Division Ring/Maximal Left Ideal implies Quotient Ring is Division Ring}}{{qed|lemma}}
Theorem: Definition:Constructed Semantics/Instance 2/Rule of Addition

The Rule of Addition:
:$q \implies (q \lor p)$
is a tautology in Instance 2 of constructed semantics.

Proof:
{{handwaving}}
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Addition can be written as:
: $\neg q \lor \left({p \lor q}\right)$
This evaluates as follows:
:$\begin{array}{|cc|c|ccc|} \hline
\neg & q & \lor & (p & \lor & q) \\
\hline
1 & 0 & 0 & 0 & 0 & 0 \\
0 & 1 & 0 & 0 & 0 & 1 \\
2 & 2 & 0 & 0 & 0 & 2 \\
1 & 0 & 0 & 1 & 0 & 0 \\
0 & 1 & 0 & 1 & 1 & 1 \\
2 & 2 & 0 & 1 & 2 & 2 \\
1 & 0 & 0 & 2 & 0 & 0 \\
0 & 1 & 0 & 2 & 2 & 1 \\
2 & 2 & 0 & 2 & 0 & 2 \\
\hline
\end{array}$
{{qed}}
Theorem: Definition:Constructed Semantics/Instance 2/Rule of Commutation

The Rule of Commutation:
:$\left({p \lor q}\right) \implies \left({q \lor p}\right)$
is a tautology in Instance 2 of constructed semantics.

Proof:
{{handwaving}}
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Rule of Commutation can be written as:
:$\neg \left({p \lor q}\right) \lor \left({q \lor p}\right)$
This evaluates as follows:
:$\begin{array}{|cccc|c|ccc|} \hline
\neg & (p & \lor & q) & \lor & (q & \lor & p) \\
\hline
1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\
1 & 0 & 0 & 1 & 0 & 1 & 0 & 0 \\
1 & 0 & 0 & 2 & 0 & 2 & 0 & 0 \\
1 & 1 & 0 & 0 & 0 & 0 & 0 & 1 \\
0 & 1 & 1 & 1 & 0 & 1 & 1 & 1 \\
2 & 1 & 2 & 2 & 0 & 2 & 2 & 1 \\
1 & 2 & 0 & 0 & 0 & 0 & 0 & 2 \\
2 & 2 & 2 & 1 & 0 & 1 & 2 & 2 \\
1 & 2 & 0 & 2 & 0 & 2 & 0 & 2 \\
\hline
\end{array}$
{{qed}}
Theorem: Definition:Constructed Semantics/Instance 2/Factor Principle

The Factor Principle:
:$\left({p \implies q}\right) \implies \left({\left({r \lor p}\right) \implies \left ({r \lor q}\right)}\right)$
is a tautology in Instance 2 of constructed semantics.

Proof:
{{handwaving}}
By the definitional abbreviation for the conditional:
:$\mathbf A \implies \mathbf B =_{\text{def}} \neg \mathbf A \lor \mathbf B$
the Factor Principle can be written as:
:$\neg \left({\neg p \lor q}\right) \lor \left({\neg \left({r \lor p}\right) \lor \left ({r \lor q}\right)}\right)$
This evaluates as follows:
:$\begin{array}{|ccccc|c|cccccccc|} \hline
\neg & (\neg & p & \lor & q) & \lor & (\neg & (r & \lor & p) & \lor & (r & \lor & q)) \\
\hline
1 & 1 & 0 & 0 & 0 & 0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\
0 & 1 & 0 & 1 & 1 & 0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 1 \\
2 & 1 & 0 & 2 & 2 & 0 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 2 \\
1 & 0 & 1 & 0 & 0 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 0 & 0 \\
1 & 0 & 1 & 0 & 1 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 0 & 1 \\
1 & 0 & 1 & 0 & 2 & 0 & 1 & 0 & 0 & 1 & 0 & 0 & 0 & 2 \\
1 & 2 & 2 & 0 & 0 & 0 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 0 \\
2 & 2 & 2 & 2 & 1 & 0 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 1 \\
1 & 2 & 2 & 0 & 2 & 0 & 1 & 0 & 0 & 2 & 0 & 0 & 0 & 2 \\
1 & 1 & 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 0 & 1 & 0 & 0 \\
0 & 1 & 0 & 1 & 1 & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 1 & 1 \\
2 & 1 & 0 & 2 & 2 & 0 & 1 & 1 & 0 & 0 & 2 & 1 & 2 & 2 \\
1 & 0 & 1 & 0 & 0 & 0 & 0 & 1 & 1 & 1 & 0 & 1 & 0 & 0 \\
1 & 0 & 1 & 0 & 1 & 0 & 0 & 1 & 1 & 1 & 0 & 1 & 1 & 1 \\
1 & 0 & 1 & 0 & 2 & 0 & 0 & 1 & 1 & 1 & 0 & 1 & 2 & 2 \\
1 & 2 & 2 & 0 & 0 & 0 & 2 & 1 & 2 & 2 & 0 & 1 & 0 & 0 \\
2 & 2 & 2 & 2 & 1 & 0 & 2 & 1 & 2 & 2 & 2 & 1 & 1 & 1 \\
1 & 2 & 2 & 0 & 2 & 0 & 2 & 1 & 2 & 2 & 0 & 1 & 2 & 2 \\
1 & 1 & 0 & 0 & 0 & 0 & 1 & 2 & 0 & 0 & 0 & 2 & 0 & 0 \\
0 & 1 & 0 & 1 & 1 & 0 & 1 & 2 & 0 & 0 & 2 & 2 & 2 & 1 \\
2 & 1 & 0 & 2 & 2 & 0 & 1 & 2 & 0 & 0 & 0 & 2 & 0 & 2 \\
1 & 0 & 1 & 0 & 0 & 0 & 2 & 2 & 2 & 1 & 0 & 2 & 0 & 0 \\
1 & 0 & 1 & 0 & 1 & 0 & 2 & 2 & 2 & 1 & 0 & 2 & 2 & 1 \\
1 & 0 & 1 & 0 & 2 & 0 & 2 & 2 & 2 & 1 & 0 & 2 & 0 & 2 \\
1 & 2 & 2 & 0 & 0 & 0 & 1 & 2 & 0 & 2 & 0 & 2 & 0 & 0 \\
2 & 2 & 2 & 2 & 1 & 0 & 1 & 2 & 0 & 2 & 2 & 2 & 2 & 1 \\
1 & 2 & 2 & 0 & 2 & 0 & 1 & 2 & 0 & 2 & 0 & 2 & 0 & 2 \\
\hline
\end{array}$
{{qed}}
Theorem: Test for Left Ideal

Let $J$ be a subset of a ring $\struct {R, +, \circ}$.
Then $J$ is an left ideal of $\struct {R, +, \circ}$ {{iff}} these all hold:
:$(1): \quad J \ne \O$
:$(2): \quad \forall x, y \in J: x + \paren {-y} \in J$
:$(3): \quad \forall j \in J, r \in R: r \circ j \in J$

Proof:
=== Necessary Condition ===
Let $J$ be a left ideal of $\struct {R, +, \circ}$.
Then conditions $(1)$ to $(3)$ hold by virtue of the ring axioms and $J$ being a left ideal.
{{qed|lemma}}
Theorem: Test for Right Ideal

Let $J$ be a subset of a ring $\struct {R, +, \circ}$.
Then $J$ is a right ideal of $\struct {R, +, \circ}$ {{iff}} these all hold:
:$(1): \quad J \ne \O$
:$(2): \quad \forall x, y \in J: x + \paren {-y} \in J$
:$(3): \quad \forall j \in J, r \in R: j \circ r \in J$

Proof:
=== Necessary Condition ===
Let $J$ be a right ideal of $\struct {R, +, \circ}$.
Then conditions $(1)$ to $(3)$ hold by virtue of the ring axioms and $J$ being a right ideal.
{{qed|lemma}}
Theorem: Maximal Left and Right Ideal iff Quotient Ring is Division Ring/Maximal Left Ideal implies Quotient Ring is Division Ring

Let $R$ be a ring with unity.
Let $J$ be an ideal of $R$.
If $J$ is a maximal left ideal then the quotient ring $R / J$ is a division ring.

Proof:
Since $J \subset R$, it follows from Quotient Ring of Ring with Unity is Ring with Unity that $R / J$ is a ring with unity.
We now need to prove that every non-zero element of $\struct {R / J, +,  \circ}$ has an inverse for $\circ$ in $R / J$.
By Left Inverse for All is Right Inverse it is sufficient to show that $\struct {R / J, +,  \circ}$ has a left inverse for every non-zero element.
Let $x + J \in R / J$ not be the zero element of $R / J$.
That is, $x + J \ne J$ and $x \notin J$.
Take $K \subseteq R$ such that $K = \set {j + r \circ x: j \in J, r \in R}$.
That is, $K$ is the subset of $R$ which can be expressed as a sum of an element of $J$ and a left product in $R$ of $x$.
Now $0_R \in K$ as $0_R \in J$ and $0_R \in R$, giving $0_R + 0_R \circ x = 0_R$.
So:
:$(1): \quad K \ne \O$
Now let $g, h \in K$.
That is:
: $g = j_1 + r_1 \circ x, h = j_2 + r_2 \circ x$
Then:
{{begin-eqn}}
{{eqn | l = g + \paren{-h }
      | r = \paren{j_1 + r_1 \circ x } - \paren{j_2 + r_2  \circ x }
}}
{{eqn | r = \paren{j_1 - j_2 } + \paren{r_1 \circ x  - r_2  \circ x }
}}
{{eqn | r = \paren{j_1 - j_2 } + \paren{r_1  - r_2 } \circ x
}}
{{eqn | r = K
      | o = \in
      | c = $j_1 - j_2 \in J$ from Test for Ideal and $r_1 - r_2 \in R$
}}
{{end-eqn}}
So we have:
:$(2) \quad \forall g, h \in K, g-h \in K$
Now consider $g = \paren {j_1 + r_1 \circ x} \in K, y \in R$.
Then:
{{begin-eqn}}
{{eqn | l = y \circ g
      | r = y \circ \paren {j_1 + r_1 \circ x}
}}
{{eqn | r = \paren {y \circ j_1 } + y  \circ \paren { r_1 \circ x }
}}
{{eqn | r = \paren {y \circ j_1 } + \paren {y \circ r_1} \circ x
}}
{{eqn | r = K
      | o = \in
      | c = $\paren{y \circ j_1} \in J$, as $J$ is an ideal, while $y \circ r_1 \in R$
}}
{{end-eqn}}
Thus:
:$(3) \quad y \circ g \in K$
So Test for Left Ideal can be applied to statements $(1)$ to $(3)$, and it is seen that $K$ is a left ideal of $R$.
Now:
{{begin-eqn}}
{{eqn | l = j
      | o = \in
      | r = J
      | c = 
}}
{{eqn | ll= \leadsto
      | l = j + 0_R \circ x
      | o = \in
      | r = K
      | c = 
}}
{{eqn | ll= \leadsto
      | l = j
      | o = \in
      | r = K
      | c = 
}}
{{eqn | ll= \leadsto
      | l = J
      | o = \subseteq
      | r = K
      | c = 
}}
{{end-eqn}}
As $x = 0_R + 1_R \circ x$, it follows that $x \in K$ also.
As $x \notin J$, it follows that $K$ is a left ideal such that $J \subset K \subseteq R$.
As $J$ is a maximal left ideal, it follows that $K = R$.
Thus $1_R \in K$ and thus:
:$\exists j_0 \in J, s \in R: 1_R = j_0 + s \circ x$
So:
:$1_R + \paren {-s \circ x} = j_0 \in J$
Hence:
:$1_R + J = s \circ x + J = \paren {s + J} \circ \paren {x + J}$
So in the ring with unity $\struct {R / J, +,  \circ}$, the left inverse of $x + J$ is $s + J$.
The result follows.
Theorem: Maximal Left and Right Ideal iff Quotient Ring is Division Ring/Maximal Right Ideal implies Quotient Ring is Division Ring

Let $R$ be a ring with unity.
Let $J$ be an ideal of $R$.
If $J$ is a maximal right ideal then the quotient ring $R / J$ is a division ring.

Proof:
Since $J \subset R$, it follows from Quotient Ring of Ring with Unity is Ring with Unity that $R / J$ is a ring with unity.
We now need to prove that every non-zero element of $\struct {R / J, +,  \circ}$ has an inverse for $\circ$ in $R / J$.
By Right Inverse for All is Left Inverse it is sufficient to show that $\struct {R / J, +,  \circ}$ has a right inverse for every non-zero element.
Let $x + J \in R / J$ not be the zero element of $R / J$.
That is, $x + J \ne J$ and $x \notin J$.
Take $K \subseteq R$ such that $K = \set {j + x \circ r: j \in J, r \in R}$.
That is, $K$ is the subset of $R$ which can be expressed as a sum of an element of $J$ and a right product in $R$ of $x$.
Now $0_R \in K$ as $0_R \in J$ and $0_R \in R$, giving $0_R + x \circ 0_R = 0_R$.
So:
:$(1): \quad K \ne \O$
Now let $g, h \in K$.
That is:
:$g = j_1 + x \circ r_1, h = j_2 + x \circ r_2$
Then:
{{begin-eqn}}
{{eqn | l = g + \paren{-h }
      | r = \paren{j_1 + x \circ r_1 } - \paren{j_2 + x \circ r_2 }
}}
{{eqn | r = \paren{j_1 - j_2 } + \paren{x \circ r_1  - x \circ r_2 }
}}
{{eqn | r = \paren{j_1 - j_2 } + x \circ \paren{r_1  - r_2 }
}}
{{eqn | r = K
      | o = \in
      | c = $j_1 - j_2 \in J$ from Test for Ideal and $r_1 - r_2 \in R$
}}
{{end-eqn}}
So we have:
:$(2) \quad \forall g, h \in K, g - h \in K$
Now consider $g = \paren {j_1 + x \circ r_1} \in K, y \in R$.
Then:
{{begin-eqn}}
{{eqn | l = g \circ y
      | r = \paren {j_1 + x \circ r_1} \circ y
}}
{{eqn | r = \paren {j_1 \circ y} + \paren { x \circ r_1} \circ y
}}
{{eqn | r = \paren {j_1 \circ y} + x \circ \paren {r_1 \circ y} 
}}
{{eqn | r = K
      | o = \in
      | c = $\paren {j_1 \circ y} \in J$, as $J$ is an ideal, while $r_1 \circ y \in R$
}}
{{end-eqn}}
Thus:
: $(3) \quad g \circ y \in K$
So Test for Right Ideal can be applied to statements $(1)$ to $(3)$, and it is seen that $K$ is a right ideal of $R$.
Now:
{{begin-eqn}}
{{eqn | l = j
      | o = \in
      | r = J
      | c = 
}}
{{eqn | ll= \leadsto
      | l = j + x \circ 0_R
      | o = \in
      | r = K
      | c = 
}}
{{eqn | ll= \leadsto
      | l = j
      | o = \in
      | r = K
      | c = 
}}
{{eqn | ll= \leadsto
      | l = J
      | o = \subseteq
      | r = K
      | c = 
}}
{{end-eqn}}
Since $x = 0_R + x \circ 1_R$, then $x \in K$ too.
Since $x \notin J$, then $K$ is a right ideal such that $J \subset K \subseteq R$.
Since $J$ is a maximal right ideal, then $K = R$.
Thus $1_R \in K$ and thus:
:$\exists j_0 \in J, s \in R: 1_R = j_0 + x \circ s$
So:
:$1_R + \paren {- x \circ s} = j_0 \in J$
Hence:
:$1_R + J = x \circ s + J = \paren {x + J} \circ \paren {s + J}$
So in the ring with unity $\struct {R / J, +,  \circ}$, the right inverse of $x + J$ is $s + J$.
The result follows.
Theorem: Inverse of Injective and Surjective Mapping is Mapping

Let $f: S \to T$ be a mapping such that:
:$(1): \quad f$ is an injection
:$(2): \quad f$ is a surjection.
Then the inverse $f^{-1}$ of $f$ is itself a mapping.

Proof:
Recall the definition of the inverse of $f$:
$f^{-1} \subseteq T \times S$ is the relation defined as:
:$f^{-1} = \set {\tuple {t, s}: t = \map f s}$
Let $f: S \to T$ be a mapping such that:
::$(1): \quad f$ is an injection
::$(2): \quad f$ is a surjection.
By Inverse of Injection is Many-to-One Relation, $f^{-1}$ is many-to-one.
From Inverse of Surjection is Relation both Left-Total and Right-Total $\map {f^{-1} } y$ is left-total.
Thus $f^{-1}$ is:
:many-to-one
and
:left-total.
Hence, by definition, $f^{-1}$ is a mapping.
{{qed}}