avewright/proofwiki-math huggingface dataset:
Theorem: Content of Monic Polynomial

If $f$ is monic, then $\cont f = \dfrac 1 n$ for some integer $n$.

Proof:
Since $f$ is monic, it can be written as:
:$f = X^r + \cdots + a_1 X + a_0$
Let $n = \inf \set {n \in \N : n f \in \Z \sqbrk X}$.
Let $d = \cont {n f}$.
Then by definition of content:
:$d = \gcd \set {n, n a_{r - 1}, \ldots, n a_1, n a_0}$
Therefore, by definition of GCD, $d$ divides $n$.
So say $n = k d$ with $k \in \Z$.
Then: 
:$\cont f = \dfrac d {k d} = \dfrac 1 k$
as required.
{{Qed}}
Category:Content of Polynomial
Category:Monic Polynomials
kblu9qebsdbv86z0a5zd2jhnb86ubfh
Theorem: Content of Scalar Multiple

:$\cont {q f} = q \cont f$

Proof:
Let $q = \dfrac a b$ with $a, b \in \Z$.
Let $\Z \sqbrk X$ denote the ring of polynomials over $\Z$.
Let $n \in \Z$ such that $n f \in \Z \sqbrk X$. 
Then we have:
:$b n \paren {q f} = a n f \in \Z \sqbrk X$
By the definition of content, and using that $a \in \Z$:
:$\cont {b n q f} = a \cont {n f}$
{{handwaving|why is $b n$ the infimum mentioned in the definition?}}
By definition of content:
:$\cont {q f} = \dfrac 1 {b n} \cont {b n q f}$
Combining the above with the definition of $\cont f$:
:$\cont {q f} = \dfrac a b \dfrac 1 n \cont {n f} = q \cont f$
{{Qed}}
Category:Polynomial Theory
Category:Content of Polynomial
jydm79bz6zwzzp09mabap9kjb8p52c8
Theorem: Fixed Point of Composition of Inflationary Mappings

Let $\struct {S, \preceq}$ be an ordered set.
Let $f, g: S \to S$ be inflationary mappings.
Let $x \in S$.
Then:
:$x$ is a fixed point of $f \circ g$
{{iff}}:
:$x$ is a fixed point of both $f$ and $g$.

Proof:
=== Necessary Condition ===
Follows from Fixed Point of Mappings is Fixed Point of Composition.
{{qed|lemma}}
Theorem: Group of Units is Group

Let $\struct {R, +, \circ}$ be a ring with unity.
Then the set of units of $\struct {R, +, \circ}$ forms a group under $\circ$.
Hence the justification for referring to the group of units of $\struct {R, +, \circ}$.

Proof:
Follows directly from Invertible Elements of Monoid form Subgroup of Cancellable Elements.
{{qed}}
Theorem: Principal Ideal of Principal Ideal Domain is of Irreducible Element iff Maximal/Forward Implication

Let $\struct {D, +, \circ}$ be a principal ideal domain.
Let $p$ be an irreducible element of $D$.
Let $\ideal p$ be the principal ideal of $D$ generated by $p$.
Then $\ideal p$ is a maximal ideal of $D$.

Proof:
Let $p$ be irreducible in $D$.
Let $U_D$ be the group of units of $D$.
By definition, an irreducible element is not a unit.
So from Principal Ideals in Integral Domain:
:$\ideal p \subset D$
Suppose the principal ideal $\ideal p$ is not maximal.
Then there exists an ideal $K$ of $D$ such that:
:$\ideal p \subset K \subset R$
Because $D$ is a principal ideal domain:
:$\exists x \in R: K = \ideal x$
Thus:
:$\ideal p \subset \ideal x \subset D$
Because $\ideal p \subset \ideal x$:
:$x \divides p$
by Principal Ideals in Integral Domain.
That is:
:$\exists t \in D: p = t \circ x$
But $p$ is irreducible in $D$, so $x \in U_D$ or $t \in U_D$.
That is, either $x$ is a unit or $x$ is an associate of $p$.
But since $K \subset D$:
:$\ideal x \ne D$ so $x \notin U_D$
by Principal Ideals in Integral Domain.
Also, since $\ideal p \subset \ideal x$:
:$\ideal p \ne \ideal x$
so $x$ is not an associate of $p$, by Principal Ideals in Integral Domain.
This contradiction shows that $\ideal p$ is a maximal ideal of $D$.
{{qed}}
Theorem: Principal Ideal of Principal Ideal Domain is of Irreducible Element iff Maximal/Reverse Implication

