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
((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_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
((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_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
((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_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
((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * 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):]; :: 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 ((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (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))] ; :: thesis: ((g2 * gf2) * (P `3_3)) * (R `2_3) = - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_3)))
set a = z `1 ;
set b = z `2 ;
g8 = (2 * 4) mod p by A1
.= g2 * g4 by A1, EC_PF_1:18 ;
then A4: g8 + (g2 * g8) = g2 * (g4 + g8) by VECTSP_1:def 7;
A5: (P `3_3) * gf3 = ((P `3_3) * ((P `1_3) * (P `2_3))) * gf2 by A2, GROUP_1:def 3
.= ((P `1_3) * gf2) * gf2 by A2, GROUP_1:def 3
.= (P `1_3) * (gf2 * gf2) by GROUP_1:def 3
.= (P `1_3) * (gf2 |^ 2) by EC_PF_1:22 ;
A6: ((P `3_3) * gf2) * gf3 = ((P `3_3) * gf3) * gf2 by GROUP_1:def 3
.= (P `1_3) * ((gf2 |^ 2) * gf2) by A5, GROUP_1:def 3
.= (P `1_3) * (gf2 |^ (2 + 1)) by EC_PF_1:24
.= (P `1_3) * (gf2 |^ 3) ;
A7: (g4 * gf3) - gf4 = (g4 * gf3) + ((g8 * gf3) - (gf1 |^ 2)) by A2, VECTSP_1:17
.= ((g4 * gf3) + (g8 * gf3)) - (gf1 |^ 2) by ALGSTR_1:7
.= ((g4 + g8) * gf3) - (gf1 |^ 2) by VECTSP_1:def 7 ;
((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)) = ((P `3_3) * ((g2 * gf4) * gf2)) - ((P `1_3) * (R `3_3)) by A3
.= ((P `3_3) * ((g2 * gf4) * gf2)) - ((P `1_3) * (g8 * (gf2 |^ 3))) by A3
.= ((P `3_3) * ((g2 * gf2) * ((gf1 |^ 2) - (g8 * gf3)))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by A2, GROUP_1:def 3
.= (((P `3_3) * (g2 * gf2)) * ((gf1 |^ 2) - (g8 * gf3))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by GROUP_1:def 3
.= ((((P `3_3) * gf2) * g2) * ((gf1 |^ 2) - (g8 * gf3))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by GROUP_1:def 3
.= (g2 * (((P `3_3) * gf2) * ((gf1 |^ 2) - (g8 * gf3)))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by GROUP_1:def 3
.= (g2 * ((((P `3_3) * gf2) * (gf1 |^ 2)) - (((P `3_3) * gf2) * (g8 * gf3)))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by VECTSP_1:11
.= (g2 * ((((P `3_3) * gf2) * (gf1 |^ 2)) - ((((P `3_3) * gf2) * gf3) * g8))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by GROUP_1:def 3
.= ((g2 * (((P `3_3) * gf2) * (gf1 |^ 2))) - (g2 * (((P `1_3) * (gf2 |^ 3)) * g8))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by A6, VECTSP_1:11
.= ((g2 * (((P `3_3) * gf2) * (gf1 |^ 2))) - ((g2 * g8) * ((P `1_3) * (gf2 |^ 3)))) - ((P `1_3) * (g8 * (gf2 |^ 3))) by GROUP_1:def 3
.= ((g2 * (((P `3_3) * gf2) * (gf1 |^ 2))) - ((g2 * g8) * ((P `1_3) * (gf2 |^ 3)))) - (g8 * ((P `1_3) * (gf2 |^ 3))) by GROUP_1:def 3
.= (g2 * (((P `3_3) * gf2) * (gf1 |^ 2))) - ((g8 * ((P `1_3) * (gf2 |^ 3))) + ((g2 * g8) * ((P `1_3) * (gf2 |^ 3)))) by VECTSP_1:17
.= (g2 * (((P `3_3) * gf2) * (gf1 |^ 2))) - ((g8 + (g2 * g8)) * ((P `1_3) * (gf2 |^ 3))) by VECTSP_1:def 7 ;
then A8: - (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) = ((g8 + (g2 * g8)) * ((P `1_3) * (gf2 |^ 3))) - (g2 * (((P `3_3) * gf2) * (gf1 |^ 2))) by VECTSP_1:17
.= (g2 * ((g4 + g8) * ((P `1_3) * (gf2 |^ 3)))) - (g2 * (((P `3_3) * gf2) * (gf1 |^ 2))) by A4, GROUP_1:def 3
.= g2 * (((g4 + g8) * ((P `1_3) * (gf2 |^ 3))) - (((P `3_3) * gf2) * (gf1 |^ 2))) by VECTSP_1:11 ;
A9: ((g2 * gf2) * (P `3_3)) * (R `2_3) = ((g2 * gf2) * (P `3_3)) * ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))) by A3
.= (((g2 * gf2) * (P `3_3)) * (gf1 * (((g4 + g8) * gf3) - (gf1 |^ 2)))) - (((g2 * gf2) * (P `3_3)) * ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))) by A7, VECTSP_1:11 ;
A10: - (((g2 * gf2) * (P `3_3)) * ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))) = - ((g2 * (gf2 * (P `3_3))) * ((g8 * ((P `2_3) |^ 2)) * (gf2 |^ 2))) by GROUP_1:def 3
.= - ((g2 * ((P `3_3) * gf2)) * (g8 * (((P `2_3) |^ 2) * (gf2 |^ 2)))) by GROUP_1:def 3
.= - (((g2 * (P `3_3)) * gf2) * (g8 * ((gf2 |^ 2) * ((P `2_3) |^ 2)))) by GROUP_1:def 3
.= - ((g2 * (P `3_3)) * (gf2 * (g8 * ((gf2 |^ 2) * ((P `2_3) |^ 2))))) by GROUP_1:def 3
.= - ((g2 * (P `3_3)) * (gf2 * ((g8 * (gf2 |^ 2)) * ((P `2_3) |^ 2)))) by GROUP_1:def 3
.= - ((g2 * (P `3_3)) * ((gf2 * (g8 * (gf2 |^ 2))) * ((P `2_3) |^ 2))) by GROUP_1:def 3
.= - ((g2 * (P `3_3)) * (((gf2 * g8) * (gf2 |^ 2)) * ((P `2_3) |^ 2))) by GROUP_1:def 3
.= - (((g2 * (P `3_3)) * ((P `2_3) |^ 2)) * ((gf2 * g8) * (gf2 |^ 2))) by GROUP_1:def 3
.= - ((g2 * ((P `3_3) * ((P `2_3) |^ 2))) * ((g8 * gf2) * (gf2 |^ 2))) by GROUP_1:def 3
.= - ((g2 * (((P `2_3) |^ 2) * (P `3_3))) * (g8 * (gf2 * (gf2 |^ 2)))) by GROUP_1:def 3
.= - ((g2 * (((P `2_3) * (P `2_3)) * (P `3_3))) * (g8 * ((gf2 |^ 2) * gf2))) by EC_PF_1:22
.= - ((g2 * ((P `2_3) * ((P `2_3) * (P `3_3)))) * (g8 * ((gf2 |^ 2) * gf2))) by GROUP_1:def 3
.= - ((g2 * ((P `2_3) * ((P `2_3) * (P `3_3)))) * (g8 * (gf2 |^ (2 + 1)))) by EC_PF_1:24
.= - (g2 * (((P `2_3) * gf2) * (g8 * (gf2 |^ 3)))) by A2, GROUP_1:def 3
.= - (g2 * ((P `2_3) * (gf2 * (g8 * (gf2 |^ 3))))) by GROUP_1:def 3
.= - (g2 * ((P `2_3) * (gf2 * (R `3_3)))) by A3
.= - (g2 * (gf2 * ((P `2_3) * (R `3_3)))) by GROUP_1:def 3
.= - ((g2 * gf2) * ((P `2_3) * (R `3_3))) by GROUP_1:def 3
.= - (((g2 * gf2) * (P `2_3)) * (R `3_3)) by GROUP_1:def 3 ;
((g2 * gf2) * (P `3_3)) * (gf1 * (((g4 + g8) * gf3) - (gf1 |^ 2))) = gf1 * (((g2 * gf2) * (P `3_3)) * (((g4 + g8) * gf3) - (gf1 |^ 2))) by GROUP_1:def 3
.= gf1 * ((g2 * (gf2 * (P `3_3))) * (((g4 + g8) * gf3) - (gf1 |^ 2))) by GROUP_1:def 3
.= gf1 * (g2 * ((gf2 * (P `3_3)) * (((g4 + g8) * gf3) - (gf1 |^ 2)))) by GROUP_1:def 3
.= gf1 * (g2 * ((((P `3_3) * gf2) * ((g4 + g8) * gf3)) - (((P `3_3) * gf2) * (gf1 |^ 2)))) by VECTSP_1:11
.= gf1 * (g2 * (((((P `3_3) * gf2) * gf3) * (g4 + g8)) - (((P `3_3) * gf2) * (gf1 |^ 2)))) by GROUP_1:def 3
.= - (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) by A6, A8, VECTSP_1:8 ;
hence ((g2 * gf2) * (P `3_3)) * (R `2_3) = (- (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) - (((g2 * gf2) * (P `2_3)) * (R `3_3)) by A9, A10
.= - ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_3))) by VECTSP_1:17 ;
:: thesis: verum