theorem LmAddEll1: :: EC_PF_3:27

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for g2, gf1, gf2, gf3 being Element of (GF p) st not P _EQ_ Q & P `3_3 = 1 & Q `3_3 = 1 & g2 = 2 mod p & gf1 = (Q `2_3) - (P `2_3) & gf2 = (Q `1_3) - (P `1_3) & gf3 = ((gf1 |^ 2) - (gf2 |^ 3)) - ((g2 * (gf2 |^ 2)) * (P `1_3)) holds
(addell_ProjCo (z,p)) . (P,Q) = [(gf2 * gf3),((gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3)) - ((gf2 |^ 3) * (P `2_3))),(gf2 |^ 3)]