Nonsplit torsion-free abelian extensions preserve absence of group-ring zero divisors

Let $B$ be the subgroup of $A$ generated by the images of the finite supports of $f$ and $g$. It is finitely generated, torsion-free and abelian, so [F2] identifies it with ${\mathbb{Z}}^r$. Transport the lexicographic order from ${\mathbb{Z}}^r$ to $B$. This is a total order invariant under addition. No order on the whole quotient or on $G$ is needed. Let $X,Y\subseteq B$ be the finite quotient supports of $f,g$. Choose lifts $t_x\in G$ for the finitely many elements of $X\cup Y\cup (X+Y)$, using the same lift for any repeated element. By grouping terms in each coset, [F1] gives unique expressions $f={\sum }_{x\in X}{r}_x{t}_x$ and $g={\sum }_{y\in Y}{s}_y{t}_y$ with $0\mathrm{\ne }{r}_x,s_y\in k[H]$. Distinct cosets have disjoint group bases, so these grouped coefficients are nonzero.

For these lifts put ${\alpha }_x(s)=t_{x}s{t}_x^{-1}$ on $k[H]$ and $h_{x,y}=t_x{t}_y{t}_{x+y}^{-1}\in H$. Normality makes ${\alpha }_x$ a ring automorphism, with inverse conjugation by $t_x^{-1}$. Direct multiplication gives $(r_x{t}_x)(s_y{t}_y)=r_x{\alpha }_x(s_y)h_{x,y}{t}_{x+y}$. This is the crossed-product multiplication on the finite supports. The factor $h_{x,y}$ is retained and is a unit; it is not assumed to be $1$. Its compatibility with iterated multiplication is inherited from associativity in $G$. Thus the calculation applies to a nonsplit extension.

Let $x_0=\max X$ and $y_0=\max Y$. Every other pair $(x,y)$ satisfies $x+y<x_0+y_0$: if $x<x_0$, then $x+y\le x+y_0<x_0+y_0$, and if $x=x_0$ but $y<y_0$, addition invariance gives the same strict inequality. Hence the coefficient of $t_{x_0+y_0}$ in $fg$ is the single term $r_{x_0}{\alpha }_{x_0}(s_{y_0})h_{x_0,y_0}$. It is nonzero by [A1], invertibility of $h_{x_0,y_0}$ and injectivity of ${\alpha }_{x_0}$. By disjointness of coset bases, $fg\mathrm{\ne }0$. Since $f,g$ were arbitrary, $k[G]$ has no zero divisors. Only finitely many lifts were chosen, so the proof introduces no choice axiom.