:: Operations of Points on Elliptic Curve in Projective Coordinates
:: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Received November 3, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


theorem Th1: :: EC_PF_2:1
for F being non empty right_complementable add-associative right_zeroed unital distributive doubleLoopStr
for a being Element of F holds a |^ 2 = (- a) |^ 2
proof end;

theorem :: EC_PF_2:2
for K being non degenerated almost_left_invertible associative commutative well-unital doubleLoopStr holds (1. K) " = 1. K
proof end;

theorem Th3: :: EC_PF_2:3
for K being Field
for a1, a2, a3, a4 being Element of K st a2 <> 0. K & a4 <> 0. K & a1 * (a2 ") = a3 * (a4 ") holds
a1 * a4 = a2 * a3
proof end;

theorem Th4: :: EC_PF_2:4
for K being Field
for a1, a2, a3, a4 being Element of K st a2 <> 0. K & a4 <> 0. K & a1 * a4 = a2 * a3 holds
a1 * (a2 ") = a3 * (a4 ")
proof end;

theorem Th5: :: EC_PF_2:5
for n being Nat
for K being Ring st n >= 1 holds
(0. K) |^ n = 0. K
proof end;

theorem :: EC_PF_2:6
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a1, a2 being Element of K st a1 = - a2 holds
- a1 = a2
proof end;

theorem Th7: :: EC_PF_2:7
for K being Abelian AddGroup
for a1, a2, a3, a4 being Element of K holds
( ((a1 + a2) + a3) + a4 = ((a4 + a2) + a3) + a1 & ((a1 + a2) + a3) + a4 = ((a1 + a4) + a3) + a2 )
proof end;

theorem Th8: :: EC_PF_2:8
for K being Abelian AddGroup
for a1, a2, a3, a4, a5 being Element of K holds
( ((a1 + a2) + a3) + a4 = a1 + ((a2 + a3) + a4) & (((a1 + a2) + a3) + a4) + a5 = a1 + (((a2 + a3) + a4) + a5) )
proof end;

theorem :: EC_PF_2:9
for K being Abelian AddGroup
for a1, a2, a3, a4, a5, a6 being Element of K holds ((((a1 + a2) + a3) + a4) + a5) + a6 = a1 + ((((a2 + a3) + a4) + a5) + a6)
proof end;

theorem Th10: :: EC_PF_2:10
for K being comRing
for a1, a2, a3, a4 being Element of K holds
( ((a1 * a2) * a3) * a4 = ((a4 * a2) * a3) * a1 & ((a1 * a2) * a3) * a4 = ((a1 * a4) * a3) * a2 )
proof end;

theorem Th11: :: EC_PF_2:11
for K being Ring
for a1, a2, a3, a4, a5 being Element of K holds
( ((a1 * a2) * a3) * a4 = a1 * ((a2 * a3) * a4) & (((a1 * a2) * a3) * a4) * a5 = a1 * (((a2 * a3) * a4) * a5) )
proof end;

theorem Th12: :: EC_PF_2:12
for K being Ring
for a1, a2, a3, a4, a5, a6 being Element of K holds
( ((((a1 * a2) * a3) * a4) * a5) * a6 = a1 * ((((a2 * a3) * a4) * a5) * a6) & ((((a1 * a2) * a3) * a4) * a5) * a6 = ((a1 * ((a2 * a3) * a4)) * a5) * a6 )
proof end;

theorem Th13: :: EC_PF_2:13
for n being Nat
for K being Ring
for a1, a2, a3 being Element of K st K is commutative holds
((a1 * a2) * a3) |^ n = ((a1 |^ n) * (a2 |^ n)) * (a3 |^ n)
proof end;

