let p be Prime; :: thesis: for a, b being Element of (GF p)
for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (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] ) } holds
F1 misses F2
let a, b be Element of (GF p); :: thesis: for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (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] ) } holds
F1 misses F2
let F1, F2 be set ; :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (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 F1 misses F2 )
assume AS: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (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: F1 misses F2
assume F1 meets F2 ; :: thesis: contradiction
then F1 /\ F2 <> {} by XBOOLE_0:def 7;
then consider z being set such that
A501: z in F1 /\ F2 by XBOOLE_0:def 1;
A50: ( z in F1 & z in F2 ) by A501, XBOOLE_0:def 4;
consider P being Element of ProjCo (GF p) such that
A52: ( z = Class ((R_EllCur (a,b,p)),P) & P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) by AS, A50;
consider X1, Y1 being Element of (GF p) such that
A53: P = [X1,Y1,1] by A52;
A55: z = Class ((R_EllCur (a,b,p)),[0,1,0]) by AS, A50, TARSKI:def 1;
reconsider Q = [0,1,0] as Element of ProjCo (GF p) by LML;
A57: Q is Element of EC_SetProjCo (a,b,p) by ECZERO;
Q in Class ((R_EllCur (a,b,p)),P) by A52, A55, EQREL_1:23;
then [P,Q] in R_EllCur (a,b,p) by EQREL_1:18;
then P _EQ_ Q by LmDefREQ0, AS, A57, A52;
then consider a being Element of (GF p) such that
P08: ( a <> 0. (GF p) & Q `1 = a * (P `1) & Q `2 = a * (P `2) & Q `3 = a * (P `3) ) by DefEQV;
PP1: p > 1 by INT_2:def 4;
P09: 1. (GF p) = 1 by PP1, INT_3:14
.= P `3 by A53, MCART_1:43 ;
0. (GF p) = 0 by XLm2
.= a * (P `3) by P08, MCART_1:43
.= a by P09, VECTSP_1:def 8 ;
hence contradiction by P08; :: thesis: verum