avewright/proofwiki-math huggingface dataset:
Theorem: Inverse Relation is Left and Right Inverse iff Bijection

Let $\RR \subseteq S \times T$ be a relation on a cartesian product $S \times T$.
Let:
:$I_S$ be the identity mapping on $S$
:$I_T$ be the identity mapping on $T$.
Let $\RR^{-1}$ be the inverse relation of $\RR$.
Then $\RR$ is a bijection {{iff}}:
:$\RR^{-1} \circ \RR = I_S$
and
:$\RR \circ \RR^{-1} = I_T$
where $\circ$ denotes composition of relations.

Proof:
=== Necessary Condition ===
Let $\RR \subseteq S \times T$ be such that:
:$\RR^{-1} \circ \RR = I_S$
and
:$\RR \circ \RR^{-1} = I_T$.
From Left and Right Inverse Relations Implies Bijection, it follows that $\RR$ is a bijection.
{{qed|lemma}}
Theorem: Integer Multiples Closed under Addition

Let $n \Z$ be the set of integer multiples of $n$.
Then the algebraic structure $\struct {n \Z, +}$ is closed under addition.

Proof:
Let $x, y \in n \Z$.
Then $\exists p, q \in \Z: x = n p, y = n q$.
So $x + y = n p + n q = n \paren {p + q}$ where $p + q \in \Z$.
Thus $x + y \in n \Z$ and so $\struct {n \Z, +}$ is closed.
{{qed}}
Theorem: Integer Multiples Closed under Multiplication

Let $n \Z$ be the set of integer multiples of $n$.
Then the algebraic structure $\struct {n \Z, \times}$ is closed under multiplication.

Proof:
Let $x, y \in n \Z$.
Then $\exists p, q \in \Z: x = n p, y = n q$.
So $x y = n p \cdot n q = n \paren {n p q}$ where $n p q \in \Z$.
Thus $x y \in n \Z$ and so $\struct {n \Z, \times}$ is closed.
{{qed}}
Theorem: Non-Zero Integers Closed under Multiplication

The set of non-zero integers is closed under multiplication.

Proof:
Let us define $\eqclass {\tuple {a, b} } \boxminus$ as in the formal definition of integers.
That is, $\eqclass {\tuple {a, b} } \boxminus$ is an equivalence class of ordered pairs of natural numbers under the congruence relation $\boxminus$.
$\boxminus$ is the congruence relation defined on $\N \times \N$ as:
:$\tuple {x_1, y_1} \boxminus \tuple {x_2, y_2} \iff x_1 + y_2 = x_2 + y_1$
In order to streamline the notation, we will use $\eqclass {a, b} {}$ to mean $\eqclass {\tuple {a, b} } \boxminus$, as suggested.
Integer multiplication is defined as:
:$\forall a, b, c, d \in \N: \eqclass {a, b} {} \times \eqclass {c, d} {} = \eqclass {a c + b d, a d + b c} {}$
From Integer Multiplication is Closed, we have that $x, y \in \Z \implies x y \in \Z$.
From Ring of Integers has no Zero Divisors, we have that $x, y \in \Z: x, y \ne 0 \implies x y \ne 0$.
Therefore multiplication on the non-zero integers is closed.
{{qed}}
Theorem: Two-Step Subgroup Test using Subset Product

Let $G$ be a group.
Let $\O\subset H \subseteq G$ be a non-empty subset of $G$.
Then $H$ is a subgroup of $G$ {{iff}}:
:$H H \subseteq H$
:$H^{-1} \subseteq H$
where:
:$H H$ is the product of $H$ with itself
:$H^{-1}$ is the inverse of $H$.

Proof:
This is a reformulation of the Two-Step Subgroup Test in terms of subset product.
Theorem: One-Step Subgroup Test using Subset Product

Let $G$ be a group.
Let $\O \subset H \subseteq G$ be a non-empty subset of $G$.
Then $H$ is a subgroup of $G$ {{iff}}:
:$H H^{-1} \subseteq H$
where:
:$H^{-1}$ is the inverse of $H$
:$H H ^{-1}$ is the product of $H$ with $H^{-1}$.

