I'm worried that my answer to this exercise from Artin's book is trying too hard to balance avoiding verbosity with avoiding circularity. The exercise is:
Let $S$ be a set with an associative law of composition and with an identity element. Prove that the subset consisting of the invertible elements in $S$ is a group.
The result is clear, but each of the verifications is hard to do precisely. For example, every element of $S$ has an inverse in $S$, but I need to check that that inverse actually is invertible. The check for closure is analogous. I want to say that the identity element and associativity are inherited, but I can't do that unless I verify that I actually have a valid law of composition on the subset, and I'm trying to do that without making the argument circular and using associativity. I suppose I can do this, as long as I make clear that I'm performing the computation in $S$.
I'm trying to balance rigor with elegance, and I think I'm much worse at the latter, so I would appreciate some feedback. Here is my attempt.
Let $S^{\times}$ denote the set of invertible elements of $S$. I claim that $S^{\times}$ is a group. We first check that $S^{\times}$ is closed. Let $a,b \in S^{\times}$. We will show that $ab \in S^{\times}$. Thus, $a$ and $b$ are invertible in $S$, so there exist $a^{-1}, b^{-1} \in S$ such that $aa^{-1} = e$ and $bb^{-1} = e$ in $S$. But $(a^{-1})^{-1} = a$ and $(b^{-1})^{-1} = b$, so $a^{-1}, b^{-1} \in S^{\times}$. Furthermore, $b^{-1} a^{-1} \in S$. Performing the computation in $S$ and using associativity, we have $$ (ab)(b^{-1} a^{-1}) = (a(bb^{-1}))a^{-1} = (ae)a^{-1} = aa^{-1} = e $$ and $$ (b^{-1} a^{-1})(ab) = (b^{-1} (a^{-1} a))b = (b^{-1} e)b = b^{-1} b = e. $$ So $ab$ is invertible in $S$, with inverse $b^{-1} a^{-1}$, so $ab \in S^{\times}$. But $(b^{-1} a^{-1})^{-1} = ab$, so $b^{-1} a^{-1} \in S^{\times}$, so $ab$ admits an inverse in $S^{\times}$. Therefore, $S^{\times}$ has a well-defined law of composition, namely the restriction of the law on $S$. Associativity is immediately inherited from $S$. Notice that $ee = e$ by definition, so $e = e^{-1} \in S^{\times}$. We've already checked inverses. If $a \in S^{\times}$, then $a^{-1} \in S$, but $(a^{-1})^{-1} = a$, so $a^{-1} \in S^{\times}$, so $S^{\times}$ is a group.
I think I've managed to check all of the axioms without making any circular arguments, but the argument is incredibly messy. I'd appreciate any advice on how to improve this proof.