let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for P, Q, O, PQ, QP being Element of EC_SetProjCo ((z `1),(z `2),p)
for d being Element of (GF p) st O = [0,1,0] & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = (d |^ 6) * (PQ `1_3) & QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) )
let z be Element of EC_WParam p; for P, Q, O, PQ, QP being Element of EC_SetProjCo ((z `1),(z `2),p)
for d being Element of (GF p) st O = [0,1,0] & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = (d |^ 6) * (PQ `1_3) & QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) )
set a = z `1 ;
set b = z `2 ;
let P, Q, O, PQ, QP be Element of EC_SetProjCo ((z `1),(z `2),p); for d being Element of (GF p) st O = [0,1,0] & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = (d |^ 6) * (PQ `1_3) & QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) )
let d be Element of (GF p); ( O = [0,1,0] & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) implies ( QP `1_3 = (d |^ 6) * (PQ `1_3) & QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) ) )
assume that
A0:
O = [0,1,0]
and
A1:
( d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) )
and
A2:
( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q )
and
A3:
PQ = (addell_ProjCo (z,p)) . (P,Q)
and
A4:
QP = (addell_ProjCo (z,p)) . (Q,P)
; ( QP `1_3 = (d |^ 6) * (PQ `1_3) & QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) )
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 gf1P = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2));
set gf2P = (P `2_3) * (P `3_3);
set gf3P = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3));
set gf4P = ((((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 gf1P = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)), gf2P = (P `2_3) * (P `3_3), gf3P = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)), gf4P = ((((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) ;
A9:
PQ = [((g2 * gf4P) * gf2P),((gf1P * ((g4 * gf3P) - gf4P)) - ((g8 * ((P `2_3) |^ 2)) * (gf2P |^ 2))),(g8 * (gf2P |^ 3))]
by A0, A2, A3, EC_PF_2:def 9;
set gf1Q = ((z `1) * ((Q `3_3) |^ 2)) + (g3 * ((Q `1_3) |^ 2));
set gf2Q = (Q `2_3) * (Q `3_3);
set gf3Q = ((Q `1_3) * (Q `2_3)) * ((Q `2_3) * (Q `3_3));
set gf4Q = ((((z `1) * ((Q `3_3) |^ 2)) + (g3 * ((Q `1_3) |^ 2))) |^ 2) - (g8 * (((Q `1_3) * (Q `2_3)) * ((Q `2_3) * (Q `3_3))));
reconsider gf1Q = ((z `1) * ((Q `3_3) |^ 2)) + (g3 * ((Q `1_3) |^ 2)), gf2Q = (Q `2_3) * (Q `3_3), gf3Q = ((Q `1_3) * (Q `2_3)) * ((Q `2_3) * (Q `3_3)), gf4Q = ((((z `1) * ((Q `3_3) |^ 2)) + (g3 * ((Q `1_3) |^ 2))) |^ 2) - (g8 * (((Q `1_3) * (Q `2_3)) * ((Q `2_3) * (Q `3_3)))) as Element of (GF p) ;
A10:
QP = [((g2 * gf4Q) * gf2Q),((gf1Q * ((g4 * gf3Q) - gf4Q)) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))),(g8 * (gf2Q |^ 3))]
by A0, A2, A4, EC_PF_2:def 9;
A11: gf1Q =
((z `1) * ((d |^ 2) * ((P `3_3) |^ 2))) + (g3 * ((d * (P `1_3)) |^ 2))
by A1, BINOM:9
.=
((z `1) * ((d |^ 2) * ((P `3_3) |^ 2))) + (g3 * ((d |^ 2) * ((P `1_3) |^ 2)))
by BINOM:9
.=
(((z `1) * (d |^ 2)) * ((P `3_3) |^ 2)) + (g3 * ((d |^ 2) * ((P `1_3) |^ 2)))
by GROUP_1:def 3
.=
(((z `1) * (d |^ 2)) * ((P `3_3) |^ 2)) + ((g3 * (d |^ 2)) * ((P `1_3) |^ 2))
by GROUP_1:def 3
.=
((d |^ 2) * ((z `1) * ((P `3_3) |^ 2))) + (((d |^ 2) * g3) * ((P `1_3) |^ 2))
by GROUP_1:def 3
.=
((d |^ 2) * ((z `1) * ((P `3_3) |^ 2))) + ((d |^ 2) * (g3 * ((P `1_3) |^ 2)))
by GROUP_1:def 3
.=
(d |^ 2) * gf1P
by VECTSP_1:def 3
;
A12: gf2Q =
d * (((P `2_3) * d) * (P `3_3))
by A1, GROUP_1:def 3
.=
d * (d * ((P `2_3) * (P `3_3)))
by GROUP_1:def 3
.=
(d * d) * ((P `2_3) * (P `3_3))
by GROUP_1:def 3
.=
(d |^ 2) * gf2P
by EC_PF_1:22
;
A13: gf3Q =
(d * (((P `1_3) * d) * (P `2_3))) * gf2Q
by A1, GROUP_1:def 3
.=
(d * (d * ((P `1_3) * (P `2_3)))) * gf2Q
by GROUP_1:def 3
.=
((d * d) * ((P `1_3) * (P `2_3))) * gf2Q
by GROUP_1:def 3
.=
((d |^ 2) * ((P `1_3) * (P `2_3))) * gf2Q
by EC_PF_1:22
.=
(d |^ 2) * ((((P `1_3) * (P `2_3)) * (d |^ 2)) * gf2P)
by A12, GROUP_1:def 3
.=
(d |^ 2) * ((d |^ 2) * gf3P)
by GROUP_1:def 3
.=
((d |^ 2) * (d |^ 2)) * gf3P
by GROUP_1:def 3
.=
((d |^ 2) |^ 2) * gf3P
by EC_PF_1:22
.=
(d |^ (2 * 2)) * gf3P
by BINOM:11
.=
(d |^ 4) * gf3P
;
A14: gf4Q =
(((d |^ 2) |^ 2) * (gf1P |^ 2)) - (g8 * ((d |^ 4) * gf3P))
by A11, A13, BINOM:9
.=
((d |^ (2 * 2)) * (gf1P |^ 2)) - (g8 * ((d |^ 4) * gf3P))
by BINOM:11
.=
((d |^ 4) * (gf1P |^ 2)) - ((d |^ 4) * (g8 * gf3P))
by GROUP_1:def 3
.=
(d |^ 4) * gf4P
by VECTSP_1:11
;
thus QP `1_3 =
(g2 * gf4Q) * gf2Q
by A10, EC_PF_2:def 3
.=
g2 * (((d |^ 4) * gf4P) * ((d |^ 2) * gf2P))
by A12, A14, GROUP_1:def 3
.=
g2 * ((d |^ 4) * (gf4P * ((d |^ 2) * gf2P)))
by GROUP_1:def 3
.=
g2 * ((d |^ 4) * ((d |^ 2) * (gf4P * gf2P)))
by GROUP_1:def 3
.=
g2 * (((d |^ 4) * (d |^ 2)) * (gf4P * gf2P))
by GROUP_1:def 3
.=
g2 * ((d |^ (4 + 2)) * (gf4P * gf2P))
by BINOM:10
.=
(d |^ 6) * (g2 * (gf4P * gf2P))
by GROUP_1:def 3
.=
(d |^ 6) * ((g2 * gf4P) * gf2P)
by GROUP_1:def 3
.=
(d |^ 6) * (PQ `1_3)
by A9, EC_PF_2:def 3
; ( QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) )
thus QP `2_3 =
(gf1Q * ((g4 * gf3Q) - gf4Q)) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))
by A10, EC_PF_2:def 4
.=
(gf1Q * (((d |^ 4) * (g4 * gf3P)) - ((d |^ 4) * gf4P))) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))
by A13, A14, GROUP_1:def 3
.=
(gf1Q * ((d |^ 4) * ((g4 * gf3P) - gf4P))) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))
by VECTSP_1:11
.=
((gf1Q * (d |^ 4)) * ((g4 * gf3P) - gf4P)) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))
by GROUP_1:def 3
.=
((((d |^ 2) * (d |^ 4)) * gf1P) * ((g4 * gf3P) - gf4P)) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))
by A11, GROUP_1:def 3
.=
(((d |^ (2 + 4)) * gf1P) * ((g4 * gf3P) - gf4P)) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))
by BINOM:10
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((Q `2_3) |^ 2)) * (gf2Q |^ 2))
by GROUP_1:def 3
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((d |^ 2) * ((P `2_3) |^ 2))) * (((d |^ 2) * gf2P) |^ 2))
by A1, A12, BINOM:9
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((d |^ 2) * ((P `2_3) |^ 2))) * (((d |^ 2) |^ 2) * (gf2P |^ 2)))
by BINOM:9
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((d |^ 2) * ((P `2_3) |^ 2))) * ((d |^ (2 * 2)) * (gf2P |^ 2)))
by BINOM:11
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - (((g8 * (d |^ 2)) * ((P `2_3) |^ 2)) * ((d |^ 4) * (gf2P |^ 2)))
by GROUP_1:def 3
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - (((((d |^ 2) * g8) * ((P `2_3) |^ 2)) * (gf2P |^ 2)) * (d |^ 4))
by GROUP_1:def 3
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ 4) * (((d |^ 2) * g8) * (((P `2_3) |^ 2) * (gf2P |^ 2))))
by GROUP_1:def 3
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ 4) * ((d |^ 2) * (g8 * (((P `2_3) |^ 2) * (gf2P |^ 2)))))
by GROUP_1:def 3
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ 4) * ((d |^ 2) * ((g8 * ((P `2_3) |^ 2)) * (gf2P |^ 2))))
by GROUP_1:def 3
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - (((d |^ 4) * (d |^ 2)) * ((g8 * ((P `2_3) |^ 2)) * (gf2P |^ 2)))
by GROUP_1:def 3
.=
((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ (4 + 2)) * ((g8 * ((P `2_3) |^ 2)) * (gf2P |^ 2)))
by BINOM:10
.=
(d |^ 6) * ((gf1P * ((g4 * gf3P) - gf4P)) - ((g8 * ((P `2_3) |^ 2)) * (gf2P |^ 2)))
by VECTSP_1:11
.=
(d |^ 6) * (PQ `2_3)
by A9, EC_PF_2:def 4
; QP `3_3 = (d |^ 6) * (PQ `3_3)
thus QP `3_3 =
g8 * (gf2Q |^ 3)
by A10, EC_PF_2:def 5
.=
g8 * (((d |^ 2) |^ 3) * (gf2P |^ 3))
by A12, BINOM:9
.=
g8 * ((d |^ (2 * 3)) * (gf2P |^ 3))
by BINOM:11
.=
(d |^ 6) * (g8 * (gf2P |^ 3))
by GROUP_1:def 3
.=
(d |^ 6) * (PQ `3_3)
by A9, EC_PF_2:def 5
; verum