Proof of Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals

Throughout, for a finite set $C$ and a map $u:C\to X$ we use Sums and Products over a Finite Set and over an Interval §operation and Sums and Products over a Finite Set and over an Interval §empty as follows: if $C=\emptyset$, then $\mathop{\ast}\limits_{x\in C}u(x)=e$; if $C\neq\emptyset$, then $\#C\in\mathbb{N}$ by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and $\mathop{\ast}\limits_{x\in C}u(x)=\mathop{\ast}\limits_{k=1}^{\#C}u(\gamma(k))$ for every bijection $\gamma$ from $[\#C]$ onto $C$. If there is a bijection from $[n]$ onto $C$ with $n\in\mathbb{N}_{0}$, then $n=\#C$ by The Number of Elements of a Finite Set §cardinality. For $u$ defined on a set containing $C$, the iterated operation over $C$ is that of $u|_{C}$ by Sums and Products over a Finite Set and over an Interval §subsets, and $u|_{C}$ has the same values as $u$ on $C$; we use this without comment. Finally $e\ast x=x\ast e=x$ for every $x\in X$ by Associative and Commutative Binary Operations, and Neutral Elements §neutral.

Singleton. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[1]=\{1\}$, so $\gamma:[1]\to\{y\}$, $1\mapsto y$, is a bijection and $\#\{y\}=1$. By Iterated Operations: Finite Sums and Finite Products §iterated, $\mathop{\ast}\limits_{k=1}^{1}f(\gamma(k))=s(1)$ for the map $s$ of Iterating a Binary Operation along a Finite List §existence belonging to $k\mapsto f(\gamma(k))$, and $s(1)=f(\gamma(1))$. Hence $\mathop{\ast}\limits_{x\in\{y\}}f(x)=f(\gamma(1))=f(y)$.

Disjoint union. If $A=\emptyset$, then $A\cup B=B$, and the right side is $e\ast\mathop{\ast}\limits_{x\in B}f(x)=\mathop{\ast}\limits_{x\in B}f(x)$, which is the left side; the case $B=\emptyset$ is symmetric. Let $A$ and $B$ be nonempty, $p=\#A$ and $q=\#B$, so $p,q\in\mathbb{N}$, and let $\alpha$ and $\beta$ be bijections from $[p]$ onto $A$ and from $[q]$ onto $B$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split with $m=1$, $n=p$ and $q$ in place of $p$, $[p+q]$ is the union of the disjoint sets $[p]$ and $\{p+1,\dots,p+q\}$, and by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift with $m=1$, $n=q$ every element of the latter is $p+j$ for exactly one $j\in[q]$. Define $\gamma:[p+q]\to A\cup B$ by $\gamma(k)=\alpha(k)$ for $k\in[p]$ and $\gamma(p+j)=\beta(j)$ for $j\in[q]$. Then $\gamma$ maps $[p]$ bijectively onto $A$ and $\{p+1,\dots,p+q\}$ bijectively onto $B$. Since $A\cap B=\emptyset$, two elements of $[p+q]$ with the same image lie in the same one of these two pieces, so $\gamma$ is injective; it is evidently surjective. Thus $\gamma$ is a bijection from $[p+q]$ onto $A\cup B$, and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §splitting, applied to $k\mapsto f(\gamma(k))$, gives

$$\mathop{\ast}\limits_{x\in A\cup B}f(x)=\mathop{\ast}\limits_{k=1}^{p+q}f(\gamma(k))=\Big(\mathop{\ast}\limits_{k=1}^{p}f(\alpha(k))\Big)\ast\Big(\mathop{\ast}\limits_{j=1}^{q}f(\beta(j))\Big)=\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)\ast\Big(\mathop{\ast}\limits_{x\in B}f(x)\Big).$$

Reindexing. If $B=\emptyset$, then $A=g(B)=\emptyset$, and both sides are $e$. Let $B\neq\emptyset$, $n=\#B$, and let $\beta$ be a bijection from $[n]$ onto $B$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §preservation, $g\circ\beta$ is a bijection from $[n]$ onto $A$, so $A\neq\emptyset$ and $\#A=n$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §composition,

$$\mathop{\ast}\limits_{y\in B}f(g(y))=\mathop{\ast}\limits_{k=1}^{n}f(g(\beta(k)))=\mathop{\ast}\limits_{k=1}^{n}f\big((g\circ\beta)(k)\big)=\mathop{\ast}\limits_{x\in A}f(x).$$

Product. First let $A=\{a\}$ be a singleton. The map $y\mapsto(a,y)$ from $B$ to $\{a\}\times B$ and the map $(a,y)\mapsto y$ back are inverse to each other, so the former is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion. Reindexing along it and the singleton clause give

$$\mathop{\ast}\limits_{(x,y)\in\{a\}\times B}f(x,y)=\mathop{\ast}\limits_{y\in B}f(a,y)=\mathop{\ast}\limits_{x\in\{a\}}\Big(\mathop{\ast}\limits_{y\in B}f(x,y)\Big).\qquad(1)$$