Let $\struct {D, +, \circ}$ be a principal ideal domain.
Let $\ideal p$ be the principal ideal of $D$ generated by $p$.
Let $\ideal p$ be a maximal ideal of $D$.
Then $p$ is irreducible.

Proof:
Let $\ideal p$ be a maximal ideal of $D$.
Let $p = f g$ be any factorization of $p$.
We must show that one of $f, g$ is a unit.
{{AimForCont}} neither of $f, g$ is a unit.
First it will be shown that:
:$\ideal p \subsetneqq \ideal f$
Let $x \in \ideal p$.
That is:
:$\exists q \in D: x = p q$
Then:
:$x = f g q \in \ideal f$
so:
:$\ideal p \subseteq \ideal f$
Now suppose $f \in \ideal p$.
Then:
:$\exists r \in D: f = r p$
and so from $p = f g$ above:
:$f = r g f$
Therefore:
:$r g = 1$
and so $g$ is a unit.
This is a contradiction.
Thus:
:$f \notin \ideal p$
and clearly:
:$f \in \ideal f$
so:
:$\ideal p \subsetneqq \ideal f$
as claimed.
{{Handwaving|"Clearly" needs to be replaced by a link to the definition which specifies this fact.}}
Therefore, since $\ideal p$ is maximal, we must have:
:$\ideal f = D$
But we assumed that $f$ is not a unit.
So there is no $h \in D$ such that $f h = 1$.
Therefore:
:$1 \notin \ideal f = \set {f h: h \in D}$
and:
:$\ideal f \subsetneqq D$
This is a contradiction.
Therefore at least one of $f, g$ must be a unit.
This completes the proof.
{{qed}}
Theorem: Subring of Polynomials over Integral Domain Contains that Domain

Let $\struct {R, +, \circ}$ be a commutative ring.
Let $\struct {D, +, \circ}$ be an integral subdomain of $R$.
Let $x \in R$.
Let $D \sqbrk x$ denote the ring of polynomials in $x$ over $D$.
Then $D \sqbrk x$ contains $D$ as a subring and $x$ as an element.

Proof:
We have that $\ds \sum_{k \mathop = 0}^m a_k \circ x^k$ is a polynomial for all $m \in \Z_{\ge 0}$.
Set $m = 0$:
:$\ds \sum_{k \mathop = 0}^0 a_k \circ x^k = a_k \circ x^0 = a_k \circ 1_D = a_k$
Thus:
:$\ds \forall a_k \in D: \sum_{k \mathop = 0}^0 a_k \circ x^k \in D$
It follows directly that $D$ is a subring of $D \sqbrk x$ by applying the Subring Test on elements of $D$.
{{qed}}
Theorem: Subring of Polynomials over Integral Domain is Smallest Subring containing Element and Domain

Let $\struct {R, +, \circ}$ be a commutative ring.
Let $\struct {D, +, \circ}$ be an integral subdomain of $R$.
Let $x \in R$.
Let $D \sqbrk x$ denote the ring of polynomials in $x$ over $D$.
Then $D \sqbrk x$ is the smallest subring of $R$ which contains $D$ as a subring and $x$ as an element.

Proof:
{{proof wanted|Whitelaw says "fairly obviously", so should be more or less straightforward.}}
Theorem: Cantor-Bernstein-Schröder Theorem/Lemma

Let $S$ be a set.
Let $T \subseteq S$.
Suppose that $f: S \to T$ is an injection.
Then there is a bijection $g: S \to T$.

