Kronecker Product and Matrix Vectorization

I demand that matrix multiplication take precedence over kronecker product.

Definitions

$F$ is some field. In fact many results can be generalized to commutative rings.
$e_{i} \in F^{n}$ is the unit vector with the
$i$ coordinate being one.
$A \otimes B \in F^{(m p) \times (n q)}$ such that
$(A \otimes B)_{p i + k, q j + l} = A_{i j} B_{k l}$ where
$A \in F^{m \times n}$ and
$B \in F^{p \times q}$ . Without ambiguity, its
$i j k l$ entry is also denoted by
$(A \otimes B)_{i k, j l}$ .
$vec (A) = \sum_{j = 1}^{n} e_{j} \otimes A e_{j}$ for
$A \in F^{m \times n}$ .

(A \otimes B) (C \otimes D) = A C \otimes B D

for compatible matrices.

((A \otimes B) (C \otimes D))_{i k, j l} = \sum_{p, q} (A \otimes B)_{i k, p q} (C \otimes D)_{p q, j l} = \sum_{p, q} A_{i p} B_{k q} C_{p j} D_{q l} = \sum_{p} A_{i p} C_{p j} \sum_{q} B_{k q} D_{q l} = (A C)_{i j} (B D)_{k l} = (A C \otimes B D)_{i k, j l}

vec (A B C) = (C^{⊤} \otimes A) vec (B)

Let

C \in F^{m \times n}

\begin{aligned} vec (A B C) & = \sum_{j = 1}^{n} e_{j} \otimes A B C e_{j} = \sum_{j = 1}^{n} e_{j} \otimes A B \sum_{i = 1}^{m} C_{i j} e_{i} = \sum_{i = 1}^{m} \sum_{j = 1}^{n} C_{i j} e_{j} \otimes A B e_{i} \\ = \sum_{i = 1}^{m} C^{⊤} e_{i} \otimes A B e_{i} = (C^{⊤} \otimes A) \sum_{i = 1}^{m} e_{i} \otimes B e_{i} = (C^{⊤} \otimes A) vec (B) \end{aligned}