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 holds
( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
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 holds
( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); ( P `3_3 <> 0 implies ( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) ) )
assume A1:
P `3_3 <> 0
; ( ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) iff ( P = Q or P = (compell_ProjCo (z,p)) . Q ) )
set a = z `1 ;
set b = z `2 ;
A2:
P `3_3 <> 0. (GF p)
by A1, EC_PF_1:11;
hereby ( ( P = Q or P = (compell_ProjCo (z,p)) . Q ) implies ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 ) )
assume A3:
(
P `1_3 = Q `1_3 &
P `3_3 = Q `3_3 )
;
( P = Q or P = (compell_ProjCo (z,p)) . Q )A4:
(((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by Th35;
(((Q `2_3) |^ 2) * (Q `3_3)) - ((((Q `1_3) |^ 3) + (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2))) + ((z `2) * ((Q `3_3) |^ 3))) = 0. (GF p)
by Th35;
then A5:
((Q `2_3) |^ 2) * (Q `3_3) =
(((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((Q `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))
by A3, VECTSP_1:19
.=
((P `2_3) |^ 2) * (P `3_3)
by A3, A4, VECTSP_1:19
;
(P `2_3) * (P `2_3) =
(P `2_3) |^ 2
by EC_PF_1:22
.=
(Q `2_3) |^ 2
by A2, A3, A5, VECTSP_1:5
.=
(Q `2_3) * (Q `2_3)
by EC_PF_1:22
;
then
(
P `2_3 = Q `2_3 or
P `2_3 = - (Q `2_3) )
by EC_PF_1:26;
then
(
P = [(Q `1_3),(Q `2_3),(Q `3_3)] or
P = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] )
by A3, Th31;
hence
(
P = Q or
P = (compell_ProjCo (z,p)) . Q )
by Th31, Def8;
verum
end;
assume A6:
( P = Q or P = (compell_ProjCo (z,p)) . Q )
; ( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 )
( P = [(Q `1_3),(Q `2_3),(Q `3_3)] or P = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] )
by A6, Th31, Def8;
hence
( P `1_3 = Q `1_3 & P `3_3 = Q `3_3 )
by Def3, Def5; verum