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 LMZ1Z2;
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) )
;
A6:
P `3_3 <> 0
proof
assume B1:
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) ;
B2:
PP `3_3 = 0
by B1, A4, ThECSet2;
consider OO being
Element of
ProjCo (GF p) such that B3:
OO in EC_SetProjCo (
(z `1),
(z `2),
p)
and B4:
PP _EQ_ OO
and B5:
(
OO `1_3 = 0 &
OO `2_3 = 1 &
OO `3_3 = 0 )
by A1, A4, B2, EC_PF_1:49;
consider O being
Element of
EC_SetProjCo (
(z `1),
(z `2),
p)
such that B6:
O = OO
by B3;
B7:
(
O `1_3 = 0 &
O `2_3 = 1 &
O `3_3 = 0 )
by B5, B6, ThECSet2;
CQ _EQ_ O
by A3, A4, B4, B6, EC_PF_1:44;
then
(compell_ProjCo (z,p)) . CQ _EQ_ (compell_ProjCo (z,p)) . O
by ThEQCOMP1;
then B9:
Q _EQ_ (compell_ProjCo (z,p)) . O
by ThCOMPELL1;
(compell_ProjCo (z,p)) . O _EQ_ O
by B7, ThECSet1, ThCOMPELL0;
then
Q _EQ_ O
by B9, EC_PF_1:44;
hence
contradiction
by A2, A4, B4, B6, EC_PF_1:44;
verum
end;
A7:
Q `3_3 <> 0
proof
assume B1:
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 DefCompEll;
then B3:
CQ `3_3 = 0
by B1, MCART_1:def 7;
consider OO being
Element of
ProjCo (GF p) such that B4:
OO in EC_SetProjCo (
(z `1),
(z `2),
p)
and B5:
CQ _EQ_ OO
and B6:
(
OO `1_3 = 0 &
OO `2_3 = 1 &
OO `3_3 = 0 )
by A1, B3, EC_PF_1:49;
consider O being
Element of
EC_SetProjCo (
(z `1),
(z `2),
p)
such that B7:
O = OO
by B4;
B8:
(
O `1_3 = 0 &
O `2_3 = 1 &
O `3_3 = 0 )
by B6, B7, ThECSet2;
P _EQ_ O
by A3, B5, B7, EC_PF_1:44;
then B10:
(compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . O
by ThEQCOMP1;
(compell_ProjCo (z,p)) . O _EQ_ O
by B8, ThECSet1, ThCOMPELL0;
then
(compell_ProjCo (z,p)) . P _EQ_ O
by B10, EC_PF_1:44;
then
CQ _EQ_ (compell_ProjCo (z,p)) . P
by B5, B7, EC_PF_1:44;
hence
contradiction
by A2, ThEQCOMP1;
verum
end;
P `2_3 <> 0
hence
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
by A3, A6, A7, ThECEQ3; verum