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 & 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; 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); ( 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 )
; ( 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
; (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)
; 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; verum