[proofplan]
Define the sesquilinear expression $(a,b)\mapsto \phi(b^*a)$ and use positivity of $\phi$ on elements of the form $x^*x$. The only point needing care is conjugate symmetry: since [positive linear functionals are Hermitian](/theorems/8556), $\phi(a^*b)=\overline{\phi(b^*a)}$. We then split into the case $\phi(b^*b)=0$, where varying a scalar parameter forces $\phi(b^*a)=0$, and the case $\phi(b^*b)>0$, where choosing the minimizing scalar gives the desired inequality.
[/proofplan]
[step:Record the Hermitian symmetry of the positive functional]
For $a,b\in A$, define the scalar
\begin{align*}
z:=\phi(b^*a).
\end{align*}
Since $\phi$ is a positive linear functional, [citetheorem:8556] gives
\begin{align*}
\phi(x^*)=\overline{\phi(x)}
\end{align*}
for every $x\in A$. Applying this to $x=b^*a$, whose adjoint is $a^*b$, yields
\begin{align*}
\phi(a^*b)=\overline{\phi(b^*a)}=\overline{z}.
\end{align*}
Also, positivity applied to $a^*a$ and $b^*b$ gives
\begin{align*}
\phi(a^*a)\geq 0, \qquad \phi(b^*b)\geq 0.
\end{align*}
[guided]
Fix $a,b\in A$, and set
\begin{align*}
z:=\phi(b^*a).
\end{align*}
The expression $\phi(b^*a)$ is the analogue of an [inner product](/page/Inner%20Product) term. To use the usual quadratic minimization argument, we need the conjugate term $\phi(a^*b)$ to equal $\overline{z}$.
This follows from the fact that positive linear functionals are Hermitian. More precisely, by [citetheorem:8556], because $\phi$ is positive, we have
\begin{align*}
\phi(x^*)=\overline{\phi(x)}
\end{align*}
for every $x\in A$. Taking $x=b^*a$, we have $x^*=a^*b$, so
\begin{align*}
\phi(a^*b)=\phi((b^*a)^*)=\overline{\phi(b^*a)}=\overline{z}.
\end{align*}
We will also use positivity on square elements. Since $a^*a$ and $b^*b$ are positive elements of the $C^*$-algebra, the definition of positive linear functional gives
\begin{align*}
\phi(a^*a)\geq 0, \qquad \phi(b^*b)\geq 0.
\end{align*}
These inequalities ensure that the quadratic expression below is a non-negative real number for every scalar parameter.
[/guided]
[/step]
[step:Expand the positive quadratic expression]
Let $\lambda\in\mathbb C$. Since $(a+\lambda b)^*(a+\lambda b)$ is positive in $A$, positivity of $\phi$ gives
\begin{align*}
0\leq \phi((a+\lambda b)^*(a+\lambda b)).
\end{align*}
Using linearity of $\phi$ and the identity
\begin{align*}
(a+\lambda b)^*(a+\lambda b)=a^*a+\lambda a^*b+\overline{\lambda}b^*a+|\lambda|^2b^*b
\end{align*}
we obtain
\begin{align*}
0\leq \phi(a^*a)+\lambda\overline{z}+\overline{\lambda}z+|\lambda|^2\phi(b^*b).
\end{align*}
[/step]
[step:Handle the case $\phi(b^*b)=0$ by varying the scalar]
Assume first that
\begin{align*}
\phi(b^*b)=0.
\end{align*}
Then the inequality from the previous step becomes, for every $\lambda\in\mathbb C$,
\begin{align*}
0\leq \phi(a^*a)+\lambda\overline{z}+\overline{\lambda}z.
\end{align*}
If $z\neq 0$, define the scalar-valued function
\begin{align*}
\lambda_t:(0,\infty)\to\mathbb C,\qquad t\mapsto -tz
\end{align*}
for $t>0$. Substituting $\lambda=\lambda_t$ gives
\begin{align*}
0\leq \phi(a^*a)-2t|z|^2
\end{align*}
for every $t>0$, which is impossible for all sufficiently large $t$. Hence $z=0$. Therefore
\begin{align*}
|\phi(b^*a)|^2=|z|^2=0=\phi(a^*a)\phi(b^*b),
\end{align*}
so the desired inequality holds in this case.
[/step]
[step:Choose the minimizing scalar when $\phi(b^*b)>0$]
Assume now that
\begin{align*}
\phi(b^*b)>0.
\end{align*}
Define
\begin{align*}
\lambda_0:=-\frac{z}{\phi(b^*b)}.
\end{align*}
Substituting $\lambda=\lambda_0$ into the quadratic inequality gives
\begin{align*}
0\leq \phi(a^*a)-\frac{|z|^2}{\phi(b^*b)}
\end{align*}
Then multiplying by the positive real number $\phi(b^*b)$ yields
\begin{align*}
|z|^2\leq \phi(a^*a)\phi(b^*b).
\end{align*}
Since $z=\phi(b^*a)$, this is exactly
\begin{align*}
|\phi(b^*a)|^2\leq \phi(a^*a)\phi(b^*b).
\end{align*}
[/step]
[step:Conclude the inequality for all pairs of elements]
The two cases $\phi(b^*b)=0$ and $\phi(b^*b)>0$ exhaust all possibilities because $\phi(b^*b)\geq 0$. Therefore, for every $a,b\in A$,
\begin{align*}
|\phi(b^*a)|^2\leq \phi(a^*a)\phi(b^*b).
\end{align*}
This proves the [Cauchy-Schwarz inequality](/theorems/432) for the positive linear functional $\phi$.
[/step]
