let p be Prime; for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
let a, b be Element of (GF p); for P being Element of ProjCo (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
let P be Element of ProjCo (GF p); ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 implies ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 ) )
assume A1:
( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3_3 = 0 )
; ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
A2:
P `3_3 = 0. (GF p)
by A1;
set d = (P `2_3) " ;
A3:
ex X0 being Element of ProjCo (GF p) st
( P = X0 & (EC_WEqProjCo (a,b,p)) . X0 = 0. (GF p) )
by A1;
A4: (P `3_3) |^ 3 =
(P `3_3) |^ (2 + 1)
.=
((P `3_3) |^ 2) * (P `3_3)
by Th24
.=
0. (GF p)
by A2
;
A5: (P `3_3) |^ 2 =
(P `3_3) |^ (1 + 1)
.=
((P `3_3) |^ 1) * (P `3_3)
by Th24
.=
0. (GF p)
by A2
;
0. (GF 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 A3, Def8
.=
(0. (GF p)) - ((((P `1_3) |^ 3) + ((a * (P `1_3)) * ((P `3_3) |^ 2))) + (b * ((P `3_3) |^ 3)))
by A2
.=
(0. (GF p)) - ((((P `1_3) |^ 3) + (0. (GF p))) + (b * ((P `3_3) |^ 3)))
by A5
.=
(0. (GF p)) - ((((P `1_3) |^ 3) + (0. (GF p))) + (0. (GF p)))
by A4
.=
(0. (GF p)) - (((P `1_3) |^ 3) + (0. (GF p)))
by RLVECT_1:4
.=
(0. (GF p)) - ((P `1_3) |^ 3)
by RLVECT_1:4
.=
- ((P `1_3) |^ 3)
by RLVECT_1:14
;
then A6:
(P `1_3) |^ 3 = ((P `1_3) |^ 3) + (- ((P `1_3) |^ 3))
by RLVECT_1:4;
A7:
P `1_3 = 0. (GF p)
A9:
P `2_3 <> 0. (GF p)
proof
assume
P `2_3 = 0. (GF p)
;
contradiction
then
P `2_3 = 0
by Th11;
then
[(P `1_3),(P `2_3),(P `3_3)] = [0,0,0]
by A1, A7;
then
P = [0,0,0]
by AA;
then
P in {[0,0,0]}
by TARSKI:def 1;
then
not
P 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
not
P in ProjCo (GF p)
by Th40;
hence
contradiction
;
verum
end;
A10:
(P `2_3) " <> 0. (GF p)
reconsider Q = [(((P `2_3) ") * (P `1_3)),(((P `2_3) ") * (P `2_3)),(((P `2_3) ") * (P `3_3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
A13:
( Q `1_3 = ((P `2_3) ") * (P `1_3) & Q `2_3 = ((P `2_3) ") * (P `2_3) & Q `3_3 = ((P `2_3) ") * (P `3_3) )
;
then
Q in EC_SetProjCo (a,b,p)
by A1, A10, Th45;
then consider PP being Element of ProjCo (GF p) such that
A14:
( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) )
;
reconsider Q = Q as Element of ProjCo (GF p) by A14;
take
Q
; ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
thus
Q in EC_SetProjCo (a,b,p)
by A13, A1, A10, Th45; ( Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
thus
Q _EQ_ P
by A10; ( Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
thus Q `1_3 =
((P `2_3) ") * (P `1_3)
.=
0. (GF p)
by A7
.=
0
by Th11
; ( Q `2_3 = 1 & Q `3_3 = 0 )
thus Q `2_3 =
((P `2_3) ") * (P `2_3)
.=
1_ (GF p)
by A9, VECTSP_1:def 10
.=
1
by Th12
; Q `3_3 = 0
thus Q `3_3 =
((P `2_3) ") * (P `3_3)
.=
0. (GF p)
by A2
.=
0
by Th11
; verum