Proof:
This is a reformulation of the One-Step Subgroup Test in terms of subset product.
Theorem: Product of Subset with Union

Let $\struct {G, \circ}$ be an algebraic structure.
Let $X, Y, Z \subseteq G$.
Then:
:$X \circ \paren {Y \cup Z} = \paren {X \circ Y} \cup \paren {X \circ Z}$
:$\paren {Y \cup Z} \circ X = \paren {Y \circ X} \cup \paren {Z \circ X}$
where $X \circ Y$ denotes the subset product of $X$ and $Y$.

Proof:
Let $x \circ t \in X \circ \paren {Y \cup Z}$.
We have $x \in X, t \in Y \cup Z$ by definition of subset product.
By definition of set union, it follows that $t \in Y$ or $t \in Z$.
So we also have $x \circ t \in X \circ Y$ or $x \circ t \in X \circ Z$.
That is:
:$x \circ t \in \paren {X \circ Y} \cup \paren {X \circ Z}$
and so:
:$X \circ \paren {Y \cup Z} \subseteq \paren {X \circ Y} \cup \paren {X \circ Z}$
Now let $x \circ t \in \paren {X \circ Y} \cup \paren {X \circ Z}$.
By definition of set union, it follows that $x \circ t \in X \circ Y$ or $x \circ t \in X \circ Z$.
So $x \in X$, and $y \in Y$ or $y \in Z$.
That is, $x \in X$, and $y \in Y \cup Z$ by definition of set union.
Hence:
:$x \circ t \in X \circ \paren {Y \cup Z}$
and so:
:$\paren {X \circ Y} \cup \paren {X \circ Z} \subseteq X \circ \paren {Y \cup Z}$
That is:
:$X \circ \paren {Y \cup Z} = \paren {X \circ Y} \cup \paren {X \circ Z}$
The result:
:$\paren {Y \cup Z} \circ X = \paren {Y \circ X} \cup \paren {Z \circ X}$
follows similarly.
{{Qed}}
Theorem: Product of Subset with Union

Let $\struct {G, \circ}$ be an algebraic structure.
Let $X, Y, Z \subseteq G$.
Then:
:$X \circ \paren {Y \cup Z} = \paren {X \circ Y} \cup \paren {X \circ Z}$
:$\paren {Y \cup Z} \circ X = \paren {Y \circ X} \cup \paren {Z \circ X}$
where $X \circ Y$ denotes the subset product of $X$ and $Y$.