theorem Th14: :: EC_PF_2:14
for K being Ring
for a1, a2, a3, a4 being Element of K holds
( a1 * ((a2 + a3) + a4) = ((a1 * a2) + (a1 * a3)) + (a1 * a4) & a1 * ((a2 + a3) - a4) = ((a1 * a2) + (a1 * a3)) - (a1 * a4) & a1 * ((a2 - a3) + a4) = ((a1 * a2) - (a1 * a3)) + (a1 * a4) & a1 * ((a2 - a3) - a4) = ((a1 * a2) - (a1 * a3)) - (a1 * a4) & a1 * (((- a2) + a3) + a4) = ((- (a1 * a2)) + (a1 * a3)) + (a1 * a4) & a1 * (((- a2) + a3) - a4) = ((- (a1 * a2)) + (a1 * a3)) - (a1 * a4) & a1 * (((- a2) - a3) + a4) = ((- (a1 * a2)) - (a1 * a3)) + (a1 * a4) & a1 * (((- a2) - a3) - a4) = ((- (a1 * a2)) - (a1 * a3)) - (a1 * a4) )
proof end;

theorem Th15: :: EC_PF_2:15
for K being comRing
for a1, a2 being Element of K holds (a1 + a2) * (a1 - a2) = (a1 |^ 2) - (a2 |^ 2)
proof end;

theorem :: EC_PF_2:16
for K being comRing
for a1, a2 being Element of K holds (a1 + a2) * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) + (a2 |^ 3)
proof end;

