let p be 5 _or_greater Prime; 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; 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); ( 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 )
; ( ( 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; verum