avewright/proofwiki-math huggingface dataset:
Theorem: Subset of Well-Ordered Set is Well-Ordered

Let $\struct {S, \preceq}$ be a well-ordered set.
Let $T \subseteq S$ be a subset of $S$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Then the relational structure $\struct {T, \preceq'}$ is a well-ordered set.

Proof:
By definition of well-ordered set, $\struct {S, \preceq}$ is:
:a totally ordered set
and:
:a well-founded set.
By Subset of Toset is Toset, $\struct {T, \preceq'}$ is a totally ordered set.
By Subset of Well-Founded Relation is Well-Founded, $\preceq'$ is a well-founded relation.
Hence the result.
{{qed}}
Theorem: Subset of Well-Ordered Set is Well-Ordered

Let $\struct {S, \preceq}$ be a well-ordered set.
Let $T \subseteq S$ be a subset of $S$.
Let $\preceq'$ be the restriction of $\preceq$ to $T$.
Then the relational structure $\struct {T, \preceq'}$ is a well-ordered set.

Proof:
Let $V$ be a basic universe.
By definition of basic universe, $S$ and $T$ are all elements of $V$.
By the {{axiom-link|Transitivity}}, $S$ and $T$ are both classes.
Thus $T$ is a subclass of $S$.
We have {{hypothesis}} that $\preceq$ is a well-ordering on $S$.
So from Subclass of Well-Ordered Class is Well-Ordered, $\preceq'$ is a well-ordering on $T$.
Hence the result.
{{qed}}
Theorem: Element Commutes with Product of Commuting Elements

Let $\struct {S, \circ}$ be a semigroup.
Let $x, y, z \in S$.
Let $x$ commute with both $y$ and $z$.
Then $x$ commutes with $y \circ z$.

Proof:
{{begin-eqn}}
{{eqn | l = x \circ \paren {y \circ z}
      | r = \paren {x \circ y} \circ z
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \paren {y \circ x} \circ z
      | c = $x$ commutes with $y$
}}
{{eqn | r = y \circ \paren {x \circ z}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = y \circ \paren {z \circ x}
      | c = $x$ commutes with $z$
}}
{{eqn | r = \paren {y \circ z} \circ x
      | c = {{Semigroup-axiom|1}}
}}
{{end-eqn}}
{{qed}}
Theorem: Associative Idempotent Anticommutative

Let $\circ$ be a binary operation on a non-empty set $S$.
Let $\circ$ be associative.
Then $\circ$ is anticommutative {{iff}}:
:$(1): \quad \circ$ is idempotent
and:
:$(2): \quad \forall a, b \in S: a \circ b \circ a = a$

Proof:
Let $\circ$ be an associative operation on $S$.
Theorem: Associative and Anticommutative

Let $\circ$ be a binary operation on a set $S$.
Let $\circ$ be both associative and anticommutative.
Then:
:$\forall x, y, z \in S: x \circ y \circ z = x \circ z$

Proof:
Let $\circ$ be both associative and anticommutative.
Then from Associative Idempotent Anticommutative:
:$\forall x, z \in S: x \circ z \circ x = x$
and $\circ$ is idempotent.
Consider $x \circ y \circ z \circ x \circ z$.
We have:
{{begin-eqn}}
{{eqn | l = x \circ y \circ z \circ x \circ z
      | r = x \circ \paren {y \circ z} \circ x \circ z
      | c = 
}}
{{eqn | r = x \circ z
      | c = 
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = x \circ y \circ z \circ x \circ z
      | r = x \circ y \circ \paren {z \circ x \circ z}
      | c = 
}}
{{eqn | r = x \circ y \circ z
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Constant Operation is Commutative

Let $S$ be a set.
Let $x \sqbrk c y = c$ be a constant operation on $S$.
Then $\sqbrk c$ is a commutative operation:
:$\forall x, y \in S: x \sqbrk c y = y \sqbrk c x$

Proof:
{{begin-eqn}}
{{eqn | l = x \sqbrk c y
      | r = c
      | c = {{Defof|Constant Operation}}
}}
{{eqn | l = y \sqbrk c x
      | r = c
      | c = {{Defof|Constant Operation}}
}}
{{eqn | ll= \leadsto
      | l = x \sqbrk c y
      | r = y \sqbrk c x
      | c = 
}}
{{end-eqn}}
Hence the result by definition of commutativity.
{{Qed}}
Category:Constant Operation
Category:Examples of Commutative Operations
jtoswnz1fv85rv1uyociy0m0cyllezn
Theorem: Constant Operation is Associative

Let $S$ be a set.
Let $x \sqbrk c y = c$ be a constant operation on $S$.
Then $\sqbrk c$ is an associative operation:
:$\forall x, y, z \in S: \paren {x \sqbrk c y} \sqbrk c z = x \sqbrk c \paren {y \sqbrk c z}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {x \sqbrk c y} \sqbrk c z
      | r = c \sqbrk c z
      | c = {{Defof|Constant Operation}}
}}
{{eqn | r = c
      | c = {{Defof|Constant Operation}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = x \sqbrk c \paren {y \sqbrk c z}
      | r = x \sqbrk c c
      | c = {{Defof|Constant Operation}}
}}
{{eqn | r = c
      | c = {{Defof|Constant Operation}}
}}
{{end-eqn}}
{{qed}}
Category:Constant Operation
Category:Examples of Associative Operations
86xmoxtm45p16bjvcjnqduccqfswnpo
Theorem: Left Operation is Idempotent

The left operation is idempotent:
:$\forall x: x \leftarrow x = x$

Proof:
Immediate from the definition of the left operation.
{{Qed}}
Theorem: Right Operation is Idempotent

The right operation is idempotent:
:$\forall x: x \rightarrow x = x$

Proof:
Immediate from the definition of the right operation.
Theorem: Left Operation is Anticommutative

The left operation is anticommutative:
:$\forall x, y: x \leftarrow y = y \leftarrow x \iff x = y$

Proof:
Immediate from the definition of the left operation.
{{qed}}
Theorem: Right Operation is Anticommutative

The right operation is anticommutative:
:$\forall x, y: x \rightarrow y = y \rightarrow x \iff x = y$

Proof:
Immediate from the definition of the right operation.
{{qed}}
Theorem: Left Operation is Associative

The left operation is associative:
:$\forall x, y, z: \paren {x \gets y} \gets z = x \gets \paren {y \gets z}$

Proof:
{{begin-eqn}}
{{eqn | l = x \gets \paren {y \gets z}
      | r = x \gets y
      | c = {{Defof|Left Operation}}
}}
{{eqn | r = x
      | c = {{Defof|Left Operation}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \paren {x \gets y} \gets z
      | r = x \gets z
      | c = {{Defof|Left Operation}}
}}
{{eqn | r = x
      | c = {{Defof|Left Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Right Operation is Associative

The right operation is associative:
:$\forall x, y, z: \paren {x \to y} \to z = x \to \paren {y \to z}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {x \to y} \to z
      | r = y \to z
      | c = {{Defof|Right Operation}}
}}
{{eqn | r = z
      | c = {{Defof|Right Operation}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = x \to \paren {y \to z}
      | r = x \to z
      | c = {{Defof|Right Operation}}
}}
{{eqn | r = z
      | c = {{Defof|Right Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Min Operation is Idempotent

The min operation operation is idempotent:
:$\map \min {x, x} = x$

Proof:
Follows immediately from the definition of min operation:
:$\map \min {a, b} = \begin {cases} a & : a \le b \\ b & : b \le a \end {cases}$
Setting $x = a = b$ returns the result.
{{Qed}}
Theorem: Equality of Algebraic Structures

Two algebraic structures $\struct {S, \circ}$ and $\struct {T, *}$ are equal {{iff}}:
:$S = T$
:$\forall a, b \in S: a \circ b = a * b$

Proof:
This follows from set equality and Equality of Ordered Pairs.
Category:Algebraic Structures
Category:Equality
gjfvo3rl6m5v407sjg2xuqj8qs3g51r
Theorem: Restriction of Associative Operation is Associative

Let $\struct {S, \circ}$ be an algebraic structure.
Let $T \subseteq S$.
Let $\circ_T$ denote the restriction of $\circ$ to $T$.
Let the operation $\circ$ be associative on $\struct {S, \circ}$.
Then $\circ_T$ is associative on $\struct {T, \circ_T}$.

Proof:
{{begin-eqn}}
{{eqn | l = T
      | o = \subseteq
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall a, b, c \in T
      | l = a, b, c
      | o = \in
      | r = S
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = a \mathop {\circ_T} \paren {b \mathop {\circ_T} c}
      | r = a \circ \paren {b \circ c}
      | c = {{Defof|Restriction of Operation}}
}}
{{eqn | r = \paren {a \circ b} \circ c
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \paren {a \mathop {\circ_T} b} \mathop {\circ_T} c
      | c = {{Defof|Restriction of Operation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Restriction of Commutative Operation is Commutative

Let $\struct {S, \circ}$ be an algebraic structure.
Let $T \subseteq S$.
Let the operation $\circ$ be commutative on $\struct {S, \circ}$.
Then the restriction $\circ {\restriction_T}$ of $\circ$ to $T$ is also commutative.

Proof:
{{begin-eqn}}
{{eqn | l = T
      | o = \subseteq
      | r = S
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall a, b \in T
      | l = a, b
      | o = \in
      | r = S
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | l = a \mathop {\circ {\restriction_T} } b
      | r = a \circ b
      | c = 
}}
{{eqn | r = b \circ a
      | c = $\circ$ is commutative
}}
{{eqn | r = b \mathop {\circ {\restriction_T} } a
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Idempotent Magma Element forms Singleton Submagma

Let $\struct {S, \circ}$ be a magma.
Let $x \in S$ be an idempotent element of $\struct {S, \circ}$.
Then $\struct {\set x, \circ}$ is a submagma of $\struct {S, \circ}$.

Proof:
By Singleton of Element is Subset:
:$x \in S \iff \set x \subseteq S$
By the definition of idempotence:
:$x \circ x = x \in \set x$
Thus $\set x$ is a subset of $S$ which is closed under $\circ$.
By the definition of submagma, the result follows.
{{qed}}
Theorem: Magma Subset Product with Self

Let $\struct {S, \circ}$ be a magma.
Let $T \subseteq S$.
Then $\struct {T, \circ}$ is a magma {{iff}} $T \circ T \subseteq T$, where $T \circ T$ is the subset product of $T$ with itself.

Proof:
By definition:
:$T \circ T = \set {x = a \circ b: a, b \in T}$
Theorem: Subset Product within Semigroup is Associative

Let $\struct {S, \circ}$ be a semigroup.
Then the operation $\circ_\PP$ induced on the power set of $S$ is also associative.

Proof:
Let $X, Y, Z \in \powerset S$.
Then:
{{begin-eqn}}
{{eqn | l = X \circ_\PP \paren {Y \circ_\PP Z}
      | r = \set {x \circ \paren {y \circ z}: x \in X, y \in Y, z \in Z}
      | c = {{Defof|Subset Product}}
}}
{{eqn | r = \set {\paren {x \circ y} \circ z: x \in X, y \in Y, z \in Z}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = \paren {X \circ_\PP Y} \circ_\PP Z
      | c = {{Defof|Subset Product}}
}}
{{end-eqn}}
demonstrating that $\circ_\PP$ is associative on $\powerset S$.
{{qed}}
Theorem: Subset Product within Commutative Structure is Commutative

Let $\struct {S, \circ}$ be a magma.
If $\circ$ is commutative, then the operation $\circ_\PP$ induced on the power set of $S$ is also commutative.

Proof:
Let $\struct {S, \circ}$ be a magma in which $\circ$ is commutative.
Let $X, Y \in \powerset S$.
Then:
{{begin-eqn}}
{{eqn | l = X \circ_\PP Y
      | r = \set {x \circ y: x \in X, y \in Y}
      | c = Definition of $\circ_\PP$
}}
{{eqn | r = \set {y \circ x: x \in X, y \in Y}
      | c = {{Defof|Commutative Operation}}
}}
{{eqn | r = Y \circ_\PP X
      | c = Definition of $\circ_\PP$
}}
{{end-eqn}}
Hence $\circ_\PP$ is commutative on $\powerset S$.
{{qed}}
Theorem: Subset Relation is Compatible with Subset Product

Let $\struct {S, \circ}$ be a magma.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Then the subset relation on $S$ is compatible with $\circ_\PP$.
That is:
{{begin-eqn}}
{{eqn | q = \forall X, Y, Z \in \powerset S
      | l = X \subseteq Y
      | o = \implies
      | r = \paren {X \circ_\PP Z} \subseteq \paren {Y \circ_\PP Z}
      | c = 
}}
{{eqn | l = X \subseteq Y
      | o = \implies
      | r = \paren {Z \circ_\PP X} \subseteq \paren {Z \circ_\PP Y}
      | c = 
}}
{{end-eqn}}

Proof:
Let $x \in X, z \in Z$.
Then:
:$x \circ z \in X \circ Z$ and $z \circ x \in Z \circ X$
Now:
:$Y \circ Z = \set {y \circ z: y \in Y, z \in Z}$
:$Z \circ Y = \set {z \circ y: y \in Y, z \in Z}$
But by the definition of a subset:
:$x \in X \implies x \in Y$
Thus:
:$x \circ z \in Y \circ Z$ and $z \circ x \in Z \circ Y$
and the result follows.
{{Qed}}
Theorem: Cancellable Element is Cancellable in Subset

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\struct {T, \circ} \subseteq \struct {S, \circ}$.
Let $x \in T$ be cancellable in $S$.
Then $x$ is also cancellable in $T$.

Proof:
Let $x \in T$ be cancellable in $S$.
Then by definition, $x \in T$ is left cancellable in $S$.
It follows from Left Cancellable Element is Left Cancellable in Subset that $x \in T$ is left cancellable in $T$.
Again by definition, $x \in T$ is right cancellable in $S$.
It follows from Right Cancellable Element is Right Cancellable in Subset that $x \in T$ is right cancellable in $T$.
Thus $x$ is also both left cancellable and right cancellable in $T$.
So by definition, $x$ is cancellable in $T$.
{{qed}}
Theorem: Subsemigroup Closure Test

To show that an algebraic structure $\struct {T, \circ_T}$ is a subsemigroup of a semigroup $\struct {S, \circ}$, we need to show only that:
:$(1): \quad T \subseteq S$
:$(2): \quad \circ$ is a closed operation in $T$.
where $\circ_T$ denotes the restriction of $\circ$ to $T$.

Proof:
From Restriction of Associative Operation is Associative, if $\circ$ is associative on $\struct {S, \circ}$, then it will also be associative on $\struct {T, \circ_T}$.
Thus we do not need to check for associativity in $\struct {T, \circ_T}$, as that has been inherited from its extension $\struct {S, \circ}$.
So, once we have established that $T \subseteq S$, all we need to do is to check for $\circ$ to be a closed operation in $T$.
{{Qed}}
Theorem: Cancellable iff Regular Representations Injective

Let $\struct {S, \circ}$ be an algebraic structure.
Then $a \in S$ is cancellable {{iff}}:
:the left regular representation $\map {\lambda_a} x$ is injective
and:
:the right regular representation $\map {\rho_a} x$ is injective.

Proof:
=== Left Cancellable ===
{{:Left Cancellable iff Left Regular Representation Injective}}
Theorem: More than one Left Identity then no Right Identity

Let $\struct {S, \circ}$ be an algebraic structure.
If $\struct {S, \circ}$ has more than one left identity, then it has no right identity.

Proof:
Let $\struct {S, \circ}$ be an algebraic structure with more than one left identity.
Take any two of these, and call them $e_{L_1}$ and $e_{L_2}$, where $e_{L_1} \ne e_{L_2}$.
Suppose $\struct {S, \circ}$ has a right identity.
Call this right identity $e_R$.
Then, by the behaviour of $e_R$, $e_{L_1}$ and $e_{L_2}$:
:$e_{L_1} = e_{L_1} \circ e_R = e_R$
:$e_{L_2} = e_{L_2} \circ e_R = e_R$
So $e_{L_1} = e_R = e_{L_2}$, which contradicts the supposition that $e_{L_1}$ and $e_{L_2}$ are different.
Therefore, in an algebraic structure with more than one left identity, there can be no right identity.
{{qed}}
Theorem: Element under Left Operation is Right Identity

Let $\struct {S, \gets}$ be an algebraic structure in which the operation $\gets$ is the left operation.
Then all of the elements of $\struct {S, \gets}$ are right identities.

Proof:
From Structure under Left Operation is Semigroup, $\struct {S, \gets}$ is a semigroup.
From the definition of left operation:
:$\forall x, y \in S: x \gets y = x$
from which it is apparent that all elements of $S$ are right identities.
{{qed}}
Theorem: Element under Right Operation is Left Identity

Let $\struct {S, \to}$ be an algebraic structure in which the operation $\to$ is the right operation.
Then all of the elements of $\struct {S, \to}$ left identities.

Proof:
From Structure under Left Operation is Semigroup, $\struct {S, \to}$ is a semigroup.
From the definition of right operation:
:$\forall x, y \in S: x \to y = y$
from which it is apparent that all elements of $S$ are left identities.
{{qed}}
Theorem: Left and Right Identity are the Same

Let $\struct {S, \circ}$ be an algebraic structure.
Let $e_L \in S$ be a left identity, and $e_R \in S$ be a right identity.
Then:
:$e_L = e_R$
that is, both the left identity and right identity are the same, and are therefore an identity $e$.
Furthermore, $e$ is the only left identity and right identity for $\circ$.

Proof:
Let $\struct {S, \circ}$ be an algebraic structure such that:
:$\exists e_L \in S: \forall x \in S: e_L \circ x = x$
:$\exists e_R \in S: \forall x \in S: x \circ e_R = x$
Then $e_L = e_L \circ e_R = e_R$ by both the above, hence the result.
The uniqueness of the left and right identity is a direct result of Identity is Unique.
{{Qed}}
Theorem: Identity Property in Semigroup

Let $\struct {S, \circ}$ be a semigroup.
Let $s \in S$ be such that:
:$\forall a \in S: \exists x, y \in S: s \circ x = a = y \circ s$
Then $\struct {S, \circ}$ has an identity.

Proof:
Suppose that:
:$\forall a \in S: \exists x, y \in S: s \circ x = a = y \circ s$.
Since $s \in S$, it follows that:
:$\exists v, w \in S: s \circ v = s = w \circ s$.
Let $a \in S$.
Then:
:$\exists x, y \in S: s \circ x = a = y \circ s$.
Thus:
{{begin-eqn}}
{{eqn | l = a
      | r = s \circ x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = w \circ a
      | r = w \circ s \circ x
      | c = 
}}
{{eqn | r = s \circ x
      | c = 
}}
{{eqn | r = a
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = a
      | r = y \circ s
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a \circ v
      | r = y \circ s \circ v
      | c = 
}}
{{eqn | r = y \circ s
      | c = 
}}
{{eqn | r = a
      | c = 
}}
{{end-eqn}}
Hence:
:$w \circ a = a$ and $a \circ v = a$
for any $a \in S$.
In particular:
:Letting $a = v$ in the first of these gives $w \circ v = v$
:Letting $a = w$ in the second gives $w \circ v = w$.
Thus $v = w \circ v = w$ is the identity element in $S$.
{{qed}}
Theorem: Identity of Monoid is Cancellable

Let $\struct {S, \circ}$ be a monoid.
Let $e$ be an identity element of $\struct {S, \circ}$.
Then $e$ is a cancellable element of $\struct {S, \circ}$.

Proof:
Let $x, y \in S$ such that $x \circ e = y \circ e$.
Then, by definition of identity element:
:$x = x \circ e = y \circ e = y$
Thus $x = y$.
{{qed}}
Theorem: Identity is only Idempotent Cancellable Element

Let $e_S$ be the identity of an algebraic structure $\struct {S, \circ}$.
Then $e_S$ is the only cancellable element of $\struct {S, \circ}$ that is idempotent.

Proof:
By Identity Element is Idempotent, $e_S$ is idempotent.
Let $x$ be a cancellable idempotent element of $\struct {S, \circ}$.
{{begin-eqn}}
{{eqn | l = x \circ x
      | r = x
      | c = $x$ is idempotent
}}
{{eqn | r = x \circ e_S
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
So $x \circ x = x \circ e_S$.
But because $x$ is also by hypothesis cancellable, it follows that $x = e_S$.
{{Qed}}
Theorem: Set of all Self-Maps under Composition forms Monoid

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 monoid whose identity element is the identity mapping on $S$.

Proof:
By Set of all Self-Maps under Composition forms Semigroup, $\struct {S^S, \circ}$ is a semigroup.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity the identity mapping on $S$ is the identity element of $\struct {S^S, \circ}$.
Since $\struct {S^S, \circ}$ is a semigroup with an identity element, it is a monoid by definition.
{{qed}}
Theorem: Test for Submonoid

To show that $\struct {T, \circ}$ is a submonoid of a monoid $\struct {S, \circ}$, we need to show that:
:$(1): \quad T \subseteq S$
:$(2): \quad \struct {T, \circ}$ is a magma (that is, that it is closed)
:$(3): \quad \struct {T, \circ}$ has an identity.

Proof:
From Subsemigroup Closure Test, $(1)$ and $(2)$ are sufficient to show that $\struct {T, \circ}$ is a subsemigroup of $\struct {S, \circ}$.
Demonstrating the presence of an identity is then sufficient to show that it is a monoid.
{{qed}}
Category:Monoids
s8ylqenh1apfl8zb5btm7g43qjgonsg
Theorem: Identity of Cancellable Monoid is Identity of Submonoid

Let $\struct {S, \circ}$ be a monoid, all of whose elements are cancellable.
Let $\struct {T, \circ}$ be a submonoid of $\struct {S, \circ}$.
Then the identity of $\struct {T, \circ}$ is the same element as the identity of $\struct {S, \circ}$.

Proof:
By Identity of Monoid is Unique:
: there is only one identity element of $\struct {S, \circ}$
and:
: there is only one identity element of $\struct {T, \circ}$.
Let $e_S$ be the identity of $\struct {S, \circ}$, and $e_T$ the identity of $\struct {T, \circ}$.
From Identity is only Idempotent Cancellable Element, $e_S$ is the only cancellable element of $\struct {S, \circ}$ which is idempotent.
But all elements of $\struct {S, \circ}$ are cancellable.
Thus $e_S$ is the only idempotent element of $\struct {S, \circ}$.
Again, all elements of $\struct {S, \circ}$ are cancellable.
Thus from Cancellable Element is Cancellable in Subset, all elements of $\struct {T, \circ}$ are cancellable.
Thus, $e_T$ is the only element of $\struct {T, \circ}$ which is idempotent.
Thus, as $e_T \in S$, we have $e_S \circ e_T = e_T = e_T \circ e_T$ and thus $e_S = e_T$.
{{qed}}
Theorem: Cancellable Elements of Monoid form Submonoid

The cancellable elements of a monoid $\struct {S, \circ}$ form a submonoid of $\struct {S, \circ}$.

Proof:
Let $C$ be the set of cancellable elements of $\struct {S, \circ}$.
Obviously $C \subseteq S$.
From Cancellable Elements of Semigroup form Subsemigroup, $\struct {C, \circ}$ is a subsemigroup of $S$.
Let $e_S$ be the identity of $\struct {S, \circ}$.
From Identity of Monoid is Cancellable, $e_S$ is cancellable, therefore $e_S \in C$.
As $e_S$ is the identity of $S$, we have that:
:$\forall x \in C: x \circ e_S = x = e_S \circ x$.
Thus $e_S$ is the identity of $\struct {C, \circ}$, which is therefore a monoid.
As $C \subseteq S$, the result follows.
{{qed}}
Category:Monoids
kbtbh08ex31xlu4bbjua3p7ib14hisw
Theorem: Product of Semigroup Element with Left Inverse is Idempotent

Let $\struct {S, \circ}$ be a semigroup with a left identity $e_L$.
Let $x \in S$ such that $\exists x_L: x_L \circ x = e_L$, that is $x$ has a left inverse with respect to the left identity.
Then:
:$\paren {x \circ x_L} \circ \paren {x \circ x_L} = x \circ x_L$
That is, $x \circ x_L$ is idempotent.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {x \circ x_L} \circ \paren {x \circ x_L}
      | r = x \circ \paren {x_L \circ x} \circ x_L
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = x \circ e_L \circ x_L
      | c = {{Defof|Left Inverse Element}}
}}
{{eqn | r = x \circ x_L
      | c = {{Defof|Left Identity}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Semigroup Element with Right Inverse is Idempotent

Let $\struct {S, \circ}$ be a semigroup with a right identity $e_R$.
Let $x \in S$ such that $\exists x_R: x \circ x_R = e_R$, that is, $x$ has a right inverse with respect to the right identity.
Then:
:$\paren {x_R \circ x} \circ \paren {x_R \circ x} = x_R \circ x$
That is, $x_R \circ x$ is idempotent.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {x_R \circ x} \circ \paren {x_R \circ x}
      | r = x_R \circ \paren {x \circ x_R} \circ x
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = x_R \circ e_R \circ x
      | c = {{Defof|Right Inverse Element}}
}}
{{eqn | r = x_R \circ x
      | c = {{Defof|Right Identity}}
}}
{{end-eqn}}
{{qed}}
Theorem: Left Inverse for All is Right Inverse

Let $\struct {S, \circ}$ be a semigroup with a left identity $e_L$ such that:
:$\forall x \in S: \exists x_L: x_L \circ x = e_L$
That is, every element of $S$ has a left inverse with respect to the left identity.
Then $x \circ x_L = e_L$, that is, $x_L$ is also a right inverse with respect to the left identity.

Proof:
Let $y = x \circ x_L$. Then:
{{begin-eqn}}
{{eqn | l = e_L \circ y
      | r = \paren {y_L \circ y} \circ y
      | c = {{Defof|Left Inverse Element}}
}}
{{eqn | r = y_L \circ \paren {y \circ y}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | r = y_L \circ y
      | c = Product of Semigroup Element with Left Inverse is Idempotent: $y = x \circ x_L$
}}
{{eqn | r = e_L
      | c = {{Defof|Left Inverse Element}}
}}
{{end-eqn}}
So $x \circ x_L = e_L$, and $x_L$ behaves as a right inverse as well as a left inverse with respect to the left identity.
{{qed}}