avewright/proofwiki-math huggingface dataset:
Theorem: Equality of Ordered Pairs

Two ordered pairs are equal {{iff}} corresponding coordinates are equal:
:$\tuple {a, b} = \tuple {c, d} \iff a = c \land b = d$

Proof:
First a lemma:
{{:Equality of Ordered Pairs/Lemma}}{{qed|lemma}}
Let $\tuple {a, b} = \tuple {c, d}$.
From the empty set formalization:
:$\set {\set {\O, a}, \set {\set \O, b} } = \set {\set {\O, c}, \set {\set \O, d} }$
First we note the special case where $a = \set \O$ and $b = \O$.
Then we have:
{{begin-eqn}}
{{eqn | l = \set {\set {\O, a}, \set {\set \O, b} }
      | r = \set {\set {\O, \set \O}, \set {\set \O, \O} }
      | c = 
}}
{{eqn | r = \set {\set {\O, \set \O}, \set {\O, \set \O} }
      | c = {{Defof|Set Equality}}: $\set {\O, \set \O } = \set {\set \O, \O}$
}}
{{eqn | r = \set {\set {\O, \set \O} }
      | c = Doubleton Class of Equal Sets is Singleton Class
}}
{{eqn | r = \set {\set {\O, c}, \set {\set \O, d} }
      | c = by definition
}}
{{end-eqn}}
Thus we have that:
:$c = d = \set {\O, \set \O}$
and so:
:$c = \set \O$ and $d = \O$
leading to the result that $a = c$ and $b = d$.
{{qed|lemma}}
Suppose otherwise, that either $a \ne \set \O$ or $b \ne \O$, or both.
Let $x \in \set {\set {\O, a}, \set {\set \O, b} }$.
Then either:
:$x = \set {\O, a}$
or:
:$x = \set {\set \O, b}$
First suppose $x = \set {\O, a}$.
Then:
:$x = \set {\O, c}$ or $x = \set {\set \O, d}$
{{AimForCont}} $x = \set {\set \O, d}$.
That is:
:$\set {\O, a} = \set {\set \O, d}$
which means that $a = \set \O$ and $d = \O$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\set \O, d}$.
Thus $x = \set {\O, c}$.
We have that:
:$x = \set {\O, a}$ and $x = \set {\O, c}$
and so:
:$\set {\O, a} = \set {\O, c}$
It follows from the lemma that:
:$a = c$
Now suppose $x = \set {\set \O, b}$.
Then:
:$x = \set {\O, c} \lor \set {\set \O, d}$
{{AimForCont}} $x = \set {\O, c}$.
That is:
:$\set {\set \O, b} = \set {\O, c}$
which means that $b = \O$ and $c = \set \O$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\O, c}$.
Thus $x = \set {\set \O, d}$.
We have that:
:$x = \set {\set \O, b}$ and $x = \set {\set \O, d}$
and so:
:$\set {\set \O, b} = \set {\set \O, d}$
It follows from the lemma that:
:$b = d$
{{qed}}
Theorem: Equality of Ordered Pairs

Two ordered pairs are equal {{iff}} corresponding coordinates are equal:
:$\tuple {a, b} = \tuple {c, d} \iff a = c \land b = d$

Proof:
First a lemma:
{{:Equality of Ordered Pairs/Lemma}}{{qed|lemma}}
Let $\tuple {a, b} = \tuple {c, d}$.
From the Kuratowski formalization:
:$\set {\set a, \set {a, b} } = \set {\set c, \set {c, d} }$ 
There are two cases: either $a = b$, or $a \ne b$.
==== Case 1 ====
Suppose $a = b$.
Then:
:$\set {\set a, \set {a, b} } = \set {\set a, \set a} = \set {\set a}$
Thus $\set {\set c, \set {c, d} }$ has only one element.
Thus $\set c = \set {c, d}$ and so $c = d$.
So:
:$\set {\set c, \set {c, d} } = \set {\set a}$
and so $a = c$ and $b = d$.
Thus the result holds.
{{qed|lemma}}
==== Case 2 ====
Now suppose $a \ne b$. By the same argument it follows that $c \ne d$.
So that means that either $\set a = \set c$ or $\set a = \set {c, d}$.
Since $\set {c, d}$ has $2$ distinct elements, $\set a \ne \set {c, d}$.
Thus:
:$\set a = \set c$
and so $a = c$.
Then:
:$\set {a, b} = \set {c, d}$
But as $a = c$ that means we have:
:$\set {a, b} = \set {a, d}$
It follows from the lemma that:
:$b = d$
{{qed}}
Theorem: Equality of Ordered Pairs

