Proof of The Positive Semidefinite Ordering is a Partial Order Compatible with the Linear Structure

Write $\mathbb{R}^n$ for Euclidean space, a real vector space by Euclidean Space $\mathbb{R}^n$ is a Real Vector Space, with the sum of points and the dot product, and write $Pz$ for the matrix-vector product. By Transpose of a Real Matrix, symmetry of a real $n\times n$ matrix $P$ means $P_{ij}=P_{ji}$ for all $i,j\in[n]$. Record also that $0\,t=0$ for every $t\in\mathbb{R}$, since $0\,t=(0+0)\,t=0\,t+0\,t$ by distributivity and claim 2 of Additive Cancellation and Elementary Additive Identities in a Field applies.

Claim 1. By Sum of Real Matrices, Difference of Real Matrices and Scalar Multiple of a Real Matrix the matrices $X+Y$, $X-Y$ and $\mu X$ have entries $X_{ij}+Y_{ij}$, $X_{ij}-Y_{ij}$ and $\mu\,X_{ij}$. Since $X_{ij}=X_{ji}$ and $Y_{ij}=Y_{ji}$ for all $i,j\in[n]$, each of these expressions is unchanged when $i$ and $j$ are interchanged, so all three matrices are symmetric.

Claim 2. The order $\le$ on $\mathbb{R}$ is a total order, hence reflexive, transitive and antisymmetric. Reflexivity gives $z\cdot(Xz)\le z\cdot(Xz)$ for every $z\in\mathbb{R}^n$, that is $X\preceq X$. If $X\preceq Y$ and $Y\preceq Z$, then for every $z\in\mathbb{R}^n$ we have $z\cdot(Xz)\le z\cdot(Yz)$ and $z\cdot(Yz)\le z\cdot(Zz)$, so transitivity gives $z\cdot(Xz)\le z\cdot(Zz)$ and $X\preceq Z$.

Claim 3. Let $z\in\mathbb{R}^n$. By claim 1 of Linearity of the Matrix-Vector Product and the Quadratic Form as a Double Sum and claim 5 of Bilinearity and Symmetry of the Dot Product on $\mathbb{R}^n$,

Hence $z\cdot((Y+Z)z)-z\cdot((X+Z)z)$ and $z\cdot(Yz)-z\cdot(Xz)$ are the same real number, and by claim 3 of Elementary Arithmetic in an Ordered Field each of the inequalities $z\cdot(Xz)\le z\cdot(Yz)$ and $z\cdot((X+Z)z)\le z\cdot((Y+Z)z)$ is equivalent to the nonnegativity of that number. Quantifying over $z\in\mathbb{R}^n$ gives claim 3.

Claim 4. For $z\in\mathbb{R}^n$, claim 1 of Linearity of the Matrix-Vector Product and the Quadratic Form as a Double Sum and claim 5 of Bilinearity and Symmetry of the Dot Product on $\mathbb{R}^n$ give $z\cdot((\mu X)z)=\mu\,(z\cdot(Xz))$, and likewise for $Y$. If $X\preceq Y$ and $0\le\mu$, then claim 5 of Elementary Arithmetic in an Ordered Field gives $\mu\,(z\cdot(Xz))\le\mu\,(z\cdot(Yz))$ for every $z$, that is $\mu X\preceq\mu Y$.

Claim 5. By claim 1 the matrix $Y-X$ is symmetric. For $z\in\mathbb{R}^n$, claim 1 of Linearity of the Matrix-Vector Product and the Quadratic Form as a Double Sum and claim 5 of Bilinearity and Symmetry of the Dot Product on $\mathbb{R}^n$ give

so by claim 3 of Elementary Arithmetic in an Ordered Field the inequality $0\le z\cdot((Y-X)z)$ holds if and only if $z\cdot(Xz)\le z\cdot(Yz)$. Quantifying over $z\in\mathbb{R}^n$ and comparing with Symmetric, Positive Semidefinite, and Positive Definite Real Matrices and Semidefinite Order on Symmetric Real Matrices gives claim 5.

Claim 6. Set $W=Y-X$, symmetric by claim 1. If $X\preceq Y$ and $Y\preceq X$, then for every $z\in\mathbb{R}^n$ both $z\cdot(Xz)\le z\cdot(Yz)$ and $z\cdot(Yz)\le z\cdot(Xz)$ hold, so $z\cdot(Xz)=z\cdot(Yz)$ by antisymmetry of the total order. As in the proof of claim 5 this gives

Let $u,v\in\mathbb{R}^n$. Taking $z=u+v$ and expanding by claim 3 of Linearity of the Matrix-Vector Product and the Quadratic Form as a Double Sum and claims 2 and 5 of Bilinearity and Symmetry of the Dot Product on $\mathbb{R}^n$,

By claim 4 of Linearity of the Matrix-Vector Product and the Quadratic Form as a Double Sum,

Interchanging the order of summation in the second double sum by Interchange of a Finite Double Sum and then renaming the two summation indices turns it into $\sum_{i=1}^{n}\sum_{j=1}^{n}W_{ji}\,v_j\,u_i$, which equals $u\cdot(Wv)$ because $W_{ji}=W_{ij}$. Hence $u\cdot(Wv)+u\cdot(Wv)=0$, that is $2\,\bigl(u\cdot(Wv)\bigr)=0$ with $2=1+1$; since $0<2$ by claim 8 of Elementary Order Arithmetic in an Ordered Field, the element $2$ is nonzero and invertible, and multiplying by $2^{-1}$ gives $u\cdot(Wv)=0$.

Finally, for $i\in[n]$ let $e_i\in\mathbb{R}^n$ be the point whose $i$th coordinate is $1$ and whose remaining coordinates are $0$, and let $i,j\in[n]$. In the double sum $\sum_{k=1}^{n}\sum_{l=1}^{n}W_{kl}(e_i)_k(e_j)_l$ every summand of the inner sum with $l\ne j$ vanishes, because $(e_j)_l=0$ and $0\,t=0$; so claim 7 of Properties of Finite Sums evaluates the inner sum as $W_{kj}(e_i)_k$. For the same reason every summand of the resulting outer sum with $k\ne i$ vanishes, and a second application of claim 7 evaluates the whole double sum as $W_{ij}$. Thus $W_{ij}=e_i\cdot(We_j)=0$ for all $i,j\in[n]$. By Difference of Real Matrices this reads $Y_{ij}-X_{ij}=0$, so $X_{ij}=Y_{ij}$ by claim 3 of Additive Cancellation and Elementary Additive Identities in a Field, and therefore $X=Y$.