Two step iteration and equivalence of forcing notions Let $\pi:\mathbb{P}\rightarrow\mathbb{Q}$ be a projection, let $H\subset \mathbb{Q}$ be some generic filter and let
$$ \mathbb{R}=\left\{p\in\mathbb{P}\  \bigg|\ \pi(p)\in H \right\}$$
Let $\dot{\mathbb{R}}$ be a $\mathbb{Q}$-name s.t $\dot{\mathbb{R}}^H = \mathbb{R}$.
Show that there is a dense subset of $\mathbb{Q}*\dot{\mathbb{R}}$ which is isomorphic to a dense subset of $\mathbb{P}$.
I'm having trouble approaching this question, I figured that the dense subset should be a subset of $\mathbb{R}$ else defining an embedding into the iteration is troublesome but I can't seem to make any progres.
Any help would be appriciated.
 A: I'm going to change your variable assignment, so that they appear in alphabetical order (I'm weird like that). I also assume your notion of projection coincides with the one presented in Abraham's chapter in the Handbook of Set Theory (minus his assumption that all posets are separative).

So, let $\pi:{\mathbb R}\to \mathbb{P} $ be a projection and $\dot {\mathbb Q}$ a $\mathbb P$-name for the set $\{r\in{\mathbb R}:\pi(r)\in \dot G\}$, where $\dot G$ is the canonical $\mathbb P$-name for the $\mathbb P$-generic filter. Such a $\dot{\mathbb Q}$ can be found by an appeal to the Maximal Principle, but a more explicit description is possible (see below).
A slight subtlety here is what exact definition of $\mathbb P\ast\dot{\mathbb Q}$ you're using. If you're following Kunen, then
$$
\mathbb{P}\ast\dot{\mathbb Q}:=\{(p,\dot q)\in \mathbb P\times\text{dom}(\dot{\mathbb Q}):p\Vdash \dot q\in\dot{\mathbb Q}\}
$$
Now, you'll probably object we don't know what $\dot{\mathbb Q}$ looks like as a set. On the one hand, this isn't too important, on the other, we can take
$$
\dot{\mathbb Q}:=\{(\check r,p):p\in\mathbb P\wedge r\in\mathbb{R}\wedge  p\Vdash \check\pi(\check r)\in \dot G\}
$$
Using these definitions, we get that
$$
\mathbb P\ast\dot {\mathbb Q}=\{(p,\check r):p\in\mathbb P\wedge r\in {\mathbb R}\wedge p\Vdash \check\pi(\check r)\in \dot G\}
$$
Now, define $i:\mathbb R\to \mathbb P\ast\dot{\mathbb Q}$ by $i(r):=(\pi(r),\check r)$.
I claim that $i$ is an order isomorphism onto a dense subset of $ \mathbb P\ast\dot{\mathbb Q}$.
Suppose first that $r,s\in\mathbb R$ and $r\le_{\mathbb{R}} s$. Then $\pi(r)\le \pi(s)$ because $\pi$ is a projection. Also, $\Vdash \check r\le_{\dot {\mathbb R}}\check s$ by absoluteness and therefore $\pi(r)\Vdash \check r\le_{\dot{\mathbb Q}}\check s$. In detail, you know that $\pi(r)\Vdash r,s\in \dot{\mathbb Q}$ (if $\pi(r)\in G$ then $\pi(s)\in G$ because $G$ is a filter). But, in $V[G]$, the underlying order of $\dot{\mathbb{Q}}_G$ is just the restriction of $\le_{\mathbb{R}}$. This means that $i(r)\le i(s)$.
Conversely, suppose $i(r)\le i(s)$. Then $r\Vdash \check{r} \le_{\mathbb{R}} \check s$ by the same comment about $\le_{\dot{\mathbb Q}}$. But that is a ground model statement which is absolute, so if it's forced by a condition then it's just true outright, i.e. $r\le s$.
We now need to check that the range of $i$ is dense in the two-step iteration $\mathbb P\ast\dot{\mathbb Q}$. To do this, fix an element of $\mathbb P\ast\dot{\mathbb Q} $, which must be of the form $(p,\check r)$ for some $p\in\mathbb P$, $r\in\mathbb R$ with $p\Vdash \pi(r)\in \dot G$. This last forcing statement means that $p$ and $\pi(r)$ are compatible, so there is some $p'\le p,\pi(r)$. Since $\pi$ is a projection, there is some $r'\le r$ with $\pi(r')=p'$. Then
$$
i(r')=(\pi(r'),\check{r'})=(p',\check{r'})\le_{\mathbb P\ast\dot{\mathbb Q}}(p,\check r)
$$
This completes the argument.

Now, if you're not following Kunen, you might not be defining $\mathbb P\ast\dot{\mathbb Q}$ as I did above. Moreover, this definition is inadequate once one moves past finite support iterations (everything works whenever you're working with finite supports though). In general, we usually define
$$
\mathbb P\ast\dot{\mathbb Q}:=\{(p,\dot q):p\in\mathbb P\wedge \dot q\in X\wedge p\Vdash \dot q\in \mathbb Q\}
$$
where $X$ is some specified set with the property that, for any name $\tau$ and any $p\in\mathbb P$, if $p\Vdash \tau\in\dot{\mathbb Q}$, then there exists some $\sigma\in X$ with $p\Vdash \sigma=\tau$: However, you still have that the set
$$
\{(p,\dot q)\in \mathbb P\times\text{dom}(\dot{\mathbb Q}):p\Vdash \dot q\in\dot{\mathbb Q}\}
$$
is dense in $\mathbb P\ast\dot{\mathbb Q}$ (with the new definition), see this answer on MO.
So, by the previous argument, there is a dense subset of $\mathbb P\ast\dot{\mathbb Q}$ which is order isomorphic to $\mathbb R$, and so we're done.

For completeness:

Lemma: Let $\mathbb P$ be any forcing notion and suppose $p\Vdash q\in G$. Then $p$ and $q$ are compatible.

Proof: Pick $G\ni p$ which is $\mathbb{P}$-generic over the ground model $V$. By assumption, $V[G]\models q\in G$, so that $V[G]\models p,q\in G$, and so $V[G]\models$ "$p$ and $q$ are compatible" because $G$ is a filter. But this is an absolute statement about two ground model objects, so $V$ thinks that $p$ and $q$ are compatible.
