let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q 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 & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
let z be Element of EC_WParam p; for g2, gf1, gf2, gf3 being Element of (GF p)
for P, Q 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 & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
let g2, gf1, gf2, gf3 be Element of (GF p); for P, Q 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 & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
let P, Q 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 & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] holds
((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `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 & gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) & R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))] implies ((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) )
assume that
A1:
g2 = 2 mod p
and
A2:
( gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)) & gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)) & gf3 = ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) )
and
A3:
R = [(gf2 * gf3),((gf1 * ((((gf2 |^ 2) * (P `1_3)) * (Q `3_3)) - gf3)) - (((gf2 |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2 |^ 3) * (P `3_3)) * (Q `3_3))]
; ((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3) = ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
set a = z `1 ;
set b = z `2 ;
A4: (gf2 * (P `2_3)) - (gf1 * (P `1_3)) =
((((Q `1_3) * (P `3_3)) * (P `2_3)) - (((P `1_3) * (Q `3_3)) * (P `2_3))) - ((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) * (P `1_3))
by A2, VECTSP_1:11
.=
((((Q `1_3) * (P `3_3)) * (P `2_3)) - (((P `1_3) * (Q `3_3)) * (P `2_3))) - ((((Q `2_3) * (P `3_3)) * (P `1_3)) - (((P `2_3) * (Q `3_3)) * (P `1_3)))
by VECTSP_1:11
.=
((((Q `1_3) * (P `3_3)) * (P `2_3)) - (((P `1_3) * (Q `3_3)) * (P `2_3))) + ((((P `2_3) * (Q `3_3)) * (P `1_3)) - (((Q `2_3) * (P `3_3)) * (P `1_3)))
by VECTSP_1:17
.=
((((Q `1_3) * (P `3_3)) * (P `2_3)) - ((P `1_3) * ((Q `3_3) * (P `2_3)))) + ((((P `2_3) * (Q `3_3)) * (P `1_3)) - (((Q `2_3) * (P `3_3)) * (P `1_3)))
by GROUP_1:def 3
.=
(((Q `1_3) * (P `3_3)) * (P `2_3)) + ((- ((P `1_3) * ((Q `3_3) * (P `2_3)))) + ((((P `2_3) * (Q `3_3)) * (P `1_3)) - (((Q `2_3) * (P `3_3)) * (P `1_3))))
by ALGSTR_1:7
.=
(((Q `1_3) * (P `3_3)) * (P `2_3)) + (((- ((P `1_3) * ((P `2_3) * (Q `3_3)))) + (((P `2_3) * (Q `3_3)) * (P `1_3))) - (((Q `2_3) * (P `3_3)) * (P `1_3)))
by ALGSTR_1:7
.=
(((Q `1_3) * (P `3_3)) * (P `2_3)) + ((0. (GF p)) - (((P `3_3) * (Q `2_3)) * (P `1_3)))
by VECTSP_1:19
.=
(((P `3_3) * (Q `1_3)) * (P `2_3)) - (((P `3_3) * (Q `2_3)) * (P `1_3))
by VECTSP_1:18
.=
((P `3_3) * ((Q `1_3) * (P `2_3))) - (((P `3_3) * (Q `2_3)) * (P `1_3))
by GROUP_1:def 3
.=
((P `3_3) * ((P `2_3) * (Q `1_3))) - ((P `3_3) * ((Q `2_3) * (P `1_3)))
by GROUP_1:def 3
.=
(P `3_3) * (((P `2_3) * (Q `1_3)) - ((Q `2_3) * (P `1_3)))
by VECTSP_1:11
;
(gf2 * (Q `2_3)) - (gf1 * (Q `1_3)) =
((((Q `1_3) * (P `3_3)) * (Q `2_3)) - (((P `1_3) * (Q `3_3)) * (Q `2_3))) - ((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) * (Q `1_3))
by A2, VECTSP_1:11
.=
((((Q `1_3) * (P `3_3)) * (Q `2_3)) - (((P `1_3) * (Q `3_3)) * (Q `2_3))) - ((((Q `2_3) * (P `3_3)) * (Q `1_3)) - (((P `2_3) * (Q `3_3)) * (Q `1_3)))
by VECTSP_1:11
.=
((((Q `1_3) * (P `3_3)) * (Q `2_3)) - (((P `1_3) * (Q `3_3)) * (Q `2_3))) + ((((P `2_3) * (Q `3_3)) * (Q `1_3)) - (((Q `2_3) * (P `3_3)) * (Q `1_3)))
by VECTSP_1:17
.=
(((((Q `1_3) * (P `3_3)) * (Q `2_3)) - (((P `1_3) * (Q `3_3)) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * (Q `1_3))) - (((Q `2_3) * (P `3_3)) * (Q `1_3))
by ALGSTR_1:7
.=
(((((Q `1_3) * (P `3_3)) * (Q `2_3)) - (((Q `2_3) * (P `3_3)) * (Q `1_3))) + (((P `2_3) * (Q `3_3)) * (Q `1_3))) - (((P `1_3) * (Q `3_3)) * (Q `2_3))
by Th7
.=
((((Q `1_3) * ((P `3_3) * (Q `2_3))) - ((Q `1_3) * ((P `3_3) * (Q `2_3)))) + (((Q `3_3) * (P `2_3)) * (Q `1_3))) - (((Q `3_3) * (P `1_3)) * (Q `2_3))
by GROUP_1:def 3
.=
((0. (GF p)) + (((Q `3_3) * (P `2_3)) * (Q `1_3))) - (((Q `3_3) * (P `1_3)) * (Q `2_3))
by VECTSP_1:19
.=
(((Q `3_3) * (P `2_3)) * (Q `1_3)) - (((Q `3_3) * (P `1_3)) * (Q `2_3))
by ALGSTR_1:7
.=
((Q `3_3) * ((P `2_3) * (Q `1_3))) - (((Q `3_3) * (P `1_3)) * (Q `2_3))
by GROUP_1:def 3
.=
((Q `3_3) * ((P `2_3) * (Q `1_3))) - ((Q `3_3) * ((P `1_3) * (Q `2_3)))
by GROUP_1:def 3
.=
(Q `3_3) * (((P `2_3) * (Q `1_3)) - ((P `1_3) * (Q `2_3)))
by VECTSP_1:11
;
then A5:
((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))) * (P `3_3) = ((gf2 * (P `2_3)) - (gf1 * (P `1_3))) * (Q `3_3)
by A4, GROUP_1:def 3;
A6: ((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)) =
(((P `1_3) * (Q `1_3)) * (R `3_3)) + ((((P `3_3) * (Q `1_3)) * (R `1_3)) + (((P `1_3) * (Q `3_3)) * (R `1_3)))
by ALGSTR_1:7
.=
(((P `1_3) * (Q `1_3)) * (R `3_3)) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (R `1_3))
by VECTSP_1:def 7
.=
(((P `1_3) * (Q `1_3)) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (R `1_3))
by A3
.=
(((P `1_3) * (Q `1_3)) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (gf2 * gf3))
by A3
.=
(((P `1_3) * (Q `1_3)) * ((gf2 |^ 3) * ((P `3_3) * (Q `3_3)))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (gf2 * gf3))
by GROUP_1:def 3
.=
((((P `1_3) * (Q `1_3)) * (gf2 |^ (2 + 1))) * ((P `3_3) * (Q `3_3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (gf2 * gf3))
by GROUP_1:def 3
.=
((((P `1_3) * (Q `1_3)) * ((gf2 |^ 2) * gf2)) * ((P `3_3) * (Q `3_3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (gf2 * gf3))
by EC_PF_1:24
.=
((((P `1_3) * (Q `1_3)) * ((gf2 |^ 2) * gf2)) * ((P `3_3) * (Q `3_3))) + (((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf2) * gf3)
by GROUP_1:def 3
.=
(((((P `1_3) * (Q `1_3)) * (gf2 |^ 2)) * gf2) * ((P `3_3) * (Q `3_3))) + ((gf2 * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * gf3)
by GROUP_1:def 3
.=
((gf2 * (((P `1_3) * (Q `1_3)) * (gf2 |^ 2))) * ((P `3_3) * (Q `3_3))) + (gf2 * ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3))
by GROUP_1:def 3
.=
(gf2 * ((((P `1_3) * (Q `1_3)) * (gf2 |^ 2)) * ((P `3_3) * (Q `3_3)))) + (gf2 * ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3))
by GROUP_1:def 3
.=
gf2 * (((((P `1_3) * (Q `1_3)) * (gf2 |^ 2)) * ((P `3_3) * (Q `3_3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3))
by VECTSP_1:def 7
;
A7: gf3 =
((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - (gf2 |^ (2 + 1))) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3))
by A2
.=
((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((gf2 |^ 2) * gf2)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3))
by EC_PF_1:24
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + ((- ((gf2 |^ 2) * gf2)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)))
by ALGSTR_1:7
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + ((- ((gf2 |^ 2) * gf2)) - ((g2 * (gf2 |^ 2)) * ((P `1_3) * (Q `3_3))))
by GROUP_1:def 3
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + ((- ((gf2 |^ 2) * gf2)) - ((gf2 |^ 2) * (g2 * ((P `1_3) * (Q `3_3)))))
by GROUP_1:def 3
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + (((- (gf2 |^ 2)) * gf2) - ((gf2 |^ 2) * (g2 * ((P `1_3) * (Q `3_3)))))
by VECTSP_1:9
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + (((- (gf2 |^ 2)) * gf2) + ((- (gf2 |^ 2)) * (g2 * ((P `1_3) * (Q `3_3)))))
by VECTSP_1:9
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + ((- (gf2 |^ 2)) * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) + (g2 * ((P `1_3) * (Q `3_3)))))
by A2, VECTSP_1:def 7
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((gf2 |^ 2) * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) + (g2 * ((P `1_3) * (Q `3_3)))))
by VECTSP_1:9
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((gf2 |^ 2) * (((Q `1_3) * (P `3_3)) + ((- ((P `1_3) * (Q `3_3))) + (g2 * ((P `1_3) * (Q `3_3))))))
by ALGSTR_1:7
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((gf2 |^ 2) * (((Q `1_3) * (P `3_3)) + ((g2 * ((P `1_3) * (Q `3_3))) - ((P `1_3) * (Q `3_3)))))
.=
(((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))))
by A1, Th24
;
((((P `1_3) * (Q `1_3)) * (gf2 |^ 2)) * ((P `3_3) * (Q `3_3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3) =
((gf2 |^ 2) * (((P `1_3) * (Q `1_3)) * ((P `3_3) * (Q `3_3)))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3)
by GROUP_1:def 3
.=
((gf2 |^ 2) * ((P `3_3) * ((Q `3_3) * ((P `1_3) * (Q `1_3))))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3)
by GROUP_1:def 3
.=
((gf2 |^ 2) * ((P `3_3) * (((Q `3_3) * (P `1_3)) * (Q `1_3)))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3)
by GROUP_1:def 3
.=
((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * gf3)
by GROUP_1:def 3
.=
((- (gf2 |^ 2)) * (- (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) - ((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))))))
by A7, VECTSP_1:10
.=
((- (gf2 |^ 2)) * (- (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + (((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))) - ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * ((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))))))
by VECTSP_1:11
.=
((- (gf2 |^ 2)) * (- (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + ((- ((gf2 |^ 2) * ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))
by GROUP_1:def 3
.=
((- (gf2 |^ 2)) * (- (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + ((- ((gf2 |^ 2) * ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))
by EC_PF_1:22
.=
((- (gf2 |^ 2)) * (- (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + (((- (gf2 |^ 2)) * ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) |^ 2)) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))
by VECTSP_1:9
.=
(((- (gf2 |^ 2)) * (- (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + ((- (gf2 |^ 2)) * ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by ALGSTR_1:7
.=
((- (gf2 |^ 2)) * ((- (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by VECTSP_1:def 7
.=
((- (gf2 |^ 2)) * ((((((P `3_3) * (Q `1_3)) |^ 2) + ((g2 * ((P `3_3) * (Q `1_3))) * ((P `1_3) * (Q `3_3)))) + (((P `1_3) * (Q `3_3)) |^ 2)) - (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by A1, Th25
.=
((- (gf2 |^ 2)) * ((((((P `3_3) * (Q `1_3)) |^ 2) + ((g2 * ((P `3_3) * (Q `1_3))) * ((P `1_3) * (Q `3_3)))) - (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + (((P `1_3) * (Q `3_3)) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by ALGSTR_1:8
.=
((- (gf2 |^ 2)) * ((((((P `3_3) * (Q `1_3)) |^ 2) + (g2 * (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) - (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + (((P `1_3) * (Q `3_3)) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by GROUP_1:def 3
.=
((- (gf2 |^ 2)) * (((((P `3_3) * (Q `1_3)) |^ 2) + ((g2 * (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) - (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3))))) + (((P `1_3) * (Q `3_3)) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by ALGSTR_1:7
.=
((- (gf2 |^ 2)) * (((((P `3_3) * (Q `1_3)) |^ 2) + (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + (((P `1_3) * (Q `3_3)) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by A1, Th24
.=
((- (gf2 * gf2)) * (((((P `3_3) * (Q `1_3)) |^ 2) + (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + (((P `1_3) * (Q `3_3)) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by EC_PF_1:22
.=
(((- gf2) * gf2) * (((((P `3_3) * (Q `1_3)) |^ 2) + (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + (((P `1_3) * (Q `3_3)) |^ 2))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by VECTSP_1:9
.=
((- gf2) * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) * (((((P `3_3) * (Q `1_3)) |^ 2) + (((P `3_3) * (Q `1_3)) * ((P `1_3) * (Q `3_3)))) + (((P `1_3) * (Q `3_3)) |^ 2)))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by A2, GROUP_1:def 3
.=
((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by Th17
;
then A8: (gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3))) =
((gf2 |^ 2) * gf2) * (((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))
by A6, GROUP_1:def 3
.=
(gf2 |^ (2 + 1)) * (((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))
by EC_PF_1:24
.=
(gf2 |^ 3) * (((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))
;
(((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 ((Q `3_3) |^ 3) * (((P `2_3) |^ 2) * (P `3_3)) =
((Q `3_3) |^ 3) * ((((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + ((z `2) * ((P `3_3) |^ 3)))
by VECTSP_1:19
.=
(((Q `3_3) |^ 3) * (((P `1_3) |^ 3) + (((z `1) * (P `1_3)) * ((P `3_3) |^ 2)))) + (((Q `3_3) |^ 3) * ((z `2) * ((P `3_3) |^ 3)))
by VECTSP_1:def 7
.=
((((Q `3_3) |^ 3) * ((P `1_3) |^ 3)) + (((Q `3_3) |^ 3) * (((z `1) * (P `1_3)) * ((P `3_3) |^ 2)))) + (((Q `3_3) |^ 3) * ((z `2) * ((P `3_3) |^ 3)))
by VECTSP_1:def 7
.=
((((Q `3_3) * (P `1_3)) |^ 3) + ((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * ((Q `3_3) |^ (2 + 1)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by BINOM:9
.=
((((P `1_3) * (Q `3_3)) |^ 3) + ((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * (((Q `3_3) |^ 2) * (Q `3_3)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by EC_PF_1:24
.=
((((P `1_3) * (Q `3_3)) |^ 3) + (((z `1) * (P `1_3)) * (((P `3_3) |^ 2) * (((Q `3_3) |^ 2) * (Q `3_3))))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
.=
((((P `1_3) * (Q `3_3)) |^ 3) + (((z `1) * (P `1_3)) * ((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (Q `3_3)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
.=
((((P `1_3) * (Q `3_3)) |^ 3) + (((z `1) * (P `1_3)) * ((((P `3_3) * (Q `3_3)) |^ 2) * (Q `3_3)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by BINOM:9
.=
((((P `1_3) * (Q `3_3)) |^ 3) + ((z `1) * ((P `1_3) * ((((P `3_3) * (Q `3_3)) |^ 2) * (Q `3_3))))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
.=
((((P `1_3) * (Q `3_3)) |^ 3) + ((z `1) * ((((P `3_3) * (Q `3_3)) |^ 2) * ((Q `3_3) * (P `1_3))))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
.=
((((P `1_3) * (Q `3_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
;
then A9: - (((Q `3_3) |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) =
(- (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))) - ((((P `1_3) * (Q `3_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3))))
by VECTSP_1:17
.=
(- (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))) + ((- (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) - (((P `1_3) * (Q `3_3)) |^ 3))
by VECTSP_1:17
;
(((Q `2_3) |^ 2) * (Q `3_3)) - ((((Q `1_3) |^ 3) + (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2))) + ((z `2) * ((Q `3_3) |^ 3))) = 0. (GF p)
by Th35;
then A10: ((P `3_3) |^ 3) * (((Q `2_3) |^ 2) * (Q `3_3)) =
((P `3_3) |^ 3) * ((((Q `1_3) |^ 3) + (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2))) + ((z `2) * ((Q `3_3) |^ 3)))
by VECTSP_1:19
.=
(((P `3_3) |^ 3) * (((Q `1_3) |^ 3) + (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)))) + (((P `3_3) |^ 3) * ((z `2) * ((Q `3_3) |^ 3)))
by VECTSP_1:def 7
.=
((((P `3_3) |^ 3) * ((Q `1_3) |^ 3)) + (((P `3_3) |^ 3) * (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)))) + (((P `3_3) |^ 3) * ((z `2) * ((Q `3_3) |^ 3)))
by VECTSP_1:def 7
.=
((((P `3_3) * (Q `1_3)) |^ 3) + ((((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)) * ((P `3_3) |^ (2 + 1)))) + (((z `2) * ((Q `3_3) |^ 3)) * ((P `3_3) |^ 3))
by BINOM:9
.=
((((P `3_3) * (Q `1_3)) |^ 3) + ((((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)) * (((P `3_3) |^ 2) * (P `3_3)))) + (((z `2) * ((Q `3_3) |^ 3)) * ((P `3_3) |^ 3))
by EC_PF_1:24
.=
((((P `3_3) * (Q `1_3)) |^ 3) + ((((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)) * (((P `3_3) |^ 2) * (P `3_3)))) + ((z `2) * (((Q `3_3) |^ 3) * ((P `3_3) |^ 3)))
by GROUP_1:def 3
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (Q `1_3)) * (((Q `3_3) |^ 2) * (((P `3_3) |^ 2) * (P `3_3))))) + ((z `2) * (((P `3_3) |^ 3) * ((Q `3_3) |^ 3)))
by GROUP_1:def 3
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (Q `1_3)) * ((((Q `3_3) |^ 2) * ((P `3_3) |^ 2)) * (P `3_3)))) + ((z `2) * (((P `3_3) |^ 3) * ((Q `3_3) |^ 3)))
by GROUP_1:def 3
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (Q `1_3)) * ((((Q `3_3) * (P `3_3)) |^ 2) * (P `3_3)))) + ((z `2) * (((P `3_3) |^ 3) * ((Q `3_3) |^ 3)))
by BINOM:9
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (Q `1_3)) * ((((P `3_3) * (Q `3_3)) |^ 2) * (P `3_3)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
.=
((((P `3_3) * (Q `1_3)) |^ 3) + ((z `1) * ((Q `1_3) * ((((P `3_3) * (Q `3_3)) |^ 2) * (P `3_3))))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
.=
((((P `3_3) * (Q `1_3)) |^ 3) + ((z `1) * ((((P `3_3) * (Q `3_3)) |^ 2) * ((P `3_3) * (Q `1_3))))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))
by GROUP_1:def 3
;
A11: (gf1 * ((P `3_3) * (Q `3_3))) * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3))) =
((P `3_3) * (Q `3_3)) * ((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) * (((Q `2_3) * (P `3_3)) + ((P `2_3) * (Q `3_3))))
by A2, GROUP_1:def 3
.=
((P `3_3) * (Q `3_3)) * ((((Q `2_3) * (P `3_3)) |^ 2) - (((P `2_3) * (Q `3_3)) |^ 2))
by Th15
.=
((P `3_3) * (Q `3_3)) * ((((Q `2_3) |^ 2) * ((P `3_3) |^ 2)) - (((P `2_3) * (Q `3_3)) |^ 2))
by BINOM:9
.=
((P `3_3) * (Q `3_3)) * ((((Q `2_3) |^ 2) * ((P `3_3) |^ 2)) - (((P `2_3) |^ 2) * ((Q `3_3) |^ 2)))
by BINOM:9
.=
(((P `3_3) * (Q `3_3)) * (((Q `2_3) |^ 2) * ((P `3_3) |^ 2))) - (((P `3_3) * (Q `3_3)) * (((P `2_3) |^ 2) * ((Q `3_3) |^ 2)))
by VECTSP_1:11
.=
((P `3_3) * ((Q `3_3) * (((Q `2_3) |^ 2) * ((P `3_3) |^ 2)))) - (((P `3_3) * (Q `3_3)) * (((Q `3_3) |^ 2) * ((P `2_3) |^ 2)))
by GROUP_1:def 3
.=
((P `3_3) * (((Q `3_3) * ((Q `2_3) |^ 2)) * ((P `3_3) |^ 2))) - (((P `3_3) * (Q `3_3)) * (((Q `3_3) |^ 2) * ((P `2_3) |^ 2)))
by GROUP_1:def 3
.=
((P `3_3) * (((P `3_3) |^ 2) * ((Q `3_3) * ((Q `2_3) |^ 2)))) - ((P `3_3) * ((Q `3_3) * (((Q `3_3) |^ 2) * ((P `2_3) |^ 2))))
by GROUP_1:def 3
.=
((P `3_3) * (((P `3_3) |^ 2) * (((Q `2_3) |^ 2) * (Q `3_3)))) - ((P `3_3) * (((Q `3_3) * ((Q `3_3) |^ 2)) * ((P `2_3) |^ 2)))
by GROUP_1:def 3
.=
(((P `3_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3))) - ((P `3_3) * ((((Q `3_3) |^ 2) * (Q `3_3)) * ((P `2_3) |^ 2)))
by GROUP_1:def 3
.=
((((P `3_3) |^ 2) * (P `3_3)) * (((Q `2_3) |^ 2) * (Q `3_3))) - ((P `3_3) * (((P `2_3) |^ 2) * ((Q `3_3) |^ (2 + 1))))
by EC_PF_1:24
.=
(((P `3_3) |^ (2 + 1)) * (((Q `2_3) |^ 2) * (Q `3_3))) - ((P `3_3) * (((P `2_3) |^ 2) * ((Q `3_3) |^ 3)))
by EC_PF_1:24
.=
(((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3)))) + (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))) - (((Q `3_3) |^ 3) * ((P `3_3) * ((P `2_3) |^ 2)))
by A10, GROUP_1:def 3
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3)))) + ((((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3)) + ((- (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))) + ((- (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) - (((P `1_3) * (Q `3_3)) |^ 3))))
by A9, ALGSTR_1:7
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3)))) + (((((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3)) - (((z `2) * ((P `3_3) |^ 3)) * ((Q `3_3) |^ 3))) + ((- (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) - (((P `1_3) * (Q `3_3)) |^ 3)))
by ALGSTR_1:7
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3)))) + ((0. (GF p)) + ((- (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) - (((P `1_3) * (Q `3_3)) |^ 3)))
by VECTSP_1:19
.=
((((P `3_3) * (Q `1_3)) |^ 3) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3)))) + ((- (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) - (((P `1_3) * (Q `3_3)) |^ 3))
by ALGSTR_1:7
.=
(((P `3_3) * (Q `1_3)) |^ 3) + ((((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3))) + ((- (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) - (((P `1_3) * (Q `3_3)) |^ 3)))
by ALGSTR_1:7
.=
(((P `3_3) * (Q `1_3)) |^ 3) + (((((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((Q `1_3) * (P `3_3))) - (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * ((P `1_3) * (Q `3_3)))) - (((P `1_3) * (Q `3_3)) |^ 3))
by ALGSTR_1:7
.=
(((P `3_3) * (Q `1_3)) |^ 3) + ((- (((P `1_3) * (Q `3_3)) |^ 3)) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * (((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)))))
by VECTSP_1:11
.=
((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3)) + (((z `1) * (((P `3_3) * (Q `3_3)) |^ 2)) * gf2)
by A2, ALGSTR_1:7
.=
((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3)) + (((z `1) * gf2) * (((P `3_3) * (Q `3_3)) |^ 2))
by GROUP_1:def 3
;
A12: (((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))) =
(((g2 * (Q `3_3)) * gf1) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))
by GROUP_1:def 3
.=
((g2 * (Q `3_3)) * (gf1 * (R `3_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))
by GROUP_1:def 3
.=
(gf1 * (R `3_3)) * ((g2 * (Q `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))
by GROUP_1:def 3
.=
(gf1 * (R `3_3)) * (g2 * ((Q `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))))
by GROUP_1:def 3
.=
(gf1 * (R `3_3)) * (((Q `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) + ((Q `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))))
by A1, Th20
.=
(gf1 * (R `3_3)) * ((((Q `3_3) * (gf2 * (P `2_3))) - ((Q `3_3) * (gf1 * (P `1_3)))) + (((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))) * (P `3_3)))
by A5, VECTSP_1:11
.=
(gf1 * (R `3_3)) * ((((gf2 * (P `2_3)) * (Q `3_3)) - ((gf1 * (P `1_3)) * (Q `3_3))) + (((gf2 * (Q `2_3)) * (P `3_3)) - ((gf1 * (Q `1_3)) * (P `3_3))))
by VECTSP_1:13
.=
(gf1 * (R `3_3)) * (((gf2 * ((P `2_3) * (Q `3_3))) - ((gf1 * (P `1_3)) * (Q `3_3))) + (((gf2 * (Q `2_3)) * (P `3_3)) - ((gf1 * (Q `1_3)) * (P `3_3))))
by GROUP_1:def 3
.=
(gf1 * (R `3_3)) * ((((gf2 * ((P `2_3) * (Q `3_3))) - ((gf1 * (P `1_3)) * (Q `3_3))) + ((gf2 * (Q `2_3)) * (P `3_3))) - ((gf1 * (Q `1_3)) * (P `3_3)))
by ALGSTR_1:7
.=
(gf1 * (R `3_3)) * ((((gf2 * ((P `2_3) * (Q `3_3))) - (gf1 * ((P `1_3) * (Q `3_3)))) + ((gf2 * (Q `2_3)) * (P `3_3))) - ((gf1 * (Q `1_3)) * (P `3_3)))
by GROUP_1:def 3
.=
(gf1 * (R `3_3)) * ((((gf2 * ((P `2_3) * (Q `3_3))) - (gf1 * ((P `1_3) * (Q `3_3)))) + (gf2 * ((Q `2_3) * (P `3_3)))) - ((gf1 * (Q `1_3)) * (P `3_3)))
by GROUP_1:def 3
.=
(gf1 * (R `3_3)) * ((((gf2 * ((P `2_3) * (Q `3_3))) + (gf2 * ((Q `2_3) * (P `3_3)))) - (gf1 * ((P `1_3) * (Q `3_3)))) - ((gf1 * (Q `1_3)) * (P `3_3)))
by ALGSTR_1:8
.=
(gf1 * (R `3_3)) * ((((gf2 * ((P `2_3) * (Q `3_3))) + (gf2 * ((Q `2_3) * (P `3_3)))) - (gf1 * ((P `1_3) * (Q `3_3)))) - (gf1 * ((Q `1_3) * (P `3_3))))
by GROUP_1:def 3
.=
(gf1 * (R `3_3)) * (((gf2 * ((P `2_3) * (Q `3_3))) + (gf2 * ((Q `2_3) * (P `3_3)))) + ((- (gf1 * ((P `1_3) * (Q `3_3)))) - (gf1 * ((Q `1_3) * (P `3_3)))))
by ALGSTR_1:7
.=
(gf1 * (R `3_3)) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) + ((- (gf1 * ((P `1_3) * (Q `3_3)))) + (- (gf1 * ((Q `1_3) * (P `3_3))))))
by VECTSP_1:def 7
.=
(gf1 * (R `3_3)) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) + (((- gf1) * ((P `1_3) * (Q `3_3))) + (- (gf1 * ((Q `1_3) * (P `3_3))))))
by VECTSP_1:9
.=
(gf1 * (R `3_3)) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) + (((- gf1) * ((P `1_3) * (Q `3_3))) + ((- gf1) * ((Q `1_3) * (P `3_3)))))
by VECTSP_1:9
.=
(gf1 * (R `3_3)) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) + ((- gf1) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by VECTSP_1:def 7
.=
(gf1 * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3))) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) + ((- gf1) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by A3
.=
(gf1 * ((gf2 |^ 3) * ((P `3_3) * (Q `3_3)))) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) + ((- gf1) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by GROUP_1:def 3
.=
((gf1 * (gf2 |^ 3)) * ((P `3_3) * (Q `3_3))) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) + ((- gf1) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by GROUP_1:def 3
.=
(((gf2 |^ 3) * gf1) * ((P `3_3) * (Q `3_3))) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) - (gf1 * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by VECTSP_1:9
.=
((gf2 |^ 3) * (gf1 * ((P `3_3) * (Q `3_3)))) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) - (gf1 * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * ((gf1 * ((P `3_3) * (Q `3_3))) * ((gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) - (gf1 * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3))))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * (((gf1 * ((P `3_3) * (Q `3_3))) * (gf2 * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3))))) - ((gf1 * ((P `3_3) * (Q `3_3))) * (gf1 * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3))))))
by VECTSP_1:11
.=
(gf2 |^ 3) * ((((gf1 * ((P `3_3) * (Q `3_3))) * gf2) * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) - ((gf1 * ((P `3_3) * (Q `3_3))) * (gf1 * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3))))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * (((gf2 * (gf1 * ((P `3_3) * (Q `3_3)))) * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3)))) - (((gf1 * ((P `3_3) * (Q `3_3))) * gf1) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * ((gf2 * ((gf1 * ((P `3_3) * (Q `3_3))) * (((P `2_3) * (Q `3_3)) + ((Q `2_3) * (P `3_3))))) - ((gf1 * (gf1 * ((P `3_3) * (Q `3_3)))) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * ((gf2 * (((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3)) + (((z `1) * gf2) * (((P `3_3) * (Q `3_3)) |^ 2)))) - (((gf1 * gf1) * ((P `3_3) * (Q `3_3))) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by A11, GROUP_1:def 3
.=
(gf2 |^ 3) * ((gf2 * (((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3)) + (((z `1) * gf2) * (((P `3_3) * (Q `3_3)) |^ 2)))) - (((gf1 |^ 2) * ((P `3_3) * (Q `3_3))) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3)))))
by EC_PF_1:22
.=
(gf2 |^ 3) * ((- (((gf1 |^ 2) * ((P `3_3) * (Q `3_3))) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3))))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (gf2 * (((z `1) * gf2) * (((P `3_3) * (Q `3_3)) |^ 2)))))
by VECTSP_1:def 7
.=
(gf2 |^ 3) * ((- ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3))))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (gf2 * (((z `1) * gf2) * (((P `3_3) * (Q `3_3)) |^ 2)))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * ((- ((((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((gf2 * ((z `1) * gf2)) * (((P `3_3) * (Q `3_3)) |^ 2))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * ((- ((((P `1_3) * (Q `3_3)) + ((Q `1_3) * (P `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((z `1) * (gf2 * gf2)) * (((P `3_3) * (Q `3_3)) |^ 2))))
by GROUP_1:def 3
.=
(gf2 |^ 3) * ((- ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2))))
by EC_PF_1:22
;
thus ((gf2 |^ 2) * (((((P `1_3) * (Q `1_3)) * (R `3_3)) + (((P `3_3) * (Q `1_3)) * (R `1_3))) + (((P `1_3) * (Q `3_3)) * (R `1_3)))) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) =
(gf2 |^ 3) * ((((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))) + ((- ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2)))))
by A8, A12, VECTSP_1:def 7
.=
(gf2 |^ 3) * (((((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))) - ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2))))
by ALGSTR_1:7
.=
(gf2 |^ 3) * ((((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))) - ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2))))
by ALGSTR_1:7
.=
(gf2 |^ 3) * ((((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (0. (GF p))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2))))
by VECTSP_1:19
.=
(gf2 |^ 3) * (((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + ((gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2))))
by ALGSTR_1:7
.=
(gf2 |^ 3) * ((((- gf2) * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3))) + (gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3)))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2)))
by ALGSTR_1:7
.=
(gf2 |^ 3) * (((- (gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3)))) + (gf2 * ((((P `3_3) * (Q `1_3)) |^ 3) - (((P `1_3) * (Q `3_3)) |^ 3)))) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2)))
by VECTSP_1:9
.=
(gf2 |^ 3) * ((0. (GF p)) + (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2)))
by RLVECT_1:5
.=
(gf2 |^ 3) * (((z `1) * (gf2 |^ 2)) * (((P `3_3) * (Q `3_3)) |^ 2))
by ALGSTR_1:7
.=
((gf2 |^ 3) * ((z `1) * (gf2 |^ 2))) * (((P `3_3) * (Q `3_3)) |^ 2)
by GROUP_1:def 3
.=
(((z `1) * (gf2 |^ 2)) * (gf2 |^ 3)) * (((P `3_3) * (Q `3_3)) * ((P `3_3) * (Q `3_3)))
by EC_PF_1:22
.=
((z `1) * (gf2 |^ 2)) * ((gf2 |^ 3) * (((P `3_3) * (Q `3_3)) * ((P `3_3) * (Q `3_3))))
by GROUP_1:def 3
.=
((z `1) * (gf2 |^ 2)) * (((gf2 |^ 3) * ((P `3_3) * (Q `3_3))) * ((P `3_3) * (Q `3_3)))
by GROUP_1:def 3
.=
((z `1) * (gf2 |^ 2)) * ((((gf2 |^ 3) * (P `3_3)) * (Q `3_3)) * ((P `3_3) * (Q `3_3)))
by GROUP_1:def 3
.=
((z `1) * (gf2 |^ 2)) * ((R `3_3) * ((P `3_3) * (Q `3_3)))
by A3
.=
((z `1) * (gf2 |^ 2)) * ((P `3_3) * ((Q `3_3) * (R `3_3)))
by GROUP_1:def 3
.=
(((z `1) * (gf2 |^ 2)) * (P `3_3)) * ((Q `3_3) * (R `3_3))
by GROUP_1:def 3
.=
((((z `1) * (gf2 |^ 2)) * (P `3_3)) * (Q `3_3)) * (R `3_3)
by GROUP_1:def 3
; verum