let p be Prime; :: thesis: 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 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1 = 0 & Q `2 = 1 & Q `3 = 0 )
let a, b be Element of (GF p); :: thesis: 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 = 0 holds
ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1 = 0 & Q `2 = 1 & Q `3 = 0 )
let P be Element of ProjCo (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3 = 0 implies ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1 = 0 & Q `2 = 1 & Q `3 = 0 ) )
assume AS: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & P in EC_SetProjCo (a,b,p) & P `3 = 0 ) ; :: thesis: ex Q being Element of ProjCo (GF p) st
( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1 = 0 & Q `2 = 1 & Q `3 = 0 )
ASX: P `3 = 0. (GF p) by AS, XLm2;
set d = (P `2) " ;
W1: ex X0 being Element of ProjCo (GF p) st
( P = X0 & (EC_WEqProjCo (a,b,p)) . X0 = 0. (GF p) ) by AS;
W2: (P `3) |^ 3 = (P `3) |^ (2 + 1)
.= ((P `3) |^ 2) * (P `3) by EX5
.= 0. (GF p) by ASX, VECTSP_1:12 ;
W3: (P `3) |^ 2 = (P `3) |^ (1 + 1)
.= ((P `3) |^ 1) * (P `3) by EX5
.= 0. (GF p) by ASX, VECTSP_1:12 ;
0. (GF p) = (((P `2) |^ 2) * (P `3)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) by W1, ECDefEQ
.= (0. (GF p)) - ((((P `1) |^ 3) + ((a * (P `1)) * ((P `3) |^ 2))) + (b * ((P `3) |^ 3))) by ASX, VECTSP_1:12
.= (0. (GF p)) - ((((P `1) |^ 3) + (0. (GF p))) + (b * ((P `3) |^ 3))) by W3, VECTSP_1:12
.= (0. (GF p)) - ((((P `1) |^ 3) + (0. (GF p))) + (0. (GF p))) by W2, VECTSP_1:12
.= (0. (GF p)) - (((P `1) |^ 3) + (0. (GF p))) by RLVECT_1:4
.= (0. (GF p)) - ((P `1) |^ 3) by RLVECT_1:4
.= - ((P `1) |^ 3) by RLVECT_1:14 ;
then W9: (P `1) |^ 3 = ((P `1) |^ 3) + (- ((P `1) |^ 3)) by RLVECT_1:4;
AS2: P `1 = 0. (GF p)

proof

assume AS21: P `1 <> 0. (GF p) ; :: thesis: contradiction
then (P `1) * (P `1) <> 0. (GF p) by VECTSP_1:12;
then ((P `1) |^ 1) * (P `1) <> 0. (GF p) by EXLm3;
then (P `1) |^ (1 + 1) <> 0. (GF p) by EX5;
then ((P `1) |^ 2) * (P `1) <> 0. (GF p) by AS21, VECTSP_1:12;
then (P `1) |^ (2 + 1) <> 0. (GF p) by EX5;
hence contradiction by W9, RLVECT_1:5; :: thesis: verum

end;

AS0: P `2 <> 0. (GF p)

proof

assume P `2 = 0. (GF p) ; :: thesis: contradiction
then P `2 = 0 by XLm2;
then [(P `1),(P `2),(P `3)] = [0,0,0] by AS, AS2, XLm2;
then P = [0,0,0] by MCART_1:44;
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 GFProjCo;
hence contradiction ; :: thesis: verum

end;

AS1: (P `2) " <> 0. (GF p)

proof

assume A1: (P `2) " = 0. (GF p) ; :: thesis: contradiction
A2: ((P `2) ") * (P `2) = 1_ (GF p) by AS0, VECTSP_1:def 10
.= 1 by XLm3 ;
((P `2) ") * (P `2) = 0. (GF p) by A1, VECTSP_1:12
.= 0 by XLm2 ;
hence contradiction by A2; :: thesis: verum

end;

reconsider Q = [(((P `2) ") * (P `1)),(((P `2) ") * (P `2)),(((P `2) ") * (P `3))] as Element of [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] ;
P1: ( Q `1 = ((P `2) ") * (P `1) & Q `2 = ((P `2) ") * (P `2) & Q `3 = ((P `2) ") * (P `3) ) by MCART_1:43;
then Q in EC_SetProjCo (a,b,p) by AS, AS1, LmEQV4;
then consider PP being Element of ProjCo (GF p) such that
P2: ( Q = PP & (EC_WEqProjCo (a,b,p)) . PP = 0. (GF p) ) ;
reconsider Q = Q as Element of ProjCo (GF p) by P2;
take Q ; :: thesis: ( Q in EC_SetProjCo (a,b,p) & Q _EQ_ P & Q `1 = 0 & Q `2 = 1 & Q `3 = 0 )
thus Q in EC_SetProjCo (a,b,p) by P1, AS, AS1, LmEQV4; :: thesis: ( Q _EQ_ P & Q `1 = 0 & Q `2 = 1 & Q `3 = 0 )
thus Q _EQ_ P by P1, AS1, DefEQV; :: thesis: ( Q `1 = 0 & Q `2 = 1 & Q `3 = 0 )
thus Q `1 = ((P `2) ") * (P `1) by MCART_1:43
.= 0. (GF p) by AS2, VECTSP_1:12
.= 0 by XLm2 ; :: thesis: ( Q `2 = 1 & Q `3 = 0 )
thus Q `2 = ((P `2) ") * (P `2) by MCART_1:43
.= 1_ (GF p) by AS0, VECTSP_1:def 10
.= 1 by XLm3 ; :: thesis: Q `3 = 0
thus Q `3 = ((P `2) ") * (P `3) by MCART_1:43
.= 0. (GF p) by ASX, VECTSP_1:12
.= 0 by XLm2 ; :: thesis: verum