:: Operations of Points on Elliptic Curve in Affine Coordinates
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users

theorem ThRepPoint5: :: EC_PF_3:1

for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st ( P = [0,1,0] or P `3_3 = 1 ) holds
rep_pt P = P

proof end;

theorem ThEQO: :: EC_PF_3:2

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( P `3_3 = 0 iff P _EQ_ O )

proof end;

theorem ThEQCOMP4: :: EC_PF_3:3

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

proof end;

theorem ThAddCompProjCo: :: EC_PF_3:4

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
(addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O

proof end;

definition

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

func EC_SetAffCo (z,p) -> non empty Subset of (EC_SetProjCo ((z `1),(z `2),p)) equals :: EC_PF_3:def 1
{ P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } ;

correctness
coherence
{ P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } is non empty Subset of (EC_SetProjCo ((z `1),(z `2),p));

proof end;

end;

:: deftheorem defines EC_SetAffCo EC_PF_3:def 1 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds EC_SetAffCo (z,p) = { P where P is Element of EC_SetProjCo ((z `1),(z `2),p) : ( P `3_3 = 1 or P = [0,1,0] ) } ;

theorem ThAffCoZero: :: EC_PF_3:5

for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds [0,1,0] is Element of EC_SetAffCo (z,p)

proof end;

theorem ThAffCo: :: EC_PF_3:6

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 is Element of EC_SetAffCo (z,p)

proof end;

theorem ThRepPoint6: :: EC_PF_3:7

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 in EC_SetAffCo (z,p) holds
rep_pt P = P

proof end;

theorem ThRepPoint7: :: EC_PF_3:8

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O holds
(rep_pt P) `3_3 = 1

proof end;

theorem :: EC_PF_3:9

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & rep_pt P _EQ_ O holds
( rep_pt P = O & P _EQ_ O )

proof end;

theorem LmRepPoint9: :: EC_PF_3:10

for p being 5 _or_greater Prime
for P being Element of ProjCo (GF p) holds rep_pt (rep_pt P) = rep_pt P

proof end;

theorem :: EC_PF_3:11

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 rep_pt P _EQ_ rep_pt Q holds
rep_pt P = rep_pt Q

proof end;

definition

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

func compell_AffCo (z,p) -> UnOp of (EC_SetAffCo (z,p)) means :DefAffCompEll: :: EC_PF_3:def 2
for P being Element of EC_SetAffCo (z,p) holds it . P = rep_pt ((compell_ProjCo (z,p)) . P);

existence
ex b₁ being UnOp of (EC_SetAffCo (z,p)) st
for P being Element of EC_SetAffCo (z,p) holds b₁ . P = rep_pt ((compell_ProjCo (z,p)) . P)

proof end;

uniqueness
for b₁, b₂ being UnOp of (EC_SetAffCo (z,p)) st ( for P being Element of EC_SetAffCo (z,p) holds b₁ . P = rep_pt ((compell_ProjCo (z,p)) . P) ) & ( for P being Element of EC_SetAffCo (z,p) holds b₂ . P = rep_pt ((compell_ProjCo (z,p)) . P) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefAffCompEll defines compell_AffCo EC_PF_3:def 2 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b₃ being UnOp of (EC_SetAffCo (z,p)) holds
( b₃ = compell_AffCo (z,p) iff for P being Element of EC_SetAffCo (z,p) holds b₃ . P = rep_pt ((compell_ProjCo (z,p)) . P) );

definition

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
let F be Function of (EC_SetAffCo (z,p)),(EC_SetAffCo (z,p));
let P be Element of EC_SetAffCo (z,p);
:: original: .
redefine func F . P -> Element of EC_SetAffCo (z,p);
correctness
coherence
F . P is Element of EC_SetAffCo (z,p);

proof end;

end;

definition

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

func addell_AffCo (z,p) -> BinOp of (EC_SetAffCo (z,p)) means :DefAffAddEll: :: EC_PF_3:def 3
for P, Q being Element of EC_SetAffCo (z,p) holds it . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q));

existence
ex b₁ being BinOp of (EC_SetAffCo (z,p)) st
for P, Q being Element of EC_SetAffCo (z,p) holds b₁ . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q))

proof end;

uniqueness
for b₁, b₂ being BinOp of (EC_SetAffCo (z,p)) st ( for P, Q being Element of EC_SetAffCo (z,p) holds b₁ . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) ) & ( for P, Q being Element of EC_SetAffCo (z,p) holds b₂ . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefAffAddEll defines addell_AffCo EC_PF_3:def 3 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b₃ being BinOp of (EC_SetAffCo (z,p)) holds
( b₃ = addell_AffCo (z,p) iff for P, Q being Element of EC_SetAffCo (z,p) holds b₃ . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) );

definition

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;
let F be Function of [:(EC_SetAffCo (z,p)),(EC_SetAffCo (z,p)):],(EC_SetAffCo (z,p));
let Q, R be Element of EC_SetAffCo (z,p);
:: original: .
redefine func F . (Q,R) -> Element of EC_SetAffCo (z,p);
correctness
coherence
F . (Q,R) is Element of EC_SetAffCo (z,p);

proof end;

end;

theorem ThUnityProjCo: :: EC_PF_3:12

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )

