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 A1: ( 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 object such that
A2: z in F1 /\ F2 by XBOOLE_0:def 1;
A3: ( z in F1 & z in F2 ) by A2, XBOOLE_0:def 4;
consider P being Element of ProjCo (GF p) such that
A4: ( 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 A1, A3;
consider X1, Y1 being Element of (GF p) such that
A5: P = [X1,Y1,1] by A4;
A6: z = Class ((R_EllCur (a,b,p)),[0,1,0]) by A1, A3, TARSKI:def 1;
reconsider Q = [0,1,0] as Element of ProjCo (GF p) by Lm5;
A7: Q is Element of EC_SetProjCo (a,b,p) by Th42;
Q in Class ((R_EllCur (a,b,p)),P) by A4, A6, EQREL_1:23;
then [P,Q] in R_EllCur (a,b,p) by EQREL_1:18;
then P _EQ_ Q by Th47, A1, A7, A4;
then consider a being Element of (GF p) such that
A8: ( a <> 0. (GF p) & Q `1_3 = a * (P `1_3) & Q `2_3 = a * (P `2_3) & Q `3_3 = a * (P `3_3) ) by Def10;
A9: p > 1 by INT_2:def 4;
A10: 1. (GF p) = 1 by A9, INT_3:14
.= P `3_3 by A5 ;
0. (GF p) = 0 by Th11
.= a * (P `3_3) by A8
.= a by A10 ;
hence contradiction by A8; :: thesis: verum