Proof of Sums over Finite Sets in a Commutative Ring and in an Ordered Field: Distributivity, Products of Sums, Vanishing Terms, Sums over Pairs, Expanding Products of Sums, Counting, Comparison, Monotonicity and the Triangle Inequality

By Commutative Rings §ring, the addition of $R$ is associative and commutative, and $0$ is a neutral element, since $x+0=x$ and $0+x=x+0$; so Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals applies to it. Two rules of $R$ are used. For $c\in R$, $c\cdot0=0$: by Commutative Rings §ring, $c\cdot0=c\cdot(0+0)=c\cdot0+c\cdot0$, and adding $-(c\cdot0)$ to both sides gives $0=c\cdot0$. For $x,y\in R$, $-0=0$ and $-(x+y)=(-x)+(-y)$: indeed $0+0=0$ and $(x+y)+\big((-x)+(-y)\big)=\big(x+(-x)\big)+\big(y+(-y)\big)=0$, and the negative is unique by Negatives, Differences, Reciprocals and Quotients §negative.

Distributive. The map $x\mapsto c\,x$ on $R$ sends $0$ to $0$ and satisfies $c(x+y)=c\,x+c\,y$ by Commutative Rings §ring. Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §homomorphism, with both operations the addition of $R$, gives $c\sum_{x\in A}f(x)=\sum_{x\in A}c\,f(x)$.

Difference. By the rules above, the map $x\mapsto-x$ on $R$ sends $0$ to $0$ and sums to sums, so $\sum_{x\in A}\big(-g(x)\big)=-\sum_{x\in A}g(x)$ by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §homomorphism. As $f(x)-g(x)=f(x)+(-g(x))$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §termwise gives

$$\sum_{x\in A}\big(f(x)-g(x)\big)=\sum_{x\in A}f(x)+\sum_{x\in A}\big(-g(x)\big)=\sum_{x\in A}f(x)-\sum_{x\in A}g(x).$$

Product of sums. Let $t=\sum_{y\in B}h(y)$. By the distributive clause and commutativity of multiplication, $\Big(\sum_{x\in A}f(x)\Big)t=t\sum_{x\in A}f(x)=\sum_{x\in A}t\,f(x)=\sum_{x\in A}f(x)\,t$, and for each $x\in A$, again by the distributive clause, $f(x)\,t=\sum_{y\in B}f(x)\,h(y)$. Hence, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §product applied to the map $(x,y)\mapsto f(x)\,h(y)$ on $A\times B$,

$$\Big(\sum_{x\in A}f(x)\Big)\Big(\sum_{y\in B}h(y)\Big)=\sum_{x\in A}\Big(\sum_{y\in B}f(x)\,h(y)\Big)=\sum_{(x,y)\in A\times B}f(x)\,h(y).$$

Vanishing. First, $\sum_{x\in D}0=0$ for every finite set $D$: by the distributive clause, applied with $D$ in place of $A$ and $c=0$, and by the rule $c\cdot0=0$ together with commutativity of multiplication, $\sum_{x\in D}0=\sum_{x\in D}0\cdot0=0\cdot\sum_{x\in D}0=0$. Now let $E\subseteq A$ with $f(x)=0$ for every $x\in A\setminus E$. The sets $E$ and $A\setminus E$ are finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §subset, disjoint, and their union is $A$. By Sums and Products over a Finite Set and over an Interval §subsets the sum $\sum_{x\in A\setminus E}f(x)$ is that of $f|_{A\setminus E}$, which is the zero map on $A\setminus E$, so it is $0$. Hence Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union gives

$$\sum_{x\in A}f(x)=\sum_{x\in E}f(x)+\sum_{x\in A\setminus E}f(x)=\sum_{x\in E}f(x)+0=\sum_{x\in E}f(x).$$

In particular, if $y\in A$ and $f(x)=0$ for every $x\in A$ with $x\neq y$, then $E=\{y\}$ is allowed, and $\sum_{x\in\{y\}}f(x)=f(y)$ by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §singleton.

