let p be Prime; :: thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
let a, b be Element of (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
assume A1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; :: thesis: Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
set A = Class (R_EllCur (a,b,p));
set B = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ;
reconsider d0 = [0,1,0] as Element of EC_SetProjCo (a,b,p) by Th42;
for x being object holds
( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
proof
let x be object ; :: thesis: ( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
hereby :: thesis: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies x in Class (R_EllCur (a,b,p)) )
assume x in Class (R_EllCur (a,b,p)) ; :: thesis: x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
then ( ex y being Element of ProjCo (GF p) st
( y in EC_SetProjCo (a,b,p) & y = [0,1,0] & x = Class ((R_EllCur (a,b,p)),y) ) or ex y being Element of ProjCo (GF p) ex e, f being Element of (GF p) st
( y in EC_SetProjCo (a,b,p) & y = [e,f,1] & x = Class ((R_EllCur (a,b,p)),y) ) ) by A1, Th50;
then ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by TARSKI:def 1;
hence x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by XBOOLE_0:def 3; :: thesis: verum
end;
assume x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; :: thesis: x in Class (R_EllCur (a,b,p))
then A2: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by XBOOLE_0:def 3;
now :: thesis: x in Class (R_EllCur (a,b,p))
per cases ( x = Class ((R_EllCur (a,b,p)),[0,1,0]) or ex y being Element of ProjCo (GF p) st
( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ) by A2, TARSKI:def 1;
suppose A3: x = Class ((R_EllCur (a,b,p)),[0,1,0]) ; :: thesis: x in Class (R_EllCur (a,b,p))
EqClass ((R_EllCur (a,b,p)),d0) is Element of Class (R_EllCur (a,b,p)) ;
hence x in Class (R_EllCur (a,b,p)) by A3; :: thesis: verum
end;
suppose ex y being Element of ProjCo (GF p) st
( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ; :: thesis: x in Class (R_EllCur (a,b,p))
then consider y being Element of ProjCo (GF p) such that
A4: ( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ;
reconsider y = y as Element of EC_SetProjCo (a,b,p) by A4;
EqClass ((R_EllCur (a,b,p)),y) is Element of Class (R_EllCur (a,b,p)) ;
hence x in Class (R_EllCur (a,b,p)) by A4; :: thesis: verum
end;
end;
end;
hence x in Class (R_EllCur (a,b,p)) ; :: thesis: verum
end;
hence Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by TARSKI:2; :: thesis: verum