[proofplan] Choose left symbols $a \in S^m(U \times \mathbb{R}^n)$ and $b \in S^{m'}(U \times \mathbb{R}^n)$ for $P$ and $Q$, modulo smoothing remainders. Proper support makes the composition globally defined on $U$, and the left-quantized composition formula supplies a left symbol $c \in S^{m+m'}(U \times \mathbb{R}^n)$ for $PQ$. The leading term of the asymptotic expansion of $c$ is $ab$, while every derivative term with positive multi-index has order at most $m+m'-1$. Passing to the quotient by $S^{m+m'-1}$ gives the product formula, and a final representative check shows that the product is independent of the chosen symbols. [/proofplan] [step:Choose left symbols representing the two operators] Let $C_c^\infty(U)$ denote the space of complex-valued smooth functions with compact support in $U$, let $\mathcal{D}'(U)$ denote the space of complex-valued distributions on $U$, and let $\mathcal{L}^n$ denote $n$-dimensional [Lebesgue measure](/page/Lebesgue%20Measure) on $\mathbb{R}^n$. For any order $s \in \mathbb{R}$ and any complex-valued symbol $p \in S^s(U \times \mathbb{R}^n)$, define \begin{align*} \operatorname{Op}_L(p): C_c^\infty(U) \to \mathcal{D}'(U), \qquad u \mapsto (2\pi)^{-n}\int_U\int_{\mathbb{R}^n} e^{i(x-y)\cdot \xi}p(x,\xi)u(y)\,d\mathcal{L}^n(\xi)\,d\mathcal{L}^n(y) \end{align*} as the left-quantized local pseudodifferential operator, interpreted in the standard oscillatory sense. Since $P \in \Psi^m_{\mathrm{prop}}(U)$, choose a left symbol \begin{align*} a: U \times \mathbb{R}^n \to \mathbb{C} \end{align*} with $a \in S^m(U \times \mathbb{R}^n)$ such that $P-\operatorname{Op}_L(a)$ is smoothing. Since $Q \in \Psi^{m'}_{\mathrm{prop}}(U)$, choose a left symbol \begin{align*} b: U \times \mathbb{R}^n \to \mathbb{C} \end{align*} with $b \in S^{m'}(U \times \mathbb{R}^n)$ such that $Q-\operatorname{Op}_L(b)$ is smoothing. The principal symbol classes are therefore represented by \begin{align*} \sigma_m(P) = [a] \in S^m(U \times \mathbb{R}^n)/S^{m-1}(U \times \mathbb{R}^n) \end{align*} and \begin{align*} \sigma_{m'}(Q) = [b] \in S^{m'}(U \times \mathbb{R}^n)/S^{m'-1}(U \times \mathbb{R}^n). \end{align*} [/step] [step:Use proper support to form the composition] Because $P$ and $Q$ are properly supported, their Schwartz kernels have proper support over $U$ in both variables. Hence the usual kernel composition is well-defined on compactly supported distributions and produces a properly supported operator. Thus $PQ$ is a well-defined properly supported operator on $U$. The hypotheses of the standard composition theorem in the properly supported left-quantized pseudodifferential calculus apply: $P$ and $Q$ are properly supported, and the preceding step represents them by left symbols $a \in S^m(U \times \mathbb{R}^n)$ and $b \in S^{m'}(U \times \mathbb{R}^n)$ modulo smoothing operators. Therefore the theorem states that $PQ \in \Psi^{m+m'}_{\mathrm{prop}}(U)$ and has a left symbol \begin{align*} c: U \times \mathbb{R}^n \to \mathbb{C} \end{align*} with $c \in S^{m+m'}(U \times \mathbb{R}^n)$ satisfying the asymptotic expansion \begin{align*} c(x,\xi) \sim \sum_{\alpha \in \mathbb{N}_0^n} \frac{1}{\alpha!}\partial_\xi^\alpha a(x,\xi)D_x^\alpha b(x,\xi). \end{align*} Here $\mathbb{N}_0 := \{0,1,2,\dots\}$, $\alpha = (\alpha_1,\dots,\alpha_n) \in \mathbb{N}_0^n$ is a multi-index, $\alpha! = \alpha_1!\cdots \alpha_n!$, $\partial_\xi^\alpha = \partial_{\xi_1}^{\alpha_1}\cdots\partial_{\xi_n}^{\alpha_n}$, and $D_x^\alpha$ denotes the left-quantization differential convention in the $x$ variable. The precise powers of $i$ in $D_x^\alpha$ affect only lower-order coefficients and not the leading term. This composition formula is the standard composition formula for left-quantized pseudodifferential operators in the local amplitude calculus. [/step] [step:Isolate the leading term in the composed symbol] The term of the expansion corresponding to $\alpha = 0$ is exactly \begin{align*} \frac{1}{0!}\partial_\xi^0 a(x,\xi)D_x^0 b(x,\xi) = a(x,\xi)b(x,\xi). \end{align*} Since $a \in S^m(U \times \mathbb{R}^n)$ and $b \in S^{m'}(U \times \mathbb{R}^n)$, the product estimate for scalar symbols gives \begin{align*} ab \in S^{m+m'}(U \times \mathbb{R}^n). \end{align*} For every multi-index $\alpha \in \mathbb{N}_0^n$ with $|\alpha| \geq 1$, symbol differentiation gives \begin{align*} \partial_\xi^\alpha a \in S^{m-|\alpha|}(U \times \mathbb{R}^n) \end{align*} and \begin{align*} D_x^\alpha b \in S^{m'}(U \times \mathbb{R}^n). \end{align*} Multiplying these two symbol estimates yields \begin{align*} \partial_\xi^\alpha a \, D_x^\alpha b \in S^{m+m'-|\alpha|}(U \times \mathbb{R}^n) \subset S^{m+m'-1}(U \times \mathbb{R}^n). \end{align*} Thus all terms with $|\alpha| \geq 1$ contribute only to order at most $m+m'-1$. [guided] Recall that $a \in S^m(U \times \mathbb{R}^n)$ and $b \in S^{m'}(U \times \mathbb{R}^n)$ are complex-valued left symbols representing $P$ and $Q$ modulo smoothing operators, and that $c \in S^{m+m'}(U \times \mathbb{R}^n)$ is the left symbol for the composed operator $PQ$ supplied by the properly supported left-symbol composition theorem. The principal symbol only records the top-order part of the full symbol. Therefore we must identify which term in the composition expansion has order $m+m'$ and prove that every other term has strictly smaller order. The expansion supplied by the left-symbol composition formula is \begin{align*} c(x,\xi) \sim \sum_{\alpha \in \mathbb{N}_0^n} \frac{1}{\alpha!}\partial_\xi^\alpha a(x,\xi)D_x^\alpha b(x,\xi). \end{align*} The multi-index $\alpha=0$ means $\partial_\xi^0$ and $D_x^0$ are the identity operators. Therefore the corresponding term is \begin{align*} \frac{1}{0!}\partial_\xi^0 a(x,\xi)D_x^0 b(x,\xi) = a(x,\xi)b(x,\xi). \end{align*} Because $a$ is a symbol of order $m$ and $b$ is a symbol of order $m'$, the symbol product estimate gives \begin{align*} ab \in S^{m+m'}(U \times \mathbb{R}^n). \end{align*} This is the only possible contributor to the principal symbol of order $m+m'$. Now take a multi-index $\alpha \in \mathbb{N}_0^n$ with $|\alpha| \geq 1$. Differentiating a symbol in the frequency variable lowers its order by the number of frequency derivatives, so \begin{align*} \partial_\xi^\alpha a \in S^{m-|\alpha|}(U \times \mathbb{R}^n). \end{align*} Differentiating in the base variable $x$ does not lower the symbol order in the standard local symbol classes, so \begin{align*} D_x^\alpha b \in S^{m'}(U \times \mathbb{R}^n). \end{align*} Multiplying these two symbols gives \begin{align*} \partial_\xi^\alpha a \, D_x^\alpha b \in S^{m-|\alpha|+m'}(U \times \mathbb{R}^n). \end{align*} Since $|\alpha| \geq 1$, we have $m-|\alpha|+m' \leq m+m'-1$, and therefore \begin{align*} \partial_\xi^\alpha a \, D_x^\alpha b \in S^{m+m'-1}(U \times \mathbb{R}^n). \end{align*} Thus the derivative terms are invisible in the quotient by $S^{m+m'-1}(U \times \mathbb{R}^n)$. This is exactly why the principal symbol of a composition is just the product of the two principal symbols: the noncommutative correction terms begin one order lower. [/guided] [/step] [step:Pass to the principal symbol quotient] By the meaning of the asymptotic expansion for the composed symbol, subtracting the terms with $|\alpha| < 1$ leaves a remainder in $S^{m+m'-1}(U \times \mathbb{R}^n)$. Since the only term with $|\alpha| < 1$ is the term $ab$ identified in the preceding step, the composed left symbol $c$ satisfies \begin{align*} c - ab \in S^{m+m'-1}(U \times \mathbb{R}^n). \end{align*} Therefore the principal symbol class of $PQ$ is \begin{align*} \sigma_{m+m'}(PQ) = [c] = [ab] \end{align*} in $S^{m+m'}(U \times \mathbb{R}^n)/S^{m+m'-1}(U \times \mathbb{R}^n)$. [/step] [step:Check that the product does not depend on the chosen representatives] Let $a_1 \in S^m(U \times \mathbb{R}^n)$ be another representative of $\sigma_m(P)$ and let $b_1 \in S^{m'}(U \times \mathbb{R}^n)$ be another representative of $\sigma_{m'}(Q)$. Then \begin{align*} a_1-a \in S^{m-1}(U \times \mathbb{R}^n) \end{align*} and \begin{align*} b_1-b \in S^{m'-1}(U \times \mathbb{R}^n). \end{align*} Using bilinearity of multiplication, write \begin{align*} a_1b_1-ab = (a_1-a)b + a(b_1-b) + (a_1-a)(b_1-b). \end{align*} The symbol product estimates give \begin{align*} (a_1-a)b \in S^{m+m'-1}(U \times \mathbb{R}^n), \end{align*} \begin{align*} a(b_1-b) \in S^{m+m'-1}(U \times \mathbb{R}^n), \end{align*} and \begin{align*} (a_1-a)(b_1-b) \in S^{m+m'-2}(U \times \mathbb{R}^n) \subset S^{m+m'-1}(U \times \mathbb{R}^n). \end{align*} Hence \begin{align*} a_1b_1-ab \in S^{m+m'-1}(U \times \mathbb{R}^n). \end{align*} Thus $[ab]$ depends only on $[a]$ and $[b]$. Combining this with the previous step gives \begin{align*} \sigma_{m+m'}(PQ) = \sigma_m(P)\sigma_{m'}(Q) \end{align*} in $S^{m+m'}(U \times \mathbb{R}^n)/S^{m+m'-1}(U \times \mathbb{R}^n)$, as claimed. [/step]