[proofplan]
We prove the identity by pairing both sides with an arbitrary Schur function $s_\rho$. The left-hand side becomes $\langle s_\mu s_\nu, s_\lambda s_\rho\rangle$ by the defining adjointness of $s_\lambda^\perp$. The right-hand side is evaluated by expanding the Hall-dual coproduct of $s_\rho$ and then applying adjointness separately to the two skewing operators. Both pairings reduce to the same coefficient of $s_\mu \otimes s_\nu$ in $\Delta(s_\lambda s_\rho)$, so orthonormality of the Schur basis identifies the two symmetric functions.
[/proofplan]
[step:Declare the Hall-dual coproduct and its Schur expansion]
Let $\Delta: \Lambda \to \Lambda \otimes \Lambda$ denote the coproduct adjoint to multiplication with respect to the Hall [inner product](/page/Inner%20Product), meaning that for all $a,b,h \in \Lambda$,
\begin{align*}
\langle ab,h\rangle
=
\langle a \otimes b,\Delta h\rangle,
\end{align*}
where the [tensor product](/page/Tensor%20Product) inner product is determined on Schur basis tensors by
\begin{align*}
\langle s_\alpha \otimes s_\beta, s_\gamma \otimes s_\delta\rangle
=
\langle s_\alpha,s_\gamma\rangle
\langle s_\beta,s_\delta\rangle.
\end{align*}
Since the Schur basis is orthonormal and
\begin{align*}
s_\alpha s_\beta=\sum_\kappa c_{\alpha\beta}^{\kappa}s_\kappa,
\end{align*}
the coproduct satisfies, for every partition $\kappa$,
\begin{align*}
\Delta s_\kappa
=
\sum_{\alpha,\beta} c_{\alpha\beta}^{\kappa}s_\alpha \otimes s_\beta.
\end{align*}
[guided]
The product formula is easiest to prove by using the structure dual to multiplication. Define $\Delta: \Lambda \to \Lambda \otimes \Lambda$ to be the [linear map](/page/Linear%20Map) adjoint to multiplication under the Hall inner product:
\begin{align*}
\langle ab,h\rangle
=
\langle a \otimes b,\Delta h\rangle
\end{align*}
for all $a,b,h \in \Lambda$. The inner product on $\Lambda \otimes \Lambda$ is the product inner product, so on Schur basis tensors it is
\begin{align*}
\langle s_\alpha \otimes s_\beta, s_\gamma \otimes s_\delta\rangle
=
\langle s_\alpha,s_\gamma\rangle
\langle s_\beta,s_\delta\rangle.
\end{align*}
We now compute $\Delta s_\kappa$ for a partition $\kappa$. Write
\begin{align*}
\Delta s_\kappa
=
\sum_{\alpha,\beta} d_{\alpha\beta}^{\kappa}s_\alpha \otimes s_\beta
\end{align*}
for uniquely determined integers $d_{\alpha\beta}^{\kappa}$, since the tensors $s_\alpha \otimes s_\beta$ form an [orthonormal basis](/page/Orthonormal%20Basis) of $\Lambda \otimes \Lambda$. Pairing with $s_\alpha \otimes s_\beta$ gives
\begin{align*}
d_{\alpha\beta}^{\kappa}
&=
\langle s_\alpha \otimes s_\beta,\Delta s_\kappa\rangle \\
&=
\langle s_\alpha s_\beta,s_\kappa\rangle.
\end{align*}
By the definition of Littlewood-Richardson coefficients,
\begin{align*}
s_\alpha s_\beta
=
\sum_\tau c_{\alpha\beta}^{\tau}s_\tau.
\end{align*}
Using Schur orthonormality, this gives
\begin{align*}
\langle s_\alpha s_\beta,s_\kappa\rangle
=
c_{\alpha\beta}^{\kappa}.
\end{align*}
Hence
\begin{align*}
\Delta s_\kappa
=
\sum_{\alpha,\beta} c_{\alpha\beta}^{\kappa}s_\alpha \otimes s_\beta.
\end{align*}
[/guided]
[/step]
[step:Compute the pairing of the left-hand side with a Schur test function]
Fix an arbitrary partition $\rho$. By the defining adjointness of $s_\lambda^\perp$,
\begin{align*}
\left\langle s_\lambda^\perp(s_\mu s_\nu),s_\rho\right\rangle
=
\left\langle s_\mu s_\nu,s_\lambda s_\rho\right\rangle.
\end{align*}
Using the coproduct adjointness of multiplication, this becomes
\begin{align*}
\left\langle s_\mu s_\nu,s_\lambda s_\rho\right\rangle
=
\left\langle s_\mu \otimes s_\nu,\Delta(s_\lambda s_\rho)\right\rangle.
\end{align*}
[/step]
[step:Compute the pairing of the right-hand side with the same Schur test function]
For the right-hand side, bilinearity of the Hall inner product gives
\begin{align*}
&\left\langle
\sum_{\alpha,\beta} c_{\alpha\beta}^{\lambda}
\bigl(s_\alpha^\perp s_\mu\bigr)
\bigl(s_\beta^\perp s_\nu\bigr),
s_\rho
\right\rangle \\
&\qquad =
\sum_{\alpha,\beta} c_{\alpha\beta}^{\lambda}
\left\langle
\bigl(s_\alpha^\perp s_\mu\bigr)
\bigl(s_\beta^\perp s_\nu\bigr),
s_\rho
\right\rangle.
\end{align*}
Applying coproduct adjointness to each product inside the sum gives
\begin{align*}
\left\langle
\bigl(s_\alpha^\perp s_\mu\bigr)
\bigl(s_\beta^\perp s_\nu\bigr),
s_\rho
\right\rangle
=
\left\langle
s_\alpha^\perp s_\mu \otimes s_\beta^\perp s_\nu,
\Delta s_\rho
\right\rangle.
\end{align*}
Using
\begin{align*}
\Delta s_\rho
=
\sum_{\gamma,\delta} c_{\gamma\delta}^{\rho}s_\gamma \otimes s_\delta,
\end{align*}
we obtain
\begin{align*}
&\left\langle
\sum_{\alpha,\beta} c_{\alpha\beta}^{\lambda}
\bigl(s_\alpha^\perp s_\mu\bigr)
\bigl(s_\beta^\perp s_\nu\bigr),
s_\rho
\right\rangle \\
&\qquad =
\sum_{\alpha,\beta,\gamma,\delta}
c_{\alpha\beta}^{\lambda}c_{\gamma\delta}^{\rho}
\left\langle s_\alpha^\perp s_\mu,s_\gamma\right\rangle
\left\langle s_\beta^\perp s_\nu,s_\delta\right\rangle.
\end{align*}
By adjointness of $s_\alpha^\perp$ and $s_\beta^\perp$,
\begin{align*}
\left\langle s_\alpha^\perp s_\mu,s_\gamma\right\rangle
=
\left\langle s_\mu,s_\alpha s_\gamma\right\rangle,
\qquad
\left\langle s_\beta^\perp s_\nu,s_\delta\right\rangle
=
\left\langle s_\nu,s_\beta s_\delta\right\rangle.
\end{align*}
Therefore
\begin{align*}
&\left\langle
\sum_{\alpha,\beta} c_{\alpha\beta}^{\lambda}
\bigl(s_\alpha^\perp s_\mu\bigr)
\bigl(s_\beta^\perp s_\nu\bigr),
s_\rho
\right\rangle \\
&\qquad =
\sum_{\alpha,\beta,\gamma,\delta}
c_{\alpha\beta}^{\lambda}c_{\gamma\delta}^{\rho}
\left\langle s_\mu,s_\alpha s_\gamma\right\rangle
\left\langle s_\nu,s_\beta s_\delta\right\rangle.
\end{align*}
[/step]
[step:Identify the right-hand pairing as the same coproduct coefficient]
Using Schur orthonormality and the [Littlewood-Richardson rule](/theorems/5183),
\begin{align*}
\left\langle s_\mu,s_\alpha s_\gamma\right\rangle
=
c_{\alpha\gamma}^{\mu},
\qquad
\left\langle s_\nu,s_\beta s_\delta\right\rangle
=
c_{\beta\delta}^{\nu}.
\end{align*}
Thus the right-hand pairing is
\begin{align*}
\sum_{\alpha,\beta,\gamma,\delta}
c_{\alpha\beta}^{\lambda}c_{\gamma\delta}^{\rho}
c_{\alpha\gamma}^{\mu}c_{\beta\delta}^{\nu}.
\end{align*}
On the other hand, since $\Delta$ is adjoint to multiplication, it is multiplicative with respect to the multiplication on $\Lambda \otimes \Lambda$. Hence
\begin{align*}
\Delta(s_\lambda s_\rho)
=
\Delta s_\lambda \, \Delta s_\rho.
\end{align*}
Expanding both factors gives
\begin{align*}
\Delta(s_\lambda s_\rho)
&=
\left(\sum_{\alpha,\beta} c_{\alpha\beta}^{\lambda}s_\alpha \otimes s_\beta\right)
\left(\sum_{\gamma,\delta} c_{\gamma\delta}^{\rho}s_\gamma \otimes s_\delta\right) \\
&=
\sum_{\alpha,\beta,\gamma,\delta}
c_{\alpha\beta}^{\lambda}c_{\gamma\delta}^{\rho}
(s_\alpha s_\gamma) \otimes (s_\beta s_\delta).
\end{align*}
Pairing with $s_\mu \otimes s_\nu$ yields
\begin{align*}
\left\langle s_\mu \otimes s_\nu,\Delta(s_\lambda s_\rho)\right\rangle
=
\sum_{\alpha,\beta,\gamma,\delta}
c_{\alpha\beta}^{\lambda}c_{\gamma\delta}^{\rho}
c_{\alpha\gamma}^{\mu}c_{\beta\delta}^{\nu}.
\end{align*}
This is exactly the value of the right-hand pairing computed above.
[/step]
[step:Conclude equality from Schur orthonormality]
Combining the computations, for every partition $\rho$ we have
\begin{align*}
\left\langle s_\lambda^\perp(s_\mu s_\nu),s_\rho\right\rangle
=
\left\langle
\sum_{\alpha,\beta} c_{\alpha\beta}^{\lambda}
\bigl(s_\alpha^\perp s_\mu\bigr)
\bigl(s_\beta^\perp s_\nu\bigr),
s_\rho
\right\rangle.
\end{align*}
The Schur functions form an orthonormal basis of $\Lambda$, so a symmetric function is determined by all of its Hall inner products with Schur functions. Therefore
\begin{align*}
s_\lambda^\perp(s_\mu s_\nu)
=
\sum_{\alpha,\beta} c_{\alpha\beta}^{\lambda}
\bigl(s_\alpha^\perp s_\mu\bigr)
\bigl(s_\beta^\perp s_\nu\bigr).
\end{align*}
This proves the skewing product formula.
[/step]