We prove the first equality of the clause. If $A=\emptyset$, then $A\times B=\emptyset$ and both sides are $e$. We prove the first equality for nonempty $A$ by induction on $n=\#A$ (Arithmetic and Order of the Natural Numbers §induction), for all finite $A$ with $\#A=n$ and all $f$; here $n\in\mathbb{N}$. If $\#A=1$, a bijection from $[1]=\{1\}$ onto $A$ shows that $A$ is a singleton, so the claim holds by (1). Suppose it holds for $n$, let $\#A=n+1$, and let $\alpha$ be a bijection from $[n+1]$ onto $A$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, $[n+1]=[n]\cup\{n+1\}$ and $n+1\notin[n]$. Put $A'=\alpha([n])$ and $a=\alpha(n+1)$. Then $A=A'\cup\{a\}$, $a\notin A'$ as $\alpha$ is injective, and $\alpha|_{[n]}$ is a bijection from $[n]$ onto $A'$, so $\#A'=n$. Hence $A\times B$ is the union of the disjoint sets $A'\times B$ and $\{a\}\times B$. The disjoint-union clause, the induction hypothesis for $A'$ and $f|_{A'\times B}$, (1), and the disjoint-union clause for $A=A'\cup\{a\}$ and the map $x\mapsto\mathop{\ast}\limits_{y\in B}f(x,y)$ give

$$\mathop{\ast}\limits_{(x,y)\in A\times B}f(x,y)=\Big(\mathop{\ast}\limits_{x\in A'}\mathop{\ast}\limits_{y\in B}f(x,y)\Big)\ast\Big(\mathop{\ast}\limits_{x\in\{a\}}\mathop{\ast}\limits_{y\in B}f(x,y)\Big)=\mathop{\ast}\limits_{x\in A}\Big(\mathop{\ast}\limits_{y\in B}f(x,y)\Big).$$

So the claim holds for $n+1$. This proves the first equality for every finite $A$.

For the second equality, the map $\tau:B\times A\to A\times B$, $(y,x)\mapsto(x,y)$, is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion, the corresponding map $A\times B\to B\times A$ being its inverse. Reindexing along $\tau$, and then the first equality with the roles of $A$ and $B$ exchanged, applied to $f\circ\tau$, give

$$\mathop{\ast}\limits_{(x,y)\in A\times B}f(x,y)=\mathop{\ast}\limits_{(y,x)\in B\times A}f(x,y)=\mathop{\ast}\limits_{y\in B}\Big(\mathop{\ast}\limits_{x\in A}f(x,y)\Big).$$

Termwise. If $A=\emptyset$, both sides are $e=e\ast e$. Otherwise, with $n=\#A$ and a bijection $\gamma$ from $[n]$ onto $A$, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §termwise applied to $k\mapsto f(\gamma(k))$ and $k\mapsto g(\gamma(k))$ gives

$$\mathop{\ast}\limits_{x\in A}\big(f(x)\ast g(x)\big)=\mathop{\ast}\limits_{k=1}^{n}\big(f(\gamma(k))\ast g(\gamma(k))\big)=\Big(\mathop{\ast}\limits_{k=1}^{n}f(\gamma(k))\Big)\ast\Big(\mathop{\ast}\limits_{k=1}^{n}g(\gamma(k))\Big)=\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)\ast\Big(\mathop{\ast}\limits_{x\in A}g(x)\Big).$$

Homomorphism. If $A=\emptyset$, the left side is $\varphi(e)=e'$, which is the right side. Otherwise, with $n=\#A$ and a bijection $\gamma$ from $[n]$ onto $A$, used for both $\ast$ and $\diamond$, Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §homomorphism gives

$$\varphi\Big(\mathop{\ast}\limits_{x\in A}f(x)\Big)=\varphi\Big(\mathop{\ast}\limits_{k=1}^{n}f(\gamma(k))\Big)=\mathop{\diamond}\limits_{k=1}^{n}\varphi(f(\gamma(k)))=\mathop{\diamond}\limits_{x\in A}\varphi(f(x)).$$

Interval recursion. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §split with $p=1$, $\{m,\dots,n+1\}$ is the union of the disjoint sets $\{m,\dots,n\}$ and $\{n+1,\dots,n+1\}=\{n+1\}$. By Sums and Products over a Finite Set and over an Interval §intervals and the disjoint-union and singleton clauses,

$$\mathop{\ast}\limits_{k=m}^{n+1}a_{k}=\Big(\mathop{\ast}\limits_{k\in\{m,\dots,n\}}a_{k}\Big)\ast\Big(\mathop{\ast}\limits_{k\in\{n+1\}}a_{k}\Big)=\Big(\mathop{\ast}\limits_{k=m}^{n}a_{k}\Big)\ast a_{n+1}.$$

Interval shift. Let $I=\{m,\dots,n\}$ and $J=\{m+p,\dots,n+p\}$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift, $s:I\to J$, $k\mapsto k+p$, is a bijection, so every $j\in J$ is $i+p$ for exactly one $i\in I$, and then $j-p=i\in I$. Hence $b:J\to X$, $b(j)=a_{j-p}$, is a map, and $b(s(k))=a_{(k+p)-p}=a_{k}$ for every $k\in I$. By Sums and Products over a Finite Set and over an Interval §intervals and the reindexing clause applied to $s$ and $b$,

$$\mathop{\ast}\limits_{k=m}^{n}a_{k}=\mathop{\ast}\limits_{k\in I}b(s(k))=\mathop{\ast}\limits_{j\in J}b(j)=\mathop{\ast}\limits_{k=m+p}^{n+p}a_{k-p}.$$