theorem Th17: :: EC_PF_2:17
for K being comRing
for a1, a2 being Element of K holds (a1 - a2) * (((a1 |^ 2) + (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) - (a2 |^ 3)
proof end;

definition
let n, p be Nat;
attr p is n _or_greater means :Def1: :: EC_PF_2:def 1
n <= p;
end;

:: deftheorem Def1 defines _or_greater EC_PF_2:def 1 :
for n, p being Nat holds
( p is n _or_greater iff n <= p );

registration
cluster V9() V10() V11() V15() V19() V20() integer dim-like prime ext-real 5 _or_greater for set ;
existence
ex b1 being Nat st
( b1 is 5 _or_greater & b1 is prime ) by Def1, PEPIN:59;
end;

theorem Th18: :: EC_PF_2:18
for i, j being Integer
for p being Prime
for gi, gj, gij, a being Element of (GF p) st gi = i mod p & gj = j mod p & gij = (i + j) mod p holds
(gi * a) + (gj * a) = gij * a
proof end;

theorem Th19: :: EC_PF_2:19
for i, j being Integer
for p being Prime
for gi, gj, a being Element of (GF p) st gi = i mod p & gj = j mod p & j = i + 1 holds
(gi * a) + a = gj * a
proof end;

theorem Th20: :: EC_PF_2:20
for p being Prime
for g2, a being Element of (GF p) st g2 = 2 mod p holds
a + a = g2 * a
proof end;

theorem Th21: :: EC_PF_2:21
for i, j being Integer
for p being Prime
for gi, gj, gij, a being Element of (GF p) st gi = i mod p & gj = j mod p & gij = (i - j) mod p holds
(gi * a) - (gj * a) = gij * a
proof end;

theorem Th22: :: EC_PF_2:22
for i, j being Integer
for p being Prime
for gi, gj, a being Element of (GF p) st gi = i mod p & gj = j mod p & i = j + 1 holds
(gi * a) - (gj * a) = a
proof end;

theorem Th23: :: EC_PF_2:23
for i, j being Integer
for p being Prime
for gi, gj, a being Element of (GF p) st gi = i mod p & gj = j mod p & i = j + 1 holds
(gi * a) - a = gj * a
proof end;

theorem Th24: :: EC_PF_2:24
for p being Prime
for g2, a being Element of (GF p) st g2 = 2 mod p holds
(g2 * a) - a = a
proof end;

theorem Th25: :: EC_PF_2:25
for p being Prime
for g2, a, b being Element of (GF p) st g2 = 2 mod p holds
(a + b) |^ 2 = ((a |^ 2) + ((g2 * a) * b)) + (b |^ 2)
proof end;

theorem Th26: :: EC_PF_2:26
for p being Prime
for g2, a, b being Element of (GF p) st g2 = 2 mod p holds
(a - b) |^ 2 = ((a |^ 2) - ((g2 * a) * b)) + (b |^ 2)
proof end;

theorem Th27: :: EC_PF_2:27
for p being Prime
for g2, a, b, c, d being Element of (GF p) st g2 = 2 mod p holds
((a * c) + (b * d)) |^ 2 = (((a |^ 2) * (c |^ 2)) + ((((g2 * a) * b) * c) * d)) + ((b |^ 2) * (d |^ 2))
proof end;

theorem Th28: :: EC_PF_2:28
for p being Prime
for n being Nat
for g2 being Element of (GF p) st p > 2 & g2 = 2 mod p holds
( g2 <> 0. (GF p) & g2 |^ n <> 0. (GF p) )
proof end;

theorem :: EC_PF_2:29
for p being Prime
for n being Nat
for g2, g3 being Element of (GF p) st p > 3 & g3 = 3 mod p holds
( g3 <> 0. (GF p) & g3 |^ n <> 0. (GF p) )
proof end;

definition
let p be 5 _or_greater Prime;
func EC_WParam p -> Subset of [: the carrier of (GF p), the carrier of (GF p):] equals :: EC_PF_2:def 2
 { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } ;
correctness
coherence
{ [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } is Subset of [: the carrier of (GF p), the carrier of (GF p):];
proof end;
end;

:: deftheorem defines EC_WParam EC_PF_2:def 2 :
for p being 5 _or_greater Prime holds EC_WParam p = { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } ;

registration
let p be 5 _or_greater Prime;
cluster EC_WParam p -> non empty ;
coherence
not EC_WParam p is empty
proof end;
end;

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
:: original: `1
redefine func z `1 -> Element of (GF p);
correctness
coherence
z `1 is Element of (GF p);
proof end;
:: original: `2
redefine func z `2 -> Element of (GF p);
correctness
coherence
z `2 is Element of (GF p);
proof end;
end;

theorem Th30: :: EC_PF_2:30
for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds
( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) )
proof end;

definition
let p be Prime;
let a, b be Element of (GF p);
let P be Element of EC_SetProjCo (a,b,p);
func P `1_3 -> Element of (GF p) means :Def3: :: EC_PF_2:def 3
 for px, py, pz being object st P = [px,py,pz] holds
it = px;
existence
ex b1 being Element of (GF p) st
for px, py, pz being object st P = [px,py,pz] holds
b1 = px
proof end;
uniqueness
for b1, b2 being Element of (GF p) st ( for px, py, pz being object st P = [px,py,pz] holds
b1 = px ) & ( for px, py, pz being object st P = [px,py,pz] holds
b2 = px ) holds
b1 = b2
proof end;
func P `2_3 -> Element of (GF p) means :Def4: :: EC_PF_2:def 4
 for px, py, pz being object st P = [px,py,pz] holds
it = py;
existence
ex b1 being Element of (GF p) st
for px, py, pz being object st P = [px,py,pz] holds
b1 = py
proof end;
uniqueness
for b1, b2 being Element of (GF p) st ( for px, py, pz being object st P = [px,py,pz] holds
b1 = py ) & ( for px, py, pz being object st P = [px,py,pz] holds
b2 = py ) holds
b1 = b2
proof end;
func P `3_3 -> Element of (GF p) means :Def5: :: EC_PF_2:def 5
 for px, py, pz being object st P = [px,py,pz] holds
it = pz;
existence
ex b1 being Element of (GF p) st
for px, py, pz being object st P = [px,py,pz] holds
b1 = pz
proof end;
uniqueness
for b1, b2 being Element of (GF p) st ( for px, py, pz being object st P = [px,py,pz] holds
b1 = pz ) & ( for px, py, pz being object st P = [px,py,pz] holds
b2 = pz ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines `1_3 EC_PF_2:def 3 :
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for b5 being Element of (GF p) holds
( b5 = P `1_3 iff for px, py, pz being object st P = [px,py,pz] holds
b5 = px );

:: deftheorem Def4 defines `2_3 EC_PF_2:def 4 :
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for b5 being Element of (GF p) holds
( b5 = P `2_3 iff for px, py, pz being object st P = [px,py,pz] holds
b5 = py );

:: deftheorem Def5 defines `3_3 EC_PF_2:def 5 :
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for b5 being Element of (GF p) holds
( b5 = P `3_3 iff for px, py, pz being object st P = [px,py,pz] holds
b5 = pz );

theorem Th31: :: EC_PF_2:31
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds P = [(P `1_3),(P `2_3),(P `3_3)]
proof end;

AA: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds x = [(x `1_3),(x `2_3),(x `3_3)]
;

theorem Th32: :: EC_PF_2:32
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p)
for Q being Element of ProjCo (GF p) holds
( P = Q iff ( P `1_3 = Q `1_3 & P `2_3 = Q `2_3 & P `3_3 = Q `3_3 ) )
proof end;

theorem :: EC_PF_2:33
for p being Prime
for a, b, Px, Py, Pz being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) st P = [Px,Py,Pz] holds
( P `1_3 = Px & P `2_3 = Py & P `3_3 = Pz ) by Def3, Def4, Def5;

definition
let p be Prime;
let P be Element of ProjCo (GF p);
let CEQ be Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p);
pred P is_on_curve CEQ means :: EC_PF_2:def 6
CEQ . P = 0. (GF p);
correctness
;
end;

:: deftheorem defines is_on_curve EC_PF_2:def 6 :
for p being Prime
for P being Element of ProjCo (GF p)
for CEQ being Function of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):],(GF p) holds
( P is_on_curve CEQ iff CEQ . P = 0. (GF p) );

theorem Th34: :: EC_PF_2:34
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) holds
( P is_on_curve EC_WEqProjCo (a,b,p) iff P is Element of EC_SetProjCo (a,b,p) )
proof end;

