avewright/proofwiki-math huggingface dataset:
Theorem: Nicely Normed Cayley-Dickson Construction from Associative Algebra is Alternative

Let $A = \struct {A_F, \oplus}$ be a $*$-algebra.
Let $A' = \struct {A_F, \oplus'}$ be constructed from $A$ using the Cayley-Dickson construction.
Then $A'$ is a nicely normed alternative algebra {{iff}} $A$ is a nicely normed associative algebra.

Proof:
Let the conjugation operator on $A$ be $*$.
Let $\tuple {a, b}, \tuple {c, d} \in A'$.
In order to streamline notation, let $\oplus$ and $\oplus'$ both be denoted by product notation:
{{begin-eqn}}
{{eqn | l = a \oplus b
      | o = =:
      | r = a b
}}
{{eqn | l = x \oplus' y
      | o = =:
      | r = x y
}}
{{end-eqn}}
The context will make it clear which is meant.
Let $A$ be a nicely normed associative algebra.
Then:
{{begin-eqn}}
{{eqn | l = \paren {\tuple {a, b} \tuple {a, b} } \tuple {c, d}
      | r = \tuple {a a - b b^*, a^* b + a b} \tuple {c, d}
      | c = 
}}
{{eqn | r = \tuple {\paren {a a - b b^*} c - d \paren {a^* b + a b}^*, \paren {a a - b b^*}^* d + c \paren {a^* b + a b} }
      | c = 
}}
{{eqn | r = \tuple {\paren {a a - b b^*} c - d \paren {b^* a + b^* a^*}, \paren {a^* a^* - b b^*} d + c \paren {a^* b + a b} }
      | c = {{Defof|Conjugation on Algebra}}
}}
{{eqn | r = \tuple {a a c - b b^* c - d b^* a - d b^* a^*, a^* a^* d - b b^* d + c a^* b + c a b}
      | c = $A$ is associative
}}
{{eqn | r = \tuple {a a c - b b^* c - d b^* \paren {a + a^*}, a^* a^* d - b b^* d + c \paren {a^* + a} b}
      | c = 
}}
{{eqn | r = \tuple {a a c - \norm b^2 c - d b^* \paren {2 \map \Re a}, a^* a^* d - \norm b^2 d + c \paren {2 \map \Re a} b}
      | c = $A$ is nicely normed
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = \tuple {a, b} \paren {\tuple {a, b} \tuple {c, d} }
      | r = \tuple {a, b} \tuple {a c - d b^*, a^* d + c b}
      | c = 
}}
{{eqn | r = \tuple {a \paren {a c - d b^*} - \paren {a^* d + c b} b^*, a^* \paren {a^* d - c b} + \paren {a c + d b^*} b}
      | c = 
}}
{{eqn | r = \tuple {a a c - a d b^* - a^* d b^* - c b b^*, a^* a^* d + a^* c b + a c b - d b^* b}
      | c = $A$ is associative
}}
{{eqn | r = \tuple {a a c - \paren {a + a^*} d b^* - c \norm b^2, a^* a^* d + \paren {a^* + a} c b - d b^* b}
      | c = 
}}
{{eqn | r = \tuple {a a c - \paren {2 \map \Re a} d b^* - c \norm b^2, a^* a^* d + \paren {2 \map \Re a} c b - d \norm b^2}
      | c = $A$ is nicely normed
}}
{{end-eqn}}
Thus it can be seen that:
:$\paren {\tuple {a, b} \tuple {a, b} } \tuple {c, d} = \tuple {a, b} \paren {\tuple {a, b} \tuple {c, d} }$
Similarly it can be shown that:
:$\paren {\tuple {c, d} \tuple {a, b} } \tuple {a, b} = \tuple {c, d} \paren {\tuple {a, b} \tuple {a, b} }$
and so $A'$ is seen to be an alternative algebra.
It follows from reversing the chain of equalities that if $A'$ is a nicely normed and alternative algebra then $A$ has to be a nicely normed associative algebra.
{{qed|lemma}}
Then from Cayley-Dickson Construction from Nicely Normed Algebra is Nicely Normed, we have that $A'$ is a nicely normed algebra {{iff}} $A$ is also a nicely normed algebra.
Hence the result.
{{qed}}
Theorem: Element of Universe