Inductions over subsets of $A$. The next two clauses are proved by induction on $n$ in the following form: a claim about the subsets $S$ of $A$ that admit a bijection $\chi:[n]\to S$ is checked for $n=0$ and shown to pass from $n$ to $n+1$ for each $n\in\mathbb{N}_{0}$. The class of $n\in\mathbb{N}$ for which it holds then contains $1=0+1$ and is closed under $n\mapsto n+1$, so it is $\mathbb{N}$ by Arithmetic and Order of the Natural Numbers §induction, and the claim holds for every $n\in\mathbb{N}_{0}=\mathbb{N}\cup\{0\}$ by The Natural Numbers with Zero and Their Embedding into the Integers §naturals. Since $A$ is finite, it admits a bijection from some $[n]$ onto $A$ by Finite Sets §finite, so the claim holds for $S=A$. For $n=0$ we have $S=\chi(\emptyset)=\emptyset$. In the step, let $\chi:[n+1]\to S$ be a bijection, $a=\chi(n+1)$ and $S'=\chi([n])$. Since $[n+1]=[n]\cup\{n+1\}$ with $n+1\notin[n]$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §successor and $\chi$ is injective, $S=S'\cup\{a\}$ with $a\notin S'$, and $\chi|_{[n]}$ is a bijection $[n]\to S'\subseteq A$, to which the induction hypothesis applies. For $x\in A$ let $v(x)=\sum_{y\in B_{x}}u(x,y)$, the sum of the map $y\mapsto u(x,y)$ on $B_{x}$, which is defined because $B_{x}\subseteq U$ by Indexed Families of Sets and Their Union, Intersection and Product §union, so that $(x,y)\in T$ for $y\in B_{x}$.

Dependent pairs. For $S\subseteq A$ let $T_{S}=\{(x,y)\in T:x\in S\}$, a subset of $T$ and hence finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §subset; then $T_{A}=T$. We prove by induction over subsets of $A$, as just described, that $\sum_{x\in S}v(x)=\sum_{(x,y)\in T_{S}}u(x,y)$. For $S=\emptyset$, also $T_{S}=\emptyset$, and both sides are $0$ by Sums and Products over a Finite Set and over an Interval §empty. In the step, an element $(x,y)$ of $T$ lies in $T_{S}$ exactly when $x\in S'$ or $x=a$, and $(a,y)\in T$ exactly when $y\in B_{a}$, since $B_{a}\subseteq U$. So $T_{S}$ is the union of $T_{S'}$ and $\{a\}\times B_{a}$, both subsets of $T$ and hence finite, and these are disjoint as $a\notin S'$. The map $y\mapsto(a,y)$ is a bijection from $B_{a}$ onto $\{a\}\times B_{a}$, with inverse $(a,y)\mapsto y$. Hence Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §singleton, the induction hypothesis, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §reindexing along this bijection, and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union once more give

