We first establish the purification-overlap formula for quantum fidelity, rather than assume the desired monotonicity. Write a canonical purification of a density operator as
Tracing the second factor gives . The Schmidt decomposition shows that any other purification on a sufficiently large fixed ancillary space differs by a unitary on that space: its orthonormal ancillary vectors can be mapped to those of the canonical purification and the map extended to a unitary operator. Zero eigenvalues are handled by padding the ancillary basis.
The overlap of two canonical purifications, with a relative ancillary unitary , is , with zero padding when the ancillary dimension is larger. The unitary variational formula for the trace norm is
Indeed if is a singular value decomposition, the trace is with unitary. Its modulus is at most because , and attains that bound. Thus the maximal absolute overlap of purifications equals ; this also proves the needed form of Uhlmann's theorem.
Choose purifications and attaining . Regard the very same vectors as purifications of with ancillary system . Their overlap is among those maximized in the marginal purification formula, so
This proves the monotonicity of quantum fidelity under partial trace.