Let $A$ be a class, which may be either a set or a proper class.
Then:
:$\forall A: \paren {A \in U \iff \exists x: x = A}$
where $U$ is the universal class.
That is, if $A$ is an element of $U$, then $A$ is a set.

Proof:
{{begin-eqn}}
{{eqn | q = \forall A
      | l = \leftparen {A \in U}
      | o = \iff
      | r = \rightparen {\exists x: \paren {x = A \land x \in U} }
      | c = Characterization of Class Membership
}}
{{eqn | q = \forall x
      | l = x \in U
      | o =
      | c = Fundamental Law of Universal Class
}}
{{eqn | ll= \leadsto
      | q = \forall A
      | l = \leftparen {A \in U}
      | o = \iff
      | r = \rightparen {\exists x: x = A}
      | c = Conjunction with Tautology
}}
{{end-eqn}}
{{qed}}
Theorem: Unordered Pairs Exist

Let $A$ and $B$ be classes.
Then:
:$\forall A, B: \set {A, B} \in U$
where $U$ is the universal class.

Proof:
{{begin-eqn}}
{{eqn | q = \forall A, B: \exists x: \forall y
      | l = \leftparen {y \in x}
      | o = \iff
      | r = \rightparen {y = A \lor y = B}
      | c = Axiom of Pairing
}}
{{eqn | ll= \leadsto
      | q = \forall A, B: \exists x
      | l = x
      | r = \set {y: y = A \lor y = B}
      | c = {{Defof|Set Equality}}
}}
{{eqn | ll= \leadsto
      | q = \forall A, B
      | l = \set {y: y = A \lor y = B}
      | o = \in
      | r = U
      | c = Element of Universe
}}
{{eqn | ll= \leadsto
      | q = \forall A, B
      | l = \set {A, B}
      | o = \in
      | r = U
      | c = {{Defof|Doubleton}}
}}
{{end-eqn}}
{{qed}}
Theorem: Conjunction with Tautology

:$p \land \top \dashv \vdash p$

Proof:
{{BeginTableau|p \land \top \vdash p}}
{{Premise|1|p \land \top}}
{{Simplification|2|1|p|1|1}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|p \vdash p \land \top}}
{{Premise|1|p}}
{{ExcludedMiddle|2|q \lor \neg q}}
{{ExcludedMiddle|3|\top}}
{{Conjunction|4|1|p \land \top|1|3}}
{{EndTableau|qed}}
Theorem: Conjunction with Tautology

:$p \land \top \dashv \vdash p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||c|} \hline
p & p & \land & \top & \top \\
\hline
\F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Disjunction with Tautology

: $p \lor \top \dashv \vdash \top$

