Demuth's theorem in set theory

Question

I am quite sure the following fact must have been known for set theorists, though I could not find it anywhere.

If $r$ is random over $L$ and $x\in L[r]\setminus L$, then there must be some real $r_0$ random over $L$ so that $r_0\in L[x]$ and $x\in L[r_0]$.

So where I could find it?

Addition

Monroe Eskew has given an answer to the question. I would like to explain the phenomenon from a recursion theory point of view.

As Jason pointed out, the result is corresponded to Demuth's theorem in recursion theory. Actually it can be proved by applying Demuth's argument.

Suppose that $r$ is random and $x\in L[r]\setminus L$. Then there is a condition $r\in p\Vdash x\mbox{ is a real}$. Since random forcing is c.c.c., we may in $L$ find a sequence $\{p^i_n\}_{i,n\in \omega}$ stronger than $p$ so that for every $n$, $\{p^i_n\}_{i\in \omega}$ is a maximal antichain below $p$ and each $p^i_n$ decides a value of $x$. Coding these condition and the relation $p^i_n\Vdash x(n)=j_i$ into a single real $z\in L$. Then $x\leq_T r_0\oplus z$ with a use function $f\in L[r]$. Then $f$ is dominated by a function $g\in L$. Now using these facts and applying Demuth's argument, we may obtain a real $r_0$ which is also $L$-random so that $x\oplus z\oplus g\equiv_T r_0\oplus z\oplus g$.

So $x\in L[r_0]$ and $r_0\in L[x]$.

Answer 1

I'm not sure if this specific claim is stated explicitly anywhere, but it follows from the more general discussion about intermediate extensions in Jech, page 247. If we take any $x \in L[r]$, then there is a complete subalgebra $A$ of the random algebra associated to $\dot{x}$, with the property that $L[x]=L[G_r \cap A]$. But any complete subalgebra of a measure algebra is also a measure algebra. So $A$ is isomorphic to random forcing.