Frobenius automorphism and cyclotomic extension

There is a lemma from a lecture I attended where I scribbled down notes and try to make sense of the proof afterwards and there is a spot at which I am stuck. First I have to set up some notations and refresh memory on Frobenius element.

Let $$l,p$$ be distinct odd primes, $$L = \mathbb{Q}(\zeta_l)$$, $$K$$ be the unique quadractic subfield contained in $$L$$. (To see what $$K$$ is, we know that $$Gal(L/\mathbb{Q}) =(\mathbb{Z}/l\mathbb{Z})^*$$ has a unique subgroup $$H$$ of index 2, and by Galois theory, $$K$$ would then be $$L^H$$).

By definition, $$Frob_p$$ is defined as follows. We know $$p$$ is unramified in $$L$$. If $$\mathfrak{q}\subseteq O_L$$ is any prime ideal containing $$p\cdot O_L$$, then the decomposition group at $$\mathfrak{q}$$ defined as $$G_\mathfrak{q}:=\{\sigma\in Gal(L/\mathbb{Q}) : \sigma(\mathfrak{q})=\mathfrak{q}\}$$ is isomorphic to $$Gal((O_L/\mathfrak{q})/\mathbb{F}_p)$$. The latter has Frobenius element $$x\mapsto x^p$$. The corresponding element in $$G_\mathfrak{q}$$ is denoted $$Frob_p$$. Note that $$Frob_p$$ does not depend on the choice of $$\mathfrak{q}$$ because the extension is Abelian.

Lemma: $$Frob_p\in Gal(L/\mathbb{Q})$$ is in $$H$$ if and only if $$p$$ splits in $$K$$.

Proof: Let $$\mathfrak{p}_1 \subseteq O_K$$ be a prime factor of $$p\cdot O_K$$. Then $$Frob_p\in H$$ $$\Leftrightarrow$$ $$Frob_p$$ acts trivially on $$O_K$$ $$\Leftrightarrow$$ $$x\mapsto x^p$$ is identity on $$O_K/\mathfrak{p}_1$$ $$\Leftrightarrow$$ $$O_K/\mathfrak{p}_1 = \mathbb{F}_p$$ $$\Leftrightarrow$$ $$p$$ splits in $$K$$.

The line that I do not get is "$$Frob_p$$ acts trivially on $$O_K$$ $$\Leftrightarrow$$ $$x\mapsto x^p$$ is identity on $$O_K/\mathfrak{p}_1$$". I think I have the forward implication, but could someone enlighten me on the backward implication?

I think you're missing the following useful observation: $Frob_p$ is characterized by the property $Frob_p x \equiv x^p \pmod{\mathfrak{q}}$ for all $x$ in $O_L$. That $Frob_p$ has this property follows from your definition. To see that it is determined among all automorphisms of $L$ by this property, note that if for some automorphism $\sigma$ of $L$ we have $\sigma x \equiv x^p \pmod{\mathfrak{q}}$, then letting $x$ be in $\mathfrak{q}$, we see that $\sigma$ fixes $\mathfrak{q}$, hence is in the decomposition group of $\mathfrak{q}$. Now as you point out, this group is isomorphic to the Galois group of $O_L/\mathfrak{q}$ over $\mathbb{F}_p$, so there is a unique such automorphism that acts as Frobenius.
Examine the above paragraph and note that nothing depends on the upper field being $L$ -- it could be any abelian extension of $\mathbb{Q}$. In particular, there is a $Frob_p$ automorphism of $K/\mathbb{Q}$. In fact, by the above characterization, this $Frob_p$ is the restriction to $K$ of the $Frob_p$ for $L/\mathbb{Q}$.
$\implies$: Choose the $\mathfrak{q}$ to lie above $\mathfrak{p}_1$. If $Frob_p$ acts trivially on $O_K$, then the $Frob_p$ for $K/\mathbb{Q}$ is the identity automorphism. In particular, $x = Frob_p x \equiv x^p \pmod{\mathfrak{p}_1}$ for all $x$ in $O_K$, so $x \mapsto x^p$ is the identity on $O_K/\mathfrak{p}_1$.
$\impliedby$: If $x \mapsto x^p$ is the identity on $O_K/\mathfrak{p}_1$, then the identity automorphism of $K$ has the property that characterizes the $Frob_p$ for $K/\mathbb{Q}$. Thus, this $Frob_p$ is the identity on $K$, so the $Frob_p$ for $L$ is trivial on $O_K$.