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

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

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}$, so that it holds for every $n\in\mathbb{N}_{0}$ by induction from $0$ on $\mathbb{N}_{0}$, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction. 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 $[0]=\emptyset$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §segment, so $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, let $\rho':P_{S}\to P_{S'}\times B_{a}$ be the map $\varphi\mapsto(\varphi|_{S'},\varphi(a))$. Its values lie in $P_{S'}\times B_{a}$: for $\varphi\in P_{S}$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction the restriction $\varphi|_{S'}$ is a function with domain $S'\cap S=S'$ and values $\varphi|_{S'}(x)=\varphi(x)\in B_{x}\subseteq U$ for $x\in S'$ (Indexed Families of Sets and Their Union, Intersection and Product §union), so it is a map $S'\to U$ by Functions, Values of a Function, and Functions from One Class to Another §map and lies in $P_{S'}$; and $\varphi(a)\in B_{a}$ since $a\in S$; hence $(\varphi|_{S'},\varphi(a))\in P_{S'}\times B_{a}$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership. So $\rho'$ is a map by Maps and Relations Given by Formulas §map, applied with the sets $P_{S}$ and $P_{S'}\times B_{a}$, the latter a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set.

$\rho'$ is injective. Let $\varphi,\varphi'\in P_{S}$ with $\rho'(\varphi)=\rho'(\varphi')$. By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, $\varphi|_{S'}=\varphi'|_{S'}$ and $\varphi(a)=\varphi'(a)$. For $x\in S'$, Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction gives $\varphi(x)=\varphi|_{S'}(x)=\varphi'|_{S'}(x)=\varphi'(x)$. As $S=S'\cup\{a\}$, the functions $\varphi$ and $\varphi'$ have the common domain $S$ and the same value at each of its elements, so $\varphi=\varphi'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. Thus $\rho'$ is injective.

$\rho'$ is surjective. By The Cartesian Product of Two Classes §product and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, every element of $P_{S'}\times B_{a}$ is a pair $(\psi,b)$ with $\psi\in P_{S'}$ and $b\in B_{a}$. For such $\psi$ and $b$, Maps Defined by Cases §cases, applied with $P(x)$ the property $x\in S'$, gives a map $\theta_{\psi,b}:S\to U$ with $\theta_{\psi,b}(x)=\psi(x)$ for $x\in S'$ and $\theta_{\psi,b}(x)=b$ for the other $x\in S$; its hypotheses hold because, for $x\in S'$, $\psi(x)$ is a value of $\psi$ at an element of its domain and $\psi(x)\in B_{x}\subseteq U$, and $b\in B_{a}\subseteq U$, by Indexed Families of Sets and Their Union, Intersection and Product §union. As $S=S'\cup\{a\}$ and $a\notin S'$, the only element of $S$ outside $S'$ is $a$, and $\theta_{\psi,b}(a)=b$; hence $\theta_{\psi,b}(x)\in B_{x}$ for every $x\in S$, and $\theta_{\psi,b}\in P_{S}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, $\theta_{\psi,b}|_{S'}$ is a function with domain $S'$ and values $\theta_{\psi,b}(x)=\psi(x)$ for $x\in S'$, so $\theta_{\psi,b}|_{S'}=\psi$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, and $\rho'(\theta_{\psi,b})=(\psi,b)$. Thus $\rho'$ is surjective, and hence a bijection.

Let $q:P_{S'}\times B_{a}\to R$ be the map $(\psi,b)\mapsto\Big(\prod_{x\in S'}u(x,\psi(x))\Big)\,u(a,b)$, given by Maps and Relations Given by Formulas §binary. Let $\varphi\in P_{S}$ and $(\psi,b)=\rho'(\varphi)$, so $\psi=\varphi|_{S'}$ and $b=\varphi(a)$. The map $x\mapsto u(x,\varphi(x))$ on $S$ agrees with $x\mapsto u(x,\psi(x))$ on $S'$, because $\varphi$ agrees with $\psi$ on $S'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, and it takes the value $u(a,b)$ at $a$, because $\varphi$ takes the value $b$ at $a$. Since $S$ is the union of the disjoint sets $S'$ and $\{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, with Sums and Products over a Finite Set and over an Interval §subsets, give

$$\prod_{x\in S}u(x,\varphi(x))=\Big(\prod_{x\in S'}u(x,\psi(x))\Big)\,u(a,b)=q(\rho'(\varphi)).$$

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 Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §reindexing along the bijection $\rho':P_{S}\to P_{S'}\times B_{a}$ applied to $q$, and finally the last display, 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}}q(\psi,b)=\sum_{\varphi\in P_{S}}q(\rho'(\varphi))=\sum_{\varphi\in P_{S}}\prod_{x\in S}u(x,\varphi(x)). \end{aligned}$$

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

Constant. By Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals, $\#A$ stands here for its image $(\#A)_{R}$ in $R$. If $A=\emptyset$, then $\sum_{x\in A}c=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, whose image $0_{R}$ is the zero $0$ of $R$ by Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals; so $\#A\cdot c=0\cdot c=c\cdot0=0$ by commutativity of multiplication and the rule $c\cdot0=0$ proved above. If $A\neq\emptyset$, then $n=\#A$ lies in $\mathbb{N}$ by The Iterated Operation over a Finite Set Does Not Depend on the Enumeration §nonempty, and there is a bijection $\varphi$ from $[n]$ onto $A$ by The Number of Elements of a Finite Set §cardinality; then Sums and Products over a Finite Set and over an Interval §operation, applied to the constant map $x\mapsto c$ on $A$, and Finite Sums in a Commutative Ring and in an Ordered Field: Distributivity, Differences, Telescoping, Constant Terms, Comparison and the Triangle Inequality §constant give $\sum_{x\in A}c=\sum_{k=1}^{n}c=n\,c=\#A\cdot c$. For $c=1$, $\#A\cdot1=\#A$ by Commutative Rings §ring.

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.

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.