Proof:
Consider the relation $\RR \subseteq G \times G$ defined as:
:$\forall g, h \in G: \tuple {g, h} \in \RR \iff \exists g \in X$
Then:
:$\forall S \subseteq G: X \circ S = \map \RR S$
Then:
{{begin-eqn}}
{{eqn | l = X \circ \paren {Y \cup Z}
      | r = \map \RR {Y \cup Z}
      | c = 
}}
{{eqn | r = \map \RR y \cup \map \RR Z
      | c = Image of Union under Relation
}}
{{eqn | r = \paren {X \circ Y} \cup \paren {X \circ Z}
      | c = 
}}
{{end-eqn}}
Next, consider the relation $\RR \subseteq G \times G$ defined as:
:$\forall g, h \in G: \tuple {g, h} \in \RR \iff \exists h \in X$
Then:
:$\forall S \subseteq G: S \circ X = \map \RR S$
Then:
{{begin-eqn}}
{{eqn | l = \paren {Y \cup Z} \circ X
      | r = \map \RR {Y \cup Z}
      | c = 
}}
{{eqn | r = \map \RR Y \cup \map \RR Z
      | c = Image of Union under Relation
}}
{{eqn | r = \paren {Y \circ X} \cup \paren {Z \circ X}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Quotient Group is Subgroup of Power Structure of Group

Let $\struct {G, \circ}$ be a group.
Let $\struct {N, \circ}$ be a normal subgroup of $\struct {G, \circ}$.
Then $\struct {G / N, \circ_N}$ is a subgroup of $\struct {\powerset G, \circ_\PP}$, where:
:$\struct {G / N, \circ_N}$ is the quotient group of $G$ by $N$
:$\struct {\powerset G, \circ_\PP}$ is the power structure of $\struct {G, \circ}$.

Proof:
Follows directly from:
* Quotient Group is Group
* Cosets of $G$ by $N$ are subsets of $G$ and therefore elements of $\powerset G$
* The operation $\circ_N$ is defined as the subset product of cosets.
{{qed}}
Theorem: Hilbert's Nullstellensatz

Let $k$ be an algebraically closed field.
Let $n \geq 0$ be an natural number.
Let $k \sqbrk {x_1, \ldots, x_n}$ be the polynomial ring in $n$ variables over $k$.
Then for every ideal $J \subseteq k \sqbrk {x_1, \ldots, x_n}$, the associated ideal of its zero-locus equals its radical:
:$\map I {\map Z J} = \map \Rad J$

Proof:
Note first that the operations $\map I {\, \cdot \,}$ and $\map Z {\, \cdot \,}$ are inclusion reversing by Ideal and Zero Locus are Order Reversing.
That is:
:$X \subseteq Y \subseteq k^n \implies \map I X \supseteq \map I Y$
:$I \subseteq J \implies \map Z I \supseteq \map Z J$
Let $m_a$ be the ideal $\ideal {x_1 - a_1, \ldots, x_n - a_n}$ with $a \in k^n$.
Theorem: Subset of Domain is Subset of Preimage of Image

Let $f: S \to T$ be a mapping.
Then:
:$A \subseteq S \implies A \subseteq \paren {f^{-1} \circ f} \sqbrk A$
where:
:$f \sqbrk A$ denotes the image of $A$ under $f$
:$f^{-1} \sqbrk A$ denotes the preimage of $A$ under $f$
:$f^{-1} \circ f$ denotes composition of $f^{-1}$ and $f$.
This can be expressed in the language and notation of direct image mappings and inverse image mappings as:
:$\forall A \in \powerset S: A \subseteq \map {\paren {f^\gets \circ f^\to} } A$

Proof:
As a mapping is by definition a left-total relation.
Therefore Preimage of Image under Left-Total Relation is Superset applies:
:$A \subseteq S \implies A \subseteq \paren {\RR^{-1} \circ \RR} \sqbrk A$
where $\RR$ is a relation.
Hence:
:$A \subseteq S \implies A \subseteq \paren {f^{-1} \circ f} \sqbrk A$
{{qed}}
Theorem: Clairaut's Differential Equation

'''Clairaut's differential equation''' is a first order ordinary differential equation which can be put into the form:
:$y = x y' + \map f {y'}$
Its general solution is:
:$y = C x + \map f C$
where $C$ is a constant.

Proof:
We have:
:$y = x y' + \map f {y'}$
Differentiating the equation {{WRT|Differentiation}} $x$ we have:
{{begin-eqn}}
{{eqn | l = y'
      | r = y' + x y'' + y'' \map {f'} {y'}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = \map {y''} {x + \map {f'} {y'} }
      | c = 
}}
{{end-eqn}}
Theorem: Noether Normalization Lemma

Let $k$ be a field.
Let $A$ be a non-trivial finitely generated $k$-algebra.
{{explain|the above link is for Definition:Non-Trivial Ring -- we need to define a Definition:Non-Trivial Algebra}}
Then there exists $n \in \N$ and a finite injective morphism of $k$-algebra:
:$k \sqbrk {x_1, \dotsc, x_n} \to A$
{{DefinitionWanted|Instead of using Definition:Finite Ring Homomorphism, another page is to be generated defining the module-theory version.}}

Proof:
Since $A$ is finitely generated, we prove this by induction on the number $m$ of generators as a $k$-algebra.
Theorem: Image of Preimage under Mapping

