:: Operations of Points on Elliptic Curve in Affine Coordinates
:: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama
::
:: 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;

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
() 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
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 b1 being UnOp of (EC_SetAffCo (z,p)) st
for P being Element of EC_SetAffCo (z,p) holds b1 . P = rep_pt ((compell_ProjCo (z,p)) . P)
proof end;
uniqueness
for b1, b2 being UnOp of (EC_SetAffCo (z,p)) st ( for P being Element of EC_SetAffCo (z,p) holds b1 . P = rep_pt ((compell_ProjCo (z,p)) . P) ) & ( for P being Element of EC_SetAffCo (z,p) holds b2 . P = rep_pt ((compell_ProjCo (z,p)) . P) ) holds
b1 = b2
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 b3 being UnOp of (EC_SetAffCo (z,p)) holds
( b3 = compell_AffCo (z,p) iff for P being Element of EC_SetAffCo (z,p) holds b3 . 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 b1 being BinOp of (EC_SetAffCo (z,p)) st
for P, Q being Element of EC_SetAffCo (z,p) holds b1 . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q))
proof end;
uniqueness
for b1, b2 being BinOp of (EC_SetAffCo (z,p)) st ( for P, Q being Element of EC_SetAffCo (z,p) holds b1 . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) ) & ( for P, Q being Element of EC_SetAffCo (z,p) holds b2 . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) ) holds
b1 = b2
proof end;
end;

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for b3 being BinOp of (EC_SetAffCo (z,p)) holds
( b3 = addell_AffCo (z,p) iff for P, Q being Element of EC_SetAffCo (z,p) holds b3 . (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
proof end;

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;
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;
coherence
by ThCommutativeAffCo;
coherence
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;
coherence
by ;
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;

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
proof end;

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
proof end;

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
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;

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;

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;

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;