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) st P `3_3 <> 0 holds
( P _EQ_ (compell_ProjCo (z,p)) . P iff P `2_3 = 0 )
let z be 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 )
let P be Element of EC_SetProjCo ((z `1),(z `2),p); ( P `3_3 <> 0 implies ( P _EQ_ (compell_ProjCo (z,p)) . P iff P `2_3 = 0 ) )
assume A1:
P `3_3 <> 0
; ( P _EQ_ (compell_ProjCo (z,p)) . P iff P `2_3 = 0 )
set a = z `1 ;
set b = z `2 ;
consider PP being Element of ProjCo (GF p) such that
A2:
( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) )
;
A3:
( PP `1_3 = P `1_3 & PP `2_3 = P `2_3 & PP `3_3 = P `3_3 )
by A2, Th32;
set CP = (compell_ProjCo (z,p)) . P;
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),(P `3_3)]
by Def8;
then A4:
( ((compell_ProjCo (z,p)) . P) `1_3 = P `1_3 & ((compell_ProjCo (z,p)) . P) `2_3 = - (P `2_3) & ((compell_ProjCo (z,p)) . P) `3_3 = P `3_3 )
by Def3, Def4, Def5;
set RP = rep_pt PP;
reconsider RP = rep_pt PP as Element of EC_SetProjCo ((z `1),(z `2),p) by A2, Th36;
RP = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1]
by A1, A3, Def7;
then A5:
RP `2_3 = (P `2_3) * ((P `3_3) ")
by Def4;
consider CPP being Element of ProjCo (GF p) such that
A6:
( CPP = (compell_ProjCo (z,p)) . P & CPP in EC_SetProjCo ((z `1),(z `2),p) )
;
A7:
( CPP `1_3 = P `1_3 & CPP `2_3 = - (P `2_3) & CPP `3_3 = P `3_3 )
by A4, A6, Th32;
set RCP = rep_pt CPP;
reconsider RCP = rep_pt CPP as Element of EC_SetProjCo ((z `1),(z `2),p) by A6, Th36;
A8:
RCP = [((P `1_3) * ((P `3_3) ")),((- (P `2_3)) * ((P `3_3) ")),1]
by A1, A7, Def7;
hereby ( P `2_3 = 0 implies P _EQ_ (compell_ProjCo (z,p)) . P )
assume A9:
P _EQ_ (compell_ProjCo (z,p)) . P
;
P `2_3 = 0
P `3_3 <> 0. (GF p)
by A1, EC_PF_1:11;
then A10:
(P `3_3) " <> 0. (GF p)
by VECTSP_1:25;
A11:
p > 2
by Th30, XXREAL_0:2;
RP = [((P `1_3) * ((P `3_3) ")),((- (P `2_3)) * ((P `3_3) ")),1]
by A2, A6, A8, A9, Th39;
then
(P `2_3) * ((P `3_3) ") = ((P `3_3) ") * (- (P `2_3))
by A5, Def4;
then
P `2_3 = - (P `2_3)
by A10, VECTSP_1:5;
then
(P `2_3) + (P `2_3) = 0. (GF p)
by VECTSP_1:19;
then
P `2_3 = 0. (GF p)
by A11, EC_PF_1:27;
hence
P `2_3 = 0
by EC_PF_1:11;
verum
end;
assume A12:
P `2_3 = 0
; P _EQ_ (compell_ProjCo (z,p)) . P
then
P `2_3 = 0. (GF p)
by EC_PF_1:11;
then
- (P `2_3) = 0. (GF p)
by VECTSP_2:3;
then
( CPP `1_3 = P `1_3 & CPP `2_3 = 0 & CPP `3_3 = P `3_3 )
by A7, EC_PF_1:11;
hence
P _EQ_ (compell_ProjCo (z,p)) . P
by A6, A12, Th32; verum