I've read in an article the following statement (which is said to be a standard fact in forcing)
Given $\mathbb{P}$ a forcing notion and $G_1,G_2\subseteq\mathbb{P}$ such that $G_1\times G_2$ is $\mathbb{P}\times\mathbb{P}$-generic over $V$ then $V[G_1]\cap V[G_2] = V$
there was no proof of this fact, but I'm wandering why it is true.
I know the hypotheses imply (by a standard theorem on product forcings) that $G_2$ is $\mathbb{P}$-generic over $V[G_1]$ (and vice-versa) and that $V[G_1][G_2]=V[G_2][G_1]=V[G_1\times G_2]$, but I'm not sure how to use this fact to prove the statement above.
Some hint? Thanks!
First argue that it is enough to show that if $x\in V[G_1]\cap V[G_2]$ is a set of ordinals then $x\in V$. Now suppose $\dot x$ is a $\mathbb P\times\mathbb P$-name for a subset of some $\alpha$ and $$(p, q)\Vdash\dot x\in V[\dot G_l]\cap V[\dot G_r]$$ where $\dot G_l$ is the $\mathbb P\times\mathbb P$-name for the "left" $\mathbb P$-generic filter and $\dot G_r$ the one for the "right" filter. Let $$\pi_l:\mathbb P\rightarrow\mathbb P\times\mathbb P,\ p\mapsto (p, 1_{\mathbb P})$$ be the "left" embedding and $\pi_r$ the "right" embedding. There will then be two $\mathbb P$-names $\dot x_l$ and $\dot x_r$ as well as $p'\leq p$ and $q'\leq q$ with $$(p', q')\Vdash \pi_l^+(\dot x_l)=\dot x=\pi_r^+(\dot x_r)$$ where $\pi_l^+$ is the map from $\mathbb P$-names to $\mathbb P\times\mathbb P$-names induced by $\pi_l$, similar for $\pi_r^+$. Now try to show that $p'$ already fully decides $\dot x_l$ (and $q'$ fully decides $\dot x_r$).