Two ordered pairs are equal {{iff}} corresponding coordinates are equal:
:$\tuple {a, b} = \tuple {c, d} \iff a = c \land b = d$

Proof:
First a lemma:
{{:Equality of Ordered Pairs/Lemma}}{{qed|lemma}}
Let $\tuple {a, b} = \tuple {c, d}$.
From the Wiener formalization:
:$\set {\set {\O, \set a}, \set {\set b} } = \set {\set {\O, \set c}, \set {\set d} }$
Let $x \in \set {\set {\O, \set a}, \set {\set b} }$.
Then either:
:$x = \set {\O, \set a}$
or:
:$x = \set {\set b}$
First suppose $x = \set {\O, \set a}$.
Then:
:$x = \set {\O, \set c}$ or $x = \set {\set d}$
{{AimForCont}} $x = \set {\set d}$.
That is:
:$\set {\O, \set a} = \set {\set d}$
Then:
:$\set d = \set a$
and also:
:$\set d = \O$
But that means:
:$a \in \O$
which contradicts the definition of the empty set $\O$.
It follows by Proof by Contradiction that $x \ne \set {\set d}$.
Thus $x = \set {\O, \set c}$.
We have that:
:$x = \set {\O, \set a}$ and $x = \set {\O, \set c}$
and so:
:$\set {\O, \set a} = \set {\O, \set c}$
It follows from the lemma that:
:$\set a = \set c$
Hence from Singleton Equality:
:$a = c$
Now suppose $x = \set {\set b}$.
Then:
:$x = \set {\O, \set c}$ or $x = \set {\set d}$
{{AimForCont}} $x = \set {\O, \set c}$.
That is:
:$\set {\set b} = \set {\O, \set c}$
which means that $\set b = \O$ and $\set b = \set c$.
But as $\O \ne \set \O$ it follows by Proof by Contradiction that $x \ne \set {\O, \set c}$.
Thus $x = \set {\set d}$.
We have that:
:$x = \set {\set b}$ and $x = \set {\set d}$
By Singleton Equality:
:$\set b = \set d$
and again by Singleton Equality:
:$b = d$
{{qed}}
Theorem: Identity is Unique

Let $\struct {S, \circ}$ be an algebraic structure that has an identity element $e \in S$.
Then $e$ is unique.

Proof:
Suppose $e_1$ and $e_2$ are both identity elements of $\struct {S, \circ}$.
Then by the definition of identity element:
:$\forall s \in S: s \circ e_1 = s = e_2 \circ s$
Then:
:$e_1 = e_2 \circ e_1 = e_2$
So:
:$e_1 = e_2$
and there is only one identity element after all.
{{qed}}
Theorem: Identity is Unique

Let $\struct {S, \circ}$ be an algebraic structure that has an identity element $e \in S$.
Then $e$ is unique.

Proof:
Let $e_S$ be an identity of $\struct {S, \circ}$.
Then by definition, $e_S$ is both a left identity and a right identity.
By More than one Left Identity then no Right Identity, if there is more than one of either, there cannot be one of the other.
So there can be only one of each.
By Left and Right Identity are the Same, they are one and the same thing.
{{qed}}
Theorem: Cancellation Laws

Let $G$ be a group.
Let $a, b, c \in G$.
Then the following hold:
;Right cancellation law
:$b a = c a \implies b = c$
;Left cancellation law
:$a b = a c \implies b = c$

