set a = z `1 ;
set b = z `2 ;
A1:
( p > 2 + 1 & Disc ((z `1),(z `2),p) <> 0. (GF p) )
by Th30;
defpred S1[ Element of EC_SetProjCo ((z `1),(z `2),p), Element of EC_SetProjCo ((z `1),(z `2),p), set ] means for O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( $1 _EQ_ O implies $3 = $2 ) & ( $2 _EQ_ O & not $1 _EQ_ O implies $3 = $1 ) & ( not $1 _EQ_ O & not $2 _EQ_ O & not $1 _EQ_ $2 implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = (($2 `2_3) * ($1 `3_3)) - (($1 `2_3) * ($2 `3_3)) & gf2 = (($2 `1_3) * ($1 `3_3)) - (($1 `1_3) * ($2 `3_3)) & gf3 = ((((gf1 |^ 2) * ($1 `3_3)) * ($2 `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * ($1 `1_3)) * ($2 `3_3)) holds
$3 = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * ($1 `1_3)) * ($2 `3_3)) - gf3)) - (((gf2 |^ 3) * ($1 `2_3)) * ($2 `3_3))),(((gf2 |^ 3) * ($1 `3_3)) * ($2 `3_3))] ) & ( not $1 _EQ_ O & not $2 _EQ_ O & $1 _EQ_ $2 implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * (($1 `3_3) |^ 2)) + (g3 * (($1 `1_3) |^ 2)) & gf2 = ($1 `2_3) * ($1 `3_3) & gf3 = (($1 `1_3) * ($1 `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
$3 = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * (($1 `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) );
A2:
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]
proof
let P,
Q be
Element of
EC_SetProjCo (
(z `1),
(z `2),
p);
ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]
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;
set O =
[0,1,0];
reconsider O =
[0,1,0] as
Element of
EC_SetProjCo (
(z `1),
(z `2),
p)
by EC_PF_1:42;
consider OO being
Element of
ProjCo (GF p) such that A7:
(
OO = O &
OO in EC_SetProjCo (
(z `1),
(z `2),
p) )
;
per cases
( P _EQ_ O or ( Q _EQ_ O & not P _EQ_ O ) or ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q ) or ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q ) )
;
suppose A10:
( not
P _EQ_ O & not
Q _EQ_ O & not
P _EQ_ Q )
;
ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]A11:
OO `3_3 = 0
by A7;
rep_pt PP <> rep_pt OO
by A3, A7, A10, Th39;
then
rep_pt PP <> [0,1,0]
by A11, Def7;
then A12:
(rep_pt PP) `3_3 <> 0
by Th37;
then A13:
P `3_3 <> 0
by A4, Th38;
rep_pt QQ <> rep_pt OO
by A5, A7, A10, Th39;
then
rep_pt QQ <> [0,1,0]
by A11, Def7;
then
(rep_pt QQ) `3_3 <> 0
by Th37;
then A14:
Q `3_3 <> 0
by A6, Th38;
reconsider g2 = 2
mod p as
Element of
(GF p) by EC_PF_1:14;
set gf1 =
((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3));
set gf2 =
((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3));
set gf3 =
(((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3));
reconsider gf1 =
((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)),
gf2 =
((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)),
gf3 =
(((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3)) as
Element of
(GF p) ;
set R =
[(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))];
reconsider R =
[(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] as
Element of
[: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
per cases
( P _EQ_ (compell_ProjCo (z,p)) . Q or not P _EQ_ (compell_ProjCo (z,p)) . Q )
;
suppose A15:
P _EQ_ (compell_ProjCo (z,p)) . Q
;
ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]then
(P `1_3) * (Q `3_3) = (Q `1_3) * (P `3_3)
by A13, A14, Th50;
then A16:
gf2 = 0. (GF p)
by VECTSP_1:19;
then A17:
(
gf2 |^ 2
= 0. (GF p) &
gf2 |^ 3
= 0. (GF p) )
by Th5;
(P `2_3) * (Q `3_3) <> (Q `2_3) * (P `3_3)
by A10, A15, Th52;
then
gf1 <> 0. (GF p)
by VECTSP_1:19;
then A18:
gf1 <> 0
by EC_PF_1:11;
then A19:
gf1 |^ 2
<> 0
by EC_PF_1:25;
A20:
gf3 =
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((0. (GF p)) + (((g2 * (0. (GF p))) * (P `1_3)) * (Q `3_3)))
by A17, VECTSP_1:17
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (0. (GF p))
by ALGSTR_1:7
.=
((gf1 |^ 2) * (P `3_3)) * (Q `3_3)
by VECTSP_1:18
.=
(gf1 |^ 2) * ((P `3_3) * (Q `3_3))
by GROUP_1:def 3
;
(P `3_3) * (Q `3_3) <> 0
by A13, A14, EC_PF_1:20;
then
gf3 <> 0
by A19, A20, EC_PF_1:20;
then
gf1 * gf3 <> 0
by A18, EC_PF_1:20;
then A21:
gf1 * gf3 <> 0. (GF p)
by EC_PF_1:11;
(gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3)) =
(gf1 * (((0. (GF p)) * ((P `1_3) * (Q `3_3))) - gf3)) - (((0. (GF p)) * (P `2_3)) * (Q `3_3))
by A17
.=
gf1 * ((0. (GF p)) - gf3)
by VECTSP_1:18
.=
gf1 * (- gf3)
by VECTSP_1:18
.=
- (gf1 * gf3)
by VECTSP_1:8
;
then
(gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3)) <> 0. (GF p)
by A21, VECTSP_2:3;
then A22:
R `2_3 <> 0. (GF p)
;
then
R <> [0,0,0]
by EC_PF_1:11;
then
not
R in {[0,0,0]}
by TARSKI:def 1;
then
R in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]}
by XBOOLE_0:def 5;
then reconsider R =
R as
Element of
ProjCo (GF p) by EC_PF_1:40;
R in EC_SetProjCo (
(z `1),
(z `2),
p)
proof
A23:
R `1_3 = 0. (GF p)
by A16;
A24:
R `3_3 = 0. (GF p)
by A17;
set d =
R `2_3 ;
reconsider d =
R `2_3 as
Element of
(GF p) ;
A25:
(
OO `1_3 = 0 &
OO `2_3 = 1 &
OO `3_3 = 0 )
by A7;
A26:
d * (OO `1_3) =
0
by A25, EC_PF_1:20
.=
R `1_3
by A23, EC_PF_1:11
;
A27:
d * (OO `3_3) =
0
by A25, EC_PF_1:20
.=
R `3_3
by A24, EC_PF_1:11
;
d * (OO `2_3) =
d * (1. (GF p))
by A25, EC_PF_1:12
.=
R `2_3
;
hence
R in EC_SetProjCo (
(z `1),
(z `2),
p)
by A1, A7, A22, A26, A27, EC_PF_1:45;
verum
end; then reconsider R =
R as
Element of
EC_SetProjCo (
(z `1),
(z `2),
p) ;
take
R
;
S1[P,Q,R]thus
S1[
P,
Q,
R]
by A10;
verum end; suppose
not
P _EQ_ (compell_ProjCo (z,p)) . Q
;
ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]then
(P `1_3) * (Q `3_3) <> (Q `1_3) * (P `3_3)
by A10, A13, A14, Th50;
then A28:
gf2 <> 0. (GF p)
by VECTSP_1:19;
then
gf2 <> 0
by EC_PF_1:11;
then A29:
gf2 |^ 3
<> 0
by EC_PF_1:25;
(P `3_3) * (Q `3_3) <> 0
by A13, A14, EC_PF_1:20;
then
(gf2 |^ 3) * ((P `3_3) * (Q `3_3)) <> 0
by A29, EC_PF_1:20;
then
(gf2 |^ 3) * ((P `3_3) * (Q `3_3)) <> 0. (GF p)
by EC_PF_1:11;
then A30:
((gf2 |^ 3) * (P `3_3)) * (Q `3_3) <> 0. (GF p)
by GROUP_1:def 3;
R `3_3 <> 0. (GF p)
by A30;
then
R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))]
;
then
not
R in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]}
by TARSKI:def 1;
then
R in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[(0. (GF p)),(0. (GF p)),(0. (GF p))]}
by XBOOLE_0:def 5;
then reconsider R =
R as
Element of
ProjCo (GF p) by EC_PF_1:def 6;
gf2 * gf2 <> 0. (GF p)
by A28, VECTSP_1:12;
then A31:
gf2 |^ 2
<> 0. (GF p)
by EC_PF_1:22;
(P `3_3) |^ 2
<> 0
by A4, A12, Th38, EC_PF_1:25;
then A32:
(P `3_3) |^ 2
<> 0. (GF p)
by EC_PF_1:11;
A33:
Q `3_3 <> 0. (GF p)
by A14, EC_PF_1:11;
(gf2 |^ 2) * ((P `3_3) |^ 2) <> 0. (GF p)
by A31, A32, VECTSP_1:12;
then A34:
((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3) <> 0. (GF p)
by A33, VECTSP_1:12;
(EC_WEqProjCo ((z `1),(z `2),p)) . R = 0. (GF p)
then
R is_on_curve EC_WEqProjCo (
(z `1),
(z `2),
p)
;
then reconsider R =
R as
Element of
EC_SetProjCo (
(z `1),
(z `2),
p)
by Th34;
take
R
;
S1[P,Q,R]thus
S1[
P,
Q,
R]
by A10;
verum end; end; suppose A35:
( not
P _EQ_ O & not
Q _EQ_ O &
P _EQ_ Q )
;
ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]A36:
OO `3_3 = 0
by A7;
rep_pt PP <> rep_pt OO
by A3, A7, A35, Th39;
then
rep_pt PP <> [0,1,0]
by A36, Def7;
then A37:
(rep_pt PP) `3_3 <> 0
by Th37;
then A38:
P `3_3 <> 0
by A4, Th38;
reconsider g2 = 2
mod p as
Element of
(GF p) by EC_PF_1:14;
reconsider g3 = 3
mod p as
Element of
(GF p) by EC_PF_1:14;
reconsider g4 = 4
mod p as
Element of
(GF p) by EC_PF_1:14;
reconsider g8 = 8
mod p as
Element of
(GF p) by EC_PF_1:14;
set gf1 =
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2));
set gf2 =
(P `2_3) * (P `3_3);
set gf3 =
((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3));
set gf4 =
((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3))));
reconsider gf1 =
((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)),
gf2 =
(P `2_3) * (P `3_3),
gf3 =
((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)),
gf4 =
((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)))) as
Element of
(GF p) ;
set R =
[((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))];
reconsider R =
[((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] as
Element of
[: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
per cases
( P `2_3 = 0 or P `2_3 <> 0 )
;
suppose A39:
P `2_3 = 0
;
ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]A40:
gf2 = 0
by A39, EC_PF_1:20;
then A41:
gf3 = 0
by EC_PF_1:20;
A42:
gf2 = 0. (GF p)
by A40, EC_PF_1:11;
A43:
gf3 = 0. (GF p)
by A41, EC_PF_1:11;
A44:
gf1 <> 0
by A4, A37, A39, Th38, Th53;
then A45:
gf1 <> 0. (GF p)
by EC_PF_1:11;
gf4 =
(gf1 |^ 2) - (0. (GF p))
by A43
.=
gf1 |^ 2
by VECTSP_1:18
;
then
gf4 <> 0
by A44, EC_PF_1:25;
then A46:
gf4 <> 0. (GF p)
by EC_PF_1:11;
R `2_3 =
(gf1 * ((g4 * (0. (GF p))) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 * gf2))
by A43, EC_PF_1:22
.=
(gf1 * (- gf4)) - ((g8 * ((P `2_3) |^ 2)) * ((0. (GF p)) * (0. (GF p))))
by VECTSP_1:18, A42
.=
gf1 * (- gf4)
by VECTSP_1:18
.=
- (gf1 * gf4)
by VECTSP_1:8
;
then
- (R `2_3) = gf1 * gf4
by RLVECT_1:17;
then
- (R `2_3) <> 0. (GF p)
by A45, A46, VECTSP_1:12;
then A47:
R `2_3 <> 0. (GF p)
by VECTSP_2:3;
then
R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))]
;
then
not
R in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]}
by TARSKI:def 1;
then
R in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[(0. (GF p)),(0. (GF p)),(0. (GF p))]}
by XBOOLE_0:def 5;
then reconsider R =
R as
Element of
ProjCo (GF p) by EC_PF_1:def 6;
R in EC_SetProjCo (
(z `1),
(z `2),
p)
proof
A48:
R `1_3 = 0. (GF p)
by A42;
0 = 0. (GF p)
by EC_PF_1:11;
then A49:
gf2 |^ 3
= 0. (GF p)
by A40, Th5;
A50:
R `3_3 = 0. (GF p)
by A49;
set d =
R `2_3 ;
reconsider d =
R `2_3 as
Element of
(GF p) ;
A51:
(
OO `1_3 = 0 &
OO `2_3 = 1 &
OO `3_3 = 0 )
by A7;
A52:
d * (OO `1_3) =
0
by A51, EC_PF_1:20
.=
R `1_3
by A48, EC_PF_1:11
;
A53:
d * (OO `3_3) =
0
by A51, EC_PF_1:20
.=
R `3_3
by A50, EC_PF_1:11
;
d * (OO `2_3) =
d * (1. (GF p))
by A51, EC_PF_1:12
.=
R `2_3
;
hence
R in EC_SetProjCo (
(z `1),
(z `2),
p)
by A1, A7, A47, A52, A53, EC_PF_1:45;
verum
end; then reconsider R =
R as
Element of
EC_SetProjCo (
(z `1),
(z `2),
p) ;
take
R
;
S1[P,Q,R]thus
S1[
P,
Q,
R]
by A35;
verum end; suppose A54:
P `2_3 <> 0
;
ex R being Element of EC_SetProjCo ((z `1),(z `2),p) st S1[P,Q,R]A55:
gf2 <> 0
by A38, A54, EC_PF_1:20;
then
gf2 |^ 3
<> 0
by EC_PF_1:25;
then A56:
gf2 |^ 3
<> 0. (GF p)
by EC_PF_1:11;
A57:
g4 =
(2 * 2) mod p
.=
g2 * g2
by EC_PF_1:18
;
A58:
p > 2
by A1, NAT_1:13;
g8 =
(4 * 2) mod p
.=
g4 * g2
by EC_PF_1:18
.=
(g2 |^ 2) * g2
by A57, EC_PF_1:22
.=
g2 |^ (2 + 1)
by EC_PF_1:24
.=
g2 |^ 3
;
then A59:
g8 <> 0. (GF p)
by Th28, A58;
R `3_3 <> 0. (GF p)
by A56, A59, VECTSP_1:12;
then
R <> [(0. (GF p)),(0. (GF p)),(0. (GF p))]
;
then
not
R in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]}
by TARSKI:def 1;
then
R in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[(0. (GF p)),(0. (GF p)),(0. (GF p))]}
by XBOOLE_0:def 5;
then reconsider R =
R as
Element of
ProjCo (GF p) by EC_PF_1:def 6;
g4 = g2 |^ 2
by A57, EC_PF_1:22;
then A60:
g4 <> 0. (GF p)
by Th28, A58;
gf2 |^ 2
<> 0
by A55, EC_PF_1:25;
then A61:
gf2 |^ 2
<> 0. (GF p)
by EC_PF_1:11;
(P `3_3) |^ 2
<> 0
by A4, A37, Th38, EC_PF_1:25;
then A62:
(P `3_3) |^ 2
<> 0. (GF p)
by EC_PF_1:11;
g4 * (gf2 |^ 2) <> 0. (GF p)
by A60, A61, VECTSP_1:12;
then A63:
(g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2) <> 0. (GF p)
by A62, VECTSP_1:12;
(EC_WEqProjCo ((z `1),(z `2),p)) . R = 0. (GF p)
then
R is_on_curve EC_WEqProjCo (
(z `1),
(z `2),
p)
;
then reconsider R =
R as
Element of
EC_SetProjCo (
(z `1),
(z `2),
p)
by Th34;
take
R
;
S1[P,Q,R]thus
S1[
P,
Q,
R]
by A35;
verum end; end;
end;
consider f being Function of [:(EC_SetProjCo ((z `1),(z `2),p)),(EC_SetProjCo ((z `1),(z `2),p)):],(EC_SetProjCo ((z `1),(z `2),p)) such that
A64:
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds S1[P,Q,f . (P,Q)]
from BINOP_1:sch 3(A2);
take
f
; for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies f . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies f . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
f . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
f . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) )
thus
for P, Q, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( ( P _EQ_ O implies f . (P,Q) = Q ) & ( Q _EQ_ O & not P _EQ_ O implies f . (P,Q) = P ) & ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q implies for g2, gf1, gf2, gf3 being Element of (GF p) st g2 = 2 mod p & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) holds
f . (P,Q) = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] ) & ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q implies for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p) st g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)) & gf2 = (P `2_3) * (P `3_3) & gf3 = ((P `1_3) * (P `2_3)) * gf2 & gf4 = (gf1 |^ 2) - (g8 * gf3) holds
f . (P,Q) = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] ) )
by A64; verum