Proof of Exponent Laws for Natural Powers in a Monoid

Throughout, $\cdot$ is associative with neutral element $e$ (Monoids (i), Associative and Commutative Binary Operations, and Neutral Elements (i), Associative and Commutative Binary Operations, and Neutral Elements (iii)), so brackets in products are dropped, and for $a\in\mathbb{N}$ the power $x^{a}$ is the iterated product of the constant function $k\mapsto x$ on $[a]$ (Powers with Exponents in the Natural Numbers with Zero (i)), while $x^{0}=e$ (Powers with Exponents in the Natural Numbers with Zero (ii)); routine facts about powers, products of constant lists and the predicative conditions behind the inductions are used without comment (Toolkit for AL1).

We first prove (i). If $a\ge1$, the recursion for iterated products (Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i)), applied to the constant function $k\mapsto x$ on $[a+1]$, gives $x^{a+1}=x^{a}x$. If $a=0$, the same clause gives $x^{1}=x$, and $x=ex=x^{0}x$.

For (ii), let first $a,b\ge1$. Splitting the iterated product of the constant function $k\mapsto x$ on $[a+b]$ after its first $a$ factors (Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (iii)) gives

$$x^{a+b}=x^{a}x^{b},$$

because the shifted function $j\mapsto x$ on $[b]$ is again constant with value $x$. If $a=0$ or $b=0$, the claim holds because $x^{0}=e$ is neutral; for instance $x^{0+b}=x^{b}=ex^{b}=x^{0}x^{b}$.

For (iii), fix $a$ and argue by induction on $b\in\mathbb{N}_{0}$ (Induction on ℕ₀ from 0 for a Condition Expressed by a Predicative Formula (ii)). For $b=0$ we have $(x^{a})^{0}=e=x^{0}=x^{a\cdot 0}$. If $(x^{a})^{b}=x^{ab}$, then

$$(x^{a})^{b+1}=(x^{a})^{b}x^{a}=x^{ab}x^{a}=x^{ab+a}=x^{a(b+1)},$$

by (i) applied to the element $x^{a}$, the induction hypothesis, and (ii).

For (iv), we induct on $a$: $e^{0}=e$, and if $e^{a}=e$, then $e^{a+1}=e^{a}e=ee=e$ by (i).

For (v), suppose $xy=yx$. We show first, by induction on $a$, that $x^{a}y=yx^{a}$. For $a=0$ both sides equal $y$, and if $x^{a}y=yx^{a}$, then by (i)

$$x^{a+1}y=x^{a}xy=x^{a}yx=yx^{a}x=yx^{a+1}.$$

Exchanging the roles of $x$ and $y$ gives likewise $y^{a}x=xy^{a}$ for every $a$. Now we induct on $a$ once more. For $a=0$, $(xy)^{0}=e=ee=x^{0}y^{0}$. If $(xy)^{a}=x^{a}y^{a}$, then

$$(xy)^{a+1}=(xy)^{a}xy=x^{a}y^{a}xy=x^{a}xy^{a}y=x^{a+1}y^{a+1},$$

by (i), the induction hypothesis and $y^{a}x=xy^{a}$.

For (vi), let $x$ be a unit with inverse $x^{-1}$. Since $xx^{-1}=e=x^{-1}x$ (Units of a Monoid (i)), the elements $x$ and $x^{-1}$ commute, so (v) and (iv) give

$$x^{a}(x^{-1})^{a}=(xx^{-1})^{a}=e^{a}=e,\qquad (x^{-1})^{a}x^{a}=(x^{-1}x)^{a}=e^{a}=e.$$

Hence $x^{a}$ is a unit and $(x^{-1})^{a}$ is an inverse of it (Units of a Monoid (i)). Since a unit has only one inverse (Units of a Monoid: Unique Inverses, Products, and the Group of Units (i)), $(x^{a})^{-1}=(x^{-1})^{a}$.