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
(((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((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, 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
(((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((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, 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
(((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((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, 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
(((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((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 & 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 (((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((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
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))]
; (((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((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: (((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3)) =
((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((R `2_3) |^ 2)) * (R `3_3)
by GROUP_1:def 3
.=
((((gf2 |^ 2) * ((P `3_3) |^ 2)) * ((R `2_3) |^ 2)) * (Q `3_3)) * (R `3_3)
by GROUP_1:def 3
.=
((((gf2 * (P `3_3)) * (R `2_3)) |^ 2) * (Q `3_3)) * (R `3_3)
by Th13
.=
(((- ((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3)))) |^ 2) * (Q `3_3)) * (R `3_3)
by A1, A2, A3, Th54
.=
((((gf1 * (((R `1_3) * (P `3_3)) - ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3))) |^ 2) * (Q `3_3)) * (R `3_3)
by Th1
.=
(((((gf1 * ((R `1_3) * (P `3_3))) - (gf1 * ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3))) |^ 2) * (Q `3_3)) * (R `3_3)
by VECTSP_1:11
.=
((((((gf1 * (P `3_3)) * (R `1_3)) - (gf1 * ((P `1_3) * (R `3_3)))) + ((gf2 * (P `2_3)) * (R `3_3))) |^ 2) * (Q `3_3)) * (R `3_3)
by GROUP_1:def 3
.=
((((((gf1 * (P `3_3)) * (R `1_3)) - ((gf1 * (P `1_3)) * (R `3_3))) + ((gf2 * (P `2_3)) * (R `3_3))) |^ 2) * (Q `3_3)) * (R `3_3)
by GROUP_1:def 3
.=
((((((gf1 * (P `3_3)) * (R `1_3)) + ((gf2 * (P `2_3)) * (R `3_3))) - ((gf1 * (P `1_3)) * (R `3_3))) |^ 2) * (Q `3_3)) * (R `3_3)
by ALGSTR_1:8
.=
(((((gf1 * (P `3_3)) * (R `1_3)) + (((gf2 * (P `2_3)) * (R `3_3)) - ((gf1 * (P `1_3)) * (R `3_3)))) |^ 2) * (Q `3_3)) * (R `3_3)
by ALGSTR_1:7
.=
(((((gf1 * (P `3_3)) * (R `1_3)) + (((gf2 * (P `2_3)) - (gf1 * (P `1_3))) * (R `3_3))) |^ 2) * (Q `3_3)) * (R `3_3)
by VECTSP_1:13
.=
((((((gf1 * (P `3_3)) |^ 2) * ((R `1_3) |^ 2)) + ((((g2 * (gf1 * (P `3_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (R `1_3)) * (R `3_3))) + ((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2))) * (Q `3_3)) * (R `3_3)
by A1, Th27
.=
(((((gf1 * (P `3_3)) |^ 2) * ((R `1_3) |^ 2)) + ((((g2 * (gf1 * (P `3_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (R `1_3)) * (R `3_3))) + ((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2))) * ((Q `3_3) * (R `3_3))
by GROUP_1:def 3
.=
(((((gf1 * (P `3_3)) |^ 2) * ((R `1_3) |^ 2)) * ((Q `3_3) * (R `3_3))) + (((((g2 * (gf1 * (P `3_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (R `1_3)) * (R `3_3)) * ((Q `3_3) * (R `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by Th14
.=
(((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * ((Q `3_3) * (R `3_3))) + (((((g2 * (gf1 * (P `3_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (R `1_3)) * (R `3_3)) * ((Q `3_3) * (R `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by BINOM:9
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * (gf1 * (P `3_3))) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (R `1_3)) * (R `3_3)) * ((Q `3_3) * (R `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((g2 * gf1) * (P `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (R `1_3)) * (R `3_3)) * ((Q `3_3) * (R `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((g2 * gf1) * (((((P `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (R `1_3)) * (R `3_3)) * ((Q `3_3) * (R `3_3))))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by Th12
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((g2 * gf1) * (((((Q `3_3) * (R `3_3)) * (R `1_3)) * (R `3_3)) * ((P `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by Th10
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * ((Q `3_3) * (R `3_3))) * (R `1_3)) * (R `3_3)) * ((P `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by Th11
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * (R `1_3)) * (R `3_3)) * ((P `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * (((R `1_3) * (R `3_3)) * ((P `3_3) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3))))))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by Th11
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * (((gf2 * (P `2_3)) - (gf1 * (P `1_3))) * (((R `1_3) * (R `3_3)) * (P `3_3))))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (R `3_3)) * (P `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * ((Q `3_3) * (R `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + ((((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * ((R `3_3) |^ 2)) * (Q `3_3)) * (R `3_3))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + ((((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) |^ 2)) * (R `3_3))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (((R `3_3) |^ 2) * (R `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) |^ (2 + 1)))
by EC_PF_1:24
;
A5: - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) =
- ((((gf2 |^ 2) * ((P `3_3) * (P `3_3))) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2)))
by EC_PF_1:22
.=
- (((((gf2 |^ 2) * (P `3_3)) * (P `3_3)) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2)))
by GROUP_1:def 3
.=
- (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (P `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2)))
by GROUP_1:def 3
.=
- (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (P `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) * (R `3_3))))
by EC_PF_1:22
.=
- (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (P `3_3)) * ((((z `1) * (R `1_3)) * (R `3_3)) * (R `3_3)))
by GROUP_1:def 3
.=
- (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (P `3_3)) * ((((z `1) * (R `3_3)) * (R `1_3)) * (R `3_3)))
by GROUP_1:def 3
.=
- ((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * ((P `3_3) * ((((z `1) * (R `3_3)) * (R `1_3)) * (R `3_3))))
by GROUP_1:def 3
.=
- ((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * ((((P `3_3) * ((z `1) * (R `3_3))) * (R `1_3)) * (R `3_3)))
by Th11
.=
- ((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (((z `1) * (R `3_3)) * (((P `3_3) * (R `1_3)) * (R `3_3))))
by Th11
.=
- (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * ((z `1) * (R `3_3))) * (((P `3_3) * (R `1_3)) * (R `3_3)))
by GROUP_1:def 3
.=
- ((((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (z `1)) * (R `3_3)) * (((R `1_3) * (P `3_3)) * (R `3_3)))
by GROUP_1:def 3
.=
- (((gf2 |^ 2) * ((((P `3_3) * (Q `3_3)) * (z `1)) * (R `3_3))) * (((P `3_3) * (R `1_3)) * (R `3_3)))
by Th11
.=
- (((gf2 |^ 2) * ((((z `1) * (P `3_3)) * (Q `3_3)) * (R `3_3))) * (((P `3_3) * (R `1_3)) * (R `3_3)))
by GROUP_1:def 3
.=
- ((((((gf2 |^ 2) * (z `1)) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((P `3_3) * (R `1_3)) * (R `3_3)))
by Th11
.=
- ((((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))))) * (((P `3_3) * (R `1_3)) * (R `3_3)))
by A1, A2, A3, Th57
.=
- ((((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)))) * (((P `3_3) * (R `1_3)) * (R `3_3))) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((P `3_3) * (R `1_3)) * (R `3_3))))
by VECTSP_1:def 7
.=
- ((((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))))) * (((P `3_3) * (R `1_3)) * (R `3_3))) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((P `3_3) * (R `1_3)) * (R `3_3))))
by ALGSTR_1:7
.=
- ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_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))))) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3))))
by GROUP_1:def 3
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - (((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_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 VECTSP_1:17
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + (((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * ((((P `3_3) * (Q `1_3)) * (R `1_3)) + (((P `1_3) * (Q `3_3)) * (R `1_3)))))
by VECTSP_1:def 7
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + (((gf2 |^ 2) * (((P `3_3) * (R `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
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `1_3)))
by GROUP_1:def 3
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((((gf2 |^ 2) * (P `3_3)) * (R `1_3)) * (R `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `1_3)))
by Th12
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((gf2 |^ 2) * (P `3_3)) * (((R `1_3) * (R `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))))) * (R `1_3)))
by Th11
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((gf2 |^ 2) * (P `3_3)) * (((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (R `1_3)) * (R `3_3))) * (R `1_3)))
by GROUP_1:def 3
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `1_3)) * (R `3_3)) * (R `1_3)))
by Th11
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) * (R `3_3)) * (R `1_3))))
by Th11
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) * (R `1_3)) * (R `3_3))))
by GROUP_1:def 3
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (R `1_3)) * (R `3_3))) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by EC_PF_1:22
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((((gf2 |^ 2) * (P `3_3)) * (R `1_3)) * (R `3_3)) * (((P `1_3) * (Q `1_3)) * (R `3_3))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by Th11
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (P `3_3)) * (((R `1_3) * (R `3_3)) * (((P `1_3) * (Q `1_3)) * (R `3_3)))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by Th11
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (P `3_3)) * (((P `1_3) * (Q `1_3)) * ((R `3_3) * ((R `1_3) * (R `3_3))))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by GROUP_1:def 3
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (P `3_3)) * (((P `1_3) * (Q `1_3)) * ((R `1_3) * ((R `3_3) * (R `3_3))))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by GROUP_1:def 3
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (P `3_3)) * (((P `1_3) * (Q `1_3)) * ((R `1_3) * ((R `3_3) |^ 2)))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by EC_PF_1:22
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((gf2 |^ 2) * (P `3_3)) * ((((P `1_3) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by GROUP_1:def 3
.=
(- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - (((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3))))
by Th11
.=
((- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (P `3_3)) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (((R `1_3) |^ 2) * (R `3_3)))
by VECTSP_1:17
.=
((- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (P `3_3)) * (((R `1_3) |^ 2) * (R `3_3)))
by GROUP_1:def 3
.=
((- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * ((P `3_3) * (((R `1_3) |^ 2) * (R `3_3))))
by GROUP_1:def 3
.=
((- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - (((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * ((R `3_3) * (((R `1_3) |^ 2) * (P `3_3))))
by GROUP_1:def 3
.=
((- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by GROUP_1:def 3
;
A6: - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((z `2) * ((R `3_3) |^ 3))) =
- (((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (z `2)) * ((R `3_3) |^ (2 + 1)))
by GROUP_1:def 3
.=
- (((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (z `2)) * (((R `3_3) |^ 2) * (R `3_3)))
by EC_PF_1:24
.=
- ((((z `2) * (((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3))) * (R `3_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
- ((((((z `2) * (gf2 |^ 2)) * ((P `3_3) |^ 2)) * (Q `3_3)) * (R `3_3)) * ((R `3_3) |^ 2))
by Th12
.=
- (((- (((((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))) * ((R `3_3) |^ 2))
by A1, A2, A3, Th56
.=
(- ((- (((((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)))) * ((R `3_3) |^ 2)
by VECTSP_1:9
.=
((- (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_3))) + (((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3))) * ((R `3_3) |^ 2)
by VECTSP_1:33
.=
((- (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_3))) * ((R `3_3) |^ 2)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:def 7
.=
(- ((((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * (R `3_3)) * ((R `3_3) |^ 2))) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))
by VECTSP_1:9
.=
(- (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) * ((R `3_3) |^ 2)))) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))
by GROUP_1:def 3
.=
(- (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) |^ (2 + 1)))) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))
by EC_PF_1:24
;
A7: ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((z `2) * ((R `3_3) |^ 3))) =
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + ((((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) |^ 3)) + ((- (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) |^ 3))) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))))
by A4, A6, ALGSTR_1:7
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + (((((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) |^ 3)) - (((((gf2 * (P `2_3)) - (gf1 * (P `1_3))) |^ 2) * (Q `3_3)) * ((R `3_3) |^ 3))) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2)))
by ALGSTR_1:7
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + ((0. (GF p)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2)))
by VECTSP_1:19
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))
by RLVECT_1:4
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))
by ALGSTR_1:8
;
A8: (((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((z `2) * ((R `3_3) |^ 3)))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) =
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3))) + (((- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) - ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))))
by A5, A7, ALGSTR_1:7
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3))) + ((- (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + ((- ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))))))
by ALGSTR_1:7
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + (((((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3))) - (((((g2 * gf1) * (Q `3_3)) * (R `3_3)) * ((gf2 * (P `2_3)) - (gf1 * (P `1_3)))) * (((R `1_3) * (P `3_3)) * (R `3_3)))) + ((- ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))))
by ALGSTR_1:7
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((0. (GF p)) + ((- ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))))
by VECTSP_1:19
.=
((((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) + ((- ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))))
by RLVECT_1:4
.=
(((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + (((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2)) + ((- ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2)) - ((((((gf2 |^ 2) * (P `3_3)) * (P `1_3)) * (Q `1_3)) * (R `1_3)) * ((R `3_3) |^ 2))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))))
by ALGSTR_1:7
.=
(((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) + ((0. (GF p)) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))))
by VECTSP_1:19
.=
(((((gf1 |^ 2) * ((P `3_3) |^ 2)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by RLVECT_1:14
.=
(((((gf1 |^ 2) * ((P `3_3) * (P `3_3))) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by EC_PF_1:22
.=
((((((gf1 |^ 2) * (P `3_3)) * (P `3_3)) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3)) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by GROUP_1:def 3
.=
(((gf1 |^ 2) * (P `3_3)) * ((((P `3_3) * ((R `1_3) |^ 2)) * (Q `3_3)) * (R `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by Th11
.=
(((gf1 |^ 2) * (P `3_3)) * (((P `3_3) * ((R `1_3) |^ 2)) * ((Q `3_3) * (R `3_3)))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by GROUP_1:def 3
.=
((((gf1 |^ 2) * (P `3_3)) * ((Q `3_3) * (R `3_3))) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by GROUP_1:def 3
;
thus (((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((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)))) =
((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3))))
by VECTSP_1:11
.=
((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3))) - ((((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((R `1_3) |^ 3)) + ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2)))) + ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((z `2) * ((R `3_3) |^ 3))))
by Th14
.=
((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3))) - (((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((R `1_3) |^ 3)) + (((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((z `2) * ((R `3_3) |^ 3)))))
by ALGSTR_1:7
.=
(((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3))) - (((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((z `2) * ((R `3_3) |^ 3))))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((R `1_3) |^ 3))
by VECTSP_1:17
.=
((((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((R `2_3) |^ 2) * (R `3_3))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((z `2) * ((R `3_3) |^ 3)))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * (((z `1) * (R `1_3)) * ((R `3_3) |^ 2)))) - ((((gf2 |^ 2) * ((P `3_3) |^ 2)) * (Q `3_3)) * ((R `1_3) |^ 3))
by VECTSP_1:17
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - ((((gf2 |^ 2) * ((P `3_3) * (P `3_3))) * (Q `3_3)) * ((R `1_3) |^ 3))
by A8, EC_PF_1:22
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - (((((gf2 |^ 2) * (P `3_3)) * (P `3_3)) * (Q `3_3)) * ((R `1_3) |^ 3))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (P `3_3)) * ((R `1_3) |^ 3))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * ((R `1_3) |^ (2 + 1))) * (P `3_3))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (((R `1_3) |^ 2) * (R `1_3))) * (P `3_3))
by EC_PF_1:24
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - ((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * ((((R `1_3) |^ 2) * (R `1_3)) * (P `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - ((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * ((R `1_3) * (((R `1_3) |^ 2) * (P `3_3))))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3))) - ((((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)) * (((R `1_3) |^ 2) * (P `3_3)))) - (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `1_3)) * (((R `1_3) |^ 2) * (P `3_3)))
by GROUP_1:def 3
.=
((((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) - (((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3))) - ((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `1_3))) * (((R `1_3) |^ 2) * (P `3_3))
by Th14
.=
(((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) - (((((gf2 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `1_3)) + (((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)))) * (((R `1_3) |^ 2) * (P `3_3))
by VECTSP_1:17
.=
(((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) - (((gf2 |^ 2) * (((P `3_3) * (Q `3_3)) * (R `1_3))) + (((gf2 |^ 2) * (((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3)))) * (R `3_3)))) * (((R `1_3) |^ 2) * (P `3_3))
by Th11
.=
(((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) - (((gf2 |^ 2) * (((P `3_3) * (Q `3_3)) * (R `1_3))) + ((gf2 |^ 2) * ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (R `3_3))))) * (((R `1_3) |^ 2) * (P `3_3))
by GROUP_1:def 3
.=
(((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3)) - ((gf2 |^ 2) * ((((P `3_3) * (Q `3_3)) * (R `1_3)) + ((((P `3_3) * (Q `1_3)) + ((P `1_3) * (Q `3_3))) * (R `3_3))))) * (((R `1_3) |^ 2) * (P `3_3))
by VECTSP_1:def 7
.=
((- ((gf2 |^ 2) * ((((P `3_3) * (Q `3_3)) * (R `1_3)) + ((((P `3_3) * (Q `1_3)) * (R `3_3)) + (((P `1_3) * (Q `3_3)) * (R `3_3)))))) + ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3))) * (((R `1_3) |^ 2) * (P `3_3))
by VECTSP_1:def 7
.=
((- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((((gf1 |^ 2) * (P `3_3)) * (Q `3_3)) * (R `3_3))) * (((R `1_3) |^ 2) * (P `3_3))
by ALGSTR_1:7
.=
((- ((gf2 |^ 2) * (((((P `3_3) * (Q `3_3)) * (R `1_3)) + (((P `3_3) * (Q `1_3)) * (R `3_3))) + (((P `1_3) * (Q `3_3)) * (R `3_3))))) + ((gf1 |^ 2) * (((P `3_3) * (Q `3_3)) * (R `3_3)))) * (((R `1_3) |^ 2) * (P `3_3))
by Th11
.=
(0. (GF p)) * (((R `1_3) |^ 2) * (P `3_3))
by A1, A2, A3, Th55
.=
0. (GF p)
; verum