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 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))
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 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))
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 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))
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 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))
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 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3))) )
assume that
g2 = 2 mod p
and
( 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
A1:
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 * (P `3_3)) * (R `2_3) = - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))
((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)) =
((gf2 * gf3) * (P `3_3)) - ((P `1_3) * (R `3_3))
by A1
.=
((gf2 * gf3) * (P `3_3)) - ((P `1_3) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3)))
by A1
.=
((gf2 * (P `3_3)) * gf3) - ((P `1_3) * (((gf2 |^ (2 + 1)) * (P `3_3)) * (Q `3_3)))
by GROUP_1:def 3
.=
((gf2 * (P `3_3)) * gf3) - ((P `1_3) * ((((gf2 |^ 2) * gf2) * (P `3_3)) * (Q `3_3)))
by EC_PF_1:24
.=
((gf2 * (P `3_3)) * gf3) - (((((gf2 |^ 2) * gf2) * (P `3_3)) * (P `1_3)) * (Q `3_3))
by GROUP_1:def 3
.=
((gf2 * (P `3_3)) * gf3) - ((((gf2 * (P `3_3)) * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3))
by GROUP_1:def 3
.=
((gf2 * (P `3_3)) * gf3) - ((gf2 * (P `3_3)) * (((gf2 |^ 2) * (P `1_3)) * (Q `3_3)))
by Th11
.=
(gf2 * (P `3_3)) * (gf3 - (((gf2 |^ 2) * (P `1_3)) * (Q `3_3)))
by VECTSP_1:11
.=
(gf2 * (P `3_3)) * (- ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3))
by VECTSP_1:17
.=
- ((gf2 * (P `3_3)) * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3))
by VECTSP_1:8
.=
(- (gf2 * (P `3_3))) * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)
by VECTSP_1:9
;
then A2:
gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3))) = (- (gf2 * (P `3_3))) * (gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3))
by GROUP_1:def 3;
A3: (gf2 * (P `2_3)) * (R `3_3) =
(gf2 * (P `2_3)) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3))
by A1
.=
gf2 * ((P `2_3) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3)))
by GROUP_1:def 3
.=
gf2 * ((((P `3_3) * (gf2 |^ 3)) * (P `2_3)) * (Q `3_3))
by GROUP_1:def 3
.=
(((gf2 * (P `3_3)) * (gf2 |^ 3)) * (P `2_3)) * (Q `3_3)
by Th11
.=
(gf2 * (P `3_3)) * (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))
by Th11
.=
(- (gf2 * (P `3_3))) * (- (((gf2 |^ 3) * (P `2_3)) * (Q `3_3)))
by VECTSP_1:10
;
thus - ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3))) =
- ((- (gf2 * (P `3_3))) * ((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))))
by A2, A3, VECTSP_1:def 7
.=
- (- ((gf2 * (P `3_3)) * (R `2_3)))
by A1, VECTSP_1:9
.=
(gf2 * (P `3_3)) * (R `2_3)
by RLVECT_1:17
; verum