let p be Prime; for a, b, d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
let a, b, d be Element of (GF p); ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b)) )
assume A1:
( p > 3 & Disc (a,b,p) <> 0. (GF p) )
; card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))
set F = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ;
set G = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ;
per cases
( { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {} or { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {} )
;
suppose A2:
{ Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = {}
;
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))A3:
{ (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = {}
proof
assume
{ (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } <> {}
;
contradiction
then consider z being
object such that A4:
z in { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) }
by XBOOLE_0:def 1;
consider Y being
Element of
(GF p) such that A5:
(
z = Class (
(R_EllCur (a,b,p)),
[d,Y,1]) &
[d,Y,1] in EC_SetProjCo (
a,
b,
p) )
by A4;
Y |^ 2
= ((d |^ 3) + (a * d)) + b
by A5, Th43;
then
Y in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b }
;
hence
contradiction
by A2;
verum
end;
2
< p
by A1, XXREAL_0:2;
hence
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1
+ (Lege_p (((d |^ 3) + (a * d)) + b))
by A3, A2, Th39;
verum end; suppose A6:
{ Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } <> {}
;
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1 + (Lege_p (((d |^ 3) + (a * d)) + b))then consider z being
object such that A7:
z in { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b }
by XBOOLE_0:def 1;
consider W being
Element of
(GF p) such that A8:
(
z = W &
W |^ 2
= ((d |^ 3) + (a * d)) + b )
by A7;
[d,W,1] is
Element of
EC_SetProjCo (
a,
b,
p)
by A8, Th43;
then A9:
Class (
(R_EllCur (a,b,p)),
[d,W,1])
in { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) }
;
consider I being
Function of
{ Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } ,
{ (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } such that A10:
(
I is
onto &
I is
one-to-one )
by A1, A6, Th58;
A11:
dom I = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b }
by A9, FUNCT_2:def 1;
A12:
rng I = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) }
by A10, FUNCT_2:def 3;
then A13:
card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } c= card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) }
by A10, A11, CARD_1:10;
reconsider h =
I " as
Function of
{ (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } ,
{ Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } by A10, A12, FUNCT_2:25;
(
(I ") * I = id { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } &
I * (I ") = id { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } )
by A10, A12, A9, FUNCT_2:29;
then A14:
(
h is
onto &
h is
one-to-one )
by FUNCT_2:23;
then A15:
rng h = { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b }
by FUNCT_2:def 3;
dom h = { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) }
by A6, FUNCT_2:def 1;
then
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } c= card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b }
by A14, A15, CARD_1:10;
then A16:
card { Y where Y is Element of (GF p) : Y |^ 2 = ((d |^ 3) + (a * d)) + b } = card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) }
by A13, XBOOLE_0:def 10;
2
< p
by A1, XXREAL_0:2;
hence
card { (Class ((R_EllCur (a,b,p)),[d,Y,1])) where Y is Element of (GF p) : [d,Y,1] in EC_SetProjCo (a,b,p) } = 1
+ (Lege_p (((d |^ 3) + (a * d)) + b))
by A16, Th39;
verum end;