let p be 5 _or_greater Prime; :: thesis: 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; :: thesis: 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); :: thesis: ( P `3_3 <> 0 implies ( P _EQ_ (compell_ProjCo (z,p)) . P iff P `2_3 = 0 ) )
assume A1: P `3_3 <> 0 ; :: thesis: ( 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 :: thesis: ( P `2_3 = 0 implies P _EQ_ (compell_ProjCo (z,p)) . P )

assume A9: P _EQ_ (compell_ProjCo (z,p)) . P ; :: thesis: 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; :: thesis: verum

end;

assume A12: P `2_3 = 0 ; :: thesis: 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; :: thesis: verum