Proof:
{{BeginTableau|p \lor \top \vdash \top}}
{{Premise|1|p \lor \top}}
{{Assumption|2|\top}}
{{Assumption|3|p}}
{{Addition|4|3|p \lor \neg p|3|1}}
{{TableauLine
| n = 5
| pool = 3
| f = \top
| rlnk = Law of Excluded Middle/Proof Rule
| rtxt = Law of Excluded Middle
| dep = 4
| c = }}
{{ProofByCases|6|1|\top|1|2|2|3|5}}
{{EndTableau}}
{{qed|lemma}}
{{questionable|The above needs to be reviewed}}
{{BeginTableau|\top \vdash p \lor \top}}
{{Premise|1|\top}}
{{Addition|2|1|p \lor \top|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Disjunction with Tautology

: $p \lor \top \dashv \vdash \top$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|c||ccc|} \hline
p & \top & p & \lor & \top \\
\hline
F & T & F & T & T \\
T & T & T & T & T \\
\hline
\end{array}$
{{qed}}
Theorem: Conjunction with Contradiction

:$p \land \bot \dashv \vdash \bot$

Proof:
{{BeginTableau|p \land \bot \vdash \bot}}
{{Premise|1|p \land \bot}}
{{Simplification|2|1|\bot|1|2}}
{{EndTableau}}
{{qed|lemma}}
{{BeginTableau|\bot \vdash p \land \bot}}
{{Premise|1|\bot}}
{{Explosion|2|1|p \land \bot|1|From a bottom, we can prove what we like}}
{{EndTableau}}
{{qed}}
Theorem: Conjunction with Contradiction

:$p \land \bot \dashv \vdash \bot$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
$\begin{array}{|c|ccc||c|ccc|} \hline
\bot & p & \land & \bot & p \\
\hline
F & F & F & F & F \\
F & T & F & F & T \\
\hline
\end{array}$
{{qed}}
Theorem: Disjunction with Contradiction

:$p \lor \bot \dashv \vdash p$

Proof:
{{BeginTableau|p \lor \bot \vdash p}}
{{Premise|1|p \lor \bot}}
{{Assumption|2|p}}
{{Assumption|3|\bot}}
{{Explosion|4|3|p|3}}
{{ProofByCases|5|1|p|1|2|2|3|4}}
{{EndTableau|lemma}}
{{BeginTableau|p \vdash p \lor \bot}}
{{Premise|1|p}}
{{Addition|2|1|p \lor \bot|1|1}}
{{EndTableau|qed}}
Theorem: Disjunction with Contradiction

:$p \lor \bot \dashv \vdash p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, in each case, the truth values in the appropriate columns match for all boolean interpretations.
:<nowiki>$\begin{array}{|c|ccc|} \hline
 p & p & \lor & \bot \\
\hline
\F & \F & \F & \F \\
\T & \T & \T & \F \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Contradiction is Negation of Tautology

A contradiction implies and is implied by the negation of a tautology:
:$\bot \dashv \vdash \neg \top$
That is, a falsehood can not be true, and a non-truth is a falsehood.

Proof:
{{BeginTableau|\bot \vdash \neg \top}}
{{Premise|1|\bot}}
{{Assumption|2|\top}}
{{Explosion|3|1|\neg \top|1|Any statement we want}}
{{Contradiction|4|1|\bot|2|3}}
{{Explosion|5|1|\neg \top|4}}
{{EndTableau|lemma}}
{{BeginTableau|\neg \top \vdash \bot}}
{{Premise|1|\neg \top}}
{{ExcludedMiddle|2|p \lor \neg p|From the Law of Excluded Middle ...}}
{{ExcludedMiddle|3|\top|... we deduce that truth ...}}
{{NonContradiction|4|1|1|3| ... is contrary to the assumption of non-truth, which must therefore be false}}
{{EndTableau|qed}}
Theorem: Contradiction is Negation of Tautology

A contradiction implies and is implied by the negation of a tautology:
:$\bot \dashv \vdash \neg \top$
That is, a falsehood can not be true, and a non-truth is a falsehood.

Proof:
Let $p$ be a propositional formula.
Let $v$ be any arbitrary boolean interpretation of $p$.
Then $\map v p = F \iff \map v {\neg p} = T$ by the definition of the logical not.
Since $v$ is arbitrary, $p$ is false in all interpretations {{iff}} $\neg p$ is true in all interpretations.
Hence:
:$\bot \dashv \vdash \neg \top$
{{qed}}
Theorem: Contradiction is Negation of Tautology

A contradiction implies and is implied by the negation of a tautology:
:$\bot \dashv \vdash \neg \top$
That is, a falsehood can not be true, and a non-truth is a falsehood.

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values in the appropriate columns match.
$\begin{array}{|c||cc|} \hline
\top & \neg & \bot \\
\hline
\T & \T & \F \\
\hline
\end{array}$
{{qed}}
Theorem: Tautology is Negation of Contradiction

A tautology implies and is implied by the negation of a contradiction:
:$\top \dashv \vdash \neg \bot$
That is, a truth can not be false, and a non-falsehood must be a truth.

Proof:
{{BeginTableau|\top \vdash \neg \bot}}
{{Premise|1|\top}}
{{Assumption|2|\bot|If a contradiction were assumed ...}}
{{Explosion|3|2|\neg \top|2}}
{{NonContradiction|4|1, 2|1|3}}
{{Contradiction|5|1|\neg \bot|2|4}}
{{EndTableau|lemma}}
{{BeginTableau|\neg \bot \vdash \top}}
{{Premise|1|\neg \bot}}
{{Assumption|2|\neg \top|To assume a non-truth ...}}
{{SequentIntro|3|2|\bot|2|from above result}}
{{Reductio|4|1|\top|2|3}}
{{EndTableau|qed}}
Theorem: Tautology is Negation of Contradiction

A tautology implies and is implied by the negation of a contradiction:
:$\top \dashv \vdash \neg \bot$
That is, a truth can not be false, and a non-falsehood must be a truth.

Proof:
Let $p$ be a propositional formula.
Let $v$ be an arbitrary boolean interpretation of $p$.
Then:
:$\map v p = T \iff \map v {\neg p} = F$ 
by the definition of the logical not.
Since $v$ is arbitrary, $p$ is true in all interpretations {{iff}} $\neg p$ is false in all interpretations.
Hence:
:$\top \dashv \vdash \neg \bot$
{{qed}}
Theorem: Tautology is Negation of Contradiction

A tautology implies and is implied by the negation of a contradiction:
:$\top \dashv \vdash \neg \bot$
That is, a truth can not be false, and a non-falsehood must be a truth.

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values in the appropriate columns match.
$\begin{array}{|c||cc|} \hline
\bot & \neg & \top \\
\hline
\F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Cayley-Dickson Construction from Nicely Normed Algebra is Nicely Normed

Let $A = \struct {A_F, \oplus}$ be a $*$-algebra.
Let $A' = \struct {A_F, \oplus'}$ be constructed from $A$ using the Cayley-Dickson construction.
Then $A'$ is a nicely normed algebra {{iff}} $A$ is also a nicely normed algebra.

