let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P 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 & 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) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))
let z be Element of EC_WParam p; for g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of (GF p)
for P 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 & 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) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))
let g2, g3, g4, g8, gf1, gf2, gf3, gf4 be Element of (GF p); for P 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 & 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) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))
let P 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 & 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) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] holds
((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (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 & 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) & R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))] implies ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3)))) )
assume that
A1:
( g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p )
and
A2:
( 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) )
and
A3:
R = [((g2 * gf4) * gf2),((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))),(g8 * (gf2 |^ 3))]
; ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) = (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))
set a = z `1 ;
set b = z `2 ;
A4: g8 =
(2 * 4) mod p
by A1
.=
g2 * g4
by A1, EC_PF_1:18
;
A5: (P `3_3) * gf3 =
((P `3_3) * ((P `1_3) * (P `2_3))) * gf2
by A2, GROUP_1:def 3
.=
((P `1_3) * ((P `2_3) * (P `3_3))) * gf2
by GROUP_1:def 3
.=
(P `1_3) * (gf2 * gf2)
by A2, GROUP_1:def 3
.=
(P `1_3) * (gf2 |^ 2)
by EC_PF_1:22
;
A6: ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3)) =
(((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (z `1)) * (R `3_3)
by GROUP_1:def 3
.=
(R `3_3) * ((g2 * (gf2 |^ 2)) * ((z `1) * ((P `3_3) |^ 2)))
by GROUP_1:def 3
;
A7: ((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) =
(R `3_3) * ((gf1 * (P `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(R `3_3) * (gf1 * ((P `3_3) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))))
by GROUP_1:def 3
.=
(R `3_3) * (gf1 * (((P `3_3) * ((g2 * gf2) * (P `2_3))) - ((P `3_3) * (gf1 * (P `1_3)))))
by VECTSP_1:11
.=
(R `3_3) * (gf1 * (((P `3_3) * ((P `2_3) * (g2 * gf2))) - (((P `3_3) * gf1) * (P `1_3))))
by GROUP_1:def 3
.=
(R `3_3) * (gf1 * ((((P `3_3) * (P `2_3)) * (g2 * gf2)) - ((P `1_3) * ((P `3_3) * gf1))))
by GROUP_1:def 3
.=
(R `3_3) * (gf1 * ((((P `2_3) * (P `3_3)) * (g2 * gf2)) - (((P `1_3) * (P `3_3)) * gf1)))
by GROUP_1:def 3
.=
(R `3_3) * (gf1 * ((g2 * (gf2 * gf2)) - (gf1 * ((P `1_3) * (P `3_3)))))
by A2, GROUP_1:def 3
.=
(R `3_3) * (gf1 * ((g2 * (gf2 |^ 2)) - (gf1 * ((P `1_3) * (P `3_3)))))
by EC_PF_1:22
.=
(R `3_3) * ((gf1 * (g2 * (gf2 |^ 2))) - (gf1 * (gf1 * ((P `1_3) * (P `3_3)))))
by VECTSP_1:11
.=
(R `3_3) * ((gf1 * (g2 * (gf2 |^ 2))) - ((gf1 * gf1) * ((P `1_3) * (P `3_3))))
by GROUP_1:def 3
.=
(R `3_3) * (((g2 * (gf2 |^ 2)) * gf1) - ((gf1 |^ 2) * ((P `1_3) * (P `3_3))))
by EC_PF_1:22
;
A8: (gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))) =
((gf2 |^ 2) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3))) + ((gf2 |^ 2) * ((g2 * ((P `1_3) |^ 2)) * (R `3_3)))
by VECTSP_1:def 7
.=
((gf2 |^ 2) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3))) + (((gf2 |^ 2) * (g2 * ((P `1_3) |^ 2))) * (R `3_3))
by GROUP_1:def 3
.=
((gf2 |^ 2) * ((R `1_3) * ((g4 * (P `1_3)) * (P `3_3)))) + ((((gf2 |^ 2) * g2) * ((P `1_3) |^ 2)) * (R `3_3))
by GROUP_1:def 3
.=
(((gf2 |^ 2) * (R `1_3)) * ((g4 * (P `1_3)) * (P `3_3))) + ((R `3_3) * (((gf2 |^ 2) * g2) * ((P `1_3) |^ 2)))
by GROUP_1:def 3
.=
(((gf2 |^ 2) * ((g2 * gf4) * gf2)) * ((g4 * (P `1_3)) * (P `3_3))) + ((R `3_3) * (((gf2 |^ 2) * g2) * ((P `1_3) |^ 2)))
by A3
.=
(((gf2 |^ 2) * (gf2 * (g2 * gf4))) * ((g4 * (P `1_3)) * (P `3_3))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
((((gf2 |^ 2) * gf2) * (g2 * gf4)) * ((g4 * (P `1_3)) * (P `3_3))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
(((gf2 |^ (2 + 1)) * (g2 * gf4)) * ((g4 * (P `1_3)) * (P `3_3))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by EC_PF_1:24
.=
((gf2 |^ 3) * ((g2 * gf4) * ((g4 * (P `1_3)) * (P `3_3)))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
((gf2 |^ 3) * ((g2 * gf4) * (g4 * ((P `1_3) * (P `3_3))))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
((gf2 |^ 3) * (((g2 * gf4) * g4) * ((P `1_3) * (P `3_3)))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
((gf2 |^ 3) * (((g2 * g4) * gf4) * ((P `1_3) * (P `3_3)))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
((gf2 |^ 3) * (g8 * (gf4 * ((P `1_3) * (P `3_3))))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by A4, GROUP_1:def 3
.=
(((gf2 |^ 3) * g8) * (gf4 * ((P `1_3) * (P `3_3)))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
((R `3_3) * (gf4 * ((P `1_3) * (P `3_3)))) + ((R `3_3) * (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by A3
.=
(R `3_3) * ((((P `1_3) * (P `3_3)) * gf4) + (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by VECTSP_1:def 7
.=
(R `3_3) * (((P `1_3) * ((P `3_3) * gf4)) + (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
;
A9:
4 = 3 + 1
;
(P `3_3) * gf4 =
((P `3_3) * (gf1 |^ 2)) - ((P `3_3) * (g8 * gf3))
by A2, VECTSP_1:11
.=
((P `3_3) * (gf1 |^ 2)) - (g8 * ((P `3_3) * gf3))
by GROUP_1:def 3
.=
((P `3_3) * (gf1 |^ 2)) - (g4 * (g2 * ((P `1_3) * (gf2 |^ 2))))
by A4, A5, GROUP_1:def 3
.=
((P `3_3) * (gf1 |^ 2)) - ((g3 * (g2 * ((P `1_3) * (gf2 |^ 2)))) + (g2 * ((P `1_3) * (gf2 |^ 2))))
by A1, A9, Th19
.=
((P `3_3) * (gf1 |^ 2)) - ((g3 * ((g2 * (gf2 |^ 2)) * (P `1_3))) + (g2 * ((gf2 |^ 2) * (P `1_3))))
by GROUP_1:def 3
.=
((P `3_3) * (gf1 |^ 2)) - (((g2 * (gf2 |^ 2)) * (g3 * (P `1_3))) + (g2 * ((gf2 |^ 2) * (P `1_3))))
by GROUP_1:def 3
;
then (P `1_3) * ((P `3_3) * gf4) =
((P `1_3) * ((P `3_3) * (gf1 |^ 2))) - ((P `1_3) * (((g2 * (gf2 |^ 2)) * (g3 * (P `1_3))) + (g2 * ((gf2 |^ 2) * (P `1_3)))))
by VECTSP_1:11
.=
(((P `1_3) * (P `3_3)) * (gf1 |^ 2)) - ((P `1_3) * (((g2 * (gf2 |^ 2)) * (g3 * (P `1_3))) + (g2 * ((gf2 |^ 2) * (P `1_3)))))
by GROUP_1:def 3
.=
(((P `1_3) * (P `3_3)) * (gf1 |^ 2)) - (((P `1_3) * ((g2 * (gf2 |^ 2)) * (g3 * (P `1_3)))) + ((P `1_3) * (g2 * ((gf2 |^ 2) * (P `1_3)))))
by VECTSP_1:def 7
.=
(((P `1_3) * (P `3_3)) * (gf1 |^ 2)) - (((g2 * (gf2 |^ 2)) * ((g3 * (P `1_3)) * (P `1_3))) + ((g2 * ((gf2 |^ 2) * (P `1_3))) * (P `1_3)))
by GROUP_1:def 3
.=
(((P `1_3) * (P `3_3)) * (gf1 |^ 2)) - (((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) * (P `1_3)))) + ((g2 * ((gf2 |^ 2) * (P `1_3))) * (P `1_3)))
by GROUP_1:def 3
.=
(((P `1_3) * (P `3_3)) * (gf1 |^ 2)) - (((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))) + ((g2 * ((gf2 |^ 2) * (P `1_3))) * (P `1_3)))
by EC_PF_1:22
.=
(((P `1_3) * (P `3_3)) * (gf1 |^ 2)) - (((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))) + (g2 * (((gf2 |^ 2) * (P `1_3)) * (P `1_3))))
by GROUP_1:def 3
.=
(((P `1_3) * (P `3_3)) * (gf1 |^ 2)) - (((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))) + (g2 * ((gf2 |^ 2) * ((P `1_3) * (P `1_3)))))
by GROUP_1:def 3
.=
((gf1 |^ 2) * ((P `1_3) * (P `3_3))) - (((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))) + (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by EC_PF_1:22
.=
(((gf1 |^ 2) * ((P `1_3) * (P `3_3))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))) - (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2)))
by VECTSP_1:17
;
then ((P `1_3) * ((P `3_3) * gf4)) + (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))) =
(((gf1 |^ 2) * ((P `1_3) * (P `3_3))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))) + ((- (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2)))) + (g2 * ((gf2 |^ 2) * ((P `1_3) |^ 2))))
by ALGSTR_1:7
.=
(((gf1 |^ 2) * ((P `1_3) * (P `3_3))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))) + (0. (GF p))
by VECTSP_1:19
.=
((gf1 |^ 2) * ((P `1_3) * (P `3_3))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))
by ALGSTR_1:7
;
hence (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))) + ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3)))) =
(R `3_3) * ((((g2 * (gf2 |^ 2)) * gf1) - ((gf1 |^ 2) * ((P `1_3) * (P `3_3)))) + (((gf1 |^ 2) * ((P `1_3) * (P `3_3))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))))
by A7, A8, VECTSP_1:def 7
.=
(R `3_3) * (((g2 * (gf2 |^ 2)) * gf1) + ((- ((gf1 |^ 2) * ((P `1_3) * (P `3_3)))) + (((gf1 |^ 2) * ((P `1_3) * (P `3_3))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))))))
by ALGSTR_1:7
.=
(R `3_3) * (((g2 * (gf2 |^ 2)) * gf1) + (((- ((gf1 |^ 2) * ((P `1_3) * (P `3_3)))) + ((gf1 |^ 2) * ((P `1_3) * (P `3_3)))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))))
by ALGSTR_1:7
.=
(R `3_3) * (((g2 * (gf2 |^ 2)) * gf1) + ((0. (GF p)) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))))
by VECTSP_1:19
.=
(R `3_3) * (((g2 * (gf2 |^ 2)) * gf1) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))))
by VECTSP_1:18
.=
(R `3_3) * ((((g2 * (gf2 |^ 2)) * ((z `1) * ((P `3_3) |^ 2))) + ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))))
by A2, VECTSP_1:def 7
.=
(R `3_3) * (((g2 * (gf2 |^ 2)) * ((z `1) * ((P `3_3) |^ 2))) + (((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2))) - ((g2 * (gf2 |^ 2)) * (g3 * ((P `1_3) |^ 2)))))
by ALGSTR_1:7
.=
(R `3_3) * (((g2 * (gf2 |^ 2)) * ((z `1) * ((P `3_3) |^ 2))) + (0. (GF p)))
by VECTSP_1:19
.=
((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3))
by A6, ALGSTR_1:7
;
verum