let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier 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)) & 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))] holds
(- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
let z be Element of EC_WParam p; for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier 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)) & 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))] holds
(- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
let g2, gf1, gf2, gf3 be Element of (GF p); for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p)
for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier 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)) & 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))] holds
(- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); for R being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier 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)) & 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))] holds
(- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
let R be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; ( 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)) & 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))] implies (- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p) )
assume that
A1:
g2 = 2 mod p
and
A2:
( 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)) )
and
A3:
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))]
; (- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
A4: (((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2) =
(R `3_3) * (((P `3_3) * (Q `3_3)) * (gf1 |^ 2))
by GROUP_1:def 3
.=
(R `3_3) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))
by GROUP_1:def 3
;
A5: (((P `3_3) * (Q `1_3)) * (R `3_3)) + (((P `1_3) * (Q `3_3)) * (R `3_3)) =
(((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (R `3_3)
by VECTSP_1:def 7
.=
((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) + (0. (GF p))) * (R `3_3)
by ALGSTR_1:7
.=
((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) + (((Q `3_3) * (P `1_3)) - ((Q `3_3) * (P `1_3)))) * (R `3_3)
by VECTSP_1:19
.=
(((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) + ((Q `3_3) * (P `1_3))) - ((Q `3_3) * (P `1_3))) * (R `3_3)
by ALGSTR_1:7
.=
(((((Q `3_3) * (P `1_3)) + ((P `1_3) * (Q `3_3))) + ((P `3_3) * (Q `1_3))) - ((Q `3_3) * (P `1_3))) * (R `3_3)
by ALGSTR_1:7
.=
(((g2 * ((Q `3_3) * (P `1_3))) + ((Q `1_3) * (P `3_3))) - ((P `1_3) * (Q `3_3))) * (R `3_3)
by A1, Th20
.=
(R `3_3) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2)
by A2, ALGSTR_1:7
;
A6: (gf2 |^ 2) * (((P `3_3) * (Q `3_3)) * (R `1_3)) =
(gf2 |^ 2) * (((P `3_3) * (Q `3_3)) * (gf2 * gf3))
by A3
.=
(((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (gf2 * gf3)
by Th11
.=
((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * gf2) * gf3
by GROUP_1:def 3
.=
(((gf2 * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * gf3
by Th11
.=
(((gf2 |^ (2 + 1)) * (P `3_3)) * (Q `3_3)) * gf3
by EC_PF_1:24
.=
(R `3_3) * gf3
by A3
;
A7: (gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))) =
(gf2 |^ 2) * ((((P `3_3) * (Q `3_3)) * (R `1_3)) + ((R `3_3) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2)))
by A5, ALGSTR_1:7
.=
((gf2 |^ 2) * (((P `3_3) * (Q `3_3)) * (R `1_3))) + ((gf2 |^ 2) * ((R `3_3) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2)))
by VECTSP_1:def 7
.=
((R `3_3) * gf3) + ((R `3_3) * ((gf2 |^ 2) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2)))
by A6, GROUP_1:def 3
.=
(R `3_3) * (gf3 + ((gf2 |^ 2) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2)))
by VECTSP_1:def 7
;
gf3 =
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) + (gf2 |^ (2 + 1)))
by A2, VECTSP_1:17
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (((((gf2 |^ 2) * g2) * (P `1_3)) * (Q `3_3)) + ((gf2 |^ 2) * gf2))
by EC_PF_1:24
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((((gf2 |^ 2) * g2) * ((P `1_3) * (Q `3_3))) + ((gf2 |^ 2) * gf2))
by GROUP_1:def 3
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (((gf2 |^ 2) * (g2 * ((P `1_3) * (Q `3_3)))) + ((gf2 |^ 2) * gf2))
by GROUP_1:def 3
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((gf2 |^ 2) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2))
by VECTSP_1:def 7
;
then (gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))) =
(R `3_3) * ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + ((- ((gf2 |^ 2) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2))) + ((gf2 |^ 2) * ((g2 * ((Q `3_3) * (P `1_3))) + gf2))))
by A7, ALGSTR_1:7
.=
(R `3_3) * ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + (0. (GF p)))
by VECTSP_1:19
.=
(R `3_3) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))
by ALGSTR_1:7
;
hence
(- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((P `3_3) * (Q `3_3)) * (R `3_3)) * (gf1 |^ 2)) = 0. (GF p)
by A4, RLVECT_1:5; verum