Let $f: S \to T$ be a mapping.
Then:
:$B \subseteq T \implies \paren {f \circ f^{-1} } \sqbrk B = B \cap f \sqbrk S$
where:
:$f \sqbrk S$ denotes the image of $S$ under $f$
:$f^{-1} \sqbrk B$ denotes the preimage of $B$ under $f$
:$f \circ f^{-1}$ denotes composition of $f$ and $f^{-1}$.

Proof:
As $f$ is a mapping it follows by definition that $f$ is also a relation
Applying Image of Preimage under Relation is Subset directly:
:$B \subseteq T \implies \paren {f \circ f^{-1} } \sqbrk B \subseteq B \implies f \sqbrk {f^{-1} \sqbrk B} \subseteq B$
From Preimage of Subset is Subset of Preimage:
:$B \subseteq T \implies f^{-1} \sqbrk B \subseteq f^{-1} \sqbrk T$
From Preimage of Mapping equals Domain:
:$f^{-1} \sqbrk T = S$
and so:
:$B \subseteq T \implies f^{-1} \sqbrk B \subseteq S$
Applying Image of Subset under Mapping is Subset of Image:
:$f^{-1} \sqbrk B \subseteq S \implies f \sqbrk {f^{-1} \sqbrk B} \subseteq f \sqbrk S$
From Intersection is Largest Subset:
:$B \subseteq T \implies \paren {f \circ f^{-1} } \sqbrk B \subseteq B \cap f \sqbrk S$
Now suppose $y \in B \cap f \sqbrk S$.
Then:
:$f^{-1} \sqbrk y \subseteq f^{-1} \sqbrk B$ and $f^{-1} \sqbrk y \subseteq f^{-1} \sqbrk {f \sqbrk S}$
and in particular:
:$f^{-1} \sqbrk y \subseteq f^{-1} \sqbrk B$
Applying Image of Subset under Mapping is Subset of Image again:
:$f \sqbrk {f^{-1} \sqbrk y} \subseteq f \sqbrk {f^{-1} \sqbrk B}$
But as $f$ is many-to-one:
:$f \sqbrk {f^{-1} \sqbrk y} = y$
and so:
:$y \in f \sqbrk {f^{-1} \sqbrk B} = \paren {f \circ f^{-1} } \sqbrk B$
So we have that:
:$B \cap f \sqbrk S \subseteq \paren {f \circ f^{-1} } \sqbrk B$
Hence the result.
{{qed}}
Theorem: Isomorphism of External Direct Products

Let:
:$\struct {S_1 \times S_2, \circ}$ be the external direct product of two algebraic structures $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$
:$\struct {T_1 \times T_2, *}$ be the external direct product of two algebraic structures $\struct {T_1, *_1}$ and $\struct {T_2, *_2}$
:$\phi_1$ be an isomorphism from $\struct {S_1, \circ_1}$ onto $\struct {T_1, *_1}$
:$\phi_2$ be an isomorphism from $\struct {S_2, \circ_2}$ onto $\struct {T_2, *_2}$.
Then the mapping $\phi_1 \times \phi_2: \struct {S_1 \times S_2, \circ} \to \struct {T_1 \times T_2, *}$ defined as:
:$\map {\paren {\phi_1 \times \phi_2} } {x, y} = \tuple {\map {\phi_1} x, \map {\phi_2} y}$
is an isomorphism from $\struct {S_1 \times S_2, \circ}$ to $\struct {T_1 \times T_2, *}$.

Proof:
From Homomorphism of External Direct Products, we have that $\phi_1 \times \phi_2: \struct {S_1 \times S_2, \circ} \to \struct {T_1 \times T_2, *}$ is a homomorphism.
From Cartesian Product of Bijections is Bijection, we have that $\phi_1 \times \phi_2$ is a bijection.
Thus $\phi_1 \times \phi_2$ is a bijective homomorphism, and so an isomorphism.
{{Qed}}
Theorem: Equivalence of Definitions of Independent Subgroups

