let p be 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) )
let z be 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) )
let P be Element of EC_SetProjCo ((z `1),(z `2),p); ( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )
set a = z `1 ;
set b = z `2 ;
A1:
( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) )
by Th30;
consider PP being Element of ProjCo (GF p) such that
A2:
( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) )
;
per cases
( P `3_3 = 0 or P `3_3 <> 0 )
;
suppose
P `3_3 = 0
;
( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )then A3:
PP `3_3 = 0
by A2, Th32;
consider Q being
Element of
ProjCo (GF p) such that A4:
(
Q in EC_SetProjCo (
(z `1),
(z `2),
p) &
Q _EQ_ PP )
and A5:
(
Q `1_3 = 0 &
Q `2_3 = 1 &
Q `3_3 = 0 )
by A1, A2, A3, EC_PF_1:49;
rep_pt PP = [0,1,0]
by A3, Def7;
hence
(
rep_pt P _EQ_ P &
rep_pt P in EC_SetProjCo (
(z `1),
(z `2),
p) )
by A2, A4, A5, AA;
verum end; suppose
P `3_3 <> 0
;
( rep_pt P _EQ_ P & rep_pt P in EC_SetProjCo ((z `1),(z `2),p) )then A6:
PP `3_3 <> 0
by A2, Th32;
consider Q being
Element of
ProjCo (GF p) such that A7:
(
Q in EC_SetProjCo (
(z `1),
(z `2),
p) &
Q _EQ_ PP )
and A8:
Q `3_3 = 1
by A1, A2, A6, EC_PF_1:48;
consider d being
Element of
(GF p) such that
d <> 0. (GF p)
and A9:
(
Q `1_3 = d * (PP `1_3) &
Q `2_3 = d * (PP `2_3) &
Q `3_3 = d * (PP `3_3) )
by A7, EC_PF_1:def 10;
A10:
d * (PP `3_3) = 1. (GF p)
by A8, A9, EC_PF_1:12;
PP `3_3 <> 0. (GF p)
by A6, EC_PF_1:11;
then
d = (PP `3_3) "
by A10, VECTSP_1:def 10;
then
Q = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1]
by A8, A9, AA;
hence
(
rep_pt P _EQ_ P &
rep_pt P in EC_SetProjCo (
(z `1),
(z `2),
p) )
by A2, A6, A7, Def7;
verum end;