$$\begin{aligned} \sum_{x\in S}v(x)&=\sum_{x\in S'}v(x)+v(a)=\sum_{(x,y)\in T_{S'}}u(x,y)+\sum_{y\in B_{a}}u(a,y)\\ &=\sum_{(x,y)\in T_{S'}}u(x,y)+\sum_{(x,y)\in\{a\}\times B_{a}}u(x,y)=\sum_{(x,y)\in T_{S}}u(x,y). \end{aligned}$$

For $S=A$ this is the dependent-pairs clause.

Distributivity. By Commutative Rings §ring, multiplication on $R$ is associative and commutative with neutral element $1$, so Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals applies to products as well. For $S\subseteq A$ let $P_{S}$ be the set of maps $\varphi:S\to U$ with $\varphi(x)\in B_{x}$ for every $x\in S$. It is a subset of $U^{S}$, hence finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §maps and Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §subset, and $P_{A}=P$. We prove by induction over subsets of $A$ that

$$\prod_{x\in S}v(x)=\sum_{\varphi\in P_{S}}\prod_{x\in S}u(x,\varphi(x)).$$

For $S=\emptyset$: a map with domain $\emptyset$ has no values, so every such map equals $\mathrm{id}_{\emptyset}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, and $\mathrm{id}_{\emptyset}\in P_{\emptyset}$, the condition on values being vacuous; so $P_{\emptyset}=\{\mathrm{id}_{\emptyset}\}$. The left side is the empty product $1$ by Sums and Products over a Finite Set and over an Interval §empty, and the right side is, by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §singleton, the single term $\prod_{x\in\emptyset}u(x,\mathrm{id}_{\emptyset}(x))=1$. In the step, for $\psi\in P_{S'}$ and $b\in B_{a}$ let $\theta(\psi,b):S\to U$ be the map with $\theta(\psi,b)(x)=\psi(x)$ for $x\in S'$ and $\theta(\psi,b)(a)=b$; it is well defined because $a\notin S'$, and it lies in $P_{S}$. The map $\theta:P_{S'}\times B_{a}\to P_{S}$ and the map $P_{S}\to P_{S'}\times B_{a}$ given by $\varphi\mapsto(\varphi|_{S'},\varphi(a))$ compose to the identities in both orders, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction and Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality (as $S=S'\cup\{a\}$), so $\theta$ is a bijection by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse-criterion. For $\psi\in P_{S'}$ and $b\in B_{a}$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §singleton for products give

$$\prod_{x\in S}u\big(x,\theta(\psi,b)(x)\big)=\Big(\prod_{x\in S'}u(x,\psi(x))\Big)\,u(a,b).$$

Using the same two rules for $v$, then the induction hypothesis, then the product-of-sums clause applied with the finite sets $P_{S'}$ and $B_{a}$ in place of $A$ and $B$, then the last display, and finally Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §reindexing along $\theta$, we get

$$\begin{aligned} \prod_{x\in S}v(x)&=\Big(\prod_{x\in S'}v(x)\Big)\,v(a)=\Big(\sum_{\psi\in P_{S'}}\prod_{x\in S'}u(x,\psi(x))\Big)\Big(\sum_{b\in B_{a}}u(a,b)\Big)\\ &=\sum_{(\psi,b)\in P_{S'}\times B_{a}}\Big(\prod_{x\in S'}u(x,\psi(x))\Big)\,u(a,b)=\sum_{(\psi,b)\in P_{S'}\times B_{a}}\prod_{x\in S}u\big(x,\theta(\psi,b)(x)\big)\\ &=\sum_{\varphi\in P_{S}}\prod_{x\in S}u(x,\varphi(x)). \end{aligned}$$

For $S=A$ this is the distributivity clause.

For the remaining clauses, the ordered field $F$ is by definition a field, and hence a commutative ring by Fields §field, so the above applies in $F$. If $A\neq\emptyset$, let $n=\#A$, which lies in $\mathbb{N}$ by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and fix a bijection $\varphi$ from $[n]$ onto $A$; by Sums and Products over a Finite Set and over an Interval §operation, $\sum_{x\in A}w(x)=\sum_{k=1}^{n}w(\varphi(k))$ for every $w:A\to F$. If $A=\emptyset$, every sum over $A$ is $0$ by Sums and Products over a Finite Set and over an Interval §empty, and $\#A=0$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §empty.

Constant. If $A=\emptyset$, both sides are $0$, since $0\cdot c=0$ by Rules of Arithmetic and Order in an Ordered Field §zero. Otherwise $\sum_{x\in A}c=\sum_{k=1}^{n}c=n\,c$ by Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §constant. For $c=1$, $\#A\cdot1=\#A$ by Commutative Rings §ring.

Comparison. If $A=\emptyset$, both sides are $0$. Otherwise apply the first part of Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §comparison to $k\mapsto f(\varphi(k))$ and $k\mapsto g(\varphi(k))$, which satisfy $f(\varphi(k))\le g(\varphi(k))$ for every $k\in[n]$.

Monotone. Let $D\subseteq A$; it is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §subset. The comparison clause for $D$, the zero map and $f|_{D}$, together with the constant clause, which gives $\sum_{x\in D}0=\#D\cdot0=0$ by the rule $c\cdot0=0$ proved above, yields $0\le\sum_{x\in D}f(x)$. This applies to $D=S$ and to $D=A\setminus S$. Since $A$ is the union of the disjoint sets $S$ and $A\setminus S$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union and Rules of Arithmetic and Order in an Ordered Field §order-sum give

$$0\le\sum_{x\in S}f(x)=\sum_{x\in S}f(x)+0\le\sum_{x\in S}f(x)+\sum_{x\in A\setminus S}f(x)=\sum_{x\in A}f(x).$$

In particular, for $y\in A$ the subset $\{y\}$ of $A$ gives $f(y)=\sum_{x\in\{y\}}f(x)\le\sum_{x\in A}f(x)$ by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §singleton.

Triangle. If $A=\emptyset$, the left side is $|0|=0$ by Rules of Arithmetic and Order in an Ordered Field §absolute-value and the right side is $0$. Otherwise Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §triangle, applied to $k\mapsto f(\varphi(k))$, gives

$$\Big|\sum_{x\in A}f(x)\Big|=\Big|\sum_{k=1}^{n}f(\varphi(k))\Big|\le\sum_{k=1}^{n}|f(\varphi(k))|=\sum_{x\in A}|f(x)|.$$

Zero sum. Let $f(x)\ge0$ for every $x\in A$ and $\sum_{x\in A}f(x)=0$, and let $y\in A$. The monotone clause gives $0\le f(y)\le\sum_{x\in A}f(x)=0$, so $f(y)=0$, because the order of $F$ is a partial order by Ordered Fields §ordered-field and hence antisymmetric.