theorem Th35: :: EC_PF_2:35
for p being Prime
for a, b being Element of (GF p)
for P being Element of EC_SetProjCo (a,b,p) holds (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))) = 0. (GF p)
proof end;

definition
let p be Prime;
let P be Element of ProjCo (GF p);
func rep_pt P -> Element of ProjCo (GF p) equals :Def7: :: EC_PF_2:def 7
[((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] if P `3_3 <> 0
[0,1,0] if P `3_3 = 0
;
coherence
( ( P `3_3 <> 0 implies [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] is Element of ProjCo (GF p) ) & ( P `3_3 = 0 implies [0,1,0] is Element of ProjCo (GF p) ) )
proof end;
consistency
for b1 being Element of ProjCo (GF p) st P `3_3 <> 0 & P `3_3 = 0 holds
( b1 = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] iff b1 = [0,1,0] ) ;
end;

:: deftheorem Def7 defines rep_pt EC_PF_2:def 7 :
for p being Prime
for P being Element of ProjCo (GF p) holds
( ( P `3_3 <> 0 implies rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] ) & ( P `3_3 = 0 implies rep_pt P = [0,1,0] ) );

theorem Th36: :: EC_PF_2:36
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )
proof end;

theorem Th37: :: EC_PF_2:37
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st (rep_pt P) `3_3 = 0 holds
( rep_pt P = [0,1,0] & P `3_3 = 0 )
proof end;

theorem Th38: :: EC_PF_2:38
for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st (rep_pt P) `3_3 <> 0 holds
( rep_pt P = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] & P `3_3 <> 0 )
proof end;

theorem Th39: :: EC_PF_2:39
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) holds
( P _EQ_ Q iff rep_pt P = rep_pt Q )
proof end;

Lm1: for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds [(P `1_3),(- (P `2_3)),(P `3_3)] is Element of EC_SetProjCo ((z `1),(z `2),p)
proof end;

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
func compell_ProjCo (z,p) -> Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) means :Def8: :: EC_PF_2:def 8
 for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds it . P = [(P `1_3),(- (P `2_3)),(P `3_3)];
existence
ex b1 being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) st
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b1 . P = [(P `1_3),(- (P `2_3)),(P `3_3)]
proof end;
uniqueness
for b1, b2 being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) st ( for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b1 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) & ( for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b2 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines compell_ProjCo EC_PF_2:def 8 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b3 being Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)) holds
( b3 = compell_ProjCo (z,p) iff for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds b3 . P = [(P `1_3),(- (P `2_3)),(P `3_3)] );

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
let F be Function of (EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p));
let P be Element of EC_SetProjCo ((z `1),(z `2),p);
:: original: .
redefine func F . P -> Element of EC_SetProjCo ((z `1),(z `2),p);
correctness
coherence
F . P is Element of EC_SetProjCo ((z `1),(z `2),p);
proof end;
end;

