Subset sums of a disjoint union form the sumset of the subset sums

Let $G$ be an abelian group and let $A, B \subseteq G$ be disjoint finite sets. Then the set of subset sums of their union is exactly the sumset of their sets of subset sums:

where $\mathcal{P}(X) = \{\sum_{x \in S} x : S \subseteq X\}$ and $U + V = \{u + v : u \in U,\ v \in V\}$ is the pointwise sumset.

Both inclusions are immediate once the right decomposition is named. A subset $S \subseteq A \cup B$ splits as $S = (S \cap A) \cup (S \cap B)$ into two disjoint pieces, so its sum is the sum over $S \cap A$ plus the sum over $S \cap B$; conversely, given $S_1 \subseteq A$ and $S_2 \subseteq B$, disjointness of $A$ and $B$ makes $S_1$ and $S_2$ disjoint, so $S_1 \cup S_2 \subseteq A \cup B$ has sum $\sum S_1 + \sum S_2$.

This identity is the interface between the two classical ingredients of the Erdős–Lev–Rauzy–Sándor–Sárközy argument. One splits a zero-sum-free sequence into blocks of distinct elements, bounds the subset sums of each block from below by Olson's theorem, and then has to combine the blocks; the identity turns that combination into a statement about a sumset, which is precisely what an addition theorem of Kemperman–Scherk type can bound. Disjointness cannot be dropped: for $A = B = \{a\}$ with $a$ of infinite order, $\mathcal{P}(A \cup B) = \{0, a\}$ has two elements while $\mathcal{P}(A) + \mathcal{P}(B) = \{0, a, 2a\}$ has three.

Formalization Note. Throughout, the set of subset sums of a finite set $A$ in an abelian group is rendered as A.powerset.image (fun S => ∑ x ∈ S, x), the image of the powerset of $A$ under the summation map. The empty subset is included, so $0$ always belongs to it. The sumset on the right is Finset pointwise addition, so the ambient preamble opens the Pointwise scope.