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
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_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
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_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
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_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
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_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 ((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_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))]
; ((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3)) = ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3))
set a = z `1 ;
set b = z `2 ;
A4: g4 =
(2 * 2) mod p
by A1
.=
g2 * g2
by A1, EC_PF_1:18
;
A5: g8 =
(2 * 4) mod p
by A1
.=
g2 * g4
by A1, EC_PF_1:18
;
A6: - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) =
- ((g4 * (gf2 |^ 2)) * (((P `1_3) |^ 2) * ((g2 * gf4) * gf2)))
by GROUP_1:def 3, A3
.=
- (g4 * ((gf2 |^ 2) * (((P `1_3) |^ 2) * ((g2 * gf4) * gf2))))
by GROUP_1:def 3
.=
- (g4 * (((gf2 |^ 2) * ((P `1_3) |^ 2)) * ((g2 * gf4) * gf2)))
by GROUP_1:def 3
.=
- (g4 * (((gf2 |^ 2) * ((P `1_3) |^ 2)) * (g2 * (gf4 * gf2))))
by GROUP_1:def 3
.=
- (g4 * ((((gf2 |^ 2) * ((P `1_3) |^ 2)) * (gf2 * gf4)) * g2))
by GROUP_1:def 3
.=
- ((g4 * g2) * (((gf2 |^ 2) * ((P `1_3) |^ 2)) * (gf2 * gf4)))
by GROUP_1:def 3
.=
- (g8 * (((P `1_3) |^ 2) * ((gf2 |^ 2) * (gf2 * gf4))))
by A5, GROUP_1:def 3
.=
- (g8 * (((P `1_3) |^ 2) * (((gf2 |^ 2) * gf2) * gf4)))
by GROUP_1:def 3
.=
- (g8 * (((P `1_3) |^ 2) * ((gf2 |^ (2 + 1)) * gf4)))
by EC_PF_1:24
.=
- (g8 * ((((P `1_3) |^ 2) * (gf2 |^ 3)) * gf4))
by GROUP_1:def 3
.=
- ((g8 * (((P `1_3) |^ 2) * (gf2 |^ 3))) * gf4)
by GROUP_1:def 3
.=
- (((g8 * (gf2 |^ 3)) * ((P `1_3) |^ 2)) * gf4)
by GROUP_1:def 3
.=
- ((((R `3_3) * ((P `1_3) |^ 2)) * (gf1 |^ 2)) - (((R `3_3) * ((P `1_3) |^ 2)) * (g8 * gf3)))
by A2, A3, VECTSP_1:11
.=
(((R `3_3) * ((P `1_3) |^ 2)) * (g8 * gf3)) - (((R `3_3) * ((P `1_3) |^ 2)) * (gf1 |^ 2))
by VECTSP_1:17
.=
((((R `3_3) * ((P `1_3) |^ 2)) * g8) * gf3) - (((R `3_3) * ((P `1_3) |^ 2)) * (gf1 |^ 2))
by GROUP_1:def 3
.=
((g8 * ((R `3_3) * ((P `1_3) |^ 2))) * gf3) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by GROUP_1:def 3
.=
(g8 * (((R `3_3) * ((P `1_3) |^ 2)) * gf3)) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by GROUP_1:def 3
.=
(g8 * ((R `3_3) * (((P `1_3) |^ 2) * (((P `1_3) * (P `2_3)) * gf2)))) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by A2, GROUP_1:def 3
.=
(g8 * ((R `3_3) * (((P `1_3) |^ 2) * ((P `1_3) * ((P `2_3) * gf2))))) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by GROUP_1:def 3
.=
(g8 * ((R `3_3) * ((((P `1_3) |^ 2) * (P `1_3)) * ((P `2_3) * gf2)))) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by GROUP_1:def 3
.=
(g8 * ((R `3_3) * (((P `1_3) |^ (2 + 1)) * ((P `2_3) * gf2)))) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by EC_PF_1:24
.=
(g8 * (((R `3_3) * ((P `2_3) * gf2)) * ((P `1_3) |^ 3))) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by GROUP_1:def 3
.=
(((g2 * g4) * ((R `3_3) * ((P `2_3) * gf2))) * ((P `1_3) |^ 3)) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by A5, GROUP_1:def 3
.=
((g2 * (g4 * ((R `3_3) * ((P `2_3) * gf2)))) * ((P `1_3) |^ 3)) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by GROUP_1:def 3
.=
((g4 * ((R `3_3) * ((P `2_3) * gf2))) * (g2 * ((P `1_3) |^ 3))) - ((R `3_3) * (((P `1_3) |^ 2) * (gf1 |^ 2)))
by GROUP_1:def 3
.=
(- ((R `3_3) * ((gf1 |^ 2) * ((P `1_3) |^ 2)))) + (((g4 * (R `3_3)) * ((P `2_3) * gf2)) * (g2 * ((P `1_3) |^ 3)))
by GROUP_1:def 3
;
A7: ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - ((R `3_3) * ((gf1 |^ 2) * ((P `1_3) |^ 2))) =
(R `3_3) * (((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) - ((gf1 |^ 2) * ((P `1_3) |^ 2)))
by VECTSP_1:11
.=
(R `3_3) * (((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) - ((gf1 * (P `1_3)) |^ 2))
by BINOM:9
.=
(R `3_3) * (((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) + (gf1 * (P `1_3))) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) - (gf1 * (P `1_3))))
by Th15
.=
(R `3_3) * ((((g2 * gf2) * (P `2_3)) - ((gf1 * (P `1_3)) - (gf1 * (P `1_3)))) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) - (gf1 * (P `1_3))))
by RLVECT_1:29
.=
(R `3_3) * ((((g2 * gf2) * (P `2_3)) - ((gf1 * (P `1_3)) - (gf1 * (P `1_3)))) * (((g2 * gf2) * (P `2_3)) - ((gf1 * (P `1_3)) + (gf1 * (P `1_3)))))
by RLVECT_1:27
.=
(R `3_3) * ((((g2 * gf2) * (P `2_3)) - ((gf1 * (P `1_3)) - (gf1 * (P `1_3)))) * (((g2 * gf2) * (P `2_3)) - (g2 * (gf1 * (P `1_3)))))
by A1, Th20
.=
(R `3_3) * ((((g2 * gf2) * (P `2_3)) - (0. (GF p))) * (((g2 * gf2) * (P `2_3)) - (g2 * (gf1 * (P `1_3)))))
by VECTSP_1:19
.=
(R `3_3) * (((g2 * gf2) * (P `2_3)) * (((g2 * gf2) * (P `2_3)) - (g2 * (gf1 * (P `1_3)))))
by RLVECT_1:13
.=
(R `3_3) * (((g2 * gf2) * (P `2_3)) * ((g2 * (gf2 * (P `2_3))) - (g2 * (gf1 * (P `1_3)))))
by GROUP_1:def 3
.=
(R `3_3) * (((g2 * gf2) * (P `2_3)) * (g2 * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))))
by VECTSP_1:11
.=
(R `3_3) * ((((g2 * gf2) * (P `2_3)) * g2) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(R `3_3) * ((g2 * (g2 * (gf2 * (P `2_3)))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(R `3_3) * ((g4 * (gf2 * (P `2_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
by A4, GROUP_1:def 3
.=
((R `3_3) * (g4 * (gf2 * (P `2_3)))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))
by GROUP_1:def 3
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))
by GROUP_1:def 3
;
A8:
3 = 2 + 1
;
(((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))) = 0. (GF p)
by Th35;
then A9: (((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3)) =
((P `2_3) |^ 2) * (P `3_3)
by VECTSP_1:19
.=
((P `2_3) * (P `2_3)) * (P `3_3)
by EC_PF_1:22
.=
gf2 * (P `2_3)
by A2, GROUP_1:def 3
;
thus ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) =
(((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - ((R `3_3) * ((gf1 |^ 2) * ((P `1_3) |^ 2)))) + (((g4 * (R `3_3)) * ((P `2_3) * gf2)) * (g2 * ((P `1_3) |^ 3)))
by A6, ALGSTR_1:7
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * (((gf2 * (P `2_3)) - (gf1 * (P `1_3))) + (g2 * ((P `1_3) |^ 3)))
by A7, VECTSP_1:def 7
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * (((gf2 * (P `2_3)) - ((((z `1) * ((P `3_3) |^ 2)) * (P `1_3)) + ((g3 * ((P `1_3) |^ 2)) * (P `1_3)))) + (g2 * ((P `1_3) |^ 3)))
by A2, VECTSP_1:def 7
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * ((gf2 * (P `2_3)) - (((((z `1) * ((P `3_3) |^ 2)) * (P `1_3)) + ((g3 * ((P `1_3) |^ 2)) * (P `1_3))) - (g2 * ((P `1_3) |^ 3))))
by RLVECT_1:29
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * ((gf2 * (P `2_3)) - (((((z `1) * ((P `3_3) |^ 2)) * (P `1_3)) + (g3 * (((P `1_3) |^ 2) * (P `1_3)))) - (g2 * ((P `1_3) |^ 3))))
by GROUP_1:def 3
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * ((gf2 * (P `2_3)) - (((((z `1) * ((P `3_3) |^ 2)) * (P `1_3)) + (g3 * ((P `1_3) |^ (2 + 1)))) - (g2 * ((P `1_3) |^ 3))))
by EC_PF_1:24
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * ((gf2 * (P `2_3)) - ((((z `1) * ((P `3_3) |^ 2)) * (P `1_3)) + ((g3 * ((P `1_3) |^ 3)) - (g2 * ((P `1_3) |^ 3)))))
by ALGSTR_1:7
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * ((gf2 * (P `2_3)) - ((((z `1) * ((P `3_3) |^ 2)) * (P `1_3)) + ((P `1_3) |^ 3)))
by A1, A8, Th22
.=
((g4 * (R `3_3)) * ((P `2_3) * gf2)) * (((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3))) - (((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))))
by A9, GROUP_1:def 3
.=
((g4 * (R `3_3)) * (gf2 * (P `2_3))) * (((z `2) * ((P `3_3) |^ 3)) + ((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) - (((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2)))))
by ALGSTR_1:7
.=
((g4 * (R `3_3)) * (gf2 * (P `2_3))) * (((z `2) * ((P `3_3) |^ 3)) + (0. (GF p)))
by RLVECT_1:5
.=
((g4 * (R `3_3)) * (gf2 * (P `2_3))) * ((z `2) * ((P `3_3) |^ 3))
by ALGSTR_1:7
.=
(((g4 * (R `3_3)) * gf2) * (P `2_3)) * ((z `2) * ((P `3_3) |^ 3))
by GROUP_1:def 3
.=
((g4 * (R `3_3)) * gf2) * ((P `2_3) * ((z `2) * ((P `3_3) |^ 3)))
by GROUP_1:def 3
.=
((g4 * (R `3_3)) * gf2) * ((z `2) * ((P `2_3) * ((P `3_3) |^ (2 + 1))))
by GROUP_1:def 3
.=
((g4 * (R `3_3)) * gf2) * ((z `2) * ((P `2_3) * (((P `3_3) |^ 2) * (P `3_3))))
by EC_PF_1:24
.=
(((g4 * (R `3_3)) * gf2) * (z `2)) * ((P `2_3) * ((P `3_3) * ((P `3_3) |^ 2)))
by GROUP_1:def 3
.=
(((g4 * (R `3_3)) * gf2) * (z `2)) * (gf2 * ((P `3_3) |^ 2))
by A2, GROUP_1:def 3
.=
((g4 * ((R `3_3) * gf2)) * (z `2)) * (gf2 * ((P `3_3) |^ 2))
by GROUP_1:def 3
.=
(g4 * (((R `3_3) * gf2) * (z `2))) * (gf2 * ((P `3_3) |^ 2))
by GROUP_1:def 3
.=
g4 * ((((R `3_3) * gf2) * (z `2)) * (gf2 * ((P `3_3) |^ 2)))
by GROUP_1:def 3
.=
g4 * (((((R `3_3) * gf2) * (z `2)) * gf2) * ((P `3_3) |^ 2))
by GROUP_1:def 3
.=
g4 * ((gf2 * (gf2 * ((R `3_3) * (z `2)))) * ((P `3_3) |^ 2))
by GROUP_1:def 3
.=
g4 * (((gf2 * gf2) * ((R `3_3) * (z `2))) * ((P `3_3) |^ 2))
by GROUP_1:def 3
.=
g4 * (((gf2 |^ 2) * ((z `2) * (R `3_3))) * ((P `3_3) |^ 2))
by EC_PF_1:22
.=
g4 * ((gf2 |^ 2) * (((z `2) * (R `3_3)) * ((P `3_3) |^ 2)))
by GROUP_1:def 3
.=
(g4 * (gf2 |^ 2)) * (((P `3_3) |^ 2) * ((z `2) * (R `3_3)))
by GROUP_1:def 3
.=
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3))
by GROUP_1:def 3
; verum