Proof:
{{begin-eqn}}
{{eqn | l = g h
      | r = g
      | c = 
}}
{{eqn | ll= \leadsto
      | l = g h
      | r = g e
      | c = {{Group-axiom|2}}
}}
{{eqn | ll= \leadsto
      | l = h
      | r = e
      | c = Left Cancellation Law
}}
{{end-eqn}}
{{qed}}
Theorem: Cancellation Laws

Let $G$ be a group.
Let $a, b, c \in G$.
Then the following hold:
;Right cancellation law
:$b a = c a \implies b = c$
;Left cancellation law
:$a b = a c \implies b = c$

Proof:
{{begin-eqn}}
{{eqn | l = g h
      | r = g
      | c = 
}}
{{eqn | ll= \leadsto
      | l = g^{-1} \paren {g h}
      | r = g^{-1} g
      | c = {{Group-axiom|2}}
}}
{{eqn | ll= \leadsto
      | l = \paren {g^{-1} g} h
      | r = g^{-1} g
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = e h
      | r = e
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = h
      | r = e
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Cancellation Laws

Let $G$ be a group.
Let $a, b, c \in G$.
Then the following hold:
;Right cancellation law
:$b a = c a \implies b = c$
;Left cancellation law
:$a b = a c \implies b = c$

Proof:
{{begin-eqn}}
{{eqn | l = h g
      | r = g
      | c = 
}}
{{eqn | ll= \leadsto
      | l = h g
      | r = e g
      | c = {{Group-axiom|2}}
}}
{{eqn | ll= \leadsto
      | l = h
      | r = e
      | c = Right Cancellation Law
}}
{{end-eqn}}
{{qed}}
Theorem: Cancellation Laws

Let $G$ be a group.
Let $a, b, c \in G$.
Then the following hold:
;Right cancellation law
:$b a = c a \implies b = c$
;Left cancellation law
:$a b = a c \implies b = c$

Proof:
{{begin-eqn}}
{{eqn | l = h g
      | r = g
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {h g} g^{-1}
      | r = g g^{-1}
      | c = {{Group-axiom|2}}
}}
{{eqn | ll= \leadsto
      | l = h \paren {g g^{-1} }
      | r = g g^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = h e
      | r = e
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = h
      | r = e
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Cancellation Laws

Let $G$ be a group.
Let $a, b, c \in G$.
Then the following hold:
;Right cancellation law
:$b a = c a \implies b = c$
;Left cancellation law
:$a b = a c \implies b = c$

Proof:
Let $a, b, c \in G$ and let $a^{-1}$ be the inverse of $a$.
Suppose $b a = c a$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {b a} a^{-1}
      | r = \paren {c a} a^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b \paren {a a^{-1} }
      | r = c \paren {a a^{-1} }
      | c = {{Defof|Associative Operation}}
}}
{{eqn | ll= \leadsto
      | l = b e
      | r = c e
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | l = b
      | r = c
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
Thus, the '''right cancellation law''' holds.
The proof of the '''left cancellation law''' is analogous.
{{qed}}
Theorem: Cancellation Laws

Let $G$ be a group.
Let $a, b, c \in G$.
Then the following hold:
;Right cancellation law
:$b a = c a \implies b = c$
;Left cancellation law
:$a b = a c \implies b = c$

Proof:
From its definition, a group is a monoid, all of whose elements have inverses and thus are invertible.
From Invertible Element of Monoid is Cancellable, it follows that all its elements are therefore cancellable.
{{qed}}
Theorem: Cancellation Laws

Let $G$ be a group.
Let $a, b, c \in G$.
Then the following hold:
;Right cancellation law
:$b a = c a \implies b = c$
;Left cancellation law
:$a b = a c \implies b = c$

Proof:
Suppose $x = b a = c a$.
By Group has Latin Square Property, there exists exactly one $y \in G$ such that $x = y a$.
That is, $x = b a = c a \implies b = c$.
Similarly, suppose $x = a b = a c$.
Again by Group has Latin Square Property, there exists exactly one $y \in G$ such that $x = a y$.
That is, $a b = a c \implies b = c$.
{{qed}}
Theorem: Center of Group is Normal Subgroup

Let $G$ be a group
The center $\map Z G$ of $G$ is a normal subgroup of $G$.

Proof:
Recall that Center of Group is Abelian Subgroup.
Since $g x = x g$ for each $g \in G$ and $x \in \map Z G$:
:$g \map Z G = \map Z G g$
Thus:
:$\map Z G \lhd G$
{{qed}}
Theorem: Center of Group is Normal Subgroup

Let $G$ be a group
The center $\map Z G$ of $G$ is a normal subgroup of $G$.

Proof:
We have:
:$\forall a \in G: x \in \map Z G^a \iff a x a^{-1} = x a a^{-1} = x \in \map Z G$
Therefore:
:$\forall a \in G: \map Z G^a = \map Z G$
and $\map Z G$ is a normal subgroup of $G$.
{{qed}}
Theorem: Composition of Relations is Associative

The composition of relations is an associative binary operation:
:$\paren {\RR_3 \circ \RR_2} \circ \RR_1 = \RR_3 \circ \paren {\RR_2 \circ \RR_1}$

Proof:
{{Rewrite|Needs to be rewritten in light of the actual definition of the composition of relations and domain of relations. These equalities may not hold for all relations}}
First, note that from the definition of composition of relations, the following must be the case before the above expression is even to be defined:
:$\Dom {\RR_2} = \Cdm {\RR_1}$
:$\Dom {\RR_3} = \Cdm {\RR_2}$
The two composite relations can be seen to have the same domain, thus:
{{begin-eqn}}
{{eqn | l = \Dom {\paren {\RR_3 \circ \RR_2} \circ \RR_1}
      | r = \Dom {\RR_1}
      | c = Domain of Composite Relation
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \Dom {\RR_3 \circ \paren {\RR_2 \circ \RR_1} }
      | r = \Dom {\RR_2 \circ \RR_1}
      | c = Domain of Composite Relation
}}
{{eqn | r = \Dom {\RR_1}
      | c = Domain of Composite Relation
}}
{{end-eqn}}
and also the same codomain, thus:
{{begin-eqn}}
{{eqn | l = \Cdm {\paren {\RR_3 \circ \RR_2} \circ \RR_1}
      | r = \Cdm {\RR_3 \circ \RR_2}
      | c = Codomain of Composite Relation
}}
{{eqn | r = \Cdm {\RR_3}
      | c = Codomain of Composite Relation
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \Cdm {\RR_3 \circ \paren {\RR_2 \circ \RR_1} }
      | r = \Cdm {\RR_3}
      | c = Codomain of Composite Relation
}}
{{end-eqn}}
{{Refactor|Put this statement into a theorem page}}
So they are equal {{iff}} they have the same value at each point in their common domain, which this shows:
{{Rewrite|These terms may not be defined for all relations. So a different approach is required}}
{{begin-eqn}}
{{eqn | q = \forall x \in \Dom {\RR_1}
      | l = \map {\paren {\paren {\RR_3 \circ \RR_2} \circ \RR_1} } x
      | r = \map {\paren {\RR_3 \circ \RR_2} } {\map {\RR_1} x}
      | c = {{Defof|Composition of Relations}}
}}
{{eqn | r = \map {\RR_3} {\map {\RR_2} {\map {\RR_1} x} }
      | c = {{Defof|Composition of Relations}}
}}
{{eqn | r = \map {\RR_3} {\map {\paren {\RR_2 \circ \RR_1} } x}
      | c = {{Defof|Composition of Relations}}
}}
{{eqn | r = \map {\paren {\RR_3 \circ \paren {\RR_2 \circ \RR_1} } } x
      | c = {{Defof|Composition of Relations}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Subsemigroups

Let $\struct {S, \circ}$ be a semigroup.
Let $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ be subsemigroups of $\struct {S, \circ}$.
Then the intersection of $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ is itself a subsemigroup of that $\struct {S, \circ}$.

Proof:
{{Proofread| check if proof is correct if $\struct {S, \circ}$ is the empty semigroup}}
Suppose $\struct {S, \circ}$ is a semigroup where $S$ is the empty set. 
Suppose $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ are subsemigroups of $\struct {S, \circ}$. 
Then it follows that $T_1$ and $T_2$ are both empty.
Since $S$, $T_1$ and $T_2$ are empty, by Intersection with Empty Set, it follows that the intersection of $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ is equal to $\struct {S, \circ}$. 
Hence, by Semigroup is Subsemigroup of Itself, it follows that the intersection of $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ is itself a subsemigroup of that $\struct {S, \circ}$.
Now suppose $\struct {S, \circ}$ is a semigroup, where $S$ is non-empty. 
Let $T = T_1 \cap T_2$ where $T_1, T_2$ are subsemigroups of $\struct {S, \circ}$. Then:
{{begin-eqn}}
{{eqn | o =
      | r = a, b \in T
}}
{{eqn | o = \leadsto
      | r = a, b \in T_1 \land a, b \in T_2
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = a \circ b \in T_1 \land a \circ b \in T_2
      | c = Subsemigroups are closed
}}
{{eqn | o = \leadsto
      | r = a \circ b \in T
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
Thus $\struct {T, \circ}$ is closed, and is therefore a semigroup from the Subsemigroup Closure Test.
{{Qed}}
Category:Set Intersection
Category:Subsemigroups
Category:Intersection of Subsemigroups
awc6gr231j0q8luzoomgbc00q4ifqor
Theorem: Intersection of Subsemigroups

Let $\struct {S, \circ}$ be a semigroup.
Let $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ be subsemigroups of $\struct {S, \circ}$.
Then the intersection of $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ is itself a subsemigroup of that $\struct {S, \circ}$.

Proof:
Let $T = \bigcap \mathbb S$.
Then:
{{begin-eqn}}
{{eqn | l = a, b
      | o = \in
      | r = T
      | c =
}}
{{eqn | ll= \leadsto
      | q = \forall K \in \mathbb S
      | l = a, b
      | o = \in
      | r = K
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadsto
      | q = \forall K \in \mathbb S
      | l = a \circ b
      | o = \in
      | r = K
      | c = Subsemigroups are closed
}}
{{eqn | ll= \leadsto
      | l = a \circ b
      | o = \in
      | r = T
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
So by Subsemigroup Closure Test, $\struct {T, \circ}$ is a subsemigroup of $\struct {S, \circ}$.
Now to show that $\struct {T, \circ}$ is the largest such subsemigroup.
Let $x, y \in T$.
Then $\forall K \subseteq T: x \circ y \in K \implies x \circ y \in T$.
Thus $\forall K \in \mathbb S: K \subseteq T$.
Thus $T$ is the largest subsemigroup of $S$ contained in each member of $\mathbb S$.
{{qed}}
Theorem: Intersection of Subsemigroups

Let $\struct {S, \circ}$ be a semigroup.
Let $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ be subsemigroups of $\struct {S, \circ}$.
Then the intersection of $\struct {T_1, \circ}$ and $\struct {T_2, \circ}$ is itself a subsemigroup of that $\struct {S, \circ}$.

Proof:
From Set of Subsemigroups forms Complete Lattice:
:$\struct {\mathbb S, \subseteq}$ is a complete lattice.
where for every set $\mathbb H$ of subsemigroups of $S$:
:the infimum of $\mathbb H$ necessarily admitted by $\mathbb H$ is $\ds \bigcap \mathbb H$.
Hence the result, by definition of infimum.
{{qed}}
Theorem: Cancellable Elements of Semigroup form Subsemigroup

Let $\struct {S, \circ}$ be a semigroup.
Let $C$ be the set of cancellable elements of $\struct {S, \circ}$.
Then $\struct {C, \circ}$ is a subsemigroup of $\struct {S, \circ}$.

Proof:
Now let $C$ be the set of cancellable elements of $\struct {S, \circ}$.
Let $x, y \in C$.
Then $x$ and $y$ are both left cancellable and right cancellable.
Thus by Left Cancellable Elements of Semigroup form Subsemigroup:
:$x \circ y$ is left cancellable
and by Right Cancellable Elements of Semigroup form Subsemigroup:
:$x \circ y$ is right cancellable.
Thus $x \circ y$ is both left cancellable and right cancellable, and therefore cancellable.
Thus $x \circ y \in C$.
Thus $\struct {C, \circ}$ is closed and is therefore by the Subsemigroup Closure Test a subsemigroup of $\struct {S, \circ}$.
{{qed}}
Theorem: Subgroup of Cyclic Group is Cyclic

Let $G$ be a cyclic group.
Let $H$ be a subgroup of $G$.
Then $H$ is cyclic.

Proof:
Let $G$ be a cyclic group generated by $a$.
Let $H$ be a subgroup of $G$.
If $H = \set e$, then $H$ is a cyclic group subgroup generated by $e$.
Let $H \ne \set e$.
By definition of cyclic group, every element of $G$ has the form $a^n$.
Then as $H$ is a subgroup of $G$, $a^n \in H$ for some $n \in \Z$.
Let $m$ be the smallest (strictly) positive integer such that $a^m \in H$.
Consider an arbitrary element $b$ of $H$.
As $H$ is a subgroup of $G$, $b = a^n$ for some $n$.
By the Division Theorem, it is possible to find integers $q$ and $r$ such that $n = m q + r$ with $0 \le r < m$.
It follows that:
:$a^n = a^{m q + r} = \paren {a^m}^q a^r$
and hence:
:$a^r = \paren {a^m}^{-q} a^n$
Since $a^m \in H$ so is its inverse $\paren {a^m}^{-1}$
By {{Group-axiom|0}}, so are all powers of its inverse.
Now $a^n$ and $\paren {a^m}^{-q}$ are both in $H$, thus so is their product $a^r$, again by {{Group-axiom|0}}.
However:
:$m$ was the smallest (strictly) positive integer such that $a^m \in H$
and:
:$0 \le r < m$
Therefore it follows that:
:$r = 0$
Therefore:
:$n = q m$
and:
:$b = a^n = \paren {a^m}^q$.
We conclude that any arbitrary element $b = a^n$ of $H$ is a power of $a^m$.
So, by definition, $H = \gen {a^m}$ is cyclic.
{{qed}}
Theorem: Subgroup of Cyclic Group is Cyclic

Let $G$ be a cyclic group.
Let $H$ be a subgroup of $G$.
Then $H$ is cyclic.

Proof:
Let $G$ be a cyclic group generated by $a$.
=== Finite Group ===
Let $G$ be finite.
By Bijection from Divisors to Subgroups of Cyclic Group there are exactly as many subgroups of $G$ as divisors of the order of $G$.
As each one of these is cyclic by Subgroup of Finite Cyclic Group is Determined by Order, the result follows.
{{qed|lemma}}
=== Infinite Group ===
By Morphism from Integers to Group, an infinite cyclic group is isomorphic to $\struct {\Z, +}$.
So all we need to do is show that any subgroup of $\struct {\Z, +}$ is cyclic.
Suppose $H$ is a subgroup of $\struct {\Z, +}$.
From Subgroup of Integers is Ideal and Ring of Integers is Principal Ideal Domain, we have that:
:$\exists m \in \Z_{> 0}: H = \ideal m$
where $\ideal m$ is the principal ideal of $\struct {\Z, +, \times}$ generated by $m$.
But $m$ is also a generator of the subgroup $\ideal m$ of $\struct {\Z, +}$, as:
:$n \in \Z: n \circ m = n \cdot m \in \gen m$
Hence the result.
{{qed}}
Theorem: Subgroup of Cyclic Group is Cyclic

Let $G$ be a cyclic group.
Let $H$ be a subgroup of $G$.
Then $H$ is cyclic.

Proof:
Let $G$ be a cyclic group generated by $a$.
Let $H$ be a subgroup of $G$.
By Cyclic Group is Abelian, $G$ is abelian.
By Subgroup of Abelian Group is Normal, $H$ is normal in $G$.
Let $G / H$ be the quotient group of $G$ by $H$.
Let $q_H: G \to G / H$ be the quotient epimorphism from $G$ to $G / H$:
:$\forall x \in G: \map {q_H} x = x H$
Then from Quotient Group Epimorphism is Epimorphism, $H$ is the kernel of $q_H$.
From Kernel of Homomorphism on Cyclic Group, $H$ is a cyclic group.
{{qed}}
Theorem: Empty Set is Subset of All Sets

The empty set $\O$ is a subset of every set (including itself).
That is:
:$\forall S: \O \subseteq S$

Proof:
By the definition of subset, $\O \subseteq S$ means:
:$\forall x: \paren {x \in \O \implies x \in S}$
By the definition of the empty set:
:$\forall x: \neg \paren {x \in \O}$
Thus $\O \subseteq S$ is vacuously true.
{{qed}}
Theorem: Empty Set is Subset of All Sets

The empty set $\O$ is a subset of every set (including itself).
That is:
:$\forall S: \O \subseteq S$

Proof:
$S \subseteq T$ means:
:'''every element of $S$ is also in $T$'''
or, equivalently:
:'''every element that is ''not'' in $T$ is not in $S$ either.'''
Thus:
{{begin-eqn}}
{{eqn | o = 
      | r = S \subseteq T
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = \forall x \in S: x \in T
      | c = {{Defof|Subset}}
}}
{{eqn | o = \leadstoandfrom
      | r = \neg \paren {\exists x \in S: \neg \paren {x \in T} }
      | c = De Morgan's Laws (Predicate Logic)
}}
{{end-eqn}}
which means '''there is no element in $S$ which is not also in $T$'''.
There are no elements of $\O$, from the definition of the empty set.
Therefore $\O$ has no elements that are not also in any other set.
Thus, from the above, all elements of $\O$ are all (vacuously) in every other set.
{{qed}}
Theorem: Relation Reflexivity

Every relation has exactly one of these properties: it is either:
:reflexive,
:antireflexive or
:non-reflexive.

Proof:
A reflexive relation can not be antireflexive, and vice versa:
:$\tuple {x, x} \in \RR \iff \neg \paren {\tuple {x, x} \notin \RR}$
By the definition of non-reflexive, a reflexive relation can not also be non-reflexive.
So a reflexive relation is neither antireflexive nor non-reflexive.
An antireflexive relation can be neither reflexive (see above) nor non-reflexive (by the definition of non-reflexive).
By its own definition, if a relation is neither reflexive nor antireflexive, then it is non-reflexive.
{{qed}}
Theorem: Set Union is Idempotent

Set union is idempotent:
:$S \cup S = S$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \cup S
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in S
      | o = \lor
      | r = x \in S
      | c = {{Defof|Set Union}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = S
      | c = Rule of Idempotence: Disjunction
}}
{{end-eqn}}
{{qed}}
Theorem: Set Intersection is Idempotent

Set intersection is idempotent:
:$S \cap S = S$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S \cap S
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in S
      | o = \land
      | r = x \in S
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = S
      | c = Rule of Idempotence: Conjunction
}}
{{end-eqn}}
{{qed}}
Theorem: Set is Subset of Union

The union of two sets is a superset of each:
:$S \subseteq S \cup T$
:$T \subseteq S \cup T$

Proof:
{{begin-eqn}}
{{eqn | l = x \in S
      | o = \leadsto
      | r = x \in S \lor x \in T
      | c = Rule of Addition
}}
{{eqn | o = \leadsto
      | r = x \in S \cup T
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadsto
      | r = S \subseteq S \cup T
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Similarly for $T$.
{{qed}}