Proof:
Let the conjugation operator on $A$ be $*$.
Let $\tuple {a, b}, \tuple {c, d} \in A'$.
In order to streamline notation, let $\oplus$ and $\oplus'$ both be denoted by product notation:
:$a \oplus b =: a b$
:$x \oplus' y =: x y$
The context will make it clear which is meant.
Let $A$ be a nicely normed algebra.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {a, b} + \tuple {a, b}^*
      | r = \tuple {a, b} + \tuple {a^*, -b}
      | c = 
}}
{{eqn | r = \tuple {a + a^*, b - b}
      | c = 
}}
{{eqn | r = \tuple {a + a^*, 0}
      | c = 
}}
{{end-eqn}}
As $A$ is itself nicely normed, we have that $a + a^*$ is real.
Hence it follows that $\tuple {a + a^*, 0}$ is real.
Next:
{{begin-eqn}}
{{eqn | l = \tuple {a, b} \tuple {a, b}^*
      | r = \tuple {a, b} \tuple {a^*, -b}
      | c = 
}}
{{eqn | r = \tuple {a a^* - \tuple {-b b^*}, a^* b + \tuple {-a^* b} }
      | c = 
}}
{{eqn | r = \tuple {\norm a^2 + \norm b^2, 0}
      | c = as $A$ is nicely normed
}}
{{end-eqn}}
We have by definition of norm that $\norm a^2 + \norm b^2$ is real.
Hence it follows that $\tuple {\norm a^2 + \norm b^2, 0}$ is real.
It follows from reversing the argument that if $A'$ is not nicely normed then nor will $A$ be.
{{qed}}
Theorem: Quaternions form Algebra

The set of quaternions $\Bbb H$ forms an algebra over the field of real numbers.
This algebra is:
:$(1): \quad$ An associative algebra, but '''not''' a commutative algebra.
:$(2): \quad$ A normed division algebra.
:$(3): \quad$ A nicely normed $*$-algebra.

Proof:
The quaternions $\Bbb H$ are formed by the Cayley-Dickson Construction from the complex numbers $\C$.
From Complex Numbers form Algebra, we have that $\C$ forms:
:$(1): \quad$ An associative algebra
:$(2): \quad$ A commutative algebra
:$(3): \quad$ A normed division algebra
:$(4): \quad$ A nicely normed $*$-algebra.
From Cayley-Dickson Construction forms Star-Algebra, $\Bbb H$ is a $*$-algebra.
From Cayley-Dickson Construction from Nicely Normed Algebra is Nicely Normed, $\Bbb H$ is a nicely normed $*$-algebra.
From Cayley-Dickson Construction from Commutative Associative Algebra is Associative, $\Bbb H$ is an associative algebra.
Now suppose $\Bbb H$ formed a commutative algebra.
Then from Cayley-Dickson Construction from Real Star-Algebra is Commutative, that would mean $\C$ is a real $*$-algebra.
But from Complex Numbers form Algebra it is explicitly demonstrated that $\C$ is '''not''' a real $*$-algebra.
So $\Bbb H$ can not be a commutative algebra.
Theorem: Octonions form Algebra

