## Formalized Name Algebra Property of Properly Supported Semiclassical Pseudodifferential Operators ## Formalized Statement Let $M$ be a smooth manifold, let $h \in (0,h_0]$ be the semiclassical parameter, and fix a properly supported semiclassical pseudodifferential calculus on $M$ defined in local coordinate charts by left semiclassical quantization of symbols in $S^m(T^*M)$, with the standard coordinate-change invariance and local Euclidean composition formula for semiclassical left quantization. Let $\Psi_h^{-\infty}(M)$ denote the residual class consisting of smoothing operators whose Schwartz kernels are $O(h^N)$ in $C^\infty$ for every $N \in \mathbb N$. For each $m \in \mathbb R$, let \begin{align*} \sigma_h : \Psi_h^m(M) \to S^m(T^*M) /\bigl(hS^{m-1}(T^*M)+S^{-\infty}(T^*M)\bigr) \end{align*} be the corresponding semiclassical principal symbol map. If $m,m' \in \mathbb R$, $A \in \Psi_h^m(M)$ and $B \in \Psi_h^{m'}(M)$ are properly supported operators, then $AB$ is a properly supported element of $\Psi_h^{m+m'}(M)$, and \begin{align*} \sigma_h(AB)=\sigma_h(A)\sigma_h(B) \end{align*} in \begin{align*} S^{m+m'}(T^*M) /\bigl(hS^{m+m'-1}(T^*M)+S^{-\infty}(T^*M)\bigr). \end{align*} ## Proof [proofplan] We localize both operators by a finite coordinate partition on the compact region relevant to a properly supported composition. Localized pieces whose cutoffs are separated have residual kernels by semiclassical nonstationary phase, while localized pieces supported in one coordinate chart are composed by the Euclidean semiclassical composition formula. The local principal symbols are the products of the local principal symbols, and these products patch because the principal symbol transformation law for the fixed global calculus is multiplicative. Finally, proper support is checked directly from the support relations of the two kernels. [/proofplan] [step:Localize the composition with an explicit cutoff identity] Let $K_A \in \mathcal{D}'(M \times M)$ and $K_B \in \mathcal{D}'(M \times M)$ denote the Schwartz kernels of $A$ and $B$, respectively. Let $R_A := \operatorname{supp} K_A \subset M \times M$ and $R_B := \operatorname{supp} K_B \subset M \times M$ denote their support relations. Proper support means that both coordinate projections from $R_A$ and $R_B$ to $M$ are proper maps. Choose a locally finite family of coordinate charts $(U_i,\varphi_i)_{i \in I}$ on $M$ and a subordinate partition of unity $(\chi_i)_{i \in I}$, where each $\chi_i: M \to [0,1]$ is a smooth compactly supported function with $\operatorname{supp}\chi_i \subset U_i$. Choose smooth functions $\widetilde{\chi}_i: M \to [0,1]$ such that $\widetilde{\chi}_i=1$ on a neighbourhood of $\operatorname{supp}\chi_i$ and $\operatorname{supp}\widetilde{\chi}_i \subset U_i$. For each $i,j,k \in I$, define the localized operator \begin{align*} C_{ijk} := \chi_i A \widetilde{\chi}_j \chi_j B \widetilde{\chi}_k. \end{align*} Here multiplication by a cutoff is the operator on $C_c^\infty(M)$ induced by pointwise multiplication. Since $\sum_{i \in I}\chi_i=1$ locally finitely, for every $u \in C_c^\infty(M)$ one has \begin{align*} ABu=\sum_{i,j,k \in I}\chi_i A\chi_j B\chi_k u. \end{align*} For each summand we insert the auxiliary cutoffs and write \begin{align*} \chi_i A\chi_j B\chi_k=\chi_i A\widetilde{\chi}_j\chi_j B\widetilde{\chi}_k\chi_k+\chi_i A(1-\widetilde{\chi}_j)\chi_j B\chi_k+\chi_i A\widetilde{\chi}_j\chi_j B(1-\widetilde{\chi}_k)\chi_k. \end{align*} The first term is $C_{ijk}\chi_k$. In the second term, $\operatorname{supp}(1-\widetilde{\chi}_j)$ is disjoint from a neighbourhood of $\operatorname{supp}\chi_j$; in the third term, $\operatorname{supp}(1-\widetilde{\chi}_k)$ is disjoint from a neighbourhood of $\operatorname{supp}\chi_k$. These are precisely separated cutoff terms for the kernels of $A$ and $B$. For compact sets $K_0,K_1 \subset M$, only finitely many triples $(i,j,k)$ can contribute to the restriction from inputs supported in $K_1$ to outputs in $K_0$. Indeed, properness of $R_A$ over the first factor makes $R_A \cap (K_0 \times M)$ compact, its second projection is compact, properness of $R_B$ over the first factor then makes the relevant set of possible input points compact, and local finiteness of the cover leaves only finitely many cutoffs meeting these compact sets. Hence the displayed sums are locally finite as operator identities on compactly supported inputs. [guided] We need a localization identity, not merely a heuristic partition argument. Let $K_A$ and $K_B$ denote the Schwartz kernels of $A$ and $B$, and set \begin{align*} R_A := \operatorname{supp} K_A \subset M \times M \end{align*} and \begin{align*} R_B := \operatorname{supp} K_B \subset M \times M. \end{align*} The proper support hypothesis says that the two coordinate projections from each of $R_A$ and $R_B$ to $M$ are proper maps. Choose coordinate charts $(U_i,\varphi_i)_{i \in I}$ and a locally finite smooth partition of unity $(\chi_i)_{i \in I}$ with $\operatorname{supp}\chi_i \subset U_i$. For every $i \in I$, choose $\widetilde{\chi}_i: M \to [0,1]$ such that $\widetilde{\chi}_i=1$ on a neighbourhood of $\operatorname{supp}\chi_i$ and $\operatorname{supp}\widetilde{\chi}_i \subset U_i$. The auxiliary cutoff is needed because the kernel of a pseudodifferential operator is singular only near the diagonal; when the two cutoffs are separated, the oscillatory integral has no stationary point and becomes residual. For $u \in C_c^\infty(M)$, the locally finite partition of unity gives \begin{align*} ABu=\sum_{i,j,k \in I}\chi_i A\chi_j B\chi_k u. \end{align*} For each triple we insert the auxiliary cutoffs by the algebraic identity $1=\widetilde{\chi}_j+(1-\widetilde{\chi}_j)$ before $\chi_j$ and $1=\widetilde{\chi}_k+(1-\widetilde{\chi}_k)$ before $\chi_k$. This gives \begin{align*} \chi_i A\chi_j B\chi_k=\chi_i A\widetilde{\chi}_j\chi_j B\widetilde{\chi}_k\chi_k+\chi_i A(1-\widetilde{\chi}_j)\chi_j B\chi_k+\chi_i A\widetilde{\chi}_j\chi_j B(1-\widetilde{\chi}_k)\chi_k. \end{align*} Define \begin{align*} C_{ijk}:=\chi_i A\widetilde{\chi}_j\chi_j B\widetilde{\chi}_k. \end{align*} The first term is the coordinate-supported piece $C_{ijk}\chi_k$. In the second term, $1-\widetilde{\chi}_j$ is supported away from $\chi_j$; in the third term, $1-\widetilde{\chi}_k$ is supported away from $\chi_k$. Thus the error terms are not mysterious remainders: they are exactly the separated cutoff terms that will be proved residual by nonstationary phase. It remains to justify local finiteness on compact input-output regions. Let $K_0,K_1 \subset M$ be compact. If an output point $x \in K_0$ can be linked by $A$ to an intermediate point $y$, then $(x,y) \in R_A$. Since the projection $R_A \to M$ onto the first factor is proper, the set $R_A \cap (K_0 \times M)$ is compact; hence its second projection is compact. Call that compact set $L_0$. If the intermediate point lies in $L_0$ and is linked by $B$ to an input point $z$, then $(y,z) \in R_B$. Properness of $R_B \to M$ over the first factor makes $R_B \cap (L_0 \times M)$ compact, and its second projection is compact. Because the chart family is locally finite, only finitely many $\chi_i$, $\chi_j$, and $\chi_k$ meet the compact sets just constructed and $K_1$. Therefore only finitely many triples affect the operator between these compact regions. [/guided] [/step] [step:Discard separated cutoff terms by semiclassical nonstationary phase] Consider a localized term in which the two cutoffs adjacent to one kernel have disjoint supports contained in coordinate charts $(U,\varphi)$ and $(U',\varphi')$. After inserting one more finite partition of unity on the compact set relevant to the term, each piece either has disjoint coordinate images in a single chart or is written in one chart by the coordinate-change invariance built into the fixed calculus. Thus it is enough to treat a kernel of the form \begin{align*} K_h(x,y)=(2\pi h)^{-n}\int_{\mathbb R^n} e^{i(\varphi(x)-\varphi(y))\cdot \xi/h} q(x,y,\xi;h)\,d\mathcal L^n(\xi), \end{align*} where $q$ is compactly supported in $(x,y)$, satisfies the usual uniform symbol estimates in $\xi$, and the cutoffs force $|\varphi(x)-\varphi(y)|\ge \delta$ for some $\delta>0$ on the support of $q$. Define the differential operator \begin{align*} L:=\frac{h}{i|\varphi(x)-\varphi(y)|^2}\sum_{r=1}^n (\varphi_r(x)-\varphi_r(y))\partial_{\xi_r}. \end{align*} Then $L e^{i(\varphi(x)-\varphi(y))\cdot \xi/h}=e^{i(\varphi(x)-\varphi(y))\cdot \xi/h}$. Integrating by parts $N$ times with the formal transpose $L^t$ gives \begin{align*} K_h(x,y)=(2\pi h)^{-n}\int_{\mathbb R^n} e^{i(\varphi(x)-\varphi(y))\cdot \xi/h}(L^t)^N q(x,y,\xi;h)\,d\mathcal L^n(\xi). \end{align*} Each application of $L^t$ contributes a factor $h$ and differentiates the symbol in $\xi$, while the denominator is bounded by $\delta^{-1}$ on the support. The uniform symbol estimates for $q$ therefore imply that every $x$- and $y$-derivative of $K_h$ is $O(h^N)$ after increasing the number of integrations by parts. Hence the kernel is smooth and $O(h^N)$ in every $C^\infty$ seminorm for each $N \in \mathbb N$. This is exactly the residual condition defining $\Psi_h^{-\infty}(M)$. [guided] The separated cutoff terms are residual because their oscillatory kernels have no stationary point in the fiber variable. After refining by finitely many coordinate cutoffs on the compact region under consideration and using the coordinate-change invariance of the fixed calculus, such a term has local kernel \begin{align*} K_h(x,y)=(2\pi h)^{-n}\int_{\mathbb R^n} e^{i(\varphi(x)-\varphi(y))\cdot \xi/h} q(x,y,\xi;h)\,d\mathcal L^n(\xi). \end{align*} Here $q$ is compactly supported in the base variables $(x,y)$ because all outer cutoffs are compactly supported, and $q$ satisfies uniform semiclassical symbol estimates in $\xi$ because it is obtained from a localized symbol of $A$ or $B$ by multiplication with smooth cutoffs and coordinate changes. The separation of the two cutoffs gives a number $\delta>0$ such that \begin{align*} |\varphi(x)-\varphi(y)|\ge \delta \end{align*} on the support of $q$. We now use semiclassical nonstationary phase in its elementary integration-by-parts form. Define \begin{align*} L:=\frac{h}{i|\varphi(x)-\varphi(y)|^2}\sum_{r=1}^n (\varphi_r(x)-\varphi_r(y))\partial_{\xi_r}. \end{align*} This operator is chosen so that differentiating the exponential reproduces the exponential: \begin{align*} L e^{i(\varphi(x)-\varphi(y))\cdot \xi/h}=e^{i(\varphi(x)-\varphi(y))\cdot \xi/h}. \end{align*} Because $|\varphi(x)-\varphi(y)|$ is bounded below by $\delta$, the coefficients of $L$ and all their base-variable derivatives are uniformly bounded on the support of $q$. Integrating by parts $N$ times in the variable $\xi$ gives \begin{align*} K_h(x,y)=(2\pi h)^{-n}\int_{\mathbb R^n} e^{i(\varphi(x)-\varphi(y))\cdot \xi/h}(L^t)^N q(x,y,\xi;h)\,d\mathcal L^n(\xi). \end{align*} The formal transpose $L^t$ differentiates only the amplitude in $\xi$ and contributes one factor of $h$ at each application. Symbol estimates imply that $(L^t)^Nq$ is bounded by $h^N$ times a symbol of sufficiently negative order after choosing $N$ large enough relative to the requested seminorm. Differentiating the kernel in $x$ or $y$ only differentiates the compactly supported amplitude and the smooth bounded coefficients, so the same argument applies to every $C^\infty$ seminorm. Therefore the separated kernel is smooth and is $O(h^N)$ in every $C^\infty$ seminorm for every $N \in \mathbb N$, which is precisely membership in $\Psi_h^{-\infty}(M)$. [/guided] [/step] [step:Reduce mixed-chart pieces to Euclidean composition] It remains to treat $C_{ijk}$ after the separated terms have been discarded. The three cutoffs need not lie in one coordinate chart. We therefore keep the output, middle, and input charts distinct: write \begin{align*} V_i:=\varphi_i(U_i), \qquad V_j:=\varphi_j(U_j), \qquad V_k:=\varphi_k(U_k). \end{align*} The localized factor $\chi_iA\widetilde{\chi}_j$ is an operator from functions supported in $U_j$ to functions supported in $U_i$, and the localized factor $\chi_jB\widetilde{\chi}_k$ is an operator from functions supported in $U_k$ to functions supported in $U_j$. By the coordinate-change invariance included in the fixed manifold calculus, each mixed-chart localized factor is, modulo a residual operator, represented in the middle chart by a left semiclassical quantization with a uniform symbol. More precisely, after conjugating by the chart maps and the compactly supported cutoff multipliers, there are symbols \begin{align*} a_{ij} \in S^m(V_j \times \mathbb R^n) \end{align*} and \begin{align*} b_{jk} \in S^{m'}(V_j \times \mathbb R^n) \end{align*} such that the two factors are represented modulo $\Psi_h^{-\infty}$ by $\operatorname{Op}_h(a_{ij})$ and $\operatorname{Op}_h(b_{jk})$ on $V_j$. The symbol estimates are uniform because all base-variable supports are compact and the coordinate transition maps have bounded derivatives of every order on those compact supports. The Euclidean semiclassical composition formula for left quantization applies to these two operators: $a_{ij}$ and $b_{jk}$ satisfy the symbol estimates of orders $m$ and $m'$, and the compact cutoff supports give proper support in the base variables. Hence \begin{align*} \operatorname{Op}_h(a_{ij})\operatorname{Op}_h(b_{jk})=\operatorname{Op}_h(c_{ijk})+R_{ijk,h}, \end{align*} where $R_{ijk,h}\in \Psi_h^{-\infty}(V_j)$ and $c_{ijk}\in S^{m+m'}(V_j\times \mathbb R^n)$ satisfies \begin{align*} c_{ijk}-a_{ij}b_{jk}\in hS^{m+m'-1}(V_j\times \mathbb R^n). \end{align*} Conjugating back by the coordinate maps preserves the class $\Psi_h^{m+m'}$ and preserves the principal symbol modulo $hS^{m+m'-1}+S^{-\infty}$ according to the same coordinate-change law. Therefore every overlapping mixed-chart localized composition belongs to $\Psi_h^{m+m'}(M)$, and its local principal symbol is the product of the local principal symbols of the two factors. [guided] The point of this step is that the indices $i,j,k$ do not imply that $U_i$, $U_j$, and $U_k$ sit inside one larger coordinate chart. The composition has an output chart, a middle chart, and an input chart. We name their coordinate images \begin{align*} V_i:=\varphi_i(U_i), \qquad V_j:=\varphi_j(U_j), \qquad V_k:=\varphi_k(U_k). \end{align*} The factor $\chi_iA\widetilde{\chi}_j$ takes input localized in $U_j$ and output localized in $U_i$, while $\chi_jB\widetilde{\chi}_k$ takes input localized in $U_k$ and output localized in $U_j$. The fixed calculus on $M$ includes the standard coordinate-change invariance for semiclassical left quantization. This result says that if a localized pseudodifferential operator is written in one chart and then conjugated by a smooth coordinate transition map, the result is again a left-quantized semiclassical pseudodifferential operator of the same order, modulo a residual operator, and its principal symbol is transformed by the induced cotangent map modulo $hS^{m-1}+S^{-\infty}$. Its hypotheses are met here because all cutoffs have compact support inside coordinate domains, so every coordinate transition is used only on a compact set where all derivatives of the transition map are bounded. Applying this coordinate-change result to the two localized factors, we may represent both of them in the middle chart $V_j$ modulo residual operators. Thus there are symbols \begin{align*} a_{ij}\in S^m(V_j\times\mathbb R^n) \end{align*} and \begin{align*} b_{jk}\in S^{m'}(V_j\times\mathbb R^n) \end{align*} such that the two factors become $\operatorname{Op}_h(a_{ij})$ and $\operatorname{Op}_h(b_{jk})$ on $V_j$, modulo $\Psi_h^{-\infty}$. Multiplication by the compactly supported cutoffs preserves symbol estimates, and coordinate changes preserve symbol estimates on compact subsets; hence the hypotheses of the Euclidean composition formula are satisfied. The Euclidean semiclassical composition formula for left quantization then gives \begin{align*} \operatorname{Op}_h(a_{ij})\operatorname{Op}_h(b_{jk})=\operatorname{Op}_h(c_{ijk})+R_{ijk,h}, \end{align*} where $R_{ijk,h}\in\Psi_h^{-\infty}(V_j)$ and $c_{ijk}\in S^{m+m'}(V_j\times\mathbb R^n)$. The first term in the asymptotic expansion of $c_{ijk}$ is the product of the two symbols, and all remaining first-order semiclassical corrections lie one power of $h$ lower in symbolic order: \begin{align*} c_{ijk}-a_{ij}b_{jk}\in hS^{m+m'-1}(V_j\times\mathbb R^n). \end{align*} Finally, conjugating this expression back to the manifold does not change the operator class and transforms the principal symbol by the prescribed cotangent coordinate law. Therefore the mixed-chart localized composition is a member of $\Psi_h^{m+m'}(M)$, and its principal symbol is the product of the two local principal symbols in the quotient defining $\sigma_h$. [/guided] [/step] [step:Patch the local products into a global principal symbol] Let $a_i \in S^m(T^*U_i)$ denote the local representative of $\sigma_h(A)$ on $U_i$, and let $b_i \in S^{m'}(T^*U_i)$ denote the local representative of $\sigma_h(B)$ on $U_i$. The global calculus fixed in the statement defines the principal symbol by quotienting local symbols modulo $hS^{m-1}+S^{-\infty}$ and requiring the standard coordinate transformation law on overlaps. On an overlap $U_i \cap U_j$, the principal symbol transformation law sends $a_i$ to $a_j$ modulo $hS^{m-1}+S^{-\infty}$ and sends $b_i$ to $b_j$ modulo $hS^{m'-1}+S^{-\infty}$. Multiplying these congruences gives \begin{align*} a_i b_i-a_j b_j \in hS^{m+m'-1}(T^*(U_i \cap U_j))+S^{-\infty}(T^*(U_i \cap U_j)). \end{align*} Thus the local products $a_i b_i$ define a global class in \begin{align*} S^{m+m'}(T^*M)/\bigl(hS^{m+m'-1}(T^*M)+S^{-\infty}(T^*M)\bigr). \end{align*} By the preceding step, this class is the principal symbol of every localized mixed-chart composition. Residual terms have zero image under $\sigma_h$, and the locally finite sum preserves the same global class. Hence it is the global principal symbol of $AB$. [guided] We now check that the symbol computed in local coordinates is independent of the chart in the quotient used to define $\sigma_h$. Let $a_i\in S^m(T^*U_i)$ represent the principal symbol of $A$ on $U_i$, and let $b_i\in S^{m'}(T^*U_i)$ represent the principal symbol of $B$ on $U_i$. On an overlap $U_i\cap U_j$, the coordinate transformation law for the fixed calculus gives \begin{align*} a_i-a_j\in hS^{m-1}(T^*(U_i\cap U_j))+S^{-\infty}(T^*(U_i\cap U_j)) \end{align*} after applying the appropriate cotangent coordinate change, and similarly \begin{align*} b_i-b_j\in hS^{m'-1}(T^*(U_i\cap U_j))+S^{-\infty}(T^*(U_i\cap U_j)). \end{align*} Multiplying the two congruences is legitimate because products of symbols add orders, products with residual symbols remain residual, and a factor in $hS^{m-1}$ multiplied by a symbol of order $m'$ lies in $hS^{m+m'-1}$. Therefore \begin{align*} a_i b_i-a_j b_j\in hS^{m+m'-1}(T^*(U_i\cap U_j))+S^{-\infty}(T^*(U_i\cap U_j)). \end{align*} So the products $a_i b_i$ patch to a well-defined global symbol class in \begin{align*} S^{m+m'}(T^*M)/\bigl(hS^{m+m'-1}(T^*M)+S^{-\infty}(T^*M)\bigr). \end{align*} The mixed-chart composition step computed the principal symbol of each localized summand to be precisely this product class. The separated summands are residual and therefore contribute zero to the principal symbol. Since the localized sum is locally finite, the same class is the principal symbol of the global composition $AB$. [/guided] [/step] [step:Verify proper support of the composed operator] Let $K_{AB}\in\mathcal D'(M\times M)$ denote the Schwartz kernel of $AB$, and set \begin{align*} S_{AB}:=\operatorname{supp}K_{AB}\subset M\times M. \end{align*} The support inclusion for composition of kernels gives \begin{align*} S_{AB}\subset \{(x,z)\in M\times M:\text{there exists }y\in M\text{ with }(x,y)\in R_A\text{ and }(y,z)\in R_B\}. \end{align*} We prove properness for the closed set $S_{AB}$ itself. Let $K \subset M$ be compact. Define \begin{align*} Y_K := \{y \in M : \text{there exists } x \in K \text{ with } (x,y)\in R_A\}. \end{align*} Since the projection $R_A \to M$ onto the first factor is proper, $R_A \cap (K \times M)$ is compact. Therefore $Y_K$ is compact as the continuous image of this compact set under the second projection. Define \begin{align*} Z_K := \{z \in M : \text{there exists } y \in Y_K \text{ with } (y,z)\in R_B\}. \end{align*} Since the projection $R_B \to M$ onto the first factor is proper, $R_B \cap (Y_K \times M)$ is compact, and therefore $Z_K$ is compact. If $(x,z)\in S_{AB}$ and $x \in K$, then the support inclusion implies $z \in Z_K$, so \begin{align*} S_{AB}\cap (K \times M) \subset K \times Z_K. \end{align*} The set $S_{AB}$ is closed because it is the support of a distribution. Hence $S_{AB}\cap (K\times M)$ is closed in the compact set $K\times Z_K$, and is compact. This proves properness of the first projection from $S_{AB}$ to $M$. For the second projection, define for compact $K\subset M$ the compact set of possible intermediate points using properness of $R_B\to M$ over the second factor, and then the compact set of possible output points using properness of $R_A\to M$ over the second factor. The same closed-subset argument gives compactness of $S_{AB}\cap(M\times K)$. Hence $AB$ is properly supported. [guided] Proper support must be checked for the actual support of the composed kernel, not for a possibly nonclosed relation that contains it. Let $K_{AB}\in\mathcal D'(M\times M)$ be the Schwartz kernel of $AB$, and define \begin{align*} S_{AB}:=\operatorname{supp}K_{AB}\subset M\times M. \end{align*} The composition of kernels has the following support property: if $(x,z)$ belongs to $S_{AB}$, then there is an intermediate point $y\in M$ such that $(x,y)\in R_A$ and $(y,z)\in R_B$. Hence \begin{align*} S_{AB}\subset \{(x,z)\in M\times M:\text{there exists }y\in M\text{ with }(x,y)\in R_A\text{ and }(y,z)\in R_B\}. \end{align*} Let $K\subset M$ be compact. We show that $S_{AB}\cap(K\times M)$ is compact. First collect all possible intermediate points reachable from $K$ through the kernel of $A$: \begin{align*} Y_K:=\{y\in M:\text{there exists }x\in K\text{ with }(x,y)\in R_A\}. \end{align*} Because $A$ is properly supported, the projection $R_A\to M$ onto the first factor is proper. Thus $R_A\cap(K\times M)$ is compact, and $Y_K$ is compact as its image under the continuous second projection. Next collect all possible final points reachable from $Y_K$ through the kernel of $B$: \begin{align*} Z_K:=\{z\in M:\text{there exists }y\in Y_K\text{ with }(y,z)\in R_B\}. \end{align*} Because $B$ is properly supported, the projection $R_B\to M$ onto the first factor is proper. Hence $R_B\cap(Y_K\times M)$ is compact, and $Z_K$ is compact as its continuous image under the second projection. If $(x,z)\in S_{AB}$ with $x\in K$, the support inclusion forces $z\in Z_K$. Therefore \begin{align*} S_{AB}\cap(K\times M)\subset K\times Z_K. \end{align*} The right-hand side is compact. The set $S_{AB}$ is closed because supports of distributions are closed, so $S_{AB}\cap(K\times M)$ is a closed subset of $K\times Z_K$. Hence it is compact. This proves that the first projection from $S_{AB}$ to $M$ is proper. The second projection is handled by the same argument with the direction reversed: start with compact final points, use properness of $R_B$ over the second factor to bound possible intermediate points, then use properness of $R_A$ over the second factor to bound possible initial points. Thus $S_{AB}\cap(M\times K)$ is compact for every compact $K\subset M$. Both projections are proper, so $AB$ is properly supported. [/guided] [/step] [step:Combine the localized symbolic calculation and the support calculation] The separated terms are residual, the overlapping localized terms are semiclassical pseudodifferential operators of order $m+m'$, and the locally finite sum is legitimate because of proper support. Therefore \begin{align*} AB \in \Psi_h^{m+m'}(M). \end{align*} The principal symbol is computed locally by the Euclidean composition formula and patched globally by the multiplicative transformation law, so \begin{align*} \sigma_h(AB)=\sigma_h(A)\sigma_h(B) \end{align*} in \begin{align*} S^{m+m'}(T^*M)/\bigl(hS^{m+m'-1}(T^*M)+S^{-\infty}(T^*M)\bigr). \end{align*} This proves both the algebra property and the principal symbol formula. [/step]