let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st P _EQ_ Q & P `3_3 = 1 & Q `3_3 = 1 & g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = (z `1) + (g3 * ((P `1_3) |^ 2)) & gf2 = P `2_3 & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
(addell_ProjCo (z,p)) . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))]
let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st P _EQ_ Q & P `3_3 = 1 & Q `3_3 = 1 & g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = (z `1) + (g3 * ((P `1_3) |^ 2)) & gf2 = P `2_3 & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
(addell_ProjCo (z,p)) . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))]
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st P _EQ_ Q & P `3_3 = 1 & Q `3_3 = 1 & g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = (z `1) + (g3 * ((P `1_3) |^ 2)) & gf2 = P `2_3 & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
(addell_ProjCo (z,p)) . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))]
let g2, g3, g4, g8, gf1, gf2, gf3, gf4 be Element of (GF p); :: thesis: ( P _EQ_ Q & P `3_3 = 1 & Q `3_3 = 1 & g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = (z `1) + (g3 * ((P `1_3) |^ 2)) & gf2 = P `2_3 & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) implies (addell_ProjCo (z,p)) . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] )
assume that
A1: ( P _EQ_ Q & P `3_3 = 1 & Q `3_3 = 1 ) and
A2: ( g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p ) and
A3: ( gf1 = (z `1) + (g3 * ((P `1_3) |^ 2)) & gf2 = P `2_3 & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) ) ; :: thesis: (addell_ProjCo (z,p)) . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))]
reconsider O = [0,1,0] as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_1:42;
A4: not P _EQ_ O by A1, ThEQO;
A5: not Q _EQ_ O by A1, ThEQO;
A6: ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) = ((z `1) * ((P `3_3) * (P `3_3))) + (g3 * ((P `1_3) |^ 2)) by EC_PF_1:22
.= ((z `1) * (1. (GF p))) + (g3 * ((P `1_3) |^ 2)) by A1
.= gf1 by A3 ;
(P `2_3) * (P `3_3) = (P `2_3) * (1. (GF p)) by A1
.= gf2 by A3 ;
hence (addell_ProjCo (z,p)) . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] by A1, A2, A3, A4, A5, A6, EC_PF_2:def 9; :: thesis: verum