The set of octonions $\Bbb O$ forms an algebra over the field of real numbers.
This algebra is:
:$(1): \quad$ An alternative algebra, but '''not''' an associative algebra.
:$(2): \quad$ A normed division algebra.
:$(3): \quad$ A nicely normed $*$-algebra.

Proof:
The octonions $\Bbb O$ are formed by the Cayley-Dickson construction from the quaternions $\Bbb H$.
From Quaternions form Algebra, we have that $\Bbb H$ forms:
:$(1): \quad$ An associative algebra
:$(2): \quad$ A normed division algebra
:$(3): \quad$ A nicely normed $*$-algebra.
From Cayley-Dickson Construction forms Star-Algebra, $\Bbb O$ is a $*$-algebra.
From Cayley-Dickson Construction from Nicely Normed Algebra is Nicely Normed, $\Bbb O$ is a nicely normed $*$-algebra.
From Nicely Normed Cayley-Dickson Construction from Associative Algebra is Alternative, $\Bbb O$ is an alternative algebra.
Now suppose $\Bbb O$ formed an associative algebra.
Then from Cayley-Dickson Construction from Commutative Associative Algebra is Associative, that would mean $\Bbb H$ is a commutative algebra.
But from Quaternions form Algebra it is explicitly demonstrated that $\Bbb H$ is '''not''' a commutative algebra.
So $\Bbb O$ cannot be a associative algebra.
Theorem: Division Algebra has No Zero Divisors

Let $A = \struct {A_F, \oplus}$ be an algebra over a field $F$.
Then $A$ is a division algebra {{iff}} it has no zero divisors.
That is:
:$\forall a, b \in A_F: a \oplus b = \mathbf 0_A \implies a = \mathbf 0_A \lor b = \mathbf 0_A$
If the product of two elements of $A$ is zero, then at least one of those elements must itself be zero.
Some sources use this as the definition of a division algebra and from it deduce:
:$\forall a, b \in A_F, b \ne \mathbf 0_A: \exists_1 x \in A_F, y \in A_F: a = b \oplus x, a = y \oplus b$

