Proof of Iterated Operations over an Interval: Extracting One Term and Reversing the Order

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Interval notation and iterated operations. For $p\in\mathbb{N}$, $\{1,\dots,p\}=[p]$ by Intervals of Natural Numbers §segment, and for a map $b$ from a set containing $[p]$ to $X$, the iterated operation $\mathop{\ast}\limits_{k=1}^{p}b_{k}$ of Sums and Products over a Finite Set and over an Interval §intervals agrees, as stated there for $1\le p$, with that of Iterated Operations: Finite Sums and Finite Products §iterated and Iterated Operations: Finite Sums and Finite Products §restriction; here $1\le p$ by Arithmetic and Order of the Natural Numbers §least. So for intervals $[p]$ with $p\in\mathbb{N}$ we may use Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms, whose hypotheses on $\ast$ (associative and commutative) hold here.

Clause extraction. Let $n$, $j$, $g_{j}$ and $a$ be as in the clause; by Bijections between Intervals: the Gap Map and the Reversal §gap, applied to $n$ and $j$, $g_{j}$ is a bijection from $[n]$ onto $[n+1]\setminus\{j\}$. By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, $n\in\mathbb{N}$ or $n=0$.

Case $n=0$. Then $n+1=0+1=1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero. Further, $\ast$ has a neutral element, by the hypothesis of the clause; let $e$ be one (it is unique by A Binary Operation Has at Most One Neutral Element §unique). By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, $[1]=\{1\}$ and $[0]=\emptyset$; so $j=1$, as $j\in[n+1]=[1]$. The left side is $\mathop{\ast}\limits_{k=1}^{1}a_{k}=a_{1}$, by the agreement above with $p=1$ and Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion (its first identity, applied to $n=1$ and $a$). On the right, $\{1,\dots,0\}=[0]=\emptyset$, so by Sums and Products over a Finite Set and over an Interval §intervals and Sums and Products over a Finite Set and over an Interval §empty, $\mathop{\ast}\limits_{k=1}^{0}a_{g_{1}(k)}=e$, and $e\ast a_{1}=a_{1}$ by Associative and Commutative Binary Operations, and Neutral Elements §neutral. Both sides equal $a_{1}=a_{j}$.

Case $n\in\mathbb{N}$. 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]$; and for $k\in[n+1]$, $k\in[n]$ if and only if $k\le n$, by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment. Define $\sigma:[n+1]\to[n+1]$ by Maps Defined by Cases §cases, applied to $A=B=[n+1]$, the property $P(k)$: $k\le n$, and the expressions $t_{1}(k)=g_{j}(k)$ and $t_{2}(k)=j$: for $k\in[n+1]$ with $k\le n$, $k\in[n]$, so $g_{j}(k)$ is defined and lies in $[n+1]\setminus\{j\}\subseteq[n+1]$; and $j\in[n+1]$. Thus $\sigma(k)=g_{j}(k)$ for $k\in[n]$, and $\sigma(n+1)=j$, since $n+1\notin[n]$; every $k\in[n+1]$ is in $[n]$ or equals $n+1$.

$\sigma$ is a bijection. Injective: let $k,k'\in[n+1]$ with $\sigma(k)=\sigma(k')$. If $k,k'\in[n]$, then $g_{j}(k)=g_{j}(k')$, so $k=k'$ as $g_{j}$ is injective. If $k\in[n]$ and $k'=n+1$, then $\sigma(k)=g_{j}(k)\in[n+1]\setminus\{j\}$ while $\sigma(k')=j$, which is impossible; likewise with $k$ and $k'$ exchanged. If $k=k'=n+1$ there is nothing to show. Surjective: $j=\sigma(n+1)$, and each $m\in[n+1]$ with $m\neq j$ lies in $[n+1]\setminus\{j\}$, so $m=g_{j}(k)=\sigma(k)$ for some $k\in[n]$, as $g_{j}$ is surjective. So $\sigma$ is bijective by Injective, Surjective and Bijective Functions between Classes §bijective.

Let $b:[n+1]\to X$ be the map $k\mapsto a_{\sigma(k)}$ of Sets and Maps: Ordinary Notation §maps. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $b|_{[n]}$ is a map on $[n]$, since $[n]\subseteq[n+1]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor, with value $b_{k}=a_{\sigma(k)}=a_{g_{j}(k)}$ at each $k\in[n]$, so $b|_{[n]}$ is the map $k\mapsto a_{g_{j}(k)}$ on $[n]$, by the uniqueness in Sets and Maps: Ordinary Notation §maps. Now $n+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §closed. By Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §reordering, applied to $n+1$ in place of $n$, the map $a$ and the bijection $\sigma$, and then by Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §recursion (its second identity), applied to $n$ and the map $b$,

$$\mathop{\ast}\limits_{k=1}^{n+1}a_{k}=\mathop{\ast}\limits_{k=1}^{n+1}a_{\sigma(k)}=\Big(\mathop{\ast}\limits_{k=1}^{n}b_{k}\Big)\ast b_{n+1}=\Big(\mathop{\ast}\limits_{k=1}^{n}a_{g_{j}(k)}\Big)\ast a_{j},$$

where the last step uses that $\mathop{\ast}\limits_{k=1}^{n}b_{k}$ is the iterated operation of $b|_{[n]}$ by Iterated Operations: Finite Sums and Finite Products §restriction, that is, of $k\mapsto a_{g_{j}(k)}$, and $b_{n+1}=a_{\sigma(n+1)}=a_{j}$. All three iterated operations are over $[n+1]$ or $[n]$ with $n,n+1\in\mathbb{N}$, so by the agreement above they are those of the clause.

Clause reversal. Let $N\in\mathbb{N}$ and $a:[N]\to X$. By Bijections between Intervals: the Gap Map and the Reversal §reversal, applied to $N$, the map $\rho:[N]\to[N]$, $\rho(k)=N+1-k$, is a bijection. By Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms §reordering, applied to $N$ in place of $n$, the map $a$ and the bijection $\sigma=\rho$,

$$\mathop{\ast}\limits_{k=1}^{N}a_{N+1-k}=\mathop{\ast}\limits_{k=1}^{N}a_{\rho(k)}=\mathop{\ast}\limits_{k=1}^{N}a_{k},$$

and by the agreement above, with $p=N$, these are the iterated operations of the clause.