let p be Prime; :: thesis: for a, b being Element of (GF p)
for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds
ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) )
let a, b be Element of (GF p); :: thesis: for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds
ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) )
let x be set ; :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) implies ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) ) ; :: thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
then consider y0 being Element of EC_SetProjCo (a,b,p) such that
A2: x = Class ((R_EllCur (a,b,p)),y0) by EQREL_1:36;
reconsider w = y0 as Element of ProjCo (GF p) ;
per cases ( w `3_3 = 0 or w `3_3 <> 0 ) ;
suppose w `3_3 = 0 ; :: thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
then consider y being Element of ProjCo (GF p) such that
A3: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `1_3 = 0 & y `2_3 = 1 & y `3_3 = 0 ) by A1, Th49;
[y,w] in R_EllCur (a,b,p) by A1, Th47, A3;
then x = Class ((R_EllCur (a,b,p)),y) by A2, A3, EQREL_1:35;
hence ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by A3, AA; :: thesis: verum
end;
suppose w `3_3 <> 0 ; :: thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
then consider y being Element of ProjCo (GF p) such that
A4: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `3_3 = 1 ) by A1, Th48;
set e = y `1_3 ;
set f = y `2_3 ;
A5: y = [(y `1_3),(y `2_3),1] by A4, AA;
[y,w] in R_EllCur (a,b,p) by A1, Th47, A4;
then x = Class ((R_EllCur (a,b,p)),y) by A2, A4, EQREL_1:35;
hence ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by A5, A4; :: thesis: verum
end;
end;