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)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p)
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)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p)
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)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p)
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)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p)
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)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p) )
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)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) = 0. (GF p)
set a = z `1 ;
set b = z `2 ;
A4: g4 =
(2 * 2) mod p
by A1
.=
g2 * g2
by A1, EC_PF_1:18
;
then A5:
g4 = g2 |^ 2
by EC_PF_1:22;
A6: g8 =
(2 * 4) mod p
by A1
.=
g2 * g4
by A1, EC_PF_1:18
;
A7: ((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3)) =
((((g2 |^ 2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((R `2_3) |^ 2)) * (R `3_3)
by A5, GROUP_1:def 3
.=
((((g2 * gf2) |^ 2) * ((P `3_3) |^ 2)) * ((R `2_3) |^ 2)) * (R `3_3)
by BINOM:9
.=
((((g2 * gf2) * (P `3_3)) * (R `2_3)) |^ 2) * (R `3_3)
by Th13
.=
((- ((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_3)))) |^ 2) * (R `3_3)
by A1, A2, A3, Th59
.=
(((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) + (((g2 * gf2) * (P `2_3)) * (R `3_3))) |^ 2) * (R `3_3)
by Th1
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + ((g2 * (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * (((g2 * gf2) * (P `2_3)) * (R `3_3)))) + ((((g2 * gf2) * (P `2_3)) * (R `3_3)) |^ 2)) * (R `3_3)
by A1, Th25
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + ((g2 * (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * (g2 * ((gf2 * (P `2_3)) * (R `3_3))))) + ((((g2 * gf2) * (P `2_3)) * (R `3_3)) |^ 2)) * (R `3_3)
by Th11
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((g2 * (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * g2) * ((gf2 * (P `2_3)) * (R `3_3)))) + ((((g2 * gf2) * (P `2_3)) * (R `3_3)) |^ 2)) * (R `3_3)
by GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((g2 * g2) * (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * ((gf2 * (P `2_3)) * (R `3_3)))) + ((((g2 * gf2) * (P `2_3)) * (R `3_3)) |^ 2)) * (R `3_3)
by GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + ((g4 * (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * ((gf2 * (P `2_3)) * (R `3_3)))) + (((g2 * gf2) * ((P `2_3) * (R `3_3))) |^ 2)) * (R `3_3)
by A4, GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + ((g4 * (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * ((gf2 * (P `2_3)) * (R `3_3)))) + (((g2 |^ 2) * (gf2 |^ 2)) * (((P `2_3) * (R `3_3)) |^ 2))) * (R `3_3)
by Th13
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + ((g4 * (gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * ((gf2 * (P `2_3)) * (R `3_3)))) + ((g4 * (gf2 |^ 2)) * (((P `2_3) |^ 2) * ((R `3_3) |^ 2)))) * (R `3_3)
by A5, BINOM:9
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((g4 * gf1) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * ((gf2 * (P `2_3)) * (R `3_3)))) + ((g4 * (gf2 |^ 2)) * (((P `2_3) |^ 2) * ((R `3_3) |^ 2)))) * (R `3_3)
by GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((g4 * gf1) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * ((gf2 * (P `2_3)) * (R `3_3)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 2))) * (R `3_3)
by GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((((g4 * gf1) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * gf2) * (P `2_3)) * (R `3_3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 2))) * (R `3_3)
by Th11
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((g4 * gf1) * (((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) * gf2) * (P `2_3))) * (R `3_3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 2))) * (R `3_3)
by Th11
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((g4 * gf1) * ((gf2 * (P `2_3)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) * (R `3_3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 2))) * (R `3_3)
by GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) + (((((g4 * gf1) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * (R `3_3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 2))) * (R `3_3)
by Th11
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * (R `3_3)) * (R `3_3))) + ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 2)) * (R `3_3))
by Th14
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * ((R `3_3) * (R `3_3)))) + ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 2)) * (R `3_3))
by GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * ((R `3_3) * (R `3_3)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * (((R `3_3) |^ 2) * (R `3_3)))
by GROUP_1:def 3
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * ((R `3_3) * (R `3_3)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ (2 + 1)))
by EC_PF_1:24
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) * ((R `3_3) |^ 2))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by EC_PF_1:22
.=
((((gf1 * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3)))) |^ 2) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by GROUP_1:def 3
.=
((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * (((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by BINOM:9
.=
((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * ((P `3_3) * (R `1_3))) - (((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * ((P `1_3) * (R `3_3))))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by VECTSP_1:11
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * ((P `3_3) * (R `1_3)))) - (((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * ((P `1_3) * (R `3_3)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + (((((g4 * gf1) * gf2) * (P `2_3)) * ((P `3_3) * (R `1_3))) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * ((P `1_3) * (R `3_3)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * ((P `1_3) * (R `3_3)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * ((R `3_3) |^ 2)) * (P `1_3)) * (R `3_3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `1_3)) * ((R `3_3) |^ 2)) * (R `3_3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `2_3)) * (P `1_3)) * (((R `3_3) |^ 2) * (R `3_3)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `2_3)) * (P `1_3)) * ((R `3_3) |^ (2 + 1)))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by EC_PF_1:24
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))
by GROUP_1:def 3
;
A8: - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) =
- ((((((g2 * g2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (R `1_3)) * (z `1)) * ((R `3_3) |^ 2))
by A4, Th11
.=
- ((((g2 * ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2))) * (R `1_3)) * (z `1)) * ((R `3_3) |^ 2))
by Th11
.=
- ((((g2 * (R `1_3)) * ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2))) * (z `1)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
- ((((g2 * (R `1_3)) * ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2))) * (z `1)) * ((R `3_3) * (R `3_3)))
by EC_PF_1:22
.=
- (((((g2 * (R `1_3)) * ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2))) * (z `1)) * (R `3_3)) * (R `3_3))
by GROUP_1:def 3
.=
- (((((g2 * (R `1_3)) * ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2))) * (R `3_3)) * (z `1)) * (R `3_3))
by GROUP_1:def 3
.=
- (((((g2 * (R `1_3)) * (R `3_3)) * ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2))) * (z `1)) * (R `3_3))
by GROUP_1:def 3
.=
- ((((g2 * (R `1_3)) * (R `3_3)) * ((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2))) * ((z `1) * (R `3_3)))
by GROUP_1:def 3
.=
- (((g2 * (R `1_3)) * (R `3_3)) * (((g2 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `1) * (R `3_3))))
by GROUP_1:def 3
.=
- (((g2 * (R `1_3)) * (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))))))
by A1, A2, A3, Th62
.=
- ((((g2 * (R `1_3)) * (R `3_3)) * (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))) + (((g2 * (R `1_3)) * (R `3_3)) * ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))))
by VECTSP_1:def 7
.=
(- (((g2 * (R `1_3)) * (R `3_3)) * ((gf2 |^ 2) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3)))))) - (((g2 * (R `1_3)) * (R `3_3)) * (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))))
by VECTSP_1:17
.=
(- ((((g2 * (R `1_3)) * (R `3_3)) * (gf2 |^ 2)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - (((g2 * (R `1_3)) * (R `3_3)) * (((gf1 * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3)))))
by GROUP_1:def 3
.=
(- ((((g2 * (R `1_3)) * (R `3_3)) * (gf2 |^ 2)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - ((((g2 * (R `1_3)) * (R `3_3)) * ((gf1 * (P `3_3)) * (R `3_3))) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- ((((g2 * (R `1_3)) * (gf2 |^ 2)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - ((((g2 * (R `1_3)) * (R `3_3)) * ((gf1 * (P `3_3)) * (R `3_3))) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - ((((g2 * (R `1_3)) * (R `3_3)) * ((gf1 * (P `3_3)) * (R `3_3))) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - ((((((g2 * (R `1_3)) * (R `3_3)) * gf1) * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by Th11
.=
(- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - (((((g2 * ((R `1_3) * (R `3_3))) * gf1) * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - (((((g2 * gf1) * ((R `1_3) * (R `3_3))) * (P `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - (((((g2 * gf1) * (P `3_3)) * ((R `1_3) * (R `3_3))) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - ((((((g2 * gf1) * (P `3_3)) * (R `1_3)) * (R `3_3)) * (R `3_3)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)) + ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) * (R `3_3))) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(- (((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3))) + ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) * (R `3_3))) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by VECTSP_1:def 7
.=
(- (((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3))) + ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((g2 * ((P `1_3) |^ 2)) * (R `3_3))))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by EC_PF_1:22
.=
((- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * ((g2 * ((P `1_3) |^ 2)) * (R `3_3)))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by VECTSP_1:17
.=
((- ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (g2 * (((P `1_3) |^ 2) * (R `3_3))))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- (((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * g2) * (((P `1_3) |^ 2) * (R `3_3)))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g2 * (gf2 |^ 2)) * ((R `1_3) * (R `3_3))) * g2) * (((P `1_3) |^ 2) * (R `3_3)))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g2 * (gf2 |^ 2)) * g2) * ((R `1_3) * (R `3_3))) * (((P `1_3) |^ 2) * (R `3_3)))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- (((g2 * (gf2 |^ 2)) * g2) * (((R `1_3) * (R `3_3)) * (((P `1_3) |^ 2) * (R `3_3))))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- (((g2 * g2) * (gf2 |^ 2)) * (((R `1_3) * (R `3_3)) * (((P `1_3) |^ 2) * (R `3_3))))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((g4 * (gf2 |^ 2)) * ((((R `1_3) * (R `3_3)) * ((P `1_3) |^ 2)) * (R `3_3)))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by A4, GROUP_1:def 3
.=
((- ((g4 * (gf2 |^ 2)) * ((((R `1_3) * ((P `1_3) |^ 2)) * (R `3_3)) * (R `3_3)))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((g4 * (gf2 |^ 2)) * (((R `1_3) * ((P `1_3) |^ 2)) * ((R `3_3) * (R `3_3))))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((g4 * (gf2 |^ 2)) * (((R `1_3) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 2)))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by EC_PF_1:22
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (((g4 * (P `1_3)) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * (g4 * (((P `1_3) * (P `3_3)) * (R `1_3))))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g2 * (gf2 |^ 2)) * (R `1_3)) * (R `3_3)) * g4) * (((P `1_3) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((g2 * (gf2 |^ 2)) * ((R `1_3) * (R `3_3))) * g4) * (((P `1_3) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((g2 * (gf2 |^ 2)) * g4) * ((R `1_3) * (R `3_3))) * (((P `1_3) * (P `3_3)) * (R `1_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((g2 * (gf2 |^ 2)) * g4) * (((R `1_3) * (R `3_3)) * (((P `1_3) * (P `3_3)) * (R `1_3))))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((g2 * g4) * (gf2 |^ 2)) * (((R `1_3) * (R `3_3)) * (((P `1_3) * (P `3_3)) * (R `1_3))))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((g8 * (gf2 |^ 2)) * (((((P `1_3) * (P `3_3)) * (R `1_3)) * (R `1_3)) * (R `3_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by A6, GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((g8 * (gf2 |^ 2)) * ((((P `1_3) * (P `3_3)) * ((R `1_3) * (R `1_3))) * (R `3_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((g8 * (gf2 |^ 2)) * ((((P `1_3) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3)))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by EC_PF_1:22
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))))
by Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) - ((((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (gf1 * (P `1_3))))
by VECTSP_1:11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * (gf1 * (P `1_3))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))))
by VECTSP_1:17
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((g2 * gf1) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))) * (gf1 * (P `1_3))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))))
by Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((g2 * gf1) * (gf1 * (P `1_3))) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + (((((g2 * gf1) * gf1) * (P `1_3)) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((g2 * (gf1 * gf1)) * (P `1_3)) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((g2 * (gf1 |^ 2)) * (P `1_3)) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))))
by EC_PF_1:22
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - (((((g2 * gf1) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) * ((g2 * gf2) * (P `2_3))))
by Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - (((g2 * gf1) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))) * ((g2 * gf2) * (P `2_3))))
by Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - (((g2 * gf1) * ((g2 * gf2) * (P `2_3))) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - (((((g2 * gf1) * g2) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))))
by Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - (((((g2 * g2) * gf1) * gf2) * (P `2_3)) * (((P `3_3) * (R `1_3)) * ((R `3_3) |^ 2))))
by GROUP_1:def 3
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))) + ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)))
by A4, Th11
.=
((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by ALGSTR_1:8
.=
(((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by ALGSTR_1:7
.=
(((- ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by ALGSTR_1:8
;
A9: - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * ((R `3_3) |^ 3))) =
- ((((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (z `2)) * ((R `3_3) |^ (2 + 1)))
by GROUP_1:def 3
.=
- ((((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (z `2)) * (((R `3_3) |^ 2) * (R `3_3)))
by EC_PF_1:24
.=
- (((((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (z `2)) * (R `3_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
- (((R `3_3) |^ 2) * (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * (R `3_3))))
by GROUP_1:def 3
.=
- (((R `3_3) |^ 2) * (((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)) - (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3))))
by A1, A2, A3, Th61
.=
- ((((R `3_3) |^ 2) * ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2))) - (((R `3_3) |^ 2) * (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3))))
by VECTSP_1:11
.=
(((R `3_3) |^ 2) * (((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3))) - (((R `3_3) |^ 2) * ((R `3_3) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2)))
by VECTSP_1:17
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) - ((((R `3_3) |^ 2) * (R `3_3)) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2))
by GROUP_1:def 3
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) - (((R `3_3) |^ (2 + 1)) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2))
by EC_PF_1:24
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * ((((g2 * gf2) * (P `2_3)) - (gf1 * (P `1_3))) |^ 2))
by VECTSP_1:9
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * (((((g2 * gf2) * (P `2_3)) |^ 2) - ((g2 * ((g2 * gf2) * (P `2_3))) * (gf1 * (P `1_3)))) + ((gf1 * (P `1_3)) |^ 2)))
by A1, Th26
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * (((((g2 |^ 2) * (gf2 |^ 2)) * ((P `2_3) |^ 2)) - ((g2 * ((g2 * gf2) * (P `2_3))) * (gf1 * (P `1_3)))) + ((gf1 * (P `1_3)) |^ 2)))
by Th13
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) - ((g2 * ((g2 * gf2) * (P `2_3))) * (gf1 * (P `1_3)))) + ((gf1 |^ 2) * ((P `1_3) |^ 2))))
by A5, BINOM:9
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) - ((((g2 * g2) * gf2) * (P `2_3)) * (gf1 * (P `1_3)))) + ((gf1 |^ 2) * ((P `1_3) |^ 2))))
by Th11
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) - (((g4 * gf2) * (gf1 * (P `1_3))) * (P `2_3))) + ((gf1 |^ 2) * ((P `1_3) |^ 2))))
by A4, GROUP_1:def 3
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) - ((((g4 * gf2) * gf1) * (P `1_3)) * (P `2_3))) + ((gf1 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((R `3_3) |^ 3)) * ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) - ((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3))) + ((gf1 |^ 2) * ((P `1_3) |^ 2))))
by GROUP_1:def 3
.=
(((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * (- ((R `3_3) |^ 3))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * (- ((R `3_3) |^ 3)))) + (((gf1 |^ 2) * ((P `1_3) |^ 2)) * (- ((R `3_3) |^ 3)))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by Th14
.=
(((- (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * (- ((R `3_3) |^ 3)))) + (((gf1 |^ 2) * ((P `1_3) |^ 2)) * (- ((R `3_3) |^ 3)))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:8
.=
(((- (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) - (- (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3)))) + (((gf1 |^ 2) * ((P `1_3) |^ 2)) * (- ((R `3_3) |^ 3)))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:8
.=
(((- (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + (((gf1 |^ 2) * ((P `1_3) |^ 2)) * (- ((R `3_3) |^ 3)))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by RLVECT_1:17
.=
(((- (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) - (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:8
;
A10: (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * ((R `3_3) |^ 3))) =
((((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) + (((- (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))))
by A7, A9, ALGSTR_1:7
.=
((((((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) - (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))
by Th8
.=
(((((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3)) - (((g4 * (gf2 |^ 2)) * ((P `2_3) |^ 2)) * ((R `3_3) |^ 3)))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))
by ALGSTR_1:7
.=
(((((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + (0. (GF p))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))
by VECTSP_1:19
.=
((((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((- (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3))) + (((((g4 * gf1) * gf2) * (P `1_3)) * (P `2_3)) * ((R `3_3) |^ 3)))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (0. (GF p))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))
by RLVECT_1:5
.=
((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((- (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 3))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) - (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ (2 + 1)))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by ALGSTR_1:8
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) - (((gf1 |^ 2) * ((P `1_3) |^ 2)) * (((R `3_3) |^ 2) * (R `3_3)))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by EC_PF_1:24
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) * (R `3_3)) - ((((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 2)) * (R `3_3))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) - (((gf1 |^ 2) * ((P `1_3) |^ 2)) * ((R `3_3) |^ 2))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:13
.=
(((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2)) - ((gf1 |^ 2) * (((P `1_3) |^ 2) * ((R `3_3) |^ 2)))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((gf1 |^ 2) * (((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2) - (((P `1_3) |^ 2) * ((R `3_3) |^ 2)))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:11
.=
((((gf1 |^ 2) * (((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) |^ 2) - (((P `1_3) * (R `3_3)) |^ 2))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by BINOM:9
.=
((((gf1 |^ 2) * (((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) + ((P `1_3) * (R `3_3))) * ((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) - ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by Th15
.=
((((gf1 |^ 2) * (((((P `3_3) * (R `1_3)) - ((P `1_3) * (R `3_3))) + ((P `1_3) * (R `3_3))) * (((P `3_3) * (R `1_3)) - (((P `1_3) * (R `3_3)) + ((P `1_3) * (R `3_3)))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:17
.=
((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) + ((- ((P `1_3) * (R `3_3))) + ((P `1_3) * (R `3_3)))) * (((P `3_3) * (R `1_3)) - (((P `1_3) * (R `3_3)) + ((P `1_3) * (R `3_3)))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by ALGSTR_1:7
.=
((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) + (0. (GF p))) * (((P `3_3) * (R `1_3)) - (((P `1_3) * (R `3_3)) + ((P `1_3) * (R `3_3)))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by RLVECT_1:5
.=
((((gf1 |^ 2) * ((((P `3_3) * (R `1_3)) + (0. (GF p))) * (((P `3_3) * (R `1_3)) - (g2 * ((P `1_3) * (R `3_3)))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by A1, Th20
.=
((((gf1 |^ 2) * (((P `3_3) * (R `1_3)) * (((P `3_3) * (R `1_3)) - (g2 * ((P `1_3) * (R `3_3)))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by RLVECT_1:4
.=
(((((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * (((P `3_3) * (R `1_3)) - (g2 * ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * ((P `3_3) * (R `1_3))) - (((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * (g2 * ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:11
.=
(((((gf1 |^ 2) * (((P `3_3) * (R `1_3)) * ((P `3_3) * (R `1_3)))) - (((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * (g2 * ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * (((P `3_3) * (R `1_3)) |^ 2)) - (((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * (g2 * ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by EC_PF_1:22
.=
(((((gf1 |^ 2) * (((P `3_3) |^ 2) * ((R `1_3) |^ 2))) - (((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * (g2 * ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by BINOM:9
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) - (((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * (g2 * ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) - ((((gf1 |^ 2) * ((P `3_3) * (R `1_3))) * g2) * ((P `1_3) * (R `3_3)))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) - ((((gf1 |^ 2) * g2) * ((P `3_3) * (R `1_3))) * ((P `1_3) * (R `3_3)))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) - ((g2 * (gf1 |^ 2)) * (((P `3_3) * (R `1_3)) * ((P `1_3) * (R `3_3))))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) - ((g2 * (gf1 |^ 2)) * ((((P `3_3) * (R `1_3)) * (P `1_3)) * (R `3_3)))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) - ((g2 * (gf1 |^ 2)) * ((((P `1_3) * (P `3_3)) * (R `1_3)) * (R `3_3)))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * (R `3_3))) * (R `3_3)) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by Th11
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - ((((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * (R `3_3)) * (R `3_3))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:13
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) * (R `3_3)))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))
by EC_PF_1:22
;
A11: (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((((z `1) * (R `1_3)) * ((R `3_3) |^ 2)) + ((z `2) * ((R `3_3) |^ 3)))) =
(((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - ((((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * ((R `3_3) |^ 3))))
by VECTSP_1:def 7
.=
((((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((z `2) * ((R `3_3) |^ 3)))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2)))
by VECTSP_1:17
.=
((((((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by A8, A10, Th8
.=
(((((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)) - ((((g4 * (gf2 |^ 2)) * ((P `1_3) |^ 2)) * (R `1_3)) * ((R `3_3) |^ 2)))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by ALGSTR_1:7
.=
(((((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (0. (GF p))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by RLVECT_1:5
.=
((((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by RLVECT_1:4
.=
(((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - ((((((g4 * gf1) * gf2) * (P `2_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by ALGSTR_1:7
.=
(((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (0. (GF p))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by RLVECT_1:5
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by RLVECT_1:4
.=
(((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) + ((- (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * (gf1 |^ 2)) * (P `1_3)) * (P `3_3)) * (R `1_3)) * ((R `3_3) |^ 2)))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) + (0. (GF p))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by RLVECT_1:5
.=
((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (R `3_3)) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by RLVECT_1:4
.=
(((gf1 |^ 2) * ((P `3_3) |^ 2)) * (((R `1_3) |^ 2) * (R `3_3))) - (((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3))
by GROUP_1:def 3
.=
(((gf1 |^ 2) * ((P `3_3) |^ 2)) * (((R `1_3) |^ 2) * (R `3_3))) - ((((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3)) * (((R `1_3) |^ 2) * (R `3_3)))
by GROUP_1:def 3
.=
(((gf1 |^ 2) * ((P `3_3) |^ 2)) - (((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3))) * (((R `1_3) |^ 2) * (R `3_3))
by VECTSP_1:13
.=
(((gf1 |^ 2) * ((P `3_3) * (P `3_3))) - (((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3))) * (((R `1_3) |^ 2) * (R `3_3))
by EC_PF_1:22
.=
((((gf1 |^ 2) * ((P `3_3) * (P `3_3))) - (((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3))) * ((R `1_3) |^ 2)) * (R `3_3)
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * (P `3_3)) * (P `3_3)) - (((g8 * (gf2 |^ 2)) * (P `1_3)) * (P `3_3))) * ((R `1_3) |^ 2)) * (R `3_3)
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3))) * (P `3_3)) * ((R `1_3) |^ 2)) * (R `3_3)
by VECTSP_1:13
.=
(((R `3_3) * (((gf1 |^ 2) * (P `3_3)) - ((g8 * (gf2 |^ 2)) * (P `1_3)))) * (P `3_3)) * ((R `1_3) |^ 2)
by Th11
.=
((((g4 * (gf2 |^ 2)) * (P `3_3)) * (R `1_3)) * (P `3_3)) * ((R `1_3) |^ 2)
by A1, A2, A3, Th60
.=
((((g4 * (gf2 |^ 2)) * (P `3_3)) * (P `3_3)) * (R `1_3)) * ((R `1_3) |^ 2)
by GROUP_1:def 3
.=
(((g4 * (gf2 |^ 2)) * ((P `3_3) * (P `3_3))) * (R `1_3)) * ((R `1_3) |^ 2)
by GROUP_1:def 3
.=
(((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (R `1_3)) * ((R `1_3) |^ 2)
by EC_PF_1:22
.=
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `1_3) |^ 2) * (R `1_3))
by GROUP_1:def 3
.=
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((R `1_3) |^ (2 + 1))
by EC_PF_1:24
.=
((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 3)
;
thus ((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3)))) =
(((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3))))
by VECTSP_1:11
.=
(((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `1_3) |^ 3) + ((((z `1) * (R `1_3)) * ((R `3_3) |^ 2)) + ((z `2) * ((R `3_3) |^ 3)))))
by ALGSTR_1:7
.=
(((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - ((((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 3)) + (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((((z `1) * (R `1_3)) * ((R `3_3) |^ 2)) + ((z `2) * ((R `3_3) |^ 3)))))
by VECTSP_1:def 7
.=
((((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (((R `2_3) |^ 2) * (R `3_3))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((((z `1) * (R `1_3)) * ((R `3_3) |^ 2)) + ((z `2) * ((R `3_3) |^ 3))))) - (((g4 * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 3))
by VECTSP_1:17
.=
0. (GF p)
by A11, RLVECT_1:5
; verum