let p be 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)]
let z be 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)]
let P, Q be 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)]
let g2, gf1, gf2, gf3 be Element of (GF p); ( 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)) implies (addell_ProjCo (z,p)) . (P,Q) = [(gf2 * gf3),((gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3)) - ((gf2 |^ 3) * (P `2_3))),(gf2 |^ 3)] )
assume that
A1:
( not P _EQ_ Q & P `3_3 = 1 & Q `3_3 = 1 )
and
A2:
g2 = 2 mod p
and
A3:
( 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)) )
; (addell_ProjCo (z,p)) . (P,Q) = [(gf2 * gf3),((gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3)) - ((gf2 |^ 3) * (P `2_3))),(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: ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) =
(Q `2_3) - ((P `2_3) * (1. (GF p)))
by A1
.=
gf1
by A3
;
A7: ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) =
(Q `1_3) - ((P `1_3) * (1. (GF p)))
by A1
.=
gf2
by A3
;
((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) =
((gf1 |^ 2) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (1. (GF p)))
by A1
.=
gf3
by A3
;
hence (addell_ProjCo (z,p)) . (P,Q) =
[(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (1. (GF p))) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))]
by A1, A2, A4, A5, A6, A7, EC_PF_2:def 9
.=
[(gf2 * gf3),((gf1 * (((gf2 |^ 2) * (P `1_3)) - gf3)) - ((gf2 |^ 3) * (P `2_3))),(gf2 |^ 3)]
by A1
;
verum