Proof:
Recursively define a sequence $\langle C_n \rangle$ in the power set of $S$ as follows:
:$C_0 = S \setminus T$, the difference between $S$ and $T$.
:$C_{n + 1} = f \sqbrk {C_n}$, the image of $C_n$ under $f$.
Let $\ds C := \bigcup_{n \mathop \in \N} C_n$.
Define a mapping $h: S \to T$ as follows:
:$\map h x = \begin {cases} \map f x & : x \in C \\ x & : x \notin C \end {cases}$
=== $h$ is a mapping from $S$ to $T$ ===
By Law of Excluded Middle, for each $x \in S$:
:$x \in C$
or:
:$x \notin C$
Thus the construction produces a mapping on S.
It remains to be shown that:
:$\forall x \in S: \map h x \in T$
Let $x \in C$.
Then:
:$\map h x = \map f x \in T$
Let $x \notin C$.
Then by Set is Subset of Union of Family:
:$x \notin C_0$
As $x \in S$:
:$x \in S \setminus C_0$
by the definition of set difference.
By Relative Complement of Relative Complement:
:$S \setminus C_0 = T$
Thus $x \in T$ by the definition of subset.
As $\map h x = x$ in this case:
:$\map h x \in T$
{{qed|lemma}}
=== $h$ is injective ===
Let $x, y \in S$.
Suppose that $\map h x = \map h y$.
By Law of Excluded Middle for Two Variables:
:$\paren {x \in C} \land \paren {y \in C}$
or:
:$\paren {x \notin C} \land \paren {y \notin C}$
or:
:$\paren {x \in C} \land \paren {y \notin C}$
or:
:$\paren {x \notin C} \paren {y \in C}$
Let $x, y \in C$.
Then $x = y$ because $f$ is injective.
Let $x, y \notin C$.
Then $x = y$ by Identity Mapping is Injection.
Let $x \in C$ and $y \notin C$.
Then $x \in C_n$ for some $n$ by the definition of union.
By Set is Subset of Union of Family:
:$\map h x = \map f x \in C_{n + 1} \subseteq C$ 
Thus $\map h x \in C$.
:$\map h y = y$ by the definition of $h$.
Since $y \notin C$, this contradicts the assumption that $\map h x = \map h y$.
The argument for the case of $x \notin C$ and $y \in C$ is identical to the preceding.
Thus $\map h x = \map h y \implies x = y$ for all $x, y \in S$, so $h$ is injective.
{{qed|lemma}}
=== $h$ is surjective ===
Let $y \in T$.
By Law of Excluded Middle:
:$y \in C$
or:
:$y \notin C$
Let $y \notin C$.
Then:
:$\map h y = y$
Let $y \in C$.
Then as $y \notin C_0 = S \setminus T$:
:$\exists n \in \N_{>0}: y \in C_{n + 1}$
Thus:
:$\exists x \in C_n: y = \map f x$
By the definition of union:
:$x \in C$
Thus:
:$\map h x = \map f x = y$
Thus:
:$\forall y \in T: \exists x \in S: \map h x = y$
Thus by definition, $h$ is surjective.
{{qed}}
Theorem: Cantor-Bernstein-Schröder Theorem/Lemma

Let $S$ be a set.
Let $T \subseteq S$.
Suppose that $f: S \to T$ is an injection.
Then there is a bijection $g: S \to T$.

Proof:
Define a mapping $E: \powerset S \to \powerset S$ as:
:$\map E K = S \setminus \paren {T \setminus f \sqbrk K}$
where $f \sqbrk K$ is the image of $K$ under $f$.
Then:
:$\map E K = \paren {S \setminus T} \cup f \sqbrk K$
By Image of Subset under Relation is Subset of Image and {{Corollary|Set Union Preserves Subsets}}, $E$ is increasing.
Thus by Knaster-Tarski Lemma: Power Set, $E$ has a fixed point $X$.
Then by definition of fixed point:
:$\map E X = X$
That is:
:$\paren {S \setminus \paren {T \setminus f \sqbrk X} } = X$
Taking the set difference from $S$:
:$T \setminus f \sqbrk X = S \setminus X$
Let $f'$ be the restriction of $f$ to $X \times f \sqbrk X$.
By Injection to Image is Bijection, $f'$ is a bijection.
By Identity Mapping is Bijection, the identity mapping $I_{S \mathop \setminus X}$ from $S \setminus X$ to $T \setminus f \sqbrk X$ is a bijection.
Thus by Union of Bijections with Disjoint Domains and Codomains is Bijection, $g = f' \cup i$ is the bijection we seek.
{{qed}}
Theorem: Cantor-Bernstein-Schröder Theorem/Lemma

Let $S$ be a set.
Let $T \subseteq S$.
Suppose that $f: S \to T$ is an injection.
Then there is a bijection $g: S \to T$.

