The real trace pairing on finite Hermitian matrices is an inner product

For Hermitian $A,B$, $\overline{\mathrm{Tr}(AB)}=\mathrm{Tr}((AB{)}^{\ast })=\mathrm{Tr}(BA)=\mathrm{Tr}(AB)$ by [F2]. The trace is additive and real-homogeneous, so the pairing is real-valued, symmetric, and real-bilinear.

Diagonalize $A\in {\mathsf{H}}_d$ by [F3] with real eigenvalues ${\lambda }_1,\dots ,{\lambda }_d$. Then $\mathrm{Tr}(A^2)={\sum }_j{\lambda }_j^2\ge 0$, with equality exactly when all ${\lambda }_j=0$, hence exactly when $A=0$. This proves positive definiteness and the displayed square-root formula.

For $c\in {\mathbb{R}}^m$, bilinearity gives $c^{\mathsf{T}}Gc=\mathrm{Tr}((Sc{)}^2)=\mathrm{\parallel }Sc{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}^2\ge 0$. For $X\in {\mathsf{H}}_d$, the vector $v$ with coordinates $v_a=\mathrm{Tr}(F_{a}X)$ satisfies $⟨Sc,X{⟩}_{\mathrm{H}\mathrm{S}}=c^{\mathsf{T}}v$ for every $c$, so it is $S^{\ast }X$. By [F2], $v_a=\mathrm{Tr}(X{F}_a)$; hence the matrix of $S^{\ast }S$ is precisely $G$. The equality $⟨c,Gc⟩=\mathrm{\parallel }Sc{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}^2$ implies $\ker G=\ker S$: $Sc=0$ gives $Gc=0$, while $Gc=0$ gives $\mathrm{\parallel }Sc{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}^2=0$ and hence $Sc=0$ by step 2.1. By [F4], $\mathrm{\mid }⟨A,B{⟩}_{\mathrm{H}\mathrm{S}}\mathrm{\mid }\le \mathrm{\parallel }A{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}\mathrm{\parallel }B{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}$; expanding $\mathrm{\parallel }A+B{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}^2$ and applying this bound gives $\mathrm{\parallel }A+B{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}\le \mathrm{\parallel }A{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}+\mathrm{\parallel }B{\mathrm{\parallel }}_{\mathrm{H}\mathrm{S}}$. Thus the formula is a norm.