[proofplan]
We prove exactness by checking each term of the sequence. The inclusion $\Psi^{m-1}(U) \hookrightarrow \Psi^m(U)$ is injective by the order filtration, and the principal symbol map is well-defined by the stated local left-symbol kernel property: a left symbol whose quantisation is smoothing is a smoothing symbol, hence belongs to every lower symbol class. Surjectivity follows by quantising an arbitrary order-$m$ symbol. Finally, the kernel of $\sigma_m$ consists exactly of those operators whose order-$m$ symbol class vanishes, which is precisely the condition that the operator has order at most $m-1$ modulo smoothing.
[/proofplan]
[step:Verify that the order filtration gives an injective first map]
The map
\begin{align*}
\iota: \Psi^{m-1}(U) \to \Psi^m(U)
\end{align*}
is the inclusion coming from the symbol-space inclusion
\begin{align*}
S^{m-1}(U \times \mathbb{R}^n) \subset S^m(U \times \mathbb{R}^n).
\end{align*}
Thus if $P \in \Psi^{m-1}(U)$ maps to $0$ in $\Psi^m(U)$, then $P$ is the zero class modulo smoothing operators. Hence $P = 0$ already in $\Psi^{m-1}(U)$, so $\iota$ is injective. Exactness at the first nonzero term follows.
[/step]
[step:Show that the principal symbol map is well-defined]
Let $P \in \Psi^m(U)$. Suppose $a,b \in S^m(U \times \mathbb{R}^n)$ are two left-symbol representatives of $P$, meaning that
\begin{align*}
P - \operatorname{Op}_L(a)
\end{align*}
and
\begin{align*}
P - \operatorname{Op}_L(b)
\end{align*}
are smoothing operators. Subtracting these two relations gives that
\begin{align*}
\operatorname{Op}_L(a-b)
\end{align*}
is smoothing modulo the same local convention. Set
\begin{align*}
c := a-b \in S^m(U \times \mathbb{R}^n).
\end{align*}
We now use the local left-symbol kernel property stated in the theorem. Its hypotheses are satisfied because $c$ is a left symbol of order $m$ on $U \times \mathbb{R}^n$ and $\operatorname{Op}_L(c)$ is smoothing. Therefore
\begin{align*}
c \in S^{-\infty}(U \times \mathbb{R}^n) := \bigcap_{r \in \mathbb{R}} S^r(U \times \mathbb{R}^n).
\end{align*}
In particular,
\begin{align*}
a-b = c \in S^{m-1}(U \times \mathbb{R}^n).
\end{align*}
Therefore $[a]=[b]$ in $S^m(U \times \mathbb{R}^n)/S^{m-1}(U \times \mathbb{R}^n)$, so $\sigma_m(P)$ is independent of the chosen representative.
[guided]
We must check that $\sigma_m(P)$ depends only on the operator $P$, not on the particular left symbol used to write it. Let $a,b \in S^m(U \times \mathbb{R}^n)$ be two possible representatives of the same operator $P \in \Psi^m(U)$. This means that both differences
\begin{align*}
P - \operatorname{Op}_L(a)
\end{align*}
and
\begin{align*}
P - \operatorname{Op}_L(b)
\end{align*}
are smoothing operators.
Subtract the second relation from the first. The operator represented by the symbol difference $a-b$ is then smoothing modulo the local convention:
\begin{align*}
\operatorname{Op}_L(a-b)
\end{align*}
is smoothing. Define the difference symbol
\begin{align*}
c := a-b \in S^m(U \times \mathbb{R}^n).
\end{align*}
The point of introducing $c$ is to isolate the one analytic input needed here. We use the local left-symbol kernel property stated in the theorem: if $r \in \mathbb{R}$, $c_0 \in S^r(U \times \mathbb{R}^n)$, and $\operatorname{Op}_L(c_0)$ is smoothing, then $c_0 \in S^{-\infty}(U \times \mathbb{R}^n)$. The hypotheses match with $r=m$ and $c_0=c$, because $c=a-b$ is an order-$m$ left symbol and $\operatorname{Op}_L(c)$ is smoothing. Therefore
\begin{align*}
c \in S^{-\infty}(U \times \mathbb{R}^n) := \bigcap_{r \in \mathbb{R}} S^r(U \times \mathbb{R}^n).
\end{align*}
Since $S^{-\infty}(U \times \mathbb{R}^n) \subset S^{m-1}(U \times \mathbb{R}^n)$, we obtain
\begin{align*}
a-b = c \in S^{m-1}(U \times \mathbb{R}^n).
\end{align*}
Hence $a$ and $b$ determine the same coset:
\begin{align*}
[a]=[b]
\end{align*}
in $S^m(U \times \mathbb{R}^n)/S^{m-1}(U \times \mathbb{R}^n)$. Therefore the assignment $P \mapsto [a]$ is well-defined.
[/guided]
[/step]
[step:Quantise an arbitrary order-$m$ symbol to prove surjectivity]
Let $[a] \in S^m(U \times \mathbb{R}^n)/S^{m-1}(U \times \mathbb{R}^n)$, with representative $a \in S^m(U \times \mathbb{R}^n)$. Define
\begin{align*}
P := \operatorname{Op}_L(a) \in \Psi^m(U).
\end{align*}
By the definition of $\sigma_m$,
\begin{align*}
\sigma_m(P) = [a].
\end{align*}
Thus every element of the quotient is in the image of $\sigma_m$, so $\sigma_m$ is surjective. Exactness at the final term follows.
[/step]
[step:Identify every lower-order operator as an element of the kernel]
Let $P \in \Psi^{m-1}(U)$. Choose a left-symbol representative $b \in S^{m-1}(U \times \mathbb{R}^n)$ such that
\begin{align*}
P = \operatorname{Op}_L(b)
\end{align*}
modulo a smoothing operator. Since
\begin{align*}
S^{m-1}(U \times \mathbb{R}^n) \subset S^m(U \times \mathbb{R}^n),
\end{align*}
we may also regard $b$ as an order-$m$ symbol. Its class in the quotient by $S^{m-1}(U \times \mathbb{R}^n)$ is zero:
\begin{align*}
[b]=0.
\end{align*}
Therefore
\begin{align*}
\sigma_m(P)=0,
\end{align*}
so $\Psi^{m-1}(U) \subseteq \ker \sigma_m$.
[/step]
[step:Use vanishing of the principal symbol to lower the order]
Let $P \in \ker \sigma_m$. Choose a left-symbol representative $a \in S^m(U \times \mathbb{R}^n)$ such that
\begin{align*}
P = \operatorname{Op}_L(a)
\end{align*}
modulo a smoothing operator. Since $\sigma_m(P)=0$, we have
\begin{align*}
[a]=0
\end{align*}
in $S^m(U \times \mathbb{R}^n)/S^{m-1}(U \times \mathbb{R}^n)$. By the definition of the quotient, this means
\begin{align*}
a \in S^{m-1}(U \times \mathbb{R}^n).
\end{align*}
Hence $\operatorname{Op}_L(a) \in \Psi^{m-1}(U)$. A smoothing operator belongs to $\Psi^r(U)$ for every $r \in \mathbb{R}$, because smoothing symbols lie in
\begin{align*}
S^{-\infty}(U \times \mathbb{R}^n) := \bigcap_{r \in \mathbb{R}} S^r(U \times \mathbb{R}^n).
\end{align*}
In particular, every smoothing remainder is an element of $\Psi^{m-1}(U)$. Therefore the equality of $P$ with $\operatorname{Op}_L(a)$ modulo smoothing implies
\begin{align*}
P \in \Psi^{m-1}(U).
\end{align*}
Thus $\ker \sigma_m \subseteq \Psi^{m-1}(U)$.
[/step]
[step:Combine the inclusions to obtain exactness of the sequence]
The first map is injective, $\sigma_m$ is surjective, and the two kernel inclusions give
\begin{align*}
\ker \sigma_m = \Psi^{m-1}(U).
\end{align*}
Since the image of the inclusion $\Psi^{m-1}(U) \hookrightarrow \Psi^m(U)$ is exactly $\Psi^{m-1}(U)$, we have
\begin{align*}
\operatorname{im}\iota = \ker \sigma_m.
\end{align*}
Therefore the displayed sequence is exact at every term.
[/step]
