let p be 5 _or_greater Prime; :: thesis: 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)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3)))
let z be Element of EC_WParam p; :: thesis: 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)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3)))
let g2, g3, g4, g8, gf1, gf2, gf3, gf4 be Element of (GF p); :: thesis: 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)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3)))
let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: 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)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3)))
let R be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; :: thesis: ( 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)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `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))] ; :: thesis: ((g4 * (gf2 |^ 2)) * (P `3_3)) * (R `1_3) = (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_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: ((g4 * (gf2 |^ 2)) * (P `3_3)) * (R `1_3) = ((g4 * (gf2 |^ 2)) * (P `3_3)) * ((g2 * gf4) * gf2) by A3
.= ((g4 * (gf2 |^ 2)) * (P `3_3)) * (g2 * (gf4 * gf2)) by GROUP_1:def 3
.= (g4 * ((gf2 |^ 2) * (P `3_3))) * (g2 * (gf2 * gf4)) by GROUP_1:def 3
.= (g4 * ((P `3_3) * (gf2 |^ 2))) * ((g2 * gf2) * gf4) by GROUP_1:def 3
.= ((g4 * (P `3_3)) * (gf2 |^ 2)) * ((gf2 * g2) * gf4) by GROUP_1:def 3
.= (((g4 * (P `3_3)) * (gf2 |^ 2)) * (gf2 * g2)) * gf4 by GROUP_1:def 3
.= ((g4 * (P `3_3)) * ((gf2 |^ 2) * (gf2 * g2))) * gf4 by GROUP_1:def 3
.= ((g4 * (P `3_3)) * (((gf2 |^ 2) * gf2) * g2)) * gf4 by GROUP_1:def 3
.= ((g4 * (P `3_3)) * ((gf2 |^ (2 + 1)) * g2)) * gf4 by EC_PF_1:24
.= (((g4 * (P `3_3)) * g2) * (gf2 |^ 3)) * gf4 by GROUP_1:def 3
.= (((g2 * g4) * (P `3_3)) * (gf2 |^ 3)) * ((gf1 |^ 2) - (g8 * gf3)) by A2, GROUP_1:def 3
.= ((g8 * (gf2 |^ 3)) * (P `3_3)) * ((gf1 |^ 2) - (g8 * gf3)) by A4, GROUP_1:def 3 ;
thus (R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3))) = (g8 * (gf2 |^ 3)) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3))) by A3
.= (g8 * (gf2 |^ 3)) * (((P `3_3) * (gf1 |^ 2)) - (g8 * ((gf2 |^ 2) * (P `1_3)))) by GROUP_1:def 3
.= (g8 * (gf2 |^ 3)) * (((P `3_3) * (gf1 |^ 2)) - ((P `3_3) * (g8 * gf3))) by A5, GROUP_1:def 3
.= (g8 * (gf2 |^ 3)) * ((P `3_3) * ((gf1 |^ 2) - (g8 * gf3))) by VECTSP_1:11
.= ((g4 * (gf2 |^ 2)) * (P `3_3)) * (R `1_3) by A6, GROUP_1:def 3 ; :: thesis: verum