let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P _EQ_ Q holds
(P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) st P _EQ_ Q holds
(P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P _EQ_ Q implies (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3) )
set a = z `1 ;
set b = z `2 ;
consider PP being Element of ProjCo (GF p) such that
A1: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;
A2: ( PP `1_3 = P `1_3 & PP `2_3 = P `2_3 & PP `3_3 = P `3_3 ) by A1, Th32;
consider QQ being Element of ProjCo (GF p) such that
A3: ( QQ = Q & QQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
A4: ( QQ `1_3 = Q `1_3 & QQ `2_3 = Q `2_3 & QQ `3_3 = Q `3_3 ) by A3, Th32;
assume A5: P _EQ_ Q ; :: thesis: (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
A6: rep_pt PP = rep_pt QQ by A1, A3, A5, Th39;
per cases ( PP `3_3 = 0 or PP `3_3 <> 0 ) ;
suppose A7: PP `3_3 = 0 ; :: thesis: (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
then P `3_3 = 0. (GF p) by A2, EC_PF_1:11;
then A8: (Q `2_3) * (P `3_3) = 0. (GF p) ;
rep_pt QQ = [0,1,0] by A6, A7, Def7;
then (rep_pt QQ) `3_3 = 0 ;
then Q `3_3 = 0 by A4, Th37
.= 0. (GF p) by EC_PF_1:11 ;
hence (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3) by A8; :: thesis: verum
end;
suppose A9: PP `3_3 <> 0 ; :: thesis: (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
then A10: PP `3_3 <> 0. (GF p) by EC_PF_1:11;
A11: rep_pt QQ = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by A6, A9, Def7;
then A12: (rep_pt QQ) `2_3 = (PP `2_3) * ((PP `3_3) ") ;
A13: (rep_pt QQ) `3_3 <> 0 by A11;
then QQ `3_3 <> 0 by Th38;
then A14: QQ `3_3 <> 0. (GF p) by EC_PF_1:11;
rep_pt QQ = [((QQ `1_3) * ((QQ `3_3) ")),((QQ `2_3) * ((QQ `3_3) ")),1] by A13, Th38;
then (PP `2_3) * ((PP `3_3) ") = (QQ `2_3) * ((QQ `3_3) ") by A12;
hence (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3) by A2, A4, A10, A14, Th3; :: thesis: verum
end;
end;