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 A2: 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
A3: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;
A4: ( PP `1_3 = P `1_3 & PP `2_3 = P `2_3 & PP `3_3 = P `3_3 ) by A3, ThECSet2;
set CP = (compell_ProjCo (z,p)) . P;
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),(P `3_3)] by DefCompEll;
then A6: ( ((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 DefX, DefY, DefZ;
set RP = rep_pt PP;
reconsider RP = rep_pt PP as Element of EC_SetProjCo ((z `1),(z `2),p) by A3, ThRepPoint1;
RP = [((P `1_3) * ((P `3_3) ")),((P `2_3) * ((P `3_3) ")),1] by A2, A4, DefRepPoint;
then A7: RP `2_3 = (P `2_3) * ((P `3_3) ") by DefY;
consider CPP being Element of ProjCo (GF p) such that
A8: ( CPP = (compell_ProjCo (z,p)) . P & CPP in EC_SetProjCo ((z `1),(z `2),p) ) ;
A9: ( CPP `1_3 = P `1_3 & CPP `2_3 = - (P `2_3) & CPP `3_3 = P `3_3 ) by A6, A8, ThECSet2;
set RCP = rep_pt CPP;
reconsider RCP = rep_pt CPP as Element of EC_SetProjCo ((z `1),(z `2),p) by A8, ThRepPoint1;
A11: RCP = [((P `1_3) * ((P `3_3) ")),((- (P `2_3)) * ((P `3_3) ")),1] by A2, A9, DefRepPoint;

hereby :: thesis: ( P `2_3 = 0 implies P _EQ_ (compell_ProjCo (z,p)) . P )

assume B1: P _EQ_ (compell_ProjCo (z,p)) . P ; :: thesis: P `2_3 = 0
P `3_3 <> 0. (GF p) by A2, EC_PF_1:11;
then B2: (P `3_3) " <> 0. (GF p) by VECTSP_1:25;
B3: p > 2 by LMZ1Z2, XXREAL_0:2;
RP = [((P `1_3) * ((P `3_3) ")),((- (P `2_3)) * ((P `3_3) ")),1] by A3, A8, A11, B1, ThRepPoint4;
then (P `2_3) * ((P `3_3) ") = ((P `3_3) ") * (- (P `2_3)) by A7, DefY;
then P `2_3 = - (P `2_3) by B2, 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 B3, EC_PF_1:27;
hence P `2_3 = 0 by EC_PF_1:11; :: thesis: verum

end;

assume B1: 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 A9, EC_PF_1:11;
hence P _EQ_ (compell_ProjCo (z,p)) . P by A8, B1, ThECSet2; :: thesis: verum