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_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); :: 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_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); :: thesis: ( 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 ) ; :: thesis: 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)

proof

assume A8: P `1_3 <> 0. (GF p) ; :: thesis: contradiction
then (P `1_3) * (P `1_3) <> 0. (GF p) by VECTSP_1:12;
then ((P `1_3) |^ 1) * (P `1_3) <> 0. (GF p) by Lm1;
then (P `1_3) |^ (1 + 1) <> 0. (GF p) by Th24;
then ((P `1_3) |^ 2) * (P `1_3) <> 0. (GF p) by A8, VECTSP_1:12;
then (P `1_3) |^ (2 + 1) <> 0. (GF p) by Th24;
hence contradiction by A6, RLVECT_1:5; :: thesis: verum

end;

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

proof

assume P `2_3 = 0. (GF p) ; :: thesis: 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 ; :: thesis: verum

end;

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

proof

assume A11: (P `2_3) " = 0. (GF p) ; :: thesis: contradiction
A12: ((P `2_3) ") * (P `2_3) = 1_ (GF p) by A9, VECTSP_1:def 10
.= 1 by Th12 ;
((P `2_3) ") * (P `2_3) = 0. (GF p) by A11
.= 0 by Th11 ;
hence contradiction by A12; :: thesis: verum

end;

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 ; :: thesis: ( 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; :: thesis: ( Q _EQ_ P & Q `1_3 = 0 & Q `2_3 = 1 & Q `3_3 = 0 )
thus Q _EQ_ P by A10; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: Q `3_3 = 0
thus Q `3_3 = ((P `2_3) ") * (P `3_3)
.= 0. (GF p) by A2
.= 0 by Th11 ; :: thesis: verum