let p be Prime; 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); ( 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) )
; 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 ;
( 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 ( 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))
;
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;
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] ) }
;
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 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
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] )
;
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;
verum end; end; end;
hence
x in Class (R_EllCur (a,b,p))
;
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; verum