Proof:
Let $A$ be a division algebra, in the sense that:
:$\forall a, b \in A_F, b \ne \mathbf 0_A: \exists_1 x \in A_F, y \in A_F: a = b \oplus x, a = y \oplus b$
Suppose that:
:$\exists a, b \in A_F \setminus \set {\mathbf 0_A}: \mathbf 0_A = b \oplus a$
Then by definition of the zero vector we also have that $\mathbf 0_A = b \oplus \mathbf 0_A$.
So there are two elements $x$ of $A_F$ such that $\mathbf 0_A = b \oplus x$, that is, $a$ and $\mathbf 0_A$.
Similarly, suppose that:
:$\exists a, b \in A_F \setminus \set {\mathbf 0_A}: \mathbf 0_A = a \oplus b$
Then by definition of the zero vector we also have that:
:$\mathbf 0_A = \mathbf 0_A \oplus b$
So there are two elements $y$ of $A_F$ such that:
:$\mathbf 0_A = y \oplus b$
that is:
:$a$ and $\mathbf 0_A$
So $A$ can not be a division algebra.
So it follows that if:
:$\forall a, b \in A_F, b \ne \mathbf 0_A: \exists_1 x \in A_F, y \in A_F: a = b \oplus x, a = y \oplus b$
then:
:$\forall a, b \in A_F: a \oplus b = \mathbf 0_A \implies a = \mathbf 0_A \lor b = \mathbf 0_A$
{{qed|lemma}}
Now suppose that:
:$\forall a, b \in A_F: a \oplus b = \mathbf 0_A \implies a = \mathbf 0_A \lor b = \mathbf 0_A$
Suppose $\exists x_1, x_2 \in A_F, x_1 \ne x_2$ such that:
:$a = b \oplus x_1$
:$a = b \oplus x_2$
We have that $x_1 \ne x_2$ and so $x_1 - x_2 = z \ne \mathbf 0_A$.
Thus $b \oplus x_1 - b \oplus x_2 = \mathbf 0_A$.
As $\oplus$ is a bilinear mapping, it follows that:
:$b \oplus \paren {x_1 - x_2} = \mathbf 0_A$ and so $b \oplus z = \mathbf 0_A$
But $z \ne \mathbf 0_A$ and so it is not the case that:
:$\forall a, b \in A_F: a \oplus b = \mathbf 0_A \implies a = \mathbf 0_A \lor b = \mathbf 0_A$
Similarly it can be shown that if $\exists y_1, y_2 \in A_F, y_1 \ne y_2$ such that:
:$a = y_1 \oplus b$
:$a = y_2 \oplus b$
then it is not the case that:
:$\forall a, b \in A_F: a \oplus b = \mathbf 0_A \implies a = \mathbf 0_A \lor b = \mathbf 0_A$
Now suppose that:
:$\exists a, b \in A_F, b \ne \mathbf 0_A: \not \exists_1 x \in A_F: a = b \oplus x$
or
:$\exists a, b \in A_F, b \ne \mathbf 0_A: \not \exists_1 y \in A_F: a = y \oplus b$
{{finish|Haven't found an approach yet ...}}
Thus it is not the case that $\forall a, b \in A_F: a \oplus b = \mathbf 0_A \implies a = \mathbf 0_A \lor b = \mathbf 0_A$.
So it follows that if:
:$\forall a, b \in A_F: a \oplus b = \mathbf 0_A \implies a = \mathbf 0_A \lor b = \mathbf 0_A$
then:
:$\forall a, b \in A_F, b \ne \mathbf 0_A: \exists_1 x \in A_F, y \in A_F: a = b \oplus x, a = y \oplus b$
{{qed}}
Category:Division Algebras
d3z46bslqta0g1etwt1v2rscopxij78
Theorem: Normed Division Algebra is Unitary Division Algebra

Let $A = \struct {A_F, \oplus}$ be a normed divison algebra over a field $F$.
Let the unit of $A$ be $1_A$, and the zero of $A$ be $0_A$.
Then $A$ is a unitary division algebra.
Also:
:$\norm {1_A} = 1$
where $\norm {1_A}$ denotes the norm of $1_A$.

Proof:
Let $A = \struct {A_F, \oplus}$ be a normed divison algebra as defined {{hypothesis}}.
The fact that $A$ is a unitary algebra is a consequence of the definition of normed divison algebra.
From the definition of a norm, we have that:
:$\forall a \in A: \norm a = 0 \iff a = 0_A$
So, let $a, b \in A \setminus \set {0_A}$.
We have:
{{begin-eqn}}
{{eqn | l = \norm a \norm b
      | o = \ne
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \norm {a \oplus b}
      | o = \ne
      | r = 0
      | c = {{Defof|Normed Division Algebra}}: $\norm {a \oplus b} = \norm a \norm b$
}}
{{eqn | ll= \leadsto
      | l = a \oplus b
      | o = \ne
      | r = 0_A
      | c = {{Defof|Norm on Vector Space}}
}}
{{end-eqn}}
Thus for any arbitrary $a, b \ne 0_A$ we have shown that $a \oplus b \ne 0_A$.
Thus $A$ is a division algebra.
{{qed|lemma}}
Next:
{{begin-eqn}}
{{eqn | o = 
      | r = \norm a \norm {1_A}
      | c = 
}}
{{eqn | r = \norm {a \oplus 1_A}
      | c = {{Defof|Normed Division Algebra}}: $\norm {a \oplus b} = \norm a \norm b$
}}
{{eqn | r = \norm a
      | c = {{Defof|Norm on Vector Space}}
}}
{{end-eqn}}
demonstrating that $\norm {1_A} = 1$.
{{qed}}
Theorem: Zermelo's Theorem (Set Theory)

Every set of cardinals is well-ordered with respect to $\le$.

Proof:
Let $S_1$ and $S_2$ be sets which are not empty.
Suppose there exists an injection $f: S_1 \to S_2$ and another injection $g: S_2 \to S_1$.
Then by the Cantor-Bernstein-Schröder Theorem there exists a bijection between $S_1$ and $S_2$ and by definition $S_1$ is equivalent to $S_2$.
Let $\AA$ be the set of invertible mappings $\phi: A \to B$ where $A \subseteq S_1$ and $B \subseteq S_2$.
Since $S_1$ and $S_2$ are not empty, $\exists s_1 \in S_1$ and $\exists s_2 \in S_2$.
Thus we can construct the mapping $\alpha: \set {s_1} \to \set {s_2}$ such that $\map \alpha {s_1} = s_2$.
This is trivially an invertible mapping, so $\AA$ is not empty.
We can impose an ordering $\le$ on $\AA$ by letting $\phi_1 \le \phi_2 \iff \phi_1 \subseteq \phi_2$, that is, if $\phi_2$ is an extension of $\phi_1$.
Let $\CC$ be a chain in $\struct {\AA, \le}$.
Then $\ds \bigcup \set {\phi \in \CC}$ is an upper bound of every $\phi \in \CC$, and it lies in $\AA$.
The conditions of Zorn's Lemma are satisfied, so we can find a maximal element $M$ in $\AA$.
Let:
:$M_1 = \set {s_1: \tuple {s_1, s_2} \in M}$
:$M_2 = \set {s_2: \tuple {s_1, s_2} \in M}$
We have that $M_1 \subsetneq S_1$ and $M_2 \subsetneq S_2$ both together contradict the fact that $M$ is maximal element.
Thus either $M_1 = S_1$ or $M_2 = S_2$, and possibly both.
Thus either:
:$M$ is an injection of $S_1$ into $S_2$
or:
:$M^{-1}$ is an injection of $S_2$ into $S_1$.
Thus either $S_1 \le S_2$ or $S_2 \le S_1$, and the result follows.
{{qed}}
{{AoC||Zorn's Lemma}}
Theorem: Cardinals form Equivalence Classes

Let $\map \Card S$ denote the cardinal of the set $S$.
Then $\map \Card S$ induces an equivalence class which contains all sets which have the same cardinality as $S$.

Proof:
Follows directly from:
:The definition of a cardinal as $S \sim T \iff \map \Card S = \map \Card T$
:Set Equivalence behaves like Equivalence Relation
:Relation Partitions Set iff Equivalence.
{{qed}}
Category:Cardinals
j21akpr62mrktbv4ttfsy07xrfrqfrt
Theorem: Integers form Commutative Ring with Unity

The integers $\struct {\Z, +, \times}$ form a commutative ring with unity under addition and multiplication.

Proof:
We have that:
:$\struct {\Z, +, \times}$ form a commutative ring.
:$\struct {\Z, +, \times}$ has a unity, and the unity is $1$.
{{Qed}}
Theorem: Ring of Square Matrices over Ring is Ring

Let $R$ be a ring.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $\struct {\map {\MM_R} n, +, \times}$ denote the ring of square matrices of order $n$ over $R$.
Then $\struct {\map {\MM_R} n, +, \times}$ is a ring.

Proof:
From Matrix Entrywise Addition forms Abelian Group we have that $\struct {\map {\MM_R} n, +}$ is an abelian group, because $\struct {R, +}$ is itself an abelian group.
Similarly, it is clear that $\struct {\map {\MM_R} n, \times}$ is a semigroup, as Matrix Multiplication over Order n Square Matrices is Closed and Matrix Multiplication is Associative.
Finally, we note that Matrix Multiplication Distributes over Matrix Addition.
{{qed}}
Theorem: Ring of Square Matrices over Ring with Unity

Let $R$ be a ring with unity.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $\struct {\map {\MM_R} n, +, \times}$ denote the ring of square matrices of order $n$ over $R$.
Then $\struct {\map {\MM_R} n, +, \times}$ is a ring with unity.

Proof:
From Ring of Square Matrices over Ring is Ring we have that $\struct {\map {\MM_R} n, +, \times}$ is a ring.
As $R$ has a unity, the unit matrix can be formed.
The unity of $\struct {\map {\MM_R} n, +, \times}$ is this unit matrix.
{{qed}}