Proof:
Define $C = \{f^k(x) | k \in \N, x \in S \setminus T \}$.
Clearly, $C = C_0 \cup C_1$, where:
$C_0 = S \setminus T$, the difference between $S$ and $T$, 
$C_1 = \{f^k(x) | k \in \N_{> 0}, x \in S \setminus T \}$.
Note, that $S \setminus C_0 = S \setminus (S \setminus T) = S \cap T = T$ (use this theorem and $T \subseteq S$).
Obviously, $im(f|C) = C_1$.
Define a mapping $h: S \to S$ as follows:
$\map h x = \begin {cases} \map f x & : x \in C \\ x & : x \notin C \end {cases}$
Clearly, $h = f|C \cup I_{S \setminus C}$, where $I_{S \setminus C}$ is the  identity mapping on the set $S \setminus C$.
Note, that $dom(h) = S$;
$im(h) = im(f|C) \cup im(I_{S \setminus C}) =$
$C_1 \cup (S \setminus C) =$
$C_1 \cup (S \setminus (C_0 \cup C_1)) =$
$S \setminus C_0 =$
$T$.
Also, $h$ is an injection because $h$ is the union of the injections $f|C$ (Restriction of Injection is Injection) and $I_{S \setminus C}$,
and also $dom(f|C) \cap dom(I_{S \setminus C}) = \{\}$
and $im(f|C) \cap im(I_{S \setminus C}) = C_1 \cap (S \setminus C) = \{\}$ because $C_1 \subseteq C$.
Now $h$ is a bijection $S \to T$ because $dom(h) = S, im(h) = T$ and $h$ is an injection.
{{qed}}
Theorem: Cantor-Bernstein-Schröder Theorem/Proof 5

Let $S$ and $T$ be sets.
Let $f: S \to T$ and $g: T \to S$ be injections.
Then there exists a bijection $\phi: S \to T$.

Proof:
By Injection to Image is Bijection:
:$g: T \to g \sqbrk T$ is a bijection.
Thus $T$ is equivalent to $g \sqbrk T$.
By Composite of Injections is Injection $g \circ f: S \to g \sqbrk T \subset S$ is also an injection (to a subset of the domain of $g \circ f$).
Then by Cantor-Bernstein-Schröder Theorem: Lemma:
:There exists a bijection $h: S \to g \sqbrk T$.
Thus $S$ is equivalent to $g \sqbrk T$.
We already know that $T$ is equivalent to $g \sqbrk T$.
Thus by Set Equivalence behaves like Equivalence Relation, $S$ is equivalent to $T$.
By the definition of set equivalence:
:There is a bijection $\phi: S \to T$.
{{qed}}
Theorem: Quotient Space of Real Line may be Indiscrete

Let $\struct {\R, \tau}$ denote the real number line with the usual (Euclidean) topology.
Let $\Q$ denote the set of rational numbers.
Let $\mathbb I$ denote the set of irrational numbers.
Then $\set {\Q, \mathbb I}$ is a partition of $\R$.
Let $\sim$ be the equivalence relation induced on $\R$ by $\set {\Q, \mathbb I}$.
Let $T_\sim := \struct {\R / {\sim}, \tau_\sim}$ be the quotient space of $\R$ by $\sim$.
Then $T_\sim$ is an indiscrete space.

Proof:
Let $\phi: \R \to \R / {\sim}$ be the quotient mapping.
Then:
:$\forall x \in \Q: \map \phi x = \Q$
:$\forall x \in \mathbb I: \map \phi x = \mathbb I$
{{AimForCont}} $\set {\mathbb I} \in \tau_\sim$.
Then by the definition of the quotient topology:
:$\O \subsetneqq \mathbb I = \phi^{-1} \sqbrk {\set {\mathbb I} } \in \tau$
Thus by Rationals are Everywhere Dense in Topological Space of Reals, $\mathbb I$ contains a rational number.
This is a contradiction.
{{AimForCont}} $\set \Q \in \tau_\sim$.
Then:
:$\O \subsetneqq \Q = \phi^{-1} \sqbrk {\set \Q} \in \tau$
Thus by Irrationals are Everywhere Dense in Topological Space of Reals, $\Q$ contains a irrational number.
This is a contradiction.
As $\R / {\sim}$ has exactly two elements, its only non-empty proper subsets are $\set \Q$ and $\set {\mathbb I}$.
As neither of these sets is $\tau_\sim$-open, $\struct {\R / {\sim}, \tau_\sim}$ is indiscrete.
{{qed}}
Category:Quotient Spaces (Topology)
Category:Real Number Line with Euclidean Topology
tcbk0spuld17fyq3aynkb7lhwjjgj8u
Theorem: Quotient Space of Real Line may not be T0