{{TFAE|def = Independent Subgroups}}
Let $G$ be a group whose identity is $e$.
Let $\sequence {H_n}$ be a sequence of independent subgroups of $G$.

Proof:
=== Definition 1 implies Definition 2 ===
Let $H_1, H_2, \ldots, H_n$ be independent by definition 1:
:$\ds \prod_{k \mathop = 1}^n h_k = e \iff \forall k \in \closedint 1 n: h_k = e$
where $h_k \in H_k$ for all $k \in \closedint 1 n$.
Let $\ds u \in \paren {\prod_{j \mathop = 1}^{k - 1} H_j} \cap H_k$.
Then:
:$\ds \exists x_1, x_2, \ldots, x_{k - 1} \in H_1, \ldots, H_{k - 1}: u = \prod_{j \mathop = 1}^{k - 1} x_j$
We have that $u \in H_k$ and $H_k$ is a group.
Therefore let $x_k = u^{-1}$, the inverse of $u$.
For each $j \in \set {k + 1, k + 2, \ldots, n}$ let $x_j = e$.
Then:
{{begin-eqn}}
{{eqn | l = \prod_{j \mathop = 1}^n x_j
      | r = \paren {\prod_{j \mathop = 1}^{k - 1} x_j} u^{-1} \paren {\prod_{j \mathop = k + 1}^n x_j}
      | c = 
}}
{{eqn | r = \paren {\prod_{j \mathop = 1}^{k - 1} x_j} u^{-1}
      | c = 
}}
{{eqn | r = e
      | c = 
}}
{{end-eqn}}
Thus by hypothesis $u^{-1} = e$ and hence $u = e$.
Hence $H_1, H_2, \ldots, H_n$ are independent by definition 2:
:$\ds \forall k \in \set {2, 3, \ldots, n}: \paren {\prod_{j \mathop = 1}^{k - 1} H_j} \cap H_k = \set e$
Theorem: Dual of Total Ordering is Total Ordering

Let $\preccurlyeq$ be a total ordering.
Then its dual ordering $\succcurlyeq$ is also a total ordering.

Proof:
Let $\struct {S, \preccurlyeq}$ be a totally ordered set.
From Dual Ordering is Ordering we have that $\succcurlyeq$ is an ordering.
Let $x, y \in S$.
Then $x \preccurlyeq y$ or $y \preccurlyeq x$ since $\preccurlyeq$ is total.
By definition of dual ordering, also $y \succcurlyeq x$ or $x \succcurlyeq y$.
Hence the result, by definition of total ordering.
{{qed}}
Theorem: Dual of Lattice Ordering is Lattice Ordering

Let $\struct {S, \preccurlyeq}$ be a lattice.
Let $\preccurlyeq$ be the lattice ordering on $\struct {S, \preccurlyeq}$.
Then its dual ordering $\succcurlyeq$ is also a lattice ordering.

