let p be Prime; for a, b being Element of (GF p)
for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]
for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds
Q in EC_SetProjCo (a,b,p)
let a, b be Element of (GF p); for P, Q being Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]
for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds
Q in EC_SetProjCo (a,b,p)
let P, Q be Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):]; for d being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) holds
Q in EC_SetProjCo (a,b,p)
let d be Element of (GF p); ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) implies Q in EC_SetProjCo (a,b,p) )
assume A1:
( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) )
; Q in EC_SetProjCo (a,b,p)
set DX = [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):];
consider PP being Element of ProjCo (GF p) such that
A2:
( P = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) )
by A1;
A3:
(EC_WEqProjCo (a,b,p)) . P = (((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))
by Def8;
A4: (EC_WEqProjCo (a,b,p)) . Q =
(((d * (P `2_3)) |^ 2) * (d * (P `3_3))) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by A1, Def8
.=
(((d |^ 2) * ((P `2_3) |^ 2)) * (d * (P `3_3))) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by BINOM:9
.=
((((d |^ 2) * ((P `2_3) |^ 2)) * d) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by GROUP_1:def 3
.=
((((d |^ 2) * d) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by GROUP_1:def 3
.=
(((d |^ (2 + 1)) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d * (P `1_3)) |^ 3) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by Th24
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (d * (P `1_3))) * ((d * (P `3_3)) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by BINOM:9
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (d * (P `1_3))) * ((d |^ 2) * ((P `3_3) |^ 2)))) + (b * ((d * (P `3_3)) |^ 3)))
by BINOM:9
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((a * (d * (P `1_3))) * (d |^ 2)) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by GROUP_1:def 3
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * ((d * (P `1_3)) * (d |^ 2))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by GROUP_1:def 3
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * (((d |^ 2) * d) * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by GROUP_1:def 3
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((a * ((d |^ (2 + 1)) * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by Th24
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d * (P `3_3)) |^ 3)))
by GROUP_1:def 3
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (b * ((d |^ 3) * ((P `3_3) |^ 3))))
by BINOM:9
.=
(((d |^ 3) * ((P `2_3) |^ 2)) * (P `3_3)) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (((d |^ 3) * b) * ((P `3_3) |^ 3)))
by GROUP_1:def 3
.=
((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + (((d |^ 3) * (a * (P `1_3))) * ((P `3_3) |^ 2))) + (((d |^ 3) * b) * ((P `3_3) |^ 3)))
by GROUP_1:def 3
.=
((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((d |^ 3) * ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + (((d |^ 3) * b) * ((P `3_3) |^ 3)))
by GROUP_1:def 3
.=
((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((((d |^ 3) * ((P `1_3) |^ 3)) + ((d |^ 3) * ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + ((d |^ 3) * (b * ((P `3_3) |^ 3))))
by GROUP_1:def 3
.=
((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - (((d |^ 3) * (((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2)))) + ((d |^ 3) * (b * ((P `3_3) |^ 3))))
by VECTSP_1:def 7
.=
((d |^ 3) * (((P `2_3) |^ 2) * (P `3_3))) - ((d |^ 3) * ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))))
by VECTSP_1:def 7
.=
(d |^ 3) * ((((P `2_3) |^ 2) * (P `3_3)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3))))
by VECTSP_1:11
.=
0. (GF p)
by A2, A3
;
PP in ProjCo (GF p)
;
then
PP in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]}
by Th40;
then
not P in {[0,0,0]}
by A2, XBOOLE_0:def 5;
then
( P `1_3 <> 0 or P `2_3 <> 0 or P `3_3 <> 0 )
by TARSKI:def 1;
then
( P `1_3 <> 0. (GF p) or P `2_3 <> 0. (GF p) or P `3_3 <> 0. (GF p) )
by Th11;
then
( d * (P `1_3) <> 0. (GF p) or d * (P `2_3) <> 0. (GF p) or d * (P `3_3) <> 0. (GF p) )
by A1, VECTSP_1:12;
then
( Q `1_3 <> 0 or Q `2_3 <> 0 or Q `3_3 <> 0 )
by A1;
then
[(Q `1_3),(Q `2_3),(Q `3_3)] <> [0,0,0]
by XTUPLE_0:3;
then
not Q in {[0,0,0]}
by TARSKI:def 1;
then
Q in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[0,0,0]}
by XBOOLE_0:def 5;
then
Q in ProjCo (GF p)
by Th40;
hence
Q in EC_SetProjCo (a,b,p)
by A4; verum