avewright/proofwiki-math huggingface dataset:
Theorem: Inverse Mapping in Induced Structure of Homomorphism to Abelian Group

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\struct {T, \oplus}$ be an abelian group.
Let $f$ be a homomorphism from $S$ into $T$.
Let $f^*$ be the pointwise inverse of $f$.
Then $f^*$ is a homomorphism from $\struct {S, \circ}$ into $\struct {T, \oplus}$.

Proof:
Let $\struct {T, \oplus}$ be an abelian group.
Let $x, y \in S$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f^*} {x \circ y}
      | r = \paren {\map f {x \circ y} }^{-1}
      | c = {{Defof|Pointwise Inverse}}
}}
{{eqn | r = \paren {\map f x \oplus \map f y}^{-1}
      | c = $f$ is a homomorphism
}}
{{eqn | r = \paren {\map f y \oplus \map f x}^{-1}
      | c = Commutativity of $\oplus$
}}
{{eqn | r = \paren {\map f x}^{-1} \oplus \paren {\map f y}^{-1}
      | c = Inverse of Group Product
}}
{{eqn | r = \map {f^*} x \oplus \map {f^*} y
      | c = {{Defof|Pointwise Inverse}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set of Homomorphisms to Abelian Group is Subgroup of All Mappings

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\struct {T, \oplus}$ be an abelian group.
Let $\struct {T^S, \oplus}$ be the algebraic structure on $T^S$ induced by $\oplus$.
Then the set of all homomorphisms from $\struct {S, \circ}$ into $\struct {T, \oplus}$ is a subgroup of $\struct {T^S, \oplus}$.

Proof:
Let $H$ be the set of all homomorphisms from $\struct {S, \circ}$ into $\struct {T, \oplus}$.
Theorem: Transplanting Theorem

Let $\struct {S, \circ}$ be an algebraic structure.
Let $f: S \to T$ be a bijection.
Then there exists one and only one operation $\oplus$ such that $f: \struct {S, \circ} \to \struct {T, \oplus}$ is an isomorphism.
The operation $\oplus$ is defined by:
:$\forall x, y \in T: x \oplus y = \map f {\map {f^{-1} } x \circ \map {f^{-1} } y}$

Proof:
=== Existence ===
To show that $\oplus$ as defined above exists:
Let $u, v \in S$, and let $x = \map f u, y = \map f v$.
Then as $f$ is a bijection, $u = \map {f^{-1} } x, v = \map {f^{-1} } y$.
Thus:
{{begin-eqn}}
{{eqn | l = \map f {u \circ v}
      | r = \map f {\map {f^{-1} } x \circ \map {f^{-1} } y}
      | c = Definition of $x$ and $y$
}}
{{eqn | r = \map f {\map {f^{-1} } x} \oplus \map f {\map {f^{-1} } y}
      | c = {{Defof|Morphism Property}}
}}
{{eqn | r = x \oplus y
      | c = Inverse of Inverse of Bijection
}}
{{eqn | r = \map f u \oplus \map f v
      | c = Definition of $x$ and $y$
}}
{{end-eqn}}
It is seen that $f$ is an isomorphism as required.
{{qed|lemma}}
Theorem: Exists Bijection to a Disjoint Set

Let $S$ and $T$ be sets.
Then there exists a bijection from $T$ onto a set $T'$ disjoint from $S$.

Proof:
Consider the set:
:$X = \text{Ran}(S) =  \set {y: \paren {\exists x : \tuple {x, y} \in S} }$
From Relation is Set implies Domain and Image are Sets, this is indeed a set.
That is, $X$ consists of all the elements which are the second coordinate of some ordered pair which happens to be in $S$.
From Exists Element Not in Set, we have that $\exists z: z \notin X$.
Now consider the cartesian product $T' = T \times \set z$.
Suppose that $p \in T'$.
Then $p = \tuple {c, z}$ where $c \in T$.
Suppose $\tuple {c, z} \in S$.
Then that would mean that $z \in X$.
But we have specifically selected $z$ such that $z \notin X$.
So $p = \tuple {c, z} \notin S$.
Thus we have that $T' \cap S = \O$.
There is an obvious bijection $g: T \to T'$:
:$\forall t \in T: \map g t = \tuple {t, z}$
and hence the result.
{{qed}}
Theorem: Quotient Structure of Inverse Completion

Let $\struct {T, \circ'}$ be an inverse completion of a commutative semigroup $\struct {S, \circ}$, where $C$ is the set of cancellable elements of $S$.
Let $f: S \times C: T$ be the mapping defined as:
:$\forall x \in S, y \in C: \map f {x, y} = x \circ' y^{-1}$
Then the mapping $g: \paren {S \times C} / \RR_f \to T$ defined by $\map g {\eqclass {x, y} {\RR_f} } = x \circ' y^{-1}$,
where $\paren {S \times C} / \RR_f$ is a quotient structure, is an isomorphism.

Proof:
$T$ is commutative, from Inverse Completion is Commutative Semigroup.
The mapping $\map f {x, y} = x \circ' y^{-1}$ is an epimorphism from the cartesian product of $\struct {S, \circ}$ and $\struct {C, \circ \restriction_C}$ onto $\struct {T, \circ'}$.
By Quotient Theorem for Epimorphisms, the proof follows.
{{Explain|The mapping $\map f {x, y} {{=}} x \circ' y^{-1}$ is an epimorphism from the cartesian product of $\struct {S, \circ}$ and $\struct {C, \circ \restriction_C}$ onto $\struct {T, \circ'}$.}}
{{Proofread}}
Category:Inverse Completions
Category:Quotient Structures
eanskff40c1p73l5es9w2z369emh7y1
Theorem: Quotient Mapping of Inverse Completion

Let $\struct {T, \circ'}$ be an inverse completion of a commutative semigroup $\struct {S, \circ}$, where $C$ is the set of cancellable elements of $S$.
Let $f: S \times C: T$ be the mapping defined as:
:$\forall x \in S, y \in C: \map f {x, y} = x \circ' y^{-1}$
Let $\RR_f$ be the equivalence relation induced by $f$.
Then:
:$\tuple {x_1, y_1} \mathrel {\RR_f} \tuple {x_2, y_2} \iff x_1 \circ y_2 = x_2 \circ y_1$

Proof:
By the definition of $\RR_f$:
:$\tuple {x_1, y_1} \mathrel {\RR_f} \tuple {x_2, y_2} \iff x_1 \circ' y_1^{-1} = x_2 \circ' y_2^{-1}$
Now:
{{begin-eqn}}
{{eqn | l = x_1 \circ' y_1^{-1}
      | r = x_2 \circ' y_2^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1 \circ' y_1^{-1} \circ' y_1 \circ' y_2
      | r = x_2 \circ' y_2^{-1} \circ' y_1 \circ' y_2
      | c = Elements $y_1$ and $y_2$ are cancellable
}}
{{eqn | ll= \leadsto
      | l = x_1 \circ' y_2
      | r = x_2 \circ' y_1
      | c = {{Defof|Inverse Element}}, and commutativity of $\circ'$
}}
{{eqn | ll= \leadsto
      | l = x_1 \circ y_2
      | r = x_2 \circ y_1
      | c = $\circ'$ extends $\circ$
}}
{{end-eqn}}
which leads us to:
:$\tuple {x_1, y_1} \mathrel {\RR_f} \tuple {x_2, y_2} \iff x_1 \circ y_2 = x_2 \circ y_1$
{{qed}}
Category:Inverse Completions
2om0id39oam1sk3ljj5keesgt7lf0w0
Theorem: Subset Product defining Inverse Completion of Commutative Semigroup is Commutative Semigroup

Let $\struct {S, \circ}$ be a commutative semigroup.
Let $\struct {C, \circ} \subseteq \struct {S, \circ}$ be the subsemigroup of cancellable elements of $\struct {S, \circ}$.
Let $\struct {T, \circ'}$ be an inverse completion of $\struct {S, \circ}$.
Then:
:$S \circ' C^{-1}$ is a commutative semigroup
where $S \circ' C^{-1}$ is the subset product of $S$ with $C^{-1}$ under $\circ'$ in $T$.

Proof:
Note that by definition of inverse completion, $\struct {T, \circ'}$ is a semigroup.
Thus $\circ'$ is associative.
First it is demonstrated that $S \circ' C^{-1}$ is a semigroup.
Let $x, z \in S$.
Let $y, w \in C$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {x \circ' y^{-1} } \circ' \paren {z \circ' w^{-1} }
      | r = x \circ' \paren {y^{-1} \circ' z} \circ' w^{-1}
      | c = Associativity of $\circ'$
}}
{{eqn | r = x \circ' \paren {z \circ' y^{-1} } \circ' w^{-1}
      | c = Commutation with Inverse in Monoid
}}
{{eqn | r = \paren {x \circ' z} \circ' \paren {y^{-1} \circ' w^{-1} }
      | c = Associativity of $\circ'$
}}
{{eqn | r = \paren {x \circ' z} \circ' \paren {w \circ' y}^{-1}
      | c = Inverse of Product in Monoid
}}
{{eqn | r = \paren {x \circ z} \circ' \paren {w \circ y}^{-1}
      | c = $\circ'$ extends $\circ$
}}
{{end-eqn}}
Thus:
:$\paren {x \circ z} \circ' \paren {w \circ y}^{-1} \in S \circ' C^{-1}$
proving that $S \circ' C^{-1}$ is closed.
Therefore by Subsemigroup Closure Test:
:$S \circ' C^{-1}$ is a subsemigroup of $\struct {T, \circ'}$
and thus a semigroup.
{{qed|lemma}}
It remains to be shown that $\circ'$ is a commutative operation.
Let $\paren {x \circ' y^{-1} }$ and $\paren {z \circ' w^{-1} }$ be two arbitrary elements of $S \circ' C^{-1}$.
By Element Commutes with Product of Commuting Elements, $x, y, z, w$ all commute with each other under $\circ$.
As $\circ'$ is an extension of $\circ$, it follows that $x, y, z, w$ also all commute with each other under $\circ'$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {x \circ' y^{-1} } \circ' \paren {z \circ' w^{-1} }
      | r = x \circ' \paren {y^{-1} \circ' z} \circ' w^{-1}
      | c = Associativity of $\circ'$
}}
{{eqn | r = x \circ' \paren {z \circ' y^{-1} } \circ' w^{-1}
      | c = Commutation with Inverse in Monoid
}}
{{eqn | r = \paren {x \circ' z} \circ' \paren {y^{-1} \circ' w^{-1} }
      | c = Associativity of $\circ'$
}}
{{eqn | r = \paren {z \circ' x} \circ' \paren {w^{-1} \circ' y^{-1} }
      | c = Commutation of Inverses in Monoid
}}
{{eqn | r = z \circ' \paren {x \circ' w^{-1} } \circ' y^{-1}
      | c = Associativity of $\circ'$
}}
{{eqn | r = z \circ' \paren {w^{-1} \circ' x} \circ' y^{-1}
      | c = Commutation with Inverse in Monoid
}}
{{eqn | r = \paren {z \circ' w^{-1} } \circ' \paren {x \circ' y^{-1} }
      | c = Associativity of $\circ'$
}}
{{end-eqn}}
So $x \circ' y^{-1}$ commutes with $z \circ' w^{-1}$.
It follows by definition that $S \circ' C^{-1}$ is a commutative semigroup.
{{qed}}
Theorem: Inverse Completion of Commutative Semigroup is Inverse Completion of Itself

Let $\struct {S, \circ}$ be a commutative semigroup.
Let $\struct {C, \circ} \subseteq \struct {S, \circ}$ be the subsemigroup of cancellable elements of $\struct {S, \circ}$.
Let $\struct {T, \circ'}$ be an inverse completion of $\struct {S, \circ}$.
Then $\struct {T, \circ'}$ is its own inverse completion.

Proof:
Let $x \circ' y^{-1}$ be cancellable for $\circ'$, where $x \in S$ and $y \in C$.
We have that $y$ is invertible for $\circ'$.
So by Invertible Element of Associative Structure is Cancellable:
:$y$ is cancellable for $\circ'$.
Now by definition of inverse element:
:$x = \paren {x \circ' y^{-1} } \circ' y$
Thus $x$ is also cancellable for $\circ'$.
By Cancellable Elements of Semigroup form Subsemigroup, $x$ is cancellable for $\circ$.
So:
:$x \in S \implies x \in C$
Thus $x$ is invertible for $\circ'$.
Hence by Inverse of Product in Associative Structure:
:$x \circ' y$ is invertible for $\circ'$.
So every cancellable element of $\struct {T, \circ'}$ is invertible.
So, by definition, $\struct {T, \circ'}$ is its own inverse completion.
{{qed}}
Theorem: Identity of Inverse Completion of Commutative Monoid

Let $\struct {S, \circ}$ be a commutative monoid whose identity is $e$.
Let $\struct {C, \circ} \subseteq \struct {S, \circ}$ be the subsemigroup of cancellable elements of $\struct {S, \circ}$.
Let $\struct {T, \circ'}$ be an inverse completion of $\struct {S, \circ}$.
Then $e \in T$ is the identity for $\circ'$.

Proof:
Let $e$ be the identity for $\circ$.
Let $e = x \circ' y^{-1}$, where $x \in S, y \in C$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | r = e \circ y
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = \paren {x \circ' y^{-1} } \circ' y
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = x \circ' \paren {y^{-1} \circ' y}
      | c = $\circ'$ is associative
}}
{{eqn | r = x \circ' e
      | c = {{Defof|Inverse Element}}
}}
{{end-eqn}}
Thus $e = y^{-1} \circ' y$, and $y^{-1} \circ' y$ is the identity for $\circ'$.
{{qed}}
Theorem: Inverse Completion of Commutative Semigroup is Abelian Group

Let $\struct {S, \circ}$ be a commutative semigroup
Let all the elements of $\struct {S, \circ}$ be cancellable.
Then an inverse completion of $\struct {S, \circ}$ is an abelian group.

Proof:
Let $\struct {S, \circ}$ be a commutative semigroup, all of whose elements are cancellable.
Let $\struct {T, \circ'}$ be an inverse completion of $\struct {S, \circ}$.
From Inverse Completion is Commutative Monoid:
:$\struct {T, \circ'} = \struct {S \circ' S^{-1}, \circ'}$
has been shown to be a commutative monoid.
Taking the group axioms in turn:
Theorem: Taylor's Theorem

Every infinitely differentiable function can be approximated by a series of polynomials.

Proof:
Let $G$ be a real-valued function continuous on $\closedint a x$ and differentiable with non-vanishing derivative on $\openint a x$.
Let:
:$\map F t = \map f t + \dfrac {\map {f'} t} {1!} \paren {x - t} + \dotsb + \dfrac {\map {f^{\paren n} } t} {n!} \paren {x - t}^n$
By the Cauchy Mean Value Theorem:
:$(1): \quad \dfrac {\map {F'} x} {\map {G'} \xi} = \dfrac {\map F x - \map F a} {\map G x - \map G a}$
for some $\xi \in \openint a x$.
Note that the numerator:
:$\map F x - \map F a = R_n$
is the remainder of the Taylor polynomial for $\map f x$.
On the other hand, computing $\map {F'} \xi$:
:$\map {F'} \xi = \map {f'} \xi - \map {f'} \xi + \dfrac {\map {f' '} \xi} {1!} \paren {x - \xi} - \dfrac {\map {f' '} \xi} {1!} \paren {x - \xi} + \dotsb + \dfrac {\map {f^{\paren {n + 1} } } t} {n!} \paren {x - \xi}^n = \dfrac {\map {f^{\paren {n + 1} } } \xi} {n!} \paren {x - \xi}^n$
Putting these two facts together and rearranging the terms of $(1)$ yields:
:$R_n = \dfrac {\map {f^{\paren {n + 1} } } \xi} {n!} \paren {x - \xi}^n \dfrac {\map G x - \map G a} {\map {G'} \xi}$
which was to be shown.
{{improve|Find a way of neatly handling the two different remainder forms}}
Note that the Lagrange Form of the Remainder comes from taking $\map G t = \paren {x - t}^{n + 1}$ and the given Cauchy Form of the Remainder comes from taking $\map G t = t - a$.
{{qed}}
Theorem: Taylor's Theorem

Every infinitely differentiable function can be approximated by a series of polynomials.

Proof:
Let the function $g$ be defined as:
:$\map g t = \map {R_n} t - \dfrac {\paren {t - a}^{n + 1} } {\paren {x - a}^{n + 1} } \map {R_n} x$
Then:
:$\map {g^{\paren k} } a = 0$
for $k = 0, \dotsc, n$, and $\map g x = 0$.
Apply Rolle's Theorem successively to $g, g', \dotsc, g^{\paren n}$.
Then there exist:
:$\xi_1, \ldots, \xi_{n + 1}$
between $a$ and $x$ such that:
:$\map {g'} {\xi_1} = 0, \map {g' '} {\xi_2} = 0, \ldots, \map {g^{\paren {n + 1} } } {\xi_{n + 1} } = 0$
Let $\xi = \xi_{n + 1}$.
Then:
:$0 = \map {g^{\paren {n + 1} } } \xi = \map {f^{\paren {n + 1} } } \xi - \dfrac {\paren {n + 1}!} {\paren {x - a}^{n + 1} } \map {R_n} x$
and the formula for $\map {R_n} x$ follows.
{{qed}}
Theorem: Inverse Completion Theorem

Every commutative semigroup containing cancellable elements admits an inverse completion.

Proof:
Let $\struct {S, \circ}$ be a commutative semigroup which has cancellable elements.
From Construction of Inverse Completion, we can construct an inverse completion $\struct {T', \oplus'}$ of $\struct {S', \oplus'}$, which is an isomorphic copy of $S$ under the mapping $\psi: S \to S'$.
{{explain|$\psi: S \to S'$ has not been defined}}
By the Embedding Theorem, there exists a semigroup $\struct {T, \circ}$  which contains $\struct {S, \circ}$, and an isomorphism $\Psi$ from $\struct {T, \circ}$ to $\struct {T', \oplus'}$ which extends $\psi$.
Thus $T$ is an inverse completion of $S$.
{{Qed}}
Theorem: Extension Theorem for Homomorphisms

Let $\struct {S, \circ}$ be a commutative semigroup with cancellable elements
Let $\struct {C, \circ} \subseteq \struct {S, \circ}$ be the subsemigroup of all cancellable elements of $S$
Let $\struct {S', \circ'}$ be an inverse completion of $\struct {S, \circ}$
Let $\phi$ be a (semigroup) homomorphism from $\struct {S, \circ}$ into a semigroup $\struct {T, *}$ such that $\map \phi y$ is invertible for all $y \in C$.
Then:
:$(1): \quad$ There is one and only one homomorphism $\psi$ from $\struct {S', \circ'}$ into $\struct {T, *}$ extending $\phi$
:$(2): \quad \forall x \in S, y \in C: \map \psi {x \circ' y^{-1} } = \map \phi * \paren {\map \phi y}^{-1}$
:$(3): \quad$ If $\phi$ is a monomorphism, then so is $\psi$.

Proof:
It is proved that $\struct {C, \circ}$ is a subsemigroup of $\struct {S, \circ}$ by Cancellable Elements of Semigroup form Subsemigroup.
Theorem: Extension Theorem for Isomorphisms

Let the following conditions be fulfilled:
:Let $\struct {S, \circ}$ be a commutative semigroup with cancellable elements
:Let $\phi$ be an isomorphism from $\struct {S, \circ}$ into a semigroup $\struct {T, *}$
:Let $\struct {S', \circ'}$ be an inverse completion of $\struct {S, \circ}$
:Let $\struct {T', \circ'}$ be an inverse completion of $\struct {T, \circ}$.
Then there is a unique isomorphism $\phi': S' \to T'$ extending $\phi$.

Proof:
Let $C$ be the subsemigroup of cancellable elements of $S$.
It is proved that this is a semigroup by Cancellable Elements of Semigroup form Subsemigroup.
The set of cancellable elements of $T$ is $\phi \sqbrk C$.
By the Extension Theorem for Homomorphisms, there is:
:A unique homomorphism $\phi'$ from $S'$ into $T'$ extending $\phi$
and:
:A unique homomorphism $\psi$ from $T'$ into $S'$ extending $\phi^{-1}$.
Therefore, $\psi \circ \phi'$ is an endomorphism of $S'$ whose restriction to $S$ is the inclusion mapping $\iota_S: S \to S'$:
:$\forall x \in S: \map \iota x = x$
From Inclusion Mapping is Monomorphism, $\iota_S$ is a monomorphism from $S$ into $S'$.
But by the Extension Theorem for Homomorphisms, the identity automorphism of $S'$ is the only endomorphism of $S'$ extending $\iota_S$ from $S$ into $S'$, so:
:$\psi \circ \phi' = I_{S'}$
Similarly:
:$\phi' \circ \psi = I_{T'}$
So by Bijection iff Left and Right Inverse, $\phi'$ is a bijection and therefore an isomorphism.
{{Qed}}
Theorem: Inverse Completion is Unique

An inverse completion of a commutative semigroup is unique up to isomorphism.

Proof:
Let $T$ and $T'$ both be inverse completions of a commutative semigroup $S$ having cancellable elements.
Then from the Extension Theorem for Isomorphisms, there is a unique isomorphism $\phi: T \to T'$ satisfying $\forall x \in S: \map \phi x = x$.
Hence the result.
{{Qed}}
Theorem: Monoid is not Empty

A monoid cannot be empty.

Proof:
Let $\left({S, \circ}\right)$ be a the monoid.
By definition:
:Identity: $\exists e_S \in S: \forall a \in S: a \circ e_S = a = e_S \circ a$
So a monoid must ''at least'' have an identity.
Therefore $e_S \in S$ and so $S$ is not the empty set.
{{qed}}
Theorem: Group is not Empty

A group cannot be empty.

Proof:
A group is defined as a monoid for which every element has an inverse.
Thus, as a group is already a monoid, it must ''at least'' have an identity, therefore can not be empty.
{{qed}}
Theorem: Identity is only Idempotent Element in Group

Every group has exactly one idempotent element: the identity.

Proof:
The Identity Element is Idempotent.
From the Cancellation Laws, all group elements are cancellable.
The result follows from Identity is only Idempotent Cancellable Element.
{{qed}}
Theorem: Identity is only Idempotent Element in Group

Every group has exactly one idempotent element: the identity.

Proof:
Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $x \in G$ such that $x \circ x = x$.
{{begin-eqn}}
{{eqn | l = e
      | r = x \circ x^{-1}
      | c = {{Group-axiom|3}}
}}
{{eqn | r = \paren {x \circ x} \circ x^{-1}
      | c = {{hypothesis}}: $x \circ x = x$
}}
{{eqn | r = x \circ \paren {x \circ x^{-1} }
      | c = {{Group-axiom|1}}
}}
{{eqn | r = x \circ e
      | c = {{Defof|Inverse Element}}
}}
{{eqn | r = x
      | c = {{Defof|Identity Element}}
}}
{{end-eqn}}
{{qed}}
Theorem: Group Product Identity therefore Inverses

Let $g$ and $h$ be elements of a group $G$ whose identity element is $e$.
Then if either:
:$g h = e$
or:
:$h g = e$
it follows that:
:$g = h^{-1}$
and:
:$h = g^{-1}$

Proof:
From the Division Laws for Groups:
:$g h = e \implies g = e h^{-1} = h^{-1}$
Also by the Division Laws for Groups:
:$g h = e \implies h = g^{-1} e = g^{-1}$
{{qed}}
Theorem: Group Product Identity therefore Inverses

Let $g$ and $h$ be elements of a group $G$ whose identity element is $e$.
Then if either:
:$g h = e$
or:
:$h g = e$
it follows that:
:$g = h^{-1}$
and:
:$h = g^{-1}$

Proof:
Let $g h = e$.
Then:
{{begin-eqn}}
{{eqn | l = h
      | r = e h
      | c = {{Group-axiom|2}}
}}
{{eqn | r = \paren {g^{-1} g} h
      | c = {{Group-axiom|3}}
}}
{{eqn | r = g^{-1} \paren {g h}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = g^{-1} e
      | c = {{hypothesis}}
}}
{{eqn | r = g^{-1}
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = g
      | r = g e
      | c = {{Group-axiom|2}}
}}
{{eqn | r = g \paren {h h^{-1} }
      | c = {{Group-axiom|3}}
}}
{{eqn | r = \paren {g h} h^{-1}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e h^{-1}
      | c = {{hypothesis}}
}}
{{eqn | r = h^{-1}
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Group Product Identity therefore Inverses

Let $g$ and $h$ be elements of a group $G$ whose identity element is $e$.
Then if either:
:$g h = e$
or:
:$h g = e$
it follows that:
:$g = h^{-1}$
and:
:$h = g^{-1}$

Proof:
From the Division Laws for Groups:
:$h g = e \implies g = e h^{-1} = h^{-1}$
Also by the Division Laws for Groups:
:$h g = e \implies h = g^{-1} e = g^{-1}$
{{qed}}
Theorem: Group Product Identity therefore Inverses

Let $g$ and $h$ be elements of a group $G$ whose identity element is $e$.
Then if either:
:$g h = e$
or:
:$h g = e$
it follows that:
:$g = h^{-1}$
and:
:$h = g^{-1}$

Proof:
Let $h g = e$.
Then:
{{begin-eqn}}
{{eqn | l = g
      | r = e g
      | c = {{Group-axiom|2}}
}}
{{eqn | r = \paren {h^{-1} h} g
      | c = {{Group-axiom|3}}
}}
{{eqn | r = h^{-1} \paren {h g}
      | c = {{Group-axiom|1}}
}}
{{eqn | r = h^{-1} e
      | c = {{hypothesis}}
}}
{{eqn | r = h^{-1}
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = h
      | r = h e
      | c = {{Group-axiom|2}}
}}
{{eqn | r = h \paren {g g^{-1} }
      | c = {{Group-axiom|3}}
}}
{{eqn | r = \paren {h g} g^{-1} 
      | c = {{Group-axiom|1}}
}}
{{eqn | r = e g^{-1}
      | c = {{hypothesis}}
}}
{{eqn | r = g^{-1}
      | c = {{Group-axiom|2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Self-Inverse Elements Commute iff Product is Self-Inverse

Let $\struct {G, \circ}$ be a group.
Let $x, y \in \struct {G, \circ}$, such that $x$ and $y$ are self-inverse.
Then $x$ and $y$ commute {{iff}} $x \circ y$ is also self-inverse.

Proof:
Let the identity element of $\struct {G, \circ}$ be $e_G$.
Theorem: Power Structure of Group is Semigroup

Let $\struct {G, \circ}$ be a group.
Let $\struct {\powerset G, \circ_\PP}$ be the power structure of $\struct {G, \circ}$.
Then $\struct {\powerset G, \circ_\PP}$ is a semigroup.

Proof:
We need to prove closure and associativity.
=== Closure ===
Let $\struct {G, \circ}$ be a group, and let $A, B \subseteq G$.
{{begin-eqn}}
{{eqn | o = 
      | r = \forall a \in A, b \in B: a \circ b \in G
      | c = 
}}
{{eqn | o = \leadsto
      | r = A \circ B \subseteq G
      | c = {{Defof|Subset Product}}
}}
{{eqn | o = \leadsto
      | r = A \circ B \in \powerset G
      | c = {{Defof|Power Set}}
}}
{{end-eqn}}
Thus $\struct {\powerset G, \circ_\PP}$ is closed.
{{qed|lemma}}
=== Associativity ===
It follows from Subset Product within Semigroup is Associative that $\circ_\PP$ is associative in $\struct {\powerset G, \circ_\PP}$.
{{qed|lemma}}
Thus $\struct {\powerset G, \circ_\PP}$ is a semigroup.
{{qed}}
Theorem: Power Structure of Group is Semigroup

Let $\struct {G, \circ}$ be a group.
Let $\struct {\powerset G, \circ_\PP}$ be the power structure of $\struct {G, \circ}$.
Then $\struct {\powerset G, \circ_\PP}$ is a semigroup.

Proof:
By definition a group is also a semigroup.
The result then follows from Power Structure of Semigroup is Semigroup.
{{qed}}
Theorem: Inverse of Product of Subsets of Group

Let $\struct {G, \circ}$ be a group.
Let $X, Y \subseteq G$.
Then:
:$\paren {X \circ Y}^{-1} = Y^{-1} \circ X^{-1}$
where $X^{-1}$ is the inverse of $X$.

Proof:
First, note that:
{{begin-eqn}}
{{eqn | o = 
      | r = x \in X, y \in Y
      | c = 
}}
{{eqn | o = \leadsto
      | r = x^{-1} \in X^{-1}, y^{-1} \in Y^{-1}
      | c = {{Defof|Inverse of Subset of Group}}
}}
{{eqn | o = \leadsto
      | r = y^{-1} \circ x^{-1} \in Y^{-1} \circ X^{-1}
      | c = {{Defof|Subset Product}}
}}
{{end-eqn}}
Now:
{{begin-eqn}}
{{eqn | l = x \circ y
      | o = \in
      | r = X \circ Y
      | c = {{Defof|Subset Product}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x \circ y}^{-1}
      | o = \in
      | r = \paren {X \circ Y}^{-1}
      | c = {{Defof|Inverse of Subset of Group}}
}}
{{eqn | ll= \leadsto
      | l = y^{-1} \circ x^{-1}
      | o = \in
      | r = \paren {X \circ Y}^{-1}
      | c = Inverse of Group Product
}}
{{eqn | ll= \leadsto
      | l = Y^{-1} \circ X^{-1}
      | o = \subseteq
      | r = \paren {X \circ Y}^{-1}
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
By a similar argument we see that $\paren {X \circ Y}^{-1} \subseteq Y^{-1} \circ X^{-1}$.
Hence the result.
{{qed}}