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 & P `2_3 <> 0 & P _EQ_ (compell_ProjCo (z,p)) . Q holds
(P `2_3) * (Q `3_3) <> (Q `2_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 & P `2_3 <> 0 & P _EQ_ (compell_ProjCo (z,p)) . Q holds
(P `2_3) * (Q `3_3) <> (Q `2_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 & P `2_3 <> 0 & P _EQ_ (compell_ProjCo (z,p)) . Q implies (P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3) )
assume A1: ( P `3_3 <> 0 & Q `3_3 <> 0 & P `2_3 <> 0 ) ; :: thesis: ( not P _EQ_ (compell_ProjCo (z,p)) . Q or (P `2_3) * (Q `3_3) <> (Q `2_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;
assume A7: P _EQ_ (compell_ProjCo (z,p)) . Q ; :: thesis: (P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
assume A8: (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3) ; :: thesis: contradiction
(P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3) by A1, A7, Th50;
then A9: (P `1_3) * ((P `3_3) ") = (Q `1_3) * ((Q `3_3) ") by A2, Th4;
A10: (P `2_3) * ((P `3_3) ") = (Q `2_3) * ((Q `3_3) ") by A2, A8, Th4;
rep_pt P = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by A1, A3, A4, Def7
.= rep_pt Q by A1, A4, A5, A6, A9, A10, Def7 ;
then A11: P _EQ_ Q by Th39;
(compell_ProjCo (z,p)) . P _EQ_ Q by A7, Th47;
then P _EQ_ (compell_ProjCo (z,p)) . P by A11, EC_PF_1:44;
hence contradiction by A1, Th44; :: thesis: verum