Let $\struct {\R, \tau}$ denote the real number line with the usual (Euclidean) topology.
Then there exists an equivalence relation $\sim$ on $\R$ such that the quotient space $\struct {\R / {\sim}, \tau_\sim}$ is not a $T_0$ space.

Proof:
By Quotient Space of Real Line may be Indiscrete, there is an equivalence relation $\sim$ on $\R$ such that the quotient space $\struct {\R / {\sim}, \tau_\sim}$ has two points and is indiscrete.
It follows directly from the definition of $T_0$ space that $\struct {\R / {\sim}, \tau_\sim}$ is not a $T_0$ space.
{{qed}}
Category:Real Number Line with Euclidean Topology
Category:Quotient Spaces (Topology)
Category:Examples of T0 Spaces
ch58k8wynw54yl53elkt6nv1phzsbq6
Theorem: Unique Representation in Polynomial Forms/General Result

Let $f$ be a polynomial form in the indeterminates $\set {X_j: j \in J}$ such that $f: \mathbf X^k \mapsto a_k$.
For $r \in \R$, $\mathbf X^k \in M$, let $r \mathbf X^k$ denote the polynomial form that takes the value $r$ on $\mathbf X^k$ and zero on all other monomials.
Let $Z$ denote the set of all multiindices indexed by $J$.
Then the sum representation:
:$\ds \hat f = \sum_{k \mathop \in Z} a_k \mathbf X^k$
has only finitely many non-zero terms.
Moreover it is everywhere equal to $f$, and is the unique such sum.

Proof:
Suppose that the sum has infinitely many non-zero terms.
Then infinitely many $a_k$ are non-zero, which contradicts the definition of a polynomial.
Therefore the sum consists of finitely many non-zero terms.
Let $\mathbf X^m \in M$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map {\hat f} {\mathbf X^m}
      | r = \paren {\sum_{k \mathop \in Z} a_k \mathbf X^k} \paren {\mathbf X^m}
}}
{{eqn | r = \paren {a_m \mathbf X^m} \paren {\mathbf X^m} + \sum_{k \mathop \ne m \mathop \in Z} \paren {a_k \mathbf X^k} \paren {\mathbf X^m}
}}
{{eqn | r = a_m
}}
{{end-eqn}}
So $\hat f = f$.
Finally suppose that:
:$\ds \tilde f = \sum_{k \mathop \in Z} b_k \mathbf X^k$
is another such representation with $b_m \ne a_m$ for some $m \in Z$.
Then:
:$\map {\tilde f} {\mathbf X^m} = b_m \ne a_m = \map f {\mathbf X^m}$
Therefore $\hat f$ as defined above is the only such representation.
{{qed}}
Category:Polynomial Theory
7o8pvns4dhu5hef6lmp7exgbdq66ayi
Theorem: Unique Representation in Polynomial Forms/General Result/Corollary

Dropping the zero terms from the sum we can write the polynomial $f$ as
:$f = a_{k_1} \mathbf X^{k_1} + \cdots + a_{k_r} \mathbf X^{k_r}$
for some $a_{k_i}\in R$, $i = 1, \ldots, r$.

Proof:
Follows directly from Unique Representation in Polynomial Forms: General Result
{{qed}}
Category:Polynomial Theory
lhg13al7b3sgikdeoaiida9jri8zfp3
Theorem: Closed Element of Composite Closure Operator

Let $\struct {S, \preceq}$ be an ordered set.
Let $f, g: S \to S$ be closure operators.
Let $h = f \circ g$, where $\circ$ represents composition.
Suppose that $h$ is also a closure operator.
Then an element $x \in S$ is closed {{WRT}} $h$ {{iff}} it is closed {{WRT}} $f$ and {{WRT}} $g$.

Proof:
An element is closed with respect to a closure operator {{iff}} it is a fixed point of that operator.
Since $f$ and $g$ are closure operators, they are inflationary.
Thus the result follows from Fixed Point of Composition of Inflationary Mappings.
{{qed}}
Category:Closure Operators
Category:Closed Elements
d5skj832j0qft258fpfon2obsy3b9t3
Theorem: Law of Excluded Middle for Two Variables

