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 not P _EQ_ Q & 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 not P _EQ_ Q & 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); ( not P _EQ_ Q & P _EQ_ (compell_ProjCo (z,p)) . Q implies (P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3) )
set a = z `1 ;
set b = z `2 ;
A1:
( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) )
by Th30;
assume A2:
not P _EQ_ Q
; ( not P _EQ_ (compell_ProjCo (z,p)) . Q or (P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3) )
assume A3:
P _EQ_ (compell_ProjCo (z,p)) . Q
; (P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
consider PP being Element of ProjCo (GF p) such that
A4:
( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) )
;
A5:
P `3_3 <> 0
proof
assume A6:
P `3_3 = 0
;
contradiction
set CQ =
(compell_ProjCo (z,p)) . Q;
reconsider CQ =
(compell_ProjCo (z,p)) . Q as
Element of
EC_SetProjCo (
(z `1),
(z `2),
p) ;
A7:
PP `3_3 = 0
by A6, A4, Th32;
consider OO being
Element of
ProjCo (GF p) such that A8:
OO in EC_SetProjCo (
(z `1),
(z `2),
p)
and A9:
PP _EQ_ OO
and A10:
(
OO `1_3 = 0 &
OO `2_3 = 1 &
OO `3_3 = 0 )
by A1, A4, A7, EC_PF_1:49;
consider O being
Element of
EC_SetProjCo (
(z `1),
(z `2),
p)
such that A11:
O = OO
by A8;
A12:
(
O `1_3 = 0 &
O `2_3 = 1 &
O `3_3 = 0 )
by A10, A11, Th32;
CQ _EQ_ O
by A3, A4, A9, A11, EC_PF_1:44;
then
(compell_ProjCo (z,p)) . CQ _EQ_ (compell_ProjCo (z,p)) . O
by Th46;
then A13:
Q _EQ_ (compell_ProjCo (z,p)) . O
by Th41;
(compell_ProjCo (z,p)) . O _EQ_ O
by A12, Th31, Th40;
then
Q _EQ_ O
by A13, EC_PF_1:44;
hence
contradiction
by A2, A4, A9, A11, EC_PF_1:44;
verum
end;
A14:
Q `3_3 <> 0
proof
assume A15:
Q `3_3 = 0
;
contradiction
set CQ =
(compell_ProjCo (z,p)) . Q;
reconsider CQ =
(compell_ProjCo (z,p)) . Q as
Element of
ProjCo (GF p) ;
CQ = [(Q `1_3),(- (Q `2_3)),(Q `3_3)]
by Def8;
then A16:
CQ `3_3 = 0
by A15;
consider OO being
Element of
ProjCo (GF p) such that A17:
OO in EC_SetProjCo (
(z `1),
(z `2),
p)
and A18:
CQ _EQ_ OO
and A19:
(
OO `1_3 = 0 &
OO `2_3 = 1 &
OO `3_3 = 0 )
by A1, A16, EC_PF_1:49;
consider O being
Element of
EC_SetProjCo (
(z `1),
(z `2),
p)
such that A20:
O = OO
by A17;
A21:
(
O `1_3 = 0 &
O `2_3 = 1 &
O `3_3 = 0 )
by A19, A20, Th32;
P _EQ_ O
by A3, A18, A20, EC_PF_1:44;
then A22:
(compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . O
by Th46;
(compell_ProjCo (z,p)) . O _EQ_ O
by A21, Th31, Th40;
then
(compell_ProjCo (z,p)) . P _EQ_ O
by A22, EC_PF_1:44;
then
CQ _EQ_ (compell_ProjCo (z,p)) . P
by A18, A20, EC_PF_1:44;
hence
contradiction
by A2, Th46;
verum
end;
P `2_3 <> 0
hence
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
by A3, A5, A14, Th51; verum