Proof of Subgroup Criterion and Basic Examples

Throughout, $\cdot$ is associative with neutral element $e$ (Groups and Abelian Groups (i), Monoids (i)), and routine facts about nonempty classes and restrictions of binary operations are used without comment (Toolkit for AL1).

We begin with the "only if" part of (i). If $H\le G$, then $e\in H$, so $H\neq\emptyset$; and for $g,h\in H$ also $h^{-1}\in H$, hence $gh^{-1}\in H$ (Subgroups (i)).

For the "if" part, suppose that $H\neq\emptyset$ and that $gh^{-1}\in H$ for all $g,h\in H$. Choose $g\in H$; the hypothesis for the pair $g,g$ gives $e=gg^{-1}\in H$ (Uniqueness of the Identity Element and of Inverses in a Group (ii)). Next, for $h\in H$, the hypothesis for the pair $e,h$ gives $h^{-1}=eh^{-1}\in H$. Finally, for $g,h\in H$ we now know that $h^{-1}\in H$, and the hypothesis for the pair $g,h^{-1}$ gives

$$gh=g(h^{-1})^{-1}\in H,$$

since $(h^{-1})^{-1}=h$ by Cancellation Laws and Basic Inverse Identities in a Group (iii). So $H\le G$ by Subgroups (i).

For (ii), let $H\le G$ and let $\cdot'$ be the restriction of $\cdot$ to $H\times H$. It is a function on $H\times H$ with the same values as $\cdot$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix)), and these values lie in $H$ because $H$ is closed under products (Subgroups (i)); so $\cdot'$ is a binary operation on $H$ (Binary Operations on a Set (i)), associative because $\cdot$ is (Semigroups (i)). Since $e\in H$ is neutral for $\cdot$, it is neutral for $\cdot'$, and $(H,\cdot')$ is a monoid with identity $e$ (Monoids (i)). Each $h\in H$ has $h^{-1}\in H$, and

$$h\cdot'h^{-1}=h^{-1}\cdot'h=e$$

(Uniqueness of the Identity Element and of Inverses in a Group (ii)), so $h$ is a unit of $(H,\cdot')$ (Units of a Monoid (i)). Hence $(H,\cdot')$ is a group (Groups and Abelian Groups (i)), and by Uniqueness of the Identity Element and of Inverses in a Group (ii), applied to this group, the inverse of $h$ in it is $h^{-1}$.

For (iii), the set $\bigcap\mathcal{S}$ is a subset of $G$, and it contains $e$, which lies in every subgroup $K\in\mathcal{S}$; so it is nonempty. If $g,h\in\bigcap\mathcal{S}$, then $gh^{-1}\in K$ for every $K\in\mathcal{S}$ by the "only if" part of (i), so $gh^{-1}\in\bigcap\mathcal{S}$. The "if" part of (i) now shows that $\bigcap\mathcal{S}$ is a subgroup of $G$.

For (iv), the subset $\{e\}$ contains $e$, is closed under products since $ee=e$, and is closed under inverses since $e^{-1}=e$ (Cancellation Laws and Basic Inverse Identities in a Group (ii)); so it is a subgroup by Subgroups (i). The whole group $G$ satisfies the three conditions of Subgroups (i) trivially.