Regular conditional kernels push forward under measurable random maps

Let $\mathcal{D}$ consist of product-measurable sets $E\subseteq \mathrm{\Omega }\times S$ for which $k_E(\omega ):=K(\omega ,E_{\omega })$ is $\mathcal{G}$-measurable and ${\int }_H{k}_{E}dP=P(H\cap \{(\omega ,X(\omega ))\in E\})$ for every $H\in \mathcal{G}$. For a rectangle $E=A\times B$, $k_E={\mathbf{1}}_{A}K(\cdot ,B)$ is measurable by [F1], and its integral identity follows by applying [F1] to $H\cap A$. Thus all rectangles lie in $\mathcal{D}$.

For each $\omega$, define $\bar{K}(\omega ,\cdot )=K(\omega ,\cdot )\otimes \lambda$, which is a probability measure by [F4]. On a rectangle $B\times C$, its evaluation is $K(\omega ,B)\lambda (C)$, a $\mathcal{G}$-measurable function. For $H\in \mathcal{G}$, the integral of this evaluation over $H$ equals $\lambda (C)P(H\cap \{X\in B\})$ by [F1]. Since $H\cap \{X\in B\}\in \mathcal{G}\vee \sigma (X)$, independence [A2, F5] makes this $P(H\cap \{X\in B\}\cap \{U\in C\})$.

The whole space is in $\mathcal{D}$. If $E\in \mathcal{D}$, then $k_{E^c}=1-k_E$ and the integral identity for $E^c$ follows by subtracting the identity for $E$ from $P(H)$. If $E_j$ are disjoint members of $\mathcal{D}$, then their sections are disjoint, so $k_{{\cup }_j{E}_j}={\sum }_j{k}_{E_j}$ pointwise; [F8] makes the increasing partial sums' limit measurable, and [F6] gives the integral identity for the union. Hence $\mathcal{D}$ is a lambda-system. Measurable rectangles contain $\mathrm{\Omega }\times S$ and are closed under finite intersections, so they form a pi-system generating $\mathcal{G}\otimes \mathrm{\Sigma }$ by [F2]; [F7] therefore gives $\mathcal{D}=\mathcal{G}\otimes \mathrm{\Sigma }$.

For $B\in \mathrm{T}$, [A1] makes $E=g^{-1}(B)$ product-measurable and [F10] makes its sections measurable, so $K_g(\omega ,B)$ is defined. The map $\omega \mapsto (\omega ,X(\omega ))$ is measurable from $(\mathrm{\Omega },\mathcal{F})$ into $(\mathrm{\Omega }\times S,\mathcal{G}\otimes \mathrm{\Sigma })$: the identity map into $(\mathrm{\Omega },\mathcal{G})$ is measurable because $\mathcal{G}\subseteq \mathcal{F}$, and $X$ is measurable, so [F9] applies. Therefore $\{g(\omega ,X(\omega ))\in B\}$ is the measurable preimage of $E$ under this map. Step 2.1 gives measurability and the conditional-event identity for $K_g(\cdot ,B)$. For every $\omega$, $K_g(\omega ,\cdot )$ is the pushforward of the probability measure $K(\omega ,\cdot )$, hence is a probability measure. These are exactly the clauses in [F1], so $K_g$ is a regular conditional distribution of $g(\omega ,X(\omega ))$.

The tuple $(X,U)$ is measurable into the product space by [F9]. The class of sets in $\mathrm{\Sigma }\otimes \mathcal{V}$ for which the evaluation of $\bar{K}$ is measurable and the conditional-event identity holds is a lambda-system: complements subtract from the whole-space identity, and disjoint unions follow from countable additivity, measurable increasing limits [F8], and [F6]. It contains all rectangles by step 1.2, so [F2, F7] show that it contains $\mathrm{\Sigma }\otimes \mathcal{V}$. Every section is the product probability measure from [F4]; consequently $\bar{K}$ is a regular conditional distribution of $(X,U)$ given $\mathcal{G}$.