[proofplan]
We verify that $\hat{A} = PAP^\top$ is symmetric and positive definite by checking each property directly. Symmetry follows from the transpose rule $(PAP^\top)^\top = PA^\top P^\top = PAP^\top$ (using $A = A^\top$). Positive definiteness follows from the identity $\langle \hat{A}y, y \rangle = \langle A(P^\topy), P^\topy \rangle$, which is strictly positive for $y \neq 0$ because $P$ is nonsingular (so $P^\topy \neq 0$) and $A$ is positive definite.
[/proofplan]
[step:Verify symmetry of $\hat{A} = PAP^\top$]
Taking the transpose:
\begin{align*}
\hat{A}^\top = (PAP^\top)^\top = (P^\top)^\top A^\top P^\top = PA^\top P^\top.
\end{align*}
Since $A$ is symmetric ($A^\top = A$):
\begin{align*}
\hat{A}^\top = PAP^\top = \hat{A}.
\end{align*}
Therefore $\hat{A}$ is symmetric.
[guided]
The transpose of a product reverses the order: $(XYZ)^\top = Z^\top Y^\top X^\top$. Applying this to $\hat{A} = PAP^\top$ gives $(PAP^\top)^\top = (P^\top)^\top A^\top P^\top$. Since $(P^\top)^\top = P$ and $A^\top = A$ (by hypothesis), this simplifies to $PAP^\top = \hat{A}$. Note that the symmetry of $\hat{A}$ depends only on the symmetry of $A$ — it holds for any nonsingular $P$, not just the specific preconditioner.
[/guided]
[/step]
[step:Verify that $P^\top$ maps nonzero vectors to nonzero vectors]
Let $y \in \mathbb{R}^n \setminus \{0\}$. Since $P$ is nonsingular, $\det(P) \neq 0$, and therefore $\det(P^\top) = \det(P) \neq 0$, so $P^\top$ is also nonsingular. It follows that $P^\topy \neq 0$.
[guided]
This intermediate fact is needed for the positive definiteness argument. We need to apply the positive definiteness of $A$ to the vector $P^\topy$, but this requires $P^\topy \neq 0$. Since $P^\top$ is invertible (its determinant equals $\det(P) \neq 0$), its kernel is trivial: $\ker(P^\top) = \{0\}$. So $y \neq 0$ implies $P^\topy \neq 0$.
Equivalently, $P^\top$ is injective because it is a square matrix with nonzero determinant. This is the only property of $P$ we use — we never need any specific structure of the preconditioner.
[/guided]
[/step]
[step:Verify positive definiteness of $\hat{A}$ using the change of variable $z = P^\topy$]
Let $y \in \mathbb{R}^n \setminus \{0\}$. We compute:
\begin{align*}
\langle \hat{A}y, y \rangle = \langle PAP^\topy, y \rangle = \langle AP^\topy, P^\topy \rangle,
\end{align*}
where the second equality uses $\langle Pv, w \rangle = \langle v, P^\topw \rangle$ applied with $v = AP^\topy$ and $w = y$: $\langle P(AP^\topy), y \rangle = \langle AP^\topy, P^\topy \rangle$.
Define $z := P^\topy$. From the previous step, $y \neq 0$ implies $z \neq 0$. By the positive definiteness of $A$:
\begin{align*}
\langle \hat{A}y, y \rangle = \langle Az, z \rangle > 0.
\end{align*}
Since $\langle \hat{A}y, y \rangle > 0$ for every nonzero $y \in \mathbb{R}^n$, the matrix $\hat{A}$ is positive definite.
[guided]
The key manipulation is moving $P$ from the left side of the inner product to the right side via $\langle Pv, w \rangle = \langle v, P^\topw \rangle$. This identity is the defining property of the transpose: $P^\top$ is the adjoint of $P$ with respect to the Euclidean inner product.
After this rearrangement, the quadratic form $\langle \hat{A}y, y \rangle$ becomes $\langle Az, z \rangle$ with $z = P^\topy$. This is the quadratic form of $A$ evaluated at $z$. Since $A$ is SPD, $\langle Az, z \rangle > 0$ for all $z \neq 0$. And $z \neq 0$ because $P^\top$ is nonsingular (established in the previous step).
Geometrically, the transformation $\hat{A} = PAP^\top$ is a congruence transformation. Congruence by a nonsingular matrix preserves the signature of a quadratic form (by Sylvester's law of inertia), so if $A$ has all positive eigenvalues, so does $\hat{A}$. The direct computation above is the explicit verification of this principle.
[/guided]
[/step]
