let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds [(P `1_3),(- (P `2_3)),(P `3_3)] is Element of EC_SetProjCo ((z `1),(z `2),p)
let z be Element of EC_WParam p; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) holds [(P `1_3),(- (P `2_3)),(P `3_3)] is Element of EC_SetProjCo ((z `1),(z `2),p)
let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: [(P `1_3),(- (P `2_3)),(P `3_3)] is Element of EC_SetProjCo ((z `1),(z `2),p)
set a = z `1 ;
set b = z `2 ;
set R = [(P `1_3),(- (P `2_3)),(P `3_3)];
P in ProjCo (GF p) ;
then P in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by EC_PF_1:def 6;
then not P in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by XBOOLE_0:def 5;
then P <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] by TARSKI:def 1;
then ( not P `1_3 = 0. (GF p) or not P `2_3 = 0. (GF p) or not P `3_3 = 0. (GF p) ) by Th31;
then ( not P `1_3 = 0. (GF p) or not - (P `2_3) = 0. (GF p) or not P `3_3 = 0. (GF p) ) by VECTSP_2:3;
then [(P `1_3),(- (P `2_3)),(P `3_3)] <> [(0. (GF p)),(0. (GF p)),(0. (GF p))] by XTUPLE_0:3;
then not [(P `1_3),(- (P `2_3)),(P `3_3)] in {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by TARSKI:def 1;
then [(P `1_3),(- (P `2_3)),(P `3_3)] in [: the carrier of (GF p), the carrier of (GF p), the carrier of (GF p):] \ {[(0. (GF p)),(0. (GF p)),(0. (GF p))]} by XBOOLE_0:def 5;
then reconsider R = [(P `1_3),(- (P `2_3)),(P `3_3)] as Element of ProjCo (GF p) by EC_PF_1:def 6;
A1: (R `2_3) |^ 2 = (P `2_3) |^ 2 by Th1;
(((R `2_3) |^ 2) * (R `3_3)) - ((((R `1_3) |^ 3) + (((z `1) * (R `1_3)) * ((R `3_3) |^ 2))) + ((z `2) * ((R `3_3) |^ 3))) = 0. (GF p) by A1, Th35;
then (EC_WEqProjCo ((z `1),(z `2),p)) . R = 0. (GF p) by EC_PF_1:def 8;
then R is_on_curve EC_WEqProjCo ((z `1),(z `2),p) ;
hence [(P `1_3),(- (P `2_3)),(P `3_3)] is Element of EC_SetProjCo ((z `1),(z `2),p) by Th34; :: thesis: verum