# Proof a given formular is equal to a specific scalar multiple of a point on an elliptic curve

$\newcommand\F{\mathbb F}$ I'm computing a special compressed way of a frobenius map on elliptic curves. For pairing-based cryptography, especially the optimal ate pairing, we need to make our computations on a specific subgroup. So I give you a really small introduction first.

# Introduction

Let $E(\mathbb F_{p^{16}}):\ y^2=x^3+x$ be an elliptic curve. This curve is isomorphic to $E'(\mathbb F_{p^4}): y^2=x^3+v^{-1}x$ over $\F_{p^{16}}$, where $v^4-c$ is irreducible over $\F_p$. (I guess this should be enough)

The Frobenius map of such a point $Q\in E$ is defined by $\pi(Q)=( x_q^p, y_q^p)$.

A $r$-torsion subgroup is defined by $rP=\mathcal O$ for any point on that group.

$\newcommand{\Ff}{\mathbb F_{p^{16}}}$ For Pairings, we consider two groups $r$-torsion groups: $G_1 = E(\Ff)[r]\cap \{ \pi = Id\}$ and $G_2 = E(\Ff)[r]\cap \{ \pi = pId\}$.

Well we can reduce G1 to $G_1 = E(\F_p)[r]$, since this only holds for points with coordinates over this field).

Another trick comes from twists. A twist is an isomorphism as described. We can compress $G_2$ to the twisted curve $E'$, therefore, $G_2= E'(\mathbb F_{p^4})[r]$. But we can't find any point $P'\in E'$ such that $\pi(P')=pP'$. But using the isomorphism and its inverse $\pi(E'\to E) \to E'$ leads to a way, to compute such a Frobenius, without lifting especially.

# Question

On my actual point, I have shown, that my found "Frobenius" on the twist dilvers a valid point on the twist. I have checked with Sage-math, that $pP' = \pi'(P')$ (where $\pi'$ is my derivation). But how can I proof, that this equation holds?

I mean, on the right side, I have an explicit point that lays on the curve. The left side is a large scalar multiplication, which can't be done efficiently. Furthermore, to say "Sage proves right" is not what I think, the mathematical society will accept :D

I've added the cryptography-tag, since it is mainly used in pairing-based cryptography. Since elliptic curves are only varieties, the commutative algebra could also help.

# Edit

I found the solution. Just use the isomorphism behaviour and apply the steps in between. The answere follows directly.