Teaching a course on algebraic combinatorics has made me aware of a technical fact about formal power series that is used throughout the subject, but that I have never seen formally stated, let alone proved. Here is a representative particular case of the fact (see below for the general case):
Infinite distributive law (positive integers version). An infinite product of infinite sums of formal power series — e.g., of the form $\prod\limits_{i=1}^\infty \left( p_{i,0} + p_{i,1} + p_{i,2} + \cdots \right)$, where each $p_{i,j}$ is a formal power series — can be expanded into an infinite sum as long as certain reasonable conditions hold. Namely, if we assume that $p_{i,0} = 1$ for each $i$, and if we assume that the family $\left(p_{i,k}\right)_{i\geq 1,\ k\geq 1}$ is summable (i.e., each monomial appears in only finitely many entries of this family), then the product $\prod\limits_{i=1}^\infty \left( p_{i,0} + p_{i,1} + p_{i,2} + \cdots \right)$ converges (in the coefficientwise topology on our ring of formal power series) and equals the sum of the products $p_{1, k_1} p_{2, k_2} p_{3, k_3} \cdots$ over all essentially finite sequences $\left(k_1, k_2, k_3, \ldots\right)$ of nonnegative integers. ("Essentially finite" means that all but finitely many $i$ satisfy $k_i = 0$.
This is used for proving various standard generating function identities, such as
\begin{align}
\prod_{i=1}^\infty \dfrac{1}{1-x^i} = \prod_{i=1}^\infty \left(1 + x^i + x^{2i} + x^{3i} + \cdots\right)
= \sum_{\lambda\text{ is a partition}} x^{\left|\lambda\right|}
\end{align}
or
\begin{align}
\prod_{i=1}^\infty \dfrac{1}{1-x_it} = \prod_{i=1}^\infty \left(1 + x_it + x_i^2t^2 + x_i^3t^3 + \cdots\right)
= \sum_{n \in \mathbb{N}} h_n t^n
\end{align}
(where the latter equality is playing out in the ring of formal power series over the ring of symmetric functions in $x_1, x_2, x_3, \ldots$, with $h_n$ standing for the $n$-th complete homogeneous symmetric function). In most simple situations (including the two I just mentioned), it is not hard to forego the use of the infinite distributive law for a limiting argument that reduces the problem to finite products (for which a distributive law isn't too hard to show). However, as one dives deeper into partitions and symmetric functions, these epicycles start getting exhausting. It is clear that the infinite distributive law belongs into the textbooks; yet I have never seen it there. Thus I started writing out a proof for my lecture notes, but so far I have not had much success.
Question. Is there a citeable source or a teachable proof for the infinite distributive law?
Note that I am looking for a proof that isn't specific to single-variable power series; at least it needs to cover the case of symmetric functions. Ideally, the proof shouldn't be spread over multiple chapters of a treatise or use heavy topological lingo. That said, so far I haven't even found such a proof.
Another complication is the fact that not all infinite products are indexed by positive integers. For example, the Cauchy formula in symmetric functions theory is about expanding $\prod\limits_{\left(i,j\right)\in\left\{1,2,3,\ldots\right\}^2} \dfrac{1}{1-x_iy_j}$. While convergence of nets can make this general case not much harder than the integer-indexed one, I'd prefer not to rely on it too much.
Here is the general version of infinite distributivity that I'm really aiming for (of course, there are even more general facts, but this one seems to suffice for my combinatorial needs):
Infinite distributive law (general version). Let $K$ be a commutative ring. Let $L$ be the ring of formal power series over $K$ in some set of variables. We equip $L$ with the usual coefficientwise topology. A family $\left(f_j\right)_{j \in J}$ is said to be multipliable if the product $\prod\limits_{j\in J} f_j$ is well-defined, i.e., if for each monomial $\mathfrak{m}$, there exists a finite subset $K$ of $J$ such that the $\mathfrak{m}$-coefficient of $\prod\limits_{j\in K} f_j$ does not change if we increase $K$ (that is, the $\mathfrak{m}$-coefficient of $\prod\limits_{j\in K} f_j$ equals the $\mathfrak{m}$-coefficient of $\prod\limits_{j\in K'} f_j$ for any finite subset $K'$ of $J$ with $K \subseteq K'$). The notion of a summable family is defined similarly (but can also be characterized in a simpler way: a family $\left(f_j\right)_{j \in J}$ is summable if and only if each monomial $\mathfrak{m}$ occurs in only finitely many of its entries).
Let $I$ be a set. For any $i\in I$, let $S_i$ be a set that contains the number $0$. Set
\begin{align}
\overline{S} = \left\{ \left( i,k\right) \ \mid\ i\in I\text{ and }k\in S_i\text{ and }k\neq0\right\} .
\end{align}For any $i\in I$ and any $k\in S_i$, let $p_{i,k}$ be an element of $L$. Assume that
\begin{equation}
p_{i,0}=1\ \ \ \ \ \ \ \ \ \ \text{for any }i\in I.
\end{equation}Assume further that the family $\left( p_{i,k}\right) _{\left( i,k\right) \in\overline{S}}$ is summable.
Then, the product $\prod\limits_{i\in I}\ \ \sum\limits_{k\in S_i}p_{i,k}$ is well-defined (i.e., the family $\left( p_{i,k}\right)_{k\in S_i}$ is summable for each $i\in I$, and the family $\left( \sum\limits_{k\in S_i}p_{i,k}\right) _{i\in I}$ is multipliable), and we have
\begin{equation}
\prod\limits_{i\in I}\ \ \sum\limits_{k\in S_i}p_{i,k}=\sum\limits_{\substack{\left(
k_{i}\right) _{i\in I}\in\prod\limits_{i\in I}S_i\\\text{is essentially finite}
}}\ \ \prod\limits_{i\in I}p_{i,k_{i}}.
\end{equation}
Here, a family $\left(k_{i}\right) _{i\in I}\in\prod\limits_{i\in I}S_i$ is said to be essentially finite if all but finitely many $i \in I$ satisfy $k_i = 0$.In particular, the family $\left( \prod\limits_{i\in I}p_{i,k_{i}}\right) _{\left(
k_{i}\right) _{i\in I}\in\prod\limits_{i\in I}S_i\text{ is essentially finite}}$
is summable.
Best Answer
So, the summability of each $(p_{i,k})_{k \in S_i}$ stems from the hypothesis that $(p_t)_{t \in \overline{S}}$ is summable.
We want to show that the family $\left(\sum_{k \in S_i}{p_{i,k}}\right)_i$ is multipliable.
Let $\mathfrak{m}$ be a monomial. Let $N$ be the (finite) set of monomials lower or equal than $\mathfrak{m}$. There is some finite set $F \subset \overline{S}$ such that for all $t \in \overline{S} \backslash F$, the coefficients of the monomials of $N$ in $p_t$ are zero. Let $J \subset I$ be the (finite) set of all the $i \in I$ such that there is $k \in S_i \backslash \{0\}$ such that $(i,k) \in F$.
Let $c_{\mathfrak{n}}(q)$ be the coefficient of a monomial $\mathfrak{n}$ in a polynomial $q$. Then, for any finite $J' \supset J$, the $\mathfrak{m}$-coefficient of $\prod_{j \in J'}{\sum_{k \in S_j}{p_{j,k}}}$ is the sum of $$\prod_{j \in J'}{c_{\mathfrak{n}_j}(p_{j,k_j})}$$ over $k \in \prod_{j \in J'}{S_j}$ and monomials $\mathfrak{n}_j$ satisfying $\sum_{j\in J'} \mathfrak{n}_j = \mathfrak{m}$ (we write monomials additively, i.e., we say "sum" for what would usually be called "product"). By the assumption on $J$, $c_{\mathfrak{n}_j}(p_{j,k})$ (the coefficient for the monomial $\mathfrak{n}_j$ of $p_{j,k}$) is zero when $j \notin J$ and $k \neq 0$, and $1$ if $k=0, \mathfrak{n}_j=0$. So
$$c_{\mathfrak{m}}\left(\prod_{j \in J'}{\sum_{k \in S_j}{p_{j,k}}}\right)=\sum{\prod_{j \in J}{c_{\mathfrak{n}_j}(p_{j,k_j})}},$$ where the sum is over the decompositions $\mathfrak{m} = \sum_{j \in J}{\mathfrak{n}_j}$ and the $k \in \prod_{j \in J}{S_j}$. Thus this coefficient does not depend on the choice of $J' \supset J$.
Therefore the family $\left(\sum_{k \in S_i}{p_{i,k}}\right)_i$ is multipliable.
Let's now show that the family $\left(\prod_{i \in I}{p_{i,k_i}}\right)_k$ is summable, over the essentially finite $k \in \prod_{i \in I}{S_i}$.
Let $\mathfrak{m}$ be a monomial. Let $k \in \prod_{i \in I}{S_i}$ be essentially finite. If $\prod_{i \in I}{p_{i,k_i}}$ has a nonzero $\mathfrak{m}$ coefficient, then there is a decomposition $\sum_{i \in I}{\mathfrak{n}_i}=\mathfrak{m}$ such that for each $i \in I$, the $\mathfrak{n}_i$ coefficient of $p_{i,k_i}$ is nonzero.
Let $N$ be, once again, the set of all monomials that are lower or equal than $\mathfrak{m}$. There is a finite subset $T \subset \overline{S}$ such that if $t \in \overline{S}\backslash T$, then $p_t$ has a zero $\mathfrak{n}$ coefficient for each $\mathfrak{n} \in N$.
Now, the set $J$ of $k \in \prod_i{S_i}$ that are essentially finite such that, for each $i \in I$, $k_i = 0$ or $(i,k_i) \in T$ is finite. Indeed, the set $J_1$ of $i$ such that $T$ meets $\{i\} \times S_i$ is finite; for each $i$, $J^i=\{k \in S_i,\, k=0 \text{ or }(i,k)\in T\}$ is finite, and $J$ injects into $\prod_{i \in J_1}{J^i}$ which is finite. Moreover, if $k \notin J$, then $\prod_{i \in I}{p_{i,k_i}}$ has a zero $\mathfrak{m}$-coefficient.
Thus the family $\left(\prod_{i \in I}{p_{i,k_i}}\right)_k$ is summable.
Let $\mathfrak{m}$ be any monomial. To show that $\prod_{i \in I}{\sum_{k \in S_i}{p_{i,k}}}$ and $\sum_k{\prod_{i \in I}{p_{i,k_i}}}$ have the same coefficient for $\mathfrak{m}$, it is thus enough to show the following:
For any finite subsets $J \subset I$ and $K$ of essentially finite elements of $\prod_{i \in I}{S_i}$, there are subsets $J' \supset J, K' \supset K$ such that $\prod_{i \in J'}{\sum_{k \in S_i}{p_{i,k}}}$ and $\sum_{k \in K'}{\prod_{i \in I}{p_{i,k_i}}}$ have the same coefficient for $\mathfrak{m}$.
So let $J,K$ be our finite subsets. Let $J_1$ be the reunion of the $\{i \in I,\,k_i \neq 0\}$ where $k \in K$. Let $K' \supset K$ be the set of all $k \in \prod_{i \in I}{S_i}$ with support in $J'=J \cup J_1 \supset J$.
Then it's elementary (distributivity for finite products of infinite summable sequences) to show that $\prod_{j \in J'}{\sum_{k \in S_j}{p_{j,k}}} = \sum_{k \in K'}{\prod_{i \in I}{p_{i,k_i}}}$, and in particular they have the same coefficient for $\mathfrak{m}$.