Proof:
Let $\struct {S, \preccurlyeq}$ be a lattice.
It is to be shown that:
:for all $x, y \in S$, the ordered set $\struct {\set {x, y}, \succcurlyeq}$ admits both a supremum and an infimum. 
Let $x, y \in S$.
Then $\struct {\set {x, y}, \preccurlyeq}$ admits both a supremum and an infimum.
Let $c = \map \sup {\set {x, y}, \preccurlyeq}$.
Then by definition of supremum:
:$\forall s \in \set {x, y}: s \preccurlyeq c$
:$\forall d \in S: c \preccurlyeq d$
where $d$ is an upper bound of $\struct {\set {x, y}, \preccurlyeq} \subseteq S$.
Hence by definition of dual ordering:
:$\forall s \in \set {x, y}: c \succcurlyeq s$
:$\forall d \in S: d \succcurlyeq c$
where $d$ is an upper bound of $\struct {\set {x, y}, \preccurlyeq} \subseteq S$.
By Upper Bound is Lower Bound for Inverse Ordering, $d$ is a lower bound of $\struct {\set {x, y}, \succcurlyeq} \subseteq S$.
So by definition of infimum:
:$c = \map \inf {\set {x, y}, \succcurlyeq}$
That is, $\struct {\set {x, y}, \succcurlyeq}$ admits an infimum.
{{qed|lemma}}
Let $c = \map \inf {\set {x, y}, \preccurlyeq}$.
Then by definition of infimum:
:$\forall s \in \set {x, y}: c \preccurlyeq s$
:$\forall d \in S: d \preccurlyeq c$
where $d$ is a lower bound of $\struct {\set {x, y}, \preccurlyeq} \subseteq S$.
Hence by definition of dual ordering:
:$\forall s \in \set{x, y}: s \succcurlyeq c$
:$\forall d \in S: c \succcurlyeq d$
where $d$ is a lower bound of $\struct {\set {x, y}, \preccurlyeq} \subseteq S$.
By Lower Bound is Upper Bound for Inverse Ordering, $d$ is an upper bound of $\struct {\set {x, y}, \succcurlyeq} \subseteq S$.
So by definition of supremum:
:$c = \map \sup {\set {x, y}, \succcurlyeq}$
That is, $\struct {\set {x, y}, \succcurlyeq}$ admits a supremum.
{{qed|lemma}}
Hence $\struct {\set {x, y}, \succcurlyeq}$ admits both a supremum and an infimum.
That is, $\succcurlyeq$ is a lattice ordering.
{{qed}}
Theorem: Order Isomorphism on Totally Ordered Set preserves Total Ordering

Let $\struct {S, \preccurlyeq_1}$ and $\struct {T, \preccurlyeq_2}$ be ordered sets.
Let $\phi: \struct {S, \preccurlyeq_1} \to \struct {T, \preccurlyeq_2}$ be an order isomorphism.
Then $\struct {S, \preccurlyeq_1}$ is a totally ordered set {{iff}} $\struct {T, \preccurlyeq_2}$ is also a totally ordered set.

Proof:
=== Necessary Condition ===
Let $\struct {S, \preccurlyeq_1}$ be a totally ordered set
Then by definition $\preccurlyeq_1$ is a total ordering.
Let $x, y \in S$.
Then either $x \preccurlyeq_1 y$ or $y \preccurlyeq_1 x$.
From the definition of order isomorphism, either:
:$\map \phi x \preccurlyeq_2 \map \phi y$
or:
:$\map \phi y \preccurlyeq_2 \map \phi x$
and so by definition $\preccurlyeq_2$ is also a total ordering.
So by definition $\struct {T, \preccurlyeq_2}$ is also a totally ordered set.
{{qed|lemma}}
Theorem: Order Isomorphism on Well-Ordered Set preserves Well-Ordering

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be ordered sets.
Let $\phi: \struct {S_1, \preccurlyeq_1} \to \struct {S_2, \preccurlyeq_2}$ be an order isomorphism.
Then $\struct {S_1, \preccurlyeq_1}$ is a well-ordered set {{iff}} $\struct {S_2, \preccurlyeq_2}$ is also a well-ordered set.

