let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 & Q `3_3 <> 0 holds
( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) )
let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 & Q `3_3 <> 0 holds
( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P `3_3 <> 0 & Q `3_3 <> 0 implies ( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) ) )
assume A1: ( P `3_3 <> 0 & Q `3_3 <> 0 ) ; :: thesis: ( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) )
A2: ( P `3_3 <> 0. (GF p) & Q `3_3 <> 0. (GF p) ) by A1, EC_PF_1:11;
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, Th32;
consider QQ being Element of ProjCo (GF p) such that
A5: ( QQ = Q & QQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
A6: ( QQ `1_3 = Q `1_3 & QQ `2_3 = Q `2_3 & QQ `3_3 = Q `3_3 ) by A5, Th32;
A7: ( PP `3_3 <> 0 & QQ `3_3 <> 0 ) by A1, A3, A5, Th32;
set RP = rep_pt PP;
reconsider RP = rep_pt PP as Element of EC_SetProjCo ((z `1),(z `2),p) by A3, Th36;
set RQ = rep_pt QQ;
reconsider RQ = rep_pt QQ as Element of EC_SetProjCo ((z `1),(z `2),p) by A5, Th36;
A8: RP = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by A7, Def7;
RQ = [((QQ `1_3) * ((QQ `3_3) ")),((QQ `2_3) * ((QQ `3_3) ")),1] by A7, Def7;
then A9: ( RQ `1_3 = (QQ `1_3) * ((QQ `3_3) ") & RQ `3_3 = 1 ) by Def3, Def5;
then A10: RP `3_3 = RQ `3_3 by A8, Def5;
A11: RP `3_3 <> 0 by A8, Def5;
then ( not RP `1_3 = RQ `1_3 or rep_pt P = rep_pt Q or RP = (compell_ProjCo (z,p)) . RQ ) by A3, A5, A10, Th45;
then A12: ( not (P `1_3) * ((PP `3_3) ") = (Q `1_3) * ((QQ `3_3) ") or P _EQ_ Q or RP = (compell_ProjCo (z,p)) . RQ ) by A4, A6, A8, A9, Def3, Th39;
( ( RP = RQ or RP = (compell_ProjCo (z,p)) . RQ ) implies RP `1_3 = RQ `1_3 ) by A11, Th45;
then ( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) implies (P `1_3) * ((P `3_3) ") = (Q `1_3) * ((Q `3_3) ") ) by A1, A3, A4, A5, A6, A8, A9, Def3, Th39, Th48;
hence ( ( P _EQ_ Q or P _EQ_ (compell_ProjCo (z,p)) . Q ) iff (P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) ) by A2, A1, A3, A4, A5, A6, A12, Th3, Th4, Th48; :: thesis: verum