proof end;

theorem ThLeftZeroedAffCo: :: EC_PF_3:13

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
(addell_AffCo (z,p)) . (O,P) = P

proof end;

theorem ThRightZeroedAffCo: :: EC_PF_3:14

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
(addell_AffCo (z,p)) . (P,O) = P

proof end;

theorem ThUnityAffCo: :: EC_PF_3:15

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
O is_a_unity_wrt addell_AffCo (z,p)

proof end;

theorem ThAddCompAffCo: :: EC_PF_3:16

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetAffCo (z,p) st O = [0,1,0] holds
(addell_AffCo (z,p)) . (P,((compell_AffCo (z,p)) . P)) = O

proof end;

theorem LmCommutative1: :: EC_PF_3:17

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q, O, PQ, QP being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = - (PQ `1_3) & QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) )

proof end;

theorem LmCommutative2: :: EC_PF_3:18

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q, O, PQ, QP being Element of EC_SetProjCo ((z `1),(z `2),p)
for d being Element of (GF p) st O = [0,1,0] & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = (d |^ 6) * (PQ `1_3) & QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) )

proof end;

theorem ThCommutativeProjCo: :: EC_PF_3:19

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 (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)

proof end;

theorem ThCommutativeAffCo: :: EC_PF_3:20

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q being Element of EC_SetAffCo (z,p) holds (addell_AffCo (z,p)) . (P,Q) = (addell_AffCo (z,p)) . (Q,P)

proof end;

registration

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

cluster addell_AffCo (z,p) -> non empty commutative having_a_unity ;

correctness
coherence
( not addell_AffCo (z,p) is empty & addell_AffCo (z,p) is commutative & addell_AffCo (z,p) is having_a_unity );

proof end;

end;

definition

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

func 0_EC (z,p) -> Element of EC_SetAffCo (z,p) equals :: EC_PF_3:def 4
[0,1,0];

correctness
coherence
[0,1,0] is Element of EC_SetAffCo (z,p);
by ThAffCoZero;

end;

:: deftheorem defines 0_EC EC_PF_3:def 4 :
for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds 0_EC (z,p) = [0,1,0];

registration

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

cluster addMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) -> Abelian ;

coherence
addMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is Abelian by ThCommutativeAffCo;

cluster addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) -> right_zeroed left_zeroed ;

coherence
( addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is left_zeroed & addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is right_zeroed )

proof end;

end;

ThECSTRLeftComp: for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is left_complementable

proof end;

ThECSTRRightComp: for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is right_complementable

proof end;

registration

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

cluster addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) -> complementable ;

coherence
addLoopStr(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)),(0_EC (z,p)) #) is complementable by ThECSTRLeftComp, ThECSTRRightComp;

end;

registration

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

cluster multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) -> unital ;

coherence
multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is unital

proof end;

end;

theorem GP0: :: EC_PF_3:21

for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds 1_ multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) = 0_EC (z,p)

proof end;

registration

let p be 5 _or_greater Prime;
let z be Element of EC_WParam p;

cluster multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) -> non empty Group-like commutative ;

coherence
( multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is commutative & multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is Group-like & not multMagma(# (EC_SetAffCo (z,p)),(addell_AffCo (z,p)) #) is empty )

proof end;

end;

theorem ThAdd1: :: EC_PF_3:22

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P1, P2, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P1 _EQ_ P2 holds
(addell_ProjCo (z,p)) . (P1,Q) _EQ_ (addell_ProjCo (z,p)) . (P2,Q)

proof end;

theorem ThAdd2: :: EC_PF_3:23

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q1, Q2 being Element of EC_SetProjCo ((z `1),(z `2),p) st Q1 _EQ_ Q2 holds
(addell_ProjCo (z,p)) . (P,Q1) _EQ_ (addell_ProjCo (z,p)) . (P,Q2)

proof end;

theorem ThAdd3: :: EC_PF_3:24

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P1, P2, Q1, Q2 being Element of EC_SetProjCo ((z `1),(z `2),p) st P1 _EQ_ P2 & Q1 _EQ_ Q2 holds
(addell_ProjCo (z,p)) . (P1,Q1) _EQ_ (addell_ProjCo (z,p)) . (P2,Q2)

proof end;

theorem ThCompellO: :: EC_PF_3:25

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( P _EQ_ O iff (compell_ProjCo (z,p)) . P _EQ_ O )

proof end;

theorem ThEQX: :: EC_PF_3:26

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 a being Element of (GF p) st a <> 0. (GF p) & P `1_3 = a * (Q `1_3) & P `2_3 = a * (Q `2_3) & P `3_3 = a * (Q `3_3) holds
P _EQ_ Q

proof end;

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)]

proof end;

theorem LmAddEll2: :: EC_PF_3:28

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, 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))]

proof end;

theorem LmCompAddCom: :: EC_PF_3:29

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 = 1 & Q `3_3 = 1 holds
(compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))

proof end;

theorem :: EC_PF_3:30

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 (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))

proof end;

theorem :: EC_PF_3:31

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O holds
( P `2_3 = 0. (GF p) iff (addell_ProjCo (z,p)) . (P,P) _EQ_ O )

proof end;