The type-A diagrammatic relations hold for Soergel bimodules

Reduction to generators: every relation of $D$ equates two composites of generating morphisms with the same bottom and top words, so it is a relation between two graded bimodule maps of the same degree; a bimodule map out of a Bott–Samelson bimodule is determined by its values on an $R$-bimodule generating set, and the sets used in [F7] are generating sets, so it suffices to evaluate both sides of each relation on those generators.

Polynomial relations: a box labelled $f$ is sent to multiplication by $f$ in its region, and a box may be moved across a strand of color $s$ precisely at the cost of the balanced-tensor relation of $B_s=R{\otimes }_{R^s}R(1)$; since every $f$ decomposes uniquely as $f^{+}+{\alpha }_s{f}^{-}$ with $f^{\pm }\in R^s$ by [F2], and the dot on a strand of color $s$ is sent to the element ${\alpha }_s$ in the appropriate slot, the two polynomial relations listed in [F1] hold with $\mathrm{deg}{\alpha }_s=2$ and ${\mathrm{\partial }}_s$ as in [F2]; the identities are checked on $1$-tensors, where they reduce to the decomposition $f=f^{+}+{\alpha }_s{f}^{-}$.

One-colour relations: the dot and trivalent morphisms of one colour are the structure maps of the Frobenius extension $R\mathrm{/}{R}^s$, namely the trace ${\mathrm{\partial }}_s$, the element ${\mathrm{\Delta }}_s$, and the two balanced multiplications; by [F4] the compositions of these maps in $B_s$ satisfy the unit and counit identities of a Frobenius algebra, and the remaining one-colour relation, the vanishing of the needle (a loop attached to a strand at a trivalent vertex), is covered by the imported generator check [F7]. In the Frobenius evaluation its closed loop contributes ${\mathrm{\partial }}_s(1)=0$; the value ${\mathrm{\partial }}_s({\alpha }_s)=2\mathrm{\ne }0$ concerns a different composite and does not prove the needle relation.

Distant two-color relations: on distant colors the image of the $4$-valent vertex is the interchange isomorphism of [F5], which is degree zero, sends $1$-tensors to $1$-tensors and squares to the identity after the evident transposition; since the two strands are colored by distinct commuting simple reflections, polynomials slide across them exactly as in the balanced tensor product of [F1], so the distant interchange relations hold on $1$-tensors.

Adjacent and three-colour relations, and the relations on mixed words: the remaining relations are the two-colour Jones–Wenzl relations for adjacent colours, in the two parities of the source, and the three-colour relations $A_1\times I_2(m)$ and $A_3$. These are exactly the relations covered by the imported generator check [F7]: the adjacent case is the pair of decompositions of [F6], which supplies the source's resolution of the two triple products, and the three-colour cases are the rank-three checks of the source. No rescaling is involved, because the library's declared images of the generators are the balanced source images: the second dot is $1\mapsto {\mathrm{\Delta }}_s=\frac{1}{2}({\alpha }_s\otimes 1+1\otimes {\alpha }_s)$ with $\frac{1}{2}\in \mathbb{Q}$, and the six-valent vertex is the source-normalized Libedinsky map of [F7], whose common summand is identified by [F6].

Conclusion: by steps 1.2–1.5 the images of the generators respect every defining relation of $D$, so $\mathcal{F}$ is well defined on hom spaces; it preserves degree by the degree dictionary of [F1] and composition and juxtaposition by construction, so it is a graded $\mathbb{Q}$-linear monoidal functor $D\to {\mathrm{B}\mathrm{S}\mathrm{B}\mathrm{i}\mathrm{m}}^{\bullet }$. For shifted objects, a degree-zero diagrammatic map $X(a)\to Y(b)$ is an unshifted map of degree $b-a$, and its evaluated bimodule map has that same degree, hence is degree zero from $B_X(a)$ to $B_Y(b)$. Extend by matrices to finite sums and restrict to these degree-zero maps. This is a functor to the categorical $\mathrm{B}\mathrm{S}\mathrm{B}\mathrm{i}\mathrm{m}$ of the statement. It extends to degree-zero idempotents by sending $(M,e)$ to the image of the evaluated idempotent, so $\mathcal{F}$ extends to $\mathrm{Kar}(D)\to {\mathrm{S}\mathrm{B}\mathrm{i}\mathrm{m}}_n$; the unit of $D$ is the empty word, sent to $R$, and the normalisation is the one displayed in [F1] and [F7]. ∎