[proofplan]
We prove the identity by testing both sides against an arbitrary symmetric function $g[X]$ in the $X$ variables. The adjointness defining $f_X^\perp$ converts the left-hand pairing into the pairing of $\Omega[X,Y]$ with $f[X]g[X]$, and the [reproducing property of the Cauchy kernel](/theorems/5218) evaluates this as $f[Y]g[Y]$. The right-hand side gives the same value because $f[Y]$ is a scalar with respect to the $X$-variable Hall [inner product](/page/Inner%20Product). Nondegeneracy degree by degree then identifies the two completed symmetric functions.
[/proofplan]
[step:Test the identity against an arbitrary symmetric function in the $X$ variables]
Let $g[X] \in \operatorname{Sym}_{\mathbb Q}[X]$ be arbitrary. Since $\Omega[X,Y]$ is a completed symmetric function in the $X$ variables with coefficients in $\operatorname{Sym}_{\mathbb Q}[Y]$, the Hall pairing in the $X$ variables defines a coefficientwise pairing
\begin{align*}
(\cdot,\cdot)_X :
\operatorname{Sym}_{\mathbb Q}[X]
\times
\widehat{\operatorname{Sym}_{\mathbb Q}[X]}\widehat{\otimes}\operatorname{Sym}_{\mathbb Q}[Y]
\to
\operatorname{Sym}_{\mathbb Q}[Y].
\end{align*}
It is enough to prove that
\begin{align*}
(g[X], f_X^\perp \Omega[X,Y])_X
=
(g[X], f[Y]\Omega[X,Y])_X
\end{align*}
for every $g[X] \in \operatorname{Sym}_{\mathbb Q}[X]$, because the Hall inner product is nondegenerate on each homogeneous component of $\operatorname{Sym}_{\mathbb Q}$.
[/step]
[step:Evaluate the pairing with the adjoint side]
By definition of $f_X^\perp$ as the adjoint of multiplication by $f[X]$, for every symmetric function $h[X]$ one has
\begin{align*}
(g[X], f_X^\perp h[X])_X
=
(f[X]g[X], h[X])_X.
\end{align*}
Applying this coefficientwise to $h[X] = \Omega[X,Y]$ gives
\begin{align*}
(g[X], f_X^\perp \Omega[X,Y])_X
=
(f[X]g[X], \Omega[X,Y])_X.
\end{align*}
The Cauchy kernel has the reproducing property
\begin{align*}
(a[X], \Omega[X,Y])_X = a[Y]
\end{align*}
for every $a[X] \in \operatorname{Sym}_{\mathbb Q}[X]$. Taking $a[X] := f[X]g[X]$, we obtain
\begin{align*}
(g[X], f_X^\perp \Omega[X,Y])_X
=
f[Y]g[Y].
\end{align*}
[guided]
The point of introducing the arbitrary [test function](/page/Test%20Function) $g[X]$ is that the operator $f_X^\perp$ is defined by an adjointness relation, and adjointness is detected through pairings. For every symmetric function $h[X] \in \operatorname{Sym}_{\mathbb Q}[X]$, the defining property of $f_X^\perp$ is
\begin{align*}
(g[X], f_X^\perp h[X])_X
=
(f[X]g[X], h[X])_X.
\end{align*}
Here multiplication by $f[X]$ acts only in the $X$ alphabet. Since $\Omega[X,Y]$ is completed in the $X$ degree, this same identity applies coefficientwise to $h[X] = \Omega[X,Y]$, giving
\begin{align*}
(g[X], f_X^\perp \Omega[X,Y])_X
=
(f[X]g[X], \Omega[X,Y])_X.
\end{align*}
Now we use the defining reproducing property of the Cauchy kernel: pairing $\Omega[X,Y]$ against any symmetric function $a[X]$ in the $X$ variables replaces the alphabet $X$ by the alphabet $Y$:
\begin{align*}
(a[X], \Omega[X,Y])_X = a[Y].
\end{align*}
With $a[X] := f[X]g[X]$, this becomes
\begin{align*}
(f[X]g[X], \Omega[X,Y])_X = f[Y]g[Y].
\end{align*}
Therefore
\begin{align*}
(g[X], f_X^\perp \Omega[X,Y])_X
=
f[Y]g[Y].
\end{align*}
This is exactly the expected effect: the adjoint operator in the $X$ variables is converted into multiplication by the same symmetric function evaluated in the independent alphabet $Y$.
[/guided]
[/step]
[step:Evaluate the pairing with the multiplication side]
Since $f[Y]$ belongs to the coefficient algebra in the $Y$ variables, it is a scalar for the Hall pairing in the $X$ variables. Hence
\begin{align*}
(g[X], f[Y]\Omega[X,Y])_X
=
f[Y](g[X], \Omega[X,Y])_X.
\end{align*}
Using the reproducing property of $\Omega[X,Y]$ with $a[X] := g[X]$ gives
\begin{align*}
(g[X], \Omega[X,Y])_X = g[Y].
\end{align*}
Therefore
\begin{align*}
(g[X], f[Y]\Omega[X,Y])_X
=
f[Y]g[Y].
\end{align*}
[/step]
[step:Use nondegeneracy to identify the two completed symmetric functions]
Combining the previous two steps, for every $g[X] \in \operatorname{Sym}_{\mathbb Q}[X]$ we have
\begin{align*}
(g[X], f_X^\perp \Omega[X,Y])_X
=
f[Y]g[Y]
=
(g[X], f[Y]\Omega[X,Y])_X.
\end{align*}
Thus
\begin{align*}
(g[X], f_X^\perp \Omega[X,Y] - f[Y]\Omega[X,Y])_X = 0
\end{align*}
for every $g[X] \in \operatorname{Sym}_{\mathbb Q}[X]$. The Hall inner product is nondegenerate on each homogeneous component, and the completed symmetric functions are determined by their homogeneous components. Therefore
\begin{align*}
f_X^\perp \Omega[X,Y] = f[Y]\Omega[X,Y].
\end{align*}
[/step]
