Proving correctness of automata construction Given a regular language $L$, I am trying to show that the following language is regular

$$\textbf{Inv}(L)=\{xyz\mid xy^Rz\in L\}$$

My try:
It is given that $L$ is regular, hence there is some DFA $M$ that accepts $L$ and assume it has $n$ states.
We will construct an NFA $N$ that accepts $\textbf{Inv}(L)$ based on three parts:


*

*A copy of $M$ without final states.

*For every $1\le i,j\le n$ construct $N_{ij}$ which is a copy of the NFA that accepts $\textbf{Rev}(L)=\{w^R\mid w\in L\}$ (it is not hard to construct such NFA).

*A copy of $M$.


For every $1\le i,j\le n$, there will be an $\varepsilon$ transition between $q_i$ of part $1$ and $q_j$ of $N_{ij}$. 
Also, we will have an $\varepsilon$ transition between $q_i$ of $N_{ij}$ and $q_j$ of part $3$.

Correctness:
\begin{align*}w\in\textbf{Inv}(L)\iff&\exists x,y,z\in\Sigma^{\ast},\, \exists q_1,q_2\in Q,\, q_f\in F:\\&\hat\delta_{N_1}(q_0^1,x)=q_1^1,\,\hat\delta_{N_1}(q_1^1,\varepsilon)\in \{q_2^{N_{1j}}\},\, \hat\delta_{N_{1j}}(q_2^{N_{1j}},y)=q_1^{N_{1j}},\\&\hat\delta_{N_{1j}}(q_1^{N_{1j}},\varepsilon)=q_2^2,\, \hat\delta_{N_2}(q_2^2,z)=q_F\in F\iff w\in L(N)\end{align*}
I don't think the correctness part is right and believe it should be fixed.
It will be very appreciated if someone could tell how to write it. Thanks.
 A: Let $\mathcal{A} = (Q, \Sigma, \cdot, i, F)$ be a DFA recognising $L$. For each pair of states $(p,q) \in Q^2$, let $L_{p,q} = \{u \in \Sigma^* \mid p\cdot u = q\}$. For each language $K$, let $K^r = \{u^r \mid u \in K\}$. I claim that
$$
  Inv(L) = \bigcup_{p \in Q,q \in Q, f \in F} L_{i,p} L^r_{p,q} L_{q,f}  \qquad (*)
$$
Let $R$ be right hand side of $(*)$. If $u$ belongs to $R$, there exist three states $p \in Q$, $q \in Q$ and $f\in F$ such that $u = xyz$ with $x \in L_{i,p}$, $y\in L^r_{p,q}$ and $z \in L_{q,f}$. It follows that $y^r \in L_{p,q}$ and thus $i \cdot xy^rz = p \cdot y^rz = q \cdot z = f$. Thus $xy^rz \in L$ and $u \in Inv(L)$.
Suppose now that $u \in Inv(L)$. Then $u = xyz$ for some $x, y, z \in \Sigma^*$ such that $xy^rz \in L$. Let $p = i \cdot x$, $q = p \cdot y^r$ and $f = q \cdot z$. Then $f \in F$ since $xy^rz \in L$. Moreover, by construction $x \in L_{i,p}$, $y \in L^r_{p,q}$ and $z \in L_{q,f}$. Thus $u \in R$.
This proves the claim and shows that $Inv(L)$ is regular. If you insist to obtain an automaton for $Inv(L)$, you can use the standard constructions for concatenation and union, which seems to be your idea.
