[proofplan]
We encode a skew-symmetric matrix $A$ as the alternating $2$-form $\omega_A$ on $\mathbb R^{2m}$ and use the coefficient of the standard volume form in $\omega_A^m/m!$ as the Pfaffian convention. The congruence formula follows by pulling back $\omega_A$ along the [linear map](/page/Linear%20Map) with matrix $B^\top$ and comparing the induced action on the top exterior power. The determinant identity is then reduced, using the real orthogonal normal form for skew-symmetric matrices, to the [direct sum](/page/Direct%20Sum) of standard $2\times 2$ skew blocks, where both sides can be computed explicitly.
[/proofplan]
[step:Relate congruence of skew matrices to pullback of alternating forms]
Let $V:=\mathbb R^{2m}$, and let $(e_1,\dots,e_{2m})$ be its standard ordered basis. Let $(e_1^*,\dots,e_{2m}^*)$ be the [dual basis](/theorems/414) of $V^*$. For a real skew-symmetric matrix $A=(A_{ij})\in M_{2m}(\mathbb R)$, define
\begin{align*}
\omega_A:=\sum_{1\le i<j\le 2m}A_{ij}e_i^*\wedge e_j^*\in \Lambda^2V^*.
\end{align*}
For vectors $u,v\in V$, written as coordinate columns in the standard basis, skew-symmetry gives
\begin{align*}
\omega_A(u,v)=u^\top A v.
\end{align*}
Let $C:V\to V$ be the linear map whose standard matrix is $C\in M_{2m}(\mathbb R)$. For each integer $k\in\{0,\dots,2m\}$, its pullback on alternating $k$-forms is the map
\begin{align*}
C^*:\Lambda^kV^*\to \Lambda^kV^*
\end{align*}
defined by
\begin{align*}
(C^*\eta)(v_1,\dots,v_k)=\eta(Cv_1,\dots,Cv_k)
\end{align*}
for every $\eta\in\Lambda^kV^*$ and $v_1,\dots,v_k\in V$. Applying this definition with $k=2$ and $\eta=\omega_A$ gives
\begin{align*}
(C^*\omega_A)(u,v)=\omega_A(Cu,Cv)=u^\top C^\top A C v.
\end{align*}
Therefore
\begin{align*}
C^*\omega_A=\omega_{C^\top A C}.
\end{align*}
Taking $C=B^\top$ gives
\begin{align*}
(B^\top)^*\omega_A=\omega_{BAB^\top}.
\end{align*}
[/step]
[step:Compare top exterior coefficients to prove the congruence law]
By the defining normalization of the Pfaffian,
\begin{align*}
\frac{1}{m!}\omega_A^m=\operatorname{Pf}(A)e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
Apply $(B^\top)^*$ to both sides. Pullback commutes with wedge products, so
\begin{align*}
\frac{1}{m!}\bigl((B^\top)^*\omega_A\bigr)^m=\operatorname{Pf}(A)(B^\top)^*(e_1^*\wedge\cdots\wedge e_{2m}^*).
\end{align*}
Since $(B^\top)^*\omega_A=\omega_{BAB^\top}$, the left-hand side is
\begin{align*}
\operatorname{Pf}(BAB^\top)e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
On the top exterior power, the pullback by a linear map with matrix $B^\top$ multiplies the standard volume covector by $\det(B^\top)=\det(B)$. Hence
\begin{align*}
(B^\top)^*(e_1^*\wedge\cdots\wedge e_{2m}^*)=\det(B)e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
Comparing the coefficient of the nonzero covector $e_1^*\wedge\cdots\wedge e_{2m}^*$ gives
\begin{align*}
\operatorname{Pf}(BAB^\top)=\det(B)\operatorname{Pf}(A).
\end{align*}
[guided]
The point of this step is to turn the matrix identity into a statement about the single coefficient of a top-degree form. The Pfaffian convention says exactly that this coefficient is $\operatorname{Pf}(A)$:
\begin{align*}
\frac{1}{m!}\omega_A^m=\operatorname{Pf}(A)e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
We apply the pullback $(B^\top)^*$ to this identity. From the preceding pullback computation, applied with $C=B^\top$, we have
\begin{align*}
(B^\top)^*\omega_A=\omega_{BAB^\top}.
\end{align*}
This is the bridge between the matrix congruence $A\mapsto BAB^\top$ and the exterior-algebra calculation. The pullback $(B^\top)^*$ is an algebra homomorphism on the exterior algebra: it preserves wedge products and scalar multiplication. Thus
\begin{align*}
(B^\top)^*\left(\frac{1}{m!}\omega_A^m\right)=\frac{1}{m!}\bigl((B^\top)^*\omega_A\bigr)^m.
\end{align*}
From the previous step, $(B^\top)^*\omega_A=\omega_{BAB^\top}$, so the left-hand side becomes
\begin{align*}
\frac{1}{m!}\omega_{BAB^\top}^m=\operatorname{Pf}(BAB^\top)e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
Now we compute the right-hand side. The space $\Lambda^{2m}V^*$ is one-dimensional and is spanned by the standard volume covector
\begin{align*}
e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
The top exterior power change-of-basis determinant law says that pullback by a linear map multiplies this volume covector by the determinant of the map. Here the map has matrix $B^\top$, so the multiplier is
\begin{align*}
\det(B^\top)=\det(B).
\end{align*}
Therefore
\begin{align*}
(B^\top)^*(e_1^*\wedge\cdots\wedge e_{2m}^*)=\det(B)e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
Putting the two computations together gives
\begin{align*}
\operatorname{Pf}(BAB^\top)e_1^*\wedge\cdots\wedge e_{2m}^*=\det(B)\operatorname{Pf}(A)e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
Because $e_1^*\wedge\cdots\wedge e_{2m}^*$ is nonzero, equality of these top-degree forms is equality of their scalar coefficients. Hence
\begin{align*}
\operatorname{Pf}(BAB^\top)=\det(B)\operatorname{Pf}(A).
\end{align*}
[/guided]
[/step]
[step:Compute the Pfaffian and determinant on skew-symmetric block normal form]
We use the standard real skew-symmetric orthogonal block diagonal normal form. It states that there exist an [orthogonal matrix](/page/Orthogonal%20Matrix) $Q\in O(2m)$ and [real numbers](/page/Real%20Numbers) $\lambda_1,\dots,\lambda_m\in\mathbb R$ such that
\begin{align*}
A=QJQ^\top,
\end{align*}
where $J\in M_{2m}(\mathbb R)$ is the block diagonal matrix with $2\times 2$ diagonal blocks $J_j\in M_2(\mathbb R)$ determined by
\begin{align*}
(J_j)_{11}=0,\quad (J_j)_{12}=\lambda_j,\quad (J_j)_{21}=-\lambda_j,\quad (J_j)_{22}=0
\end{align*}
for $j\in\{1,\dots,m\}$.
For this block diagonal matrix,
\begin{align*}
\omega_J=\sum_{j=1}^m \lambda_j e_{2j-1}^*\wedge e_{2j}^*.
\end{align*}
In the expansion of $\omega_J^m$, the only nonzero terms are those in which each of the $m$ two-forms $\lambda_j e_{2j-1}^*\wedge e_{2j}^*$ appears exactly once. Since two-forms commute under the wedge product, the $m!$ such terms have the same sign. Hence
\begin{align*}
\frac{1}{m!}\omega_J^m=\lambda_1\cdots\lambda_m e_1^*\wedge\cdots\wedge e_{2m}^*.
\end{align*}
Thus
\begin{align*}
\operatorname{Pf}(J)=\lambda_1\cdots\lambda_m.
\end{align*}
The determinant of a block diagonal matrix is the product of the determinants of its diagonal blocks, and
\begin{align*}
\det J_j=\lambda_j^2.
\end{align*}
Therefore
\begin{align*}
\det J=\prod_{j=1}^m \lambda_j^2=(\lambda_1\cdots\lambda_m)^2=\operatorname{Pf}(J)^2.
\end{align*}
[/step]
[step:Transfer the block computation back to the original matrix]
Since $A=QJQ^\top$ and $Q\in O(2m)\subset GL(2m,\mathbb R)$, the congruence formula gives
\begin{align*}
\operatorname{Pf}(A)=\operatorname{Pf}(QJQ^\top)=\det(Q)\operatorname{Pf}(J).
\end{align*}
Squaring and using $\det(Q)^2=1$, we obtain
\begin{align*}
\operatorname{Pf}(A)^2=\operatorname{Pf}(J)^2.
\end{align*}
From the block computation,
\begin{align*}
\operatorname{Pf}(J)^2=\det J.
\end{align*}
Finally,
\begin{align*}
\det A=\det(QJQ^\top)=\det(Q)\det(J)\det(Q^\top)=\det(Q)^2\det(J)=\det J.
\end{align*}
Combining these equalities yields
\begin{align*}
\operatorname{Pf}(A)^2=\det A.
\end{align*}
Together with the congruence law already proved, this completes the proof.
[/step]