Proof:
Let $\struct {S_1, \preccurlyeq_1}$ be a well-ordered set.
Then by definition $\preccurlyeq_1$ is a well-ordering.
By Well-Ordering is Total Ordering, $\preccurlyeq_1$ is a total ordering.
From Order Isomorphism on Totally Ordered Set preserves Total Ordering, it follows that $\struct {S_2, \preccurlyeq_2}$ is a totally ordered set.
All that remains is to show that $\preccurlyeq$ is a well-founded relation.
Let $T_1 \subseteq S_1$.
As $\struct {S_1, \preccurlyeq_1}$ is a well-ordered set:
:$\exists m_1 \in T_1: \forall t \in T_1: t = m_1 \lor \neg \paren {t \preccurlyeq_1 m_1}$
Now consider the image $m_2$ of $m_1$ in $S_2$:
:$m_2 = \map \phi {m_1}$
{{AimForCont}} $\struct {S_2, \preccurlyeq_2}$ is not a well-ordered set.
Let there exist $T_2 \subseteq S_2$ such that:
:$\exists x \in T_2: x \ne m_2, x \preccurlyeq_2 m_2$
By Inverse of Order Isomorphism is Order Isomorphism, if $\phi$ is an order isomorphism then so is $\phi^{-1}$.
Hence:
:$\map {\phi^{-1} } x \ne \map {\phi^{-1} } {m_2}, \map {\phi^{-1} } x \preccurlyeq_2 \map {\phi^{-1} } {m_2}$
But this contradicts the fact that $\struct {S_1, \preccurlyeq_1}$ is well-ordered.
Hence by Proof by Contradiction $\struct {S_2, \preccurlyeq_2}$ must be a well-ordered set.
The same technique is used to show that if $\struct {S_2, \preccurlyeq_2}$ is a well-ordered set then so is $\struct {S_1, \preccurlyeq_1}$.
{{qed}}
Theorem: Order Isomorphism on Lattice preserves Lattice Structure

Let $\struct {S, \preccurlyeq_1}$ and $\struct {T, \preccurlyeq_2}$ be ordered sets.
Let $\phi: \struct {S, \preccurlyeq_1} \to \struct {T, \preccurlyeq_2}$ be an order isomorphism.
Then $\struct {S, \preccurlyeq_1}$ is a lattice {{iff}} $\struct {T, \preccurlyeq_2}$ is also a lattice.

Proof:
Let $\struct {S, \preccurlyeq_1}$ be a lattice
Then by definition $\preccurlyeq_1$ is a lattice ordering.
We need to show that for all $x, y \in S$, the ordered set $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$ admits both a supremum and an infimum. 
Let $x, y \in S$.
Then $\struct {\set {x, y}, \preccurlyeq_1}$ admits both a supremum and an infimum.
Let $c = \map \sup {\set {x, y}, \preccurlyeq_1}$.
Then by definition of supremum:
:$\forall s \in \set {x, y}: s \preccurlyeq_1 c$
:$\forall d \in S: c \preccurlyeq_1 d$
where $d$ is an upper bound of $\struct {\set {x, y}, \preccurlyeq_1} \subseteq S$.
Now consider the image of $\set {x, y}$ under $\phi$.
By definition of order isomorphism:
:$\forall \map \phi s \in \set {\map \phi x, \map \phi y}: \map \phi c \preccurlyeq_2 \map \phi s$
:$\forall \map \phi d \in T: \map \phi c \preccurlyeq_2 \map \phi d$
where $\map \phi d$ is an upper bound of $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2} \subseteq T$.
So by definition of supremum:
:$\map \phi c = \map \sup {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$
That is, $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$ admits a supremum.
Using a similar technique it can be shown that:
:If $c = \map \inf {\set {x, y}, \preccurlyeq}$, then:
:$\map \phi c = \map \inf {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$
Hence $\struct {\set {\map \phi x, \map \phi y}, \preccurlyeq_2}$ admits both a supremum and an infimum.
That is, $\preccurlyeq_2$ is a lattice ordering and so $\struct {T, \preccurlyeq_2}$ is a lattice.
By Inverse of Order Isomorphism is Order Isomorphism, if $\phi$ is an order isomorphism then so is $\phi^{-1}$.
So the same technique is used to show that if $\struct {T, \preccurlyeq_2}$ is a lattice then so is $\struct {S, \preccurlyeq_1}$.
{{qed}}
Theorem: Set of Subgroups forms Complete Lattice

Let $\struct {G, \circ}$ be a group.
Let $\mathbb G$ be the set of all subgroups of $G$.
Then:
:$\struct {\mathbb G, \subseteq}$ is a complete lattice.
where for every set $\mathbb H$ of subgroups of $G$:
:the infimum of $\mathbb H$ necessarily admitted by $\mathbb H$ is $\ds \bigcap \mathbb H$.

Proof:
Let $\O \subset \mathbb H \subseteq \mathbb G$.
By Intersection of Subgroups: General Result, $\bigcap \mathbb H$ is the largest subgroup of $G$ contained in each of the elements of $\mathbb H$.
Thus, not only is $\ds \bigcap \mathbb H$ a lower bound of $\mathbb H$, but also the largest, and therefore an infimum.
The supremum of $\mathbb H$ is the smallest subgroup of $G$ containing $\bigcup \mathbb H$.
Therefore $\struct {\mathbb G, \subseteq}$ is a complete lattice.
{{qed}}
Theorem: Set of Subgroups forms Complete Lattice

Let $\struct {G, \circ}$ be a group.
Let $\mathbb G$ be the set of all subgroups of $G$.
Then:
:$\struct {\mathbb G, \subseteq}$ is a complete lattice.
where for every set $\mathbb H$ of subgroups of $G$:
:the infimum of $\mathbb H$ necessarily admitted by $\mathbb H$ is $\ds \bigcap \mathbb H$.

Proof:
From Group is Subgroup of Itself:
:$\struct {G, \circ} \in \mathbb G$
Let $\mathbb H$ be a non-empty subset of $\mathbb G$.
From Intersection of Subgroups is Subgroup: General Result:
:$\ds \bigcap \mathbb H \in \mathbb G$
Hence, from Set of Subsets which contains Set and Intersection of Subsets is Complete Lattice:
:$\struct {\mathbb G, \subseteq}$ is a complete lattice
where $\ds \bigcap \mathbb H$ is the infimum of $\mathbb H$.
{{qed}}
Theorem: Index Laws/Sum of Indices/Monoid

Let $\struct {S, \circ}$ be a monoid whose identity element is $e$.
For $a \in S$, let $\circ^n a = a^n$ be defined as the $n$th power of $a$:
:<nowiki>$a^n = \begin{cases}
e & : n = 0 \\
a^x \circ a & : n = x + 1
\end{cases}$</nowiki>
That is:
:$a^n = \underbrace {a \circ a \circ \cdots \circ a}_{n \text{ copies of } a} = \map {\circ^n} a$
while:
:$a^0 = e$
Then:
:$\forall m, n \in \N: a^{n + m} = a^n \circ a^m$

Proof:
Because $\struct {S, \circ}$ is a monoid, it is {{afortiori}} also a semigroup.
From Index Laws for Semigroup: Sum of Indices:
:$\forall m, n \in \N_{>0}: \circ^{n + m} a = \paren {\circ^n a} \circ \paren {\circ^m a}$
That is:
:$\forall m, n \in \N_{>0}: a^{n + m} = a^n \circ a^m$
It remains to be shown that the result holds for the cases where $m = 0$ and $n = 0$.
Let $n \in \N$:
{{begin-eqn}}
{{eqn | l = a^{n + 0}
      | r = a^n
      | c = Integer Addition Identity is Zero
}}
{{eqn | r = a^n \circ e
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = a^n \circ a^0
      | c = Definition of $a^0$
}}
{{end-eqn}}
Similarly, let $m \in \N$:
{{begin-eqn}}
{{eqn | l = a^{0 + m}
      | r = a^m
      | c = Identity Element of Natural Number Addition is Zero
}}
{{eqn | r = e \circ a_m
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = a^0 \circ a^m
      | c = Definition of $a^0$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = a^{0 + 0}
      | r = a^0
      | c = Identity Element of Natural Number Addition is Zero
}}
{{eqn | r = e
      | c = Definition of $a^0$
}}
{{eqn | r = e \circ e
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = a^0 \circ a^0
      | c = Definition of $a^0$
}}
{{end-eqn}}
Thus:
:$a^{n + m} = a^n \circ a^m$
holds for $n = 0$ and $m = 0$.
Thus:
:$\forall m, n \in \N: a^{n + m} = a^n \circ a^m$
{{qed}}