theorem Th40: :: EC_PF_2:40
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
(compell_ProjCo (z,p)) . O _EQ_ O
proof end;

theorem Th41: :: EC_PF_2:41
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds (compell_ProjCo (z,p)) . ((compell_ProjCo (z,p)) . P) = P
proof end;

theorem Th42: :: EC_PF_2:42
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P)
proof end;

theorem Th43: :: EC_PF_2:43
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) holds
( P = Q iff (compell_ProjCo (z,p)) . P = (compell_ProjCo (z,p)) . Q )
proof end;

theorem Th44: :: EC_PF_2:44
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
( P _EQ_ (compell_ProjCo (z,p)) . P iff P `2_3 = 0 )
proof end;

theorem Th45: :: EC_PF_2:45
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) st P `3_3 <> 0 holds
( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
proof end;

theorem Th46: :: EC_PF_2:46
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) holds
( P _EQ_ Q iff (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q )
proof end;

theorem Th47: :: EC_PF_2:47
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) holds
( P _EQ_ (compell_ProjCo (z,p)) . Q iff (compell_ProjCo (z,p)) . P _EQ_ Q )
proof end;

theorem Th48: :: EC_PF_2:48
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) st P `3_3 <> 0 & Q `3_3 <> 0 holds
( rep_pt P = (compell_ProjCo (z,p)) . (rep_pt Q) iff P _EQ_ (compell_ProjCo (z,p)) . Q )
proof end;

theorem :: EC_PF_2:49
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) st P _EQ_ Q holds
(P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
proof end;

theorem Th50: :: EC_PF_2:50
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) st P `3_3 <> 0 & Q `3_3 <> 0 holds
( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) )
proof end;

theorem Th51: :: EC_PF_2:51
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) st P `3_3 <> 0 & Q `3_3 <> 0 & P `2_3 <> 0 & P _EQ_ (compell_ProjCo (z,p)) . Q holds
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
proof end;

theorem Th52: :: EC_PF_2:52
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) st not P _EQ_ Q & P _EQ_ (compell_ProjCo (z,p)) . Q holds
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
proof end;

theorem Th53: :: EC_PF_2:53
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g3 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p) st g3 = 3 mod p & P `2_3 = 0 & P `3_3 <> 0 holds
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) <> 0
proof end;

theorem Th54: :: EC_PF_2:54
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
(gf2 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))
proof end;

theorem Th55: :: EC_PF_2:55
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
(- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
proof end;

theorem Th56: :: EC_PF_2:56
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
((((z `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_3))
proof end;

theorem Th57: :: EC_PF_2:57
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
proof end;

theorem Th58: :: EC_PF_2:58
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
(((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p)
proof end;

theorem Th59: :: EC_PF_2:59
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_3)))
proof end;

theorem Th60: :: EC_PF_2:60
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g4 * (gf2 |^ 2)) * (P `3_3)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3)))
proof end;

theorem Th61: :: EC_PF_2:61
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3))
proof end;

theorem Th62: :: EC_PF_2:62
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))
proof end;

theorem Th63: :: EC_PF_2:63
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p)
proof end;

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
func addell_ProjCo (z,p) -> Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) means :: EC_PF_2:def 9
 for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies it . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies it . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
it . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
it . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) );
existence
ex b1 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) st
for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b1 . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies b1 . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b1 . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b1 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) )
proof end;
uniqueness
for b1, b2 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) st ( for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b1 . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies b1 . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b1 . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b1 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) ) & ( for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b2 . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies b2 . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b2 . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b2 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines addell_ProjCo EC_PF_2:def 9 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b3 being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) holds
( b3 = addell_ProjCo (z,p) iff for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies b3 . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies b3 . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
b3 . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
b3 . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) ) );

definition
let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
let F be Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p));
let Q, R be Element of EC_SetProjCo ((z `1),(z `2),p);
:: original: .
redefine func F . (Q,R) -> Element of EC_SetProjCo ((z `1),(z `2),p);
correctness
coherence
F . (Q,R) is Element of EC_SetProjCo ((z `1),(z `2),p);
proof end;
end;