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 `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_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 `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_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 `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_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 `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_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 `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_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 `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3) = (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_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: - (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) =
- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (gf2 * gf3))
by A3
.=
- ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * gf3) * gf2)
by GROUP_1:def 3
.=
- (((((gf2 * (gf2 |^ 2)) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * gf3)
by Th12
.=
- (((((gf2 |^ (2 + 1)) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * gf3)
by EC_PF_1:24
.=
- (((gf2 |^ 3) * (P `3_3)) * (((P `1_3) * (Q `1_3)) * gf3))
by Th11
.=
((gf2 |^ 3) * (P `3_3)) * (- (((P `1_3) * (Q `1_3)) * gf3))
by VECTSP_1:8
;
- (gf1 * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3)))) =
- ((((Q `2_3) * (P `3_3)) * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3)))) - (((P `2_3) * (Q `3_3)) * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3)))))
by A2, VECTSP_1:13
.=
- (((((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3))) + (((Q `2_3) * (P `3_3)) * ((Q `1_3) * (P `2_3)))) - (((P `2_3) * (Q `3_3)) * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3)))))
by VECTSP_1:def 7
.=
- (((((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3))) + (((Q `2_3) * (P `3_3)) * ((Q `1_3) * (P `2_3)))) - ((((P `2_3) * (Q `3_3)) * ((P `1_3) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))))
by VECTSP_1:def 7
.=
((((P `2_3) * (Q `3_3)) * ((P `1_3) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - ((((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3))) + (((Q `2_3) * (P `3_3)) * ((Q `1_3) * (P `2_3))))
by VECTSP_1:17
.=
(((((P `2_3) * (Q `3_3)) * ((P `1_3) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by VECTSP_1:17
.=
(((((P `2_3) * (Q `3_3)) * ((P `1_3) * (Q `2_3))) - (((Q `2_3) * (P `3_3)) * ((Q `1_3) * (P `2_3)))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by ALGSTR_1:8
.=
(((((P `2_3) * (Q `3_3)) * ((P `1_3) * (Q `2_3))) - (((P `3_3) * ((Q `1_3) * (P `2_3))) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by GROUP_1:def 3
.=
((((((P `2_3) * (Q `3_3)) * (P `1_3)) * (Q `2_3)) - (((P `3_3) * ((Q `1_3) * (P `2_3))) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by GROUP_1:def 3
.=
((((((P `1_3) * (Q `3_3)) * (P `2_3)) * (Q `2_3)) - (((P `3_3) * ((Q `1_3) * (P `2_3))) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by GROUP_1:def 3
.=
((((((P `1_3) * (Q `3_3)) * (P `2_3)) * (Q `2_3)) - ((((P `3_3) * (Q `1_3)) * (P `2_3)) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by GROUP_1:def 3
.=
(((((P `1_3) * (Q `3_3)) * ((P `2_3) * (Q `2_3))) - ((((P `3_3) * (Q `1_3)) * (P `2_3)) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by GROUP_1:def 3
.=
(((((P `1_3) * (Q `3_3)) * ((P `2_3) * (Q `2_3))) - (((P `3_3) * (Q `1_3)) * ((P `2_3) * (Q `2_3)))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by GROUP_1:def 3
.=
(((((P `1_3) * (Q `3_3)) - ((P `3_3) * (Q `1_3))) * ((P `2_3) * (Q `2_3))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by VECTSP_1:13
.=
(((- (((P `1_3) * (Q `3_3)) - ((P `3_3) * (Q `1_3)))) * (- ((P `2_3) * (Q `2_3)))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by VECTSP_1:10
.=
(((((P `3_3) * (Q `1_3)) - ((P `1_3) * (Q `3_3))) * (- ((P `2_3) * (Q `2_3)))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by VECTSP_1:17
.=
((- ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) * ((P `2_3) * (Q `2_3)))) + (((P `2_3) * (Q `3_3)) * ((Q `1_3) * (P `2_3)))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by VECTSP_1:8
.=
((- (gf2 * ((P `2_3) * (Q `2_3)))) + (((Q `3_3) * ((Q `1_3) * (P `2_3))) * (P `2_3))) - (((Q `2_3) * (P `3_3)) * ((P `1_3) * (Q `2_3)))
by A2, GROUP_1:def 3
.=
((- (gf2 * ((P `2_3) * (Q `2_3)))) + (((Q `3_3) * ((Q `1_3) * (P `2_3))) * (P `2_3))) - (((P `3_3) * ((P `1_3) * (Q `2_3))) * (Q `2_3))
by GROUP_1:def 3
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `3_3) * ((Q `1_3) * (P `2_3))) * (P `2_3))) - (((P `3_3) * ((P `1_3) * (Q `2_3))) * (Q `2_3))
by GROUP_1:def 3
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + ((((Q `3_3) * (Q `1_3)) * (P `2_3)) * (P `2_3))) - (((P `3_3) * ((P `1_3) * (Q `2_3))) * (Q `2_3))
by GROUP_1:def 3
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `3_3) * (Q `1_3)) * ((P `2_3) * (P `2_3)))) - (((P `3_3) * ((P `1_3) * (Q `2_3))) * (Q `2_3))
by GROUP_1:def 3
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `3_3) * (Q `1_3)) * ((P `2_3) |^ 2))) - (((P `3_3) * ((P `1_3) * (Q `2_3))) * (Q `2_3))
by EC_PF_1:22
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `3_3) * (Q `1_3)) * ((P `2_3) |^ 2))) - ((((P `3_3) * (P `1_3)) * (Q `2_3)) * (Q `2_3))
by GROUP_1:def 3
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `3_3) * (Q `1_3)) * ((P `2_3) |^ 2))) - (((P `3_3) * (P `1_3)) * ((Q `2_3) * (Q `2_3)))
by GROUP_1:def 3
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `3_3) * (Q `1_3)) * ((P `2_3) |^ 2))) - (((P `3_3) * (P `1_3)) * ((Q `2_3) |^ 2))
by EC_PF_1:22
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3))) - (((P `3_3) * (P `1_3)) * ((Q `2_3) |^ 2))
by GROUP_1:def 3
.=
((- ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3))) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3))
by GROUP_1:def 3
;
then A7: ((gf2 * (P `2_3)) * (Q `2_3)) - (gf1 * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3)))) =
((((gf2 * (P `2_3)) * (Q `2_3)) - ((gf2 * (P `2_3)) * (Q `2_3))) + (((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3))) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3))
by Th8
.=
((0. (GF p)) + (((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3))) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3))
by RLVECT_1:5
.=
(((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3))
by RLVECT_1:4
;
A8: (((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3) =
(((gf2 * (P `2_3)) - (gf1 * (P `1_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (Q `3_3)
by EC_PF_1:22
.=
((gf2 * (P `2_3)) - (gf1 * (P `1_3))) * (((gf2 * (P `2_3)) - (gf1 * (P `1_3))) * (Q `3_3))
by GROUP_1:def 3
.=
(((gf2 * (P `2_3)) - (gf1 * (P `1_3))) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3)))) * (P `3_3)
by A5, GROUP_1:def 3
.=
(((gf2 * (P `2_3)) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3)))) - ((gf1 * (P `1_3)) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))))) * (P `3_3)
by VECTSP_1:13
.=
((((gf2 * (P `2_3)) * (gf2 * (Q `2_3))) - ((gf2 * (P `2_3)) * (gf1 * (Q `1_3)))) - ((gf1 * (P `1_3)) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))))) * (P `3_3)
by VECTSP_1:11
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * (P `2_3)) * (gf1 * (Q `1_3)))) - ((gf1 * (P `1_3)) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))))) * (P `3_3)
by GROUP_1:def 3
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * (gf1 * (Q `1_3))) * (P `2_3))) - ((gf1 * (P `1_3)) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))))) * (P `3_3)
by GROUP_1:def 3
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - (((gf2 * gf1) * (Q `1_3)) * (P `2_3))) - ((gf1 * (P `1_3)) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))))) * (P `3_3)
by GROUP_1:def 3
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) - ((gf1 * (P `1_3)) * ((gf2 * (Q `2_3)) - (gf1 * (Q `1_3))))) * (P `3_3)
by GROUP_1:def 3
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) - (((gf1 * (P `1_3)) * (gf2 * (Q `2_3))) - ((gf1 * (P `1_3)) * (gf1 * (Q `1_3))))) * (P `3_3)
by VECTSP_1:11
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) + (((gf1 * (P `1_3)) * (gf1 * (Q `1_3))) - ((gf1 * (P `1_3)) * (gf2 * (Q `2_3))))) * (P `3_3)
by VECTSP_1:17
.=
((((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) - ((gf1 * (P `1_3)) * (gf2 * (Q `2_3)))) * (P `3_3)
by ALGSTR_1:7
.=
((((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) - ((gf1 * (P `1_3)) * (gf2 * (Q `2_3)))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by ALGSTR_1:8
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) + ((- ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) - ((gf1 * (P `1_3)) * (gf2 * (Q `2_3))))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by ALGSTR_1:7
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) + ((- ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) - (((gf1 * (P `1_3)) * gf2) * (Q `2_3)))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by GROUP_1:def 3
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) + ((- ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) - (((gf2 * gf1) * (P `1_3)) * (Q `2_3)))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by GROUP_1:def 3
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) + ((- ((gf2 * gf1) * ((Q `1_3) * (P `2_3)))) - ((gf2 * gf1) * ((P `1_3) * (Q `2_3))))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by GROUP_1:def 3
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - (((gf2 * gf1) * ((P `1_3) * (Q `2_3))) + ((gf2 * gf1) * ((Q `1_3) * (P `2_3))))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by VECTSP_1:17
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - ((gf2 * gf1) * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3))))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by VECTSP_1:def 7
.=
(((gf2 * ((gf2 * (P `2_3)) * (Q `2_3))) - (gf2 * (gf1 * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3)))))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by GROUP_1:def 3
.=
((gf2 * (((gf2 * (P `2_3)) * (Q `2_3)) - (gf1 * (((P `1_3) * (Q `2_3)) + ((Q `1_3) * (P `2_3)))))) + ((gf1 * (P `1_3)) * (gf1 * (Q `1_3)))) * (P `3_3)
by VECTSP_1:11
.=
((gf2 * ((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3)))) + (((gf1 * (P `1_3)) * gf1) * (Q `1_3))) * (P `3_3)
by A7, GROUP_1:def 3
.=
((gf2 * ((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3)))) + (((gf1 * gf1) * (P `1_3)) * (Q `1_3))) * (P `3_3)
by GROUP_1:def 3
.=
((gf2 * ((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3)))) + (((gf1 |^ 2) * (P `1_3)) * (Q `1_3))) * (P `3_3)
by EC_PF_1:22
.=
((gf2 * ((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3)))) * (P `3_3)) + ((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3))
by VECTSP_1:def 7
.=
(gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3))) * (P `3_3))) + ((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3))
by GROUP_1:def 3
.=
(gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) * (P `3_3)) - ((((P `1_3) * ((Q `2_3) |^ 2)) * (P `3_3)) * (P `3_3)))) + ((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3))
by VECTSP_1:13
.=
(gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) * (P `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * ((P `3_3) * (P `3_3))))) + ((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3))
by GROUP_1:def 3
.=
(gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (Q `3_3)) * (P `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * ((P `3_3) |^ 2)))) + ((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3))
by EC_PF_1:22
.=
(gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((Q `2_3) |^ 2)) * ((P `3_3) |^ 2)))) + ((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3))
by GROUP_1:def 3
.=
(gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) + ((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3))
by GROUP_1:def 3
;
A9: (((gf2 |^ 3) * (P `3_3)) * (- (((P `1_3) * (Q `1_3)) * gf3))) + (((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (R `3_3)) =
(((gf2 |^ 3) * (P `3_3)) * (((P `1_3) * (Q `1_3)) * (- gf3))) + (((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (R `3_3))
by VECTSP_1:8
.=
((((gf2 |^ 3) * (P `3_3)) * ((P `1_3) * (Q `1_3))) * (- gf3)) + (((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (R `3_3))
by GROUP_1:def 3
.=
((((gf2 |^ 3) * ((P `1_3) * (Q `1_3))) * (P `3_3)) * (- gf3)) + (((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (R `3_3))
by GROUP_1:def 3
.=
(((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (- gf3)) + (((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (R `3_3))
by GROUP_1:def 3
.=
(((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (- gf3)) + (((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3)))
by A3
.=
(((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (- gf3)) + (((gf1 |^ 2) * (((P `1_3) * (Q `1_3)) * (P `3_3))) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3)))
by Th11
.=
(((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (- gf3)) + (((((gf1 |^ 2) * (((P `1_3) * (Q `1_3)) * (P `3_3))) * (gf2 |^ 3)) * (P `3_3)) * (Q `3_3))
by Th11
.=
(((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (- gf3)) + (((((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (gf1 |^ 2)) * (P `3_3)) * (Q `3_3))
by Th11
.=
(((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (- gf3)) + (((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by Th11
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((- gf3) + (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by VECTSP_1:def 7
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((- ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) + ((- (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3))))) + (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by A2, ALGSTR_1:7
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (((- ((- (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)))) - (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))) + (((gf1 |^ 2) * (P `3_3)) * (Q `3_3)))
by VECTSP_1:17
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((- ((- (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)))) + ((- (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))) + (((gf1 |^ 2) * (P `3_3)) * (Q `3_3))))
by ALGSTR_1:7
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((- ((- (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)))) + (0. (GF p)))
by RLVECT_1:5
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (- ((- (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3))))
by RLVECT_1:4
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) + (gf2 |^ (2 + 1)))
by VECTSP_1:17
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((((g2 * (gf2 |^ 2)) * (P `1_3)) * (Q `3_3)) + ((gf2 |^ 2) * gf2))
by EC_PF_1:24
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (((gf2 |^ 2) * ((g2 * (P `1_3)) * (Q `3_3))) + ((gf2 |^ 2) * gf2))
by Th11
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((gf2 |^ 2) * (((g2 * (P `1_3)) * (Q `3_3)) + gf2))
by VECTSP_1:def 7
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `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, GROUP_1:def 3
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((gf2 |^ 2) * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) + (((P `1_3) * (Q `3_3)) + ((P `1_3) * (Q `3_3)))))
by A1, Th20
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((gf2 |^ 2) * (((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) + ((P `1_3) * (Q `3_3))) + ((P `1_3) * (Q `3_3))))
by ALGSTR_1:7
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((gf2 |^ 2) * ((((Q `1_3) * (P `3_3)) + ((- ((P `1_3) * (Q `3_3))) + ((P `1_3) * (Q `3_3)))) + ((P `1_3) * (Q `3_3))))
by ALGSTR_1:7
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((gf2 |^ 2) * ((((Q `1_3) * (P `3_3)) + (0. (GF p))) + ((P `1_3) * (Q `3_3))))
by RLVECT_1:5
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((gf2 * gf2) * ((((Q `1_3) * (P `3_3)) + (0. (GF p))) + ((P `1_3) * (Q `3_3))))
by EC_PF_1:22
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((gf2 * (((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)))) * (((Q `1_3) * (P `3_3)) + ((P `1_3) * (Q `3_3))))
by A2, RLVECT_1:4
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (gf2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) * (((Q `1_3) * (P `3_3)) + ((P `1_3) * (Q `3_3)))))
by GROUP_1:def 3
.=
((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (gf2 * ((((Q `1_3) * (P `3_3)) |^ 2) - (((P `1_3) * (Q `3_3)) |^ 2)))
by Th15
.=
(((((gf2 |^ 3) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * gf2) * ((((Q `1_3) * (P `3_3)) |^ 2) - (((P `1_3) * (Q `3_3)) |^ 2))
by GROUP_1:def 3
.=
((((gf2 * (gf2 |^ 3)) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((((Q `1_3) * (P `3_3)) |^ 2) - (((P `1_3) * (Q `3_3)) |^ 2))
by Th11
.=
((((gf2 |^ (3 + 1)) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * ((((Q `1_3) * (P `3_3)) |^ 2) - (((P `1_3) * (Q `3_3)) |^ 2))
by EC_PF_1:24
.=
(((gf2 |^ 4) * ((P `1_3) * (Q `1_3))) * (P `3_3)) * ((((Q `1_3) * (P `3_3)) |^ 2) - (((P `1_3) * (Q `3_3)) |^ 2))
by GROUP_1:def 3
.=
(((gf2 |^ 4) * (P `3_3)) * ((P `1_3) * (Q `1_3))) * ((((Q `1_3) * (P `3_3)) |^ 2) - (((P `1_3) * (Q `3_3)) |^ 2))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((P `1_3) * (Q `1_3)) * ((((Q `1_3) * (P `3_3)) |^ 2) - (((P `1_3) * (Q `3_3)) |^ 2)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * (Q `1_3)) * (((Q `1_3) * (P `3_3)) |^ 2)) - (((P `1_3) * (Q `1_3)) * (((P `1_3) * (Q `3_3)) |^ 2)))
by VECTSP_1:11
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * (Q `1_3)) * (((Q `1_3) |^ 2) * ((P `3_3) |^ 2))) - (((P `1_3) * (Q `1_3)) * (((P `1_3) * (Q `3_3)) |^ 2)))
by BINOM:9
.=
((gf2 |^ 4) * (P `3_3)) * (((((P `1_3) * (Q `1_3)) * ((Q `1_3) |^ 2)) * ((P `3_3) |^ 2)) - (((P `1_3) * (Q `1_3)) * (((P `1_3) * (Q `3_3)) |^ 2)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 2)) * (Q `1_3)) - (((P `1_3) * (Q `1_3)) * (((P `1_3) * (Q `3_3)) |^ 2)))
by Th10
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * (((Q `1_3) |^ 2) * (Q `1_3))) - (((P `1_3) * (Q `1_3)) * (((P `1_3) * (Q `3_3)) |^ 2)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ (2 + 1))) - (((P `1_3) * (Q `1_3)) * (((P `1_3) * (Q `3_3)) |^ 2)))
by EC_PF_1:24
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - (((P `1_3) * (Q `1_3)) * (((P `1_3) |^ 2) * ((Q `3_3) |^ 2))))
by BINOM:9
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - ((((P `1_3) * (Q `1_3)) * ((P `1_3) |^ 2)) * ((Q `3_3) |^ 2)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - (((((Q `3_3) |^ 2) * (Q `1_3)) * ((P `1_3) |^ 2)) * (P `1_3)))
by Th10
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - ((((Q `3_3) |^ 2) * (Q `1_3)) * (((P `1_3) |^ 2) * (P `1_3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - (((Q `1_3) * ((Q `3_3) |^ 2)) * ((P `1_3) |^ (2 + 1))))
by EC_PF_1:24
.=
((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - (((Q `1_3) * ((Q `3_3) |^ 2)) * ((P `1_3) |^ 3)))
;
A10: (gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) * (R `3_3) =
(gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3))
by A3
.=
((gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) * ((gf2 |^ 3) * (P `3_3))) * (Q `3_3)
by GROUP_1:def 3
.=
((gf2 * ((gf2 |^ 3) * (P `3_3))) * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) * (Q `3_3)
by GROUP_1:def 3
.=
(((gf2 * (gf2 |^ 3)) * (P `3_3)) * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) * (Q `3_3)
by GROUP_1:def 3
.=
(((gf2 |^ (3 + 1)) * (P `3_3)) * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) * (Q `3_3)
by EC_PF_1:24
.=
((gf2 |^ 4) * (P `3_3)) * ((((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2))) * (Q `3_3))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) * (Q `3_3)) - ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)) * (Q `3_3)))
by VECTSP_1:13
.=
((gf2 |^ 4) * (P `3_3)) * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * ((Q `3_3) * (Q `3_3))) - ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)) * (Q `3_3)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * ((Q `3_3) |^ 2)) - ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)) * (Q `3_3)))
by EC_PF_1:22
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * (((P `2_3) |^ 2) * (P `3_3))) * ((Q `3_3) |^ 2)) - ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)) * (Q `3_3)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * (((P `2_3) |^ 2) * (P `3_3))) - ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)) * (Q `3_3)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * (((P `2_3) |^ 2) * (P `3_3))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3))))
by GROUP_1:def 3
;
0. (GF p) =
(((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)))
by Th35
.=
(((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))))
by ALGSTR_1:7
.=
((((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)))
by VECTSP_1:17
;
then A11:
(((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))
by VECTSP_1:19;
A12: 0. (GF p) =
(((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)))
by Th35
.=
(((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))))
by ALGSTR_1:7
.=
((((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)))
by VECTSP_1:17
;
thus (- (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_3)) =
(((gf2 |^ 3) * (P `3_3)) * (- (((P `1_3) * (Q `1_3)) * gf3))) + (((gf2 * (((((Q `1_3) * ((P `2_3) |^ 2)) * (P `3_3)) * (Q `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `2_3) |^ 2)))) * (R `3_3)) + (((((gf1 |^ 2) * (P `1_3)) * (Q `1_3)) * (P `3_3)) * (R `3_3)))
by A6, A8, VECTSP_1:def 7
.=
(((gf2 |^ 4) * (P `3_3)) * ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - (((Q `1_3) * ((Q `3_3) |^ 2)) * ((P `1_3) |^ 3)))) + (((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * (((P `2_3) |^ 2) * (P `3_3))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3)))))
by A9, A10, ALGSTR_1:7
.=
((gf2 |^ 4) * (P `3_3)) * (((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - (((Q `1_3) * ((Q `3_3) |^ 2)) * ((P `1_3) |^ 3))) + ((((Q `1_3) * ((Q `3_3) |^ 2)) * (((P `2_3) |^ 2) * (P `3_3))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3)))))
by VECTSP_1:def 7
.=
((gf2 |^ 4) * (P `3_3)) * ((((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) + (- (((Q `1_3) * ((Q `3_3) |^ 2)) * ((P `1_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * (((P `2_3) |^ 2) * (P `3_3)))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3))))
by ALGSTR_1:7
.=
((gf2 |^ 4) * (P `3_3)) * ((((((Q `1_3) * ((Q `3_3) |^ 2)) * (((P `2_3) |^ 2) * (P `3_3))) - (((Q `1_3) * ((Q `3_3) |^ 2)) * ((P `1_3) |^ 3))) + (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3))))
by ALGSTR_1:8
.=
((gf2 |^ 4) * (P `3_3)) * (((((Q `1_3) * ((Q `3_3) |^ 2)) * ((((P `2_3) |^ 2) * (P `3_3)) - ((P `1_3) |^ 3))) + (((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3))))
by VECTSP_1:11
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * ((((P `2_3) |^ 2) * (P `3_3)) - ((P `1_3) |^ 3))) + ((((P `1_3) * ((P `3_3) |^ 2)) * ((Q `1_3) |^ 3)) - (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `2_3) |^ 2) * (Q `3_3)))))
by ALGSTR_1:7
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * ((((P `2_3) |^ 2) * (P `3_3)) - ((P `1_3) |^ 3))) + (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `1_3) |^ 3) - (((Q `2_3) |^ 2) * (Q `3_3)))))
by VECTSP_1:11
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * ((((P `2_3) |^ 2) * (P `3_3)) - ((P `1_3) |^ 3))) - (- (((P `1_3) * ((P `3_3) |^ 2)) * (((Q `1_3) |^ 3) - (((Q `2_3) |^ 2) * (Q `3_3))))))
by RLVECT_1:17
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * ((((P `2_3) |^ 2) * (P `3_3)) - ((P `1_3) |^ 3))) - (((P `1_3) * ((P `3_3) |^ 2)) * (- (((Q `1_3) |^ 3) - (((Q `2_3) |^ 2) * (Q `3_3))))))
by VECTSP_1:8
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * ((((P `2_3) |^ 2) * (P `3_3)) - ((P `1_3) |^ 3))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((((Q `2_3) |^ 2) * (Q `3_3)) - ((Q `1_3) |^ 3))))
by VECTSP_1:17
.=
((gf2 |^ 4) * (P `3_3)) * ((((Q `1_3) * ((Q `3_3) |^ 2)) * ((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) + ((z `2) * ((P `3_3) |^ 3)))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)) + ((z `2) * ((Q `3_3) |^ 3)))))
by A11, A12, VECTSP_1:19
.=
((gf2 |^ 4) * (P `3_3)) * (((((Q `1_3) * ((Q `3_3) |^ 2)) * (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3)))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)) + ((z `2) * ((Q `3_3) |^ 3)))))
by VECTSP_1:def 7
.=
((gf2 |^ 4) * (P `3_3)) * (((((Q `1_3) * ((Q `3_3) |^ 2)) * (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3)))) - ((((P `1_3) * ((P `3_3) |^ 2)) * (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2))) + (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))))
by VECTSP_1:def 7
.=
((gf2 |^ 4) * (P `3_3)) * ((((((Q `1_3) * ((Q `3_3) |^ 2)) * (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3)))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2))))
by VECTSP_1:17
.=
((gf2 |^ 4) * (P `3_3)) * ((((((Q `1_3) * ((Q `3_3) |^ 2)) * (((z `1) * (P `1_3)) * ((P `3_3) |^ 2))) - (((P `1_3) * ((P `3_3) |^ 2)) * (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by Th7
.=
((gf2 |^ 4) * (P `3_3)) * ((((((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * (Q `1_3)) * ((Q `3_3) |^ 2)) - (((P `1_3) * ((P `3_3) |^ 2)) * (((z `1) * (Q `1_3)) * ((Q `3_3) |^ 2)))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * (Q `1_3)) * ((Q `3_3) |^ 2)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `1) * ((Q `1_3) * ((Q `3_3) |^ 2))))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * (Q `1_3)) * ((Q `3_3) |^ 2)) - ((((P `1_3) * ((P `3_3) |^ 2)) * (z `1)) * ((Q `1_3) * ((Q `3_3) |^ 2)))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * (Q `1_3)) * ((Q `3_3) |^ 2)) - ((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * ((Q `1_3) * ((Q `3_3) |^ 2)))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * (Q `1_3)) * ((Q `3_3) |^ 2)) - (((((z `1) * (P `1_3)) * ((P `3_3) |^ 2)) * (Q `1_3)) * ((Q `3_3) |^ 2))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((0. (GF p)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by RLVECT_1:5
.=
((gf2 |^ 4) * (P `3_3)) * ((- (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3)))) + (((Q `1_3) * ((Q `3_3) |^ 2)) * ((z `2) * ((P `3_3) |^ 3))))
by RLVECT_1:4
.=
((gf2 |^ 4) * (P `3_3)) * (((((Q `1_3) * ((Q `3_3) |^ 2)) * (z `2)) * ((P `3_3) |^ (2 + 1))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((((Q `1_3) * ((Q `3_3) |^ 2)) * (z `2)) * (((P `3_3) |^ 2) * (P `3_3))) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3))))
by EC_PF_1:24
.=
((gf2 |^ 4) * (P `3_3)) * ((((((Q `1_3) * ((Q `3_3) |^ 2)) * (z `2)) * ((P `3_3) |^ 2)) * (P `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * (Q `1_3)) * (P `3_3)) - (((P `1_3) * ((P `3_3) |^ 2)) * ((z `2) * ((Q `3_3) |^ 3))))
by Th10
.=
((gf2 |^ 4) * (P `3_3)) * (((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * (Q `1_3)) * (P `3_3)) - ((((P `1_3) * ((P `3_3) |^ 2)) * (z `2)) * ((Q `3_3) |^ (2 + 1))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * (Q `1_3)) * (P `3_3)) - ((((P `1_3) * ((P `3_3) |^ 2)) * (z `2)) * (((Q `3_3) |^ 2) * (Q `3_3))))
by EC_PF_1:24
.=
((gf2 |^ 4) * (P `3_3)) * (((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * (Q `1_3)) * (P `3_3)) - (((((P `1_3) * ((P `3_3) |^ 2)) * (z `2)) * ((Q `3_3) |^ 2)) * (Q `3_3)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * (Q `1_3)) * (P `3_3)) - ((((((Q `3_3) |^ 2) * ((P `3_3) |^ 2)) * (z `2)) * (P `1_3)) * (Q `3_3)))
by Th10
.=
((gf2 |^ 4) * (P `3_3)) * ((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * ((Q `1_3) * (P `3_3))) - ((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * (P `1_3)) * (Q `3_3)))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * ((((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * ((Q `1_3) * (P `3_3))) - (((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * ((P `1_3) * (Q `3_3))))
by GROUP_1:def 3
.=
((gf2 |^ 4) * (P `3_3)) * (((((P `3_3) |^ 2) * ((Q `3_3) |^ 2)) * (z `2)) * (((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))))
by VECTSP_1:11
.=
(((((gf2 |^ 4) * (P `3_3)) * ((Q `3_3) |^ 2)) * ((P `3_3) |^ 2)) * (z `2)) * gf2
by A2, Th11
.=
(((((gf2 |^ 4) * (P `3_3)) * ((Q `3_3) * (Q `3_3))) * ((P `3_3) |^ 2)) * (z `2)) * gf2
by EC_PF_1:22
.=
((((((gf2 |^ (3 + 1)) * (P `3_3)) * (Q `3_3)) * (Q `3_3)) * ((P `3_3) |^ 2)) * (z `2)) * gf2
by GROUP_1:def 3
.=
(((((((gf2 |^ 3) * gf2) * (P `3_3)) * (Q `3_3)) * (Q `3_3)) * ((P `3_3) |^ 2)) * (z `2)) * gf2
by EC_PF_1:24
.=
((((gf2 * (((gf2 |^ 3) * (P `3_3)) * (Q `3_3))) * (Q `3_3)) * ((P `3_3) |^ 2)) * (z `2)) * gf2
by Th11
.=
((((gf2 * (R `3_3)) * (Q `3_3)) * ((P `3_3) |^ 2)) * (z `2)) * gf2
by A3
.=
gf2 * (gf2 * ((((R `3_3) * (Q `3_3)) * ((P `3_3) |^ 2)) * (z `2)))
by Th12
.=
(gf2 * gf2) * ((((R `3_3) * (Q `3_3)) * ((P `3_3) |^ 2)) * (z `2))
by GROUP_1:def 3
.=
(gf2 |^ 2) * ((((R `3_3) * (Q `3_3)) * ((P `3_3) |^ 2)) * (z `2))
by EC_PF_1:22
.=
(gf2 |^ 2) * ((((z `2) * (Q `3_3)) * ((P `3_3) |^ 2)) * (R `3_3))
by Th10
.=
((((gf2 |^ 2) * (z `2)) * (Q `3_3)) * ((P `3_3) |^ 2)) * (R `3_3)
by Th11
.=
((((z `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3)
by GROUP_1:def 3
; verum