:$\vdash (p \land q) \lor (\lnot p \land q) \lor (p \land \lnot q) \lor (\lnot p \land \lnot q)$

Proof:
{{BeginTableau| \vdash ((p \land q) \lor (\lnot p \land q)) \lor ( (p \land \lnot q) \lor (\lnot p \land \lnot q)) }}
{{ExcludedMiddle|1|p \lor \lnot p}}
{{ExcludedMiddle|2|q \lor \lnot q}}
{{Conjunction|3||(p \lor \lnot p) \land (q \lor \lnot q)|1|2}}
{{SequentIntro|4||((p \lor \lnot p) \land q) \lor ((p \lor \lnot p) \land \lnot q)|3|Conjunction Distributes over Disjunction}}
{{Assumption|5|(p \lor \lnot p) \land q}}
{{SequentIntro|6|5|(p \land q) \lor (\lnot p \land q)|5|Conjunction Distributes over Disjunction}}
{{Implication|7||(p \lor \lnot p) \land q \implies (p \land q) \lor (\lnot p \land q)|5|6 }}
{{Assumption|8|(p \lor \lnot p) \land \lnot q}}
{{SequentIntro|9|8| (p \land \lnot q) \lor (\lnot p \land \lnot q)|8| Conjunction Distributes over Disjunction }}
{{Implication|10|| (p \lor \lnot p) \land \lnot q \implies (p \land \lnot q) \lor (\lnot p \land \lnot q)|8|9}}
{{SequentIntro|11|| ((p \lor \lnot p) \land q) \lor ((p \lor \lnot p) \land \lnot q) \implies ((p \land q) \lor (\lnot p \land q)) \lor ( (p \land \lnot q) \lor (\lnot p \land \lnot q))|7,10|Constructive Dilemma}}
{{ModusPonens|12|| ((p \land q) \lor (\lnot p \land q)) \lor ( (p \land \lnot q) \lor (\lnot p \land \lnot q))|11|4 }}
{{EndTableau}}
{{qed}}
{{LEM}}
Category:Propositional Logic
48jjx3jhedwa77osqylwqo68vmo427a
Theorem: Cardinality of Finite Set is Well-Defined

Let $S$ be a finite set.
Then there is a unique natural number $n$ such that $S \sim \N_n$, where:
:$\sim$ represents set equivalence
and:
:$\N_n = \set {0, 1, \dotsc, n - 1}$ is the initial segment of $\N$ determined by $n$.

Proof:
By the definition of finite set, there is an $n \in \N$ such that $S \sim \N_n$.
Suppose $m \in \N$ and $S \sim \N_m$.
It follows from Set Equivalence behaves like Equivalence Relation that $\N_n \sim \N_m$.
Thus by Equality of Natural Numbers, $n = m$.  
Therefore the cardinality of a finite set is well-defined.
{{qed}}
Theorem: Ring of Polynomial Forms is Commutative Ring with Unity

Let $\struct {R, +, \circ}$ be a commutative ring with unity.
Let $A = R \sqbrk {\set {X_j: j \in J} }$ be the set of all polynomial forms over $R$ in the indeterminates $\set {X_j: j \in J}$.
Then $\struct {A, +, \circ}$ is a commutative ring with unity.

Proof:
We must show that the commutative and unitary ring axioms are satisfied:
{{:Axiom:Commutative and Unitary Ring Axioms}}
Theorem: Idempotent Elements form Subsemigroup of Commutative Semigroup

Let $\struct {S, \circ}$ be a semigroup such that $\circ$ is commutative.
Let $I$ be the set of all elements of $S$ that are idempotent under $\circ$.
That is:
:$I = \set {x \in S: x \circ x = x}$
Then $\struct {I, \circ}$ is a subsemigroup of $\struct {S, \circ}$.

Proof:
By Subsemigroup Closure Test we need only show that:
:For all $x, y \in I$: $x \circ y \in I$.
That is:
:$\paren {x \circ y} \circ \paren {x \circ y} = x \circ y$
We reason as follows:
{{begin-eqn}}
{{eqn | l = \paren {x \circ y} \circ \paren {x \circ y}
      | r = \paren {x \circ y} \circ \paren {y \circ x}
      | c = $\circ$ is commutative
}}
{{eqn | r = \paren {x \circ \paren {y \circ x} } \circ y
      | c = $\circ$ is associative
}}
{{eqn | r = \paren {x \circ \paren {x \circ y} } \circ y
      | c = $\circ$ is commutative
}}
{{eqn | r = \paren {x \circ x} \circ \paren {y \circ y}
      | c = $\circ$ is associative
}}
{{eqn | r = x \circ y
      | c = $x$ and $y$ are idempotent
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Idempotent Elements form Subsemigroup of Commutative Semigroup

Let $\struct {S, \circ}$ be a semigroup such that $\circ$ is commutative.
Let $I$ be the set of all elements of $S$ that are idempotent under $\circ$.
That is:
:$I = \set {x \in S: x \circ x = x}$
Then $\struct {I, \circ}$ is a subsemigroup of $\struct {S, \circ}$.

Proof:
By Subsemigroup Closure Test we need only show that:
: For all $x, y \in I$: $x \circ y \in I$.
As $x, y \in I$, they are idempotent.
We have that $\circ$ is commutative.
Thus, by definition, $x$ and $y$ commute.
From Product of Commuting Idempotent Elements is Idempotent, $\left({x \circ y}\right)$ is idempotent.
That is:
:$x \circ y \in I$
{{qed}}
Theorem: Product of Commuting Idempotent Elements is Idempotent

Let $\struct {S, \circ}$ be a semigroup.
Let $a, b \in S$ be idempotent elements of $S$.
Let $a$ and $b$ commute:
:$a \circ b = b \circ a$
Then $a \circ b$ is idempotent.

Proof:
From {{Semigroup-axiom|0}} we take it for granted that $\struct {S, \circ}$ is closed under $\circ$.
Hence:
{{begin-eqn}}
{{eqn | l = \paren {a \circ b} \circ \paren {a \circ b}
      | r = \paren {a \circ \paren {b \circ a} } \circ b
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \paren {a \circ \paren {a \circ b} } \circ b
      | c = $a$ and $b$ commute
}}
{{eqn | r = \paren {a \circ a} \circ \paren {b \circ b}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = a \circ b
      | c = $a$ and $b$ are idempotent by the premise
}}
{{end-eqn}}
Thus $a \circ b$ is idempotent.
{{qed}}
Category:Semigroups
Category:Idempotence
amo3ix1vhxjfziu2nqxzwgdpc7tzaf2
Theorem: Set of all Self-Maps under Composition forms Semigroup

Let $S$ be a set.
Let $S^S$ be the set of all mappings from $S$ to itself.
Let the operation $\circ$ represent composition of mappings.
Then the algebraic structure $\struct {S^S, \circ}$ is a semigroup.

Proof:
Let $f, g \in S^S$.
As the domain of $g$ and codomain of $f$ are the same, the composition $f \circ g$ is defined.
By the definition of composition, $f \circ g$ is a mapping from the domain of $g$ to the codomain of $f$.
Thus $f \circ g: S \to S$, so $f \circ g \in S^S$.
Since this holds for all $f, g \in S^S$,  $\struct {S^S, \circ}$ is closed.
By Composition of Mappings is Associative, $\circ$ is associative.
Since $\struct {S^S, \circ}$ is closed and $\circ$ is associative:
:$\struct {S^S, \circ}$ is a semigroup.
{{qed}}
Theorem: Integers form Subdomain of Reals

The integral domain of integers $\struct {\Z, +, \times}$ forms a subdomain of the field of real numbers.

Proof:
We have that Integers form Subdomain of Rationals.
We have that Rational Numbers form Subfield of Real Numbers.
Hence the result, from the definition of subdomain.
{{qed}}
Category:Integers
Category:Real Numbers
k7dkktib40yaper07azh5367u9i60v8
Theorem: Identity of Algebraic Structure is Preserved in Substructure

Let $\struct {S, \circ}$ be an algebraic structure with identity $e$.
Let $\struct {T, \circ}$ be a algebraic substructure of $\struct {S, \circ}$.
That is, let $T \subseteq S$.
Let $e \in T$.
Then $e$ is an identity of $\struct {T, \circ}$.

Proof:
Let $x \in T$.
By the definition of subset, $x \in S$.
Since $e$ is an identity of $\struct {S, \circ}$:
:$e \circ x = x \circ e = x$
Since this holds for all $x \in T$, $e$ is an identity of $\struct {T, \circ}$.
{{qed}}
Category:Identity Elements
n2ie5wgzy61jxufp2t0pdsatrdnts8o