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
A2: ( PP = P & PP in EC_SetProjCo ((z `1),(z `2),p) ) ;
A3: ( PP `1_3 = P `1_3 & PP `2_3 = P `2_3 & PP `3_3 = P `3_3 ) by A2, ThECSet2;
consider QQ being Element of ProjCo (GF p) such that
A4: ( QQ = Q & QQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
A5: ( QQ `1_3 = Q `1_3 & QQ `2_3 = Q `2_3 & QQ `3_3 = Q `3_3 ) by A4, ThECSet2;
assume B1: P _EQ_ Q ; :: thesis: (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)
B2: rep_pt PP = rep_pt QQ by A2, A4, B1, ThRepPoint4;

per cases ( PP `3_3 = 0 or PP `3_3 <> 0 ) ;

suppose C1: 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 A3, EC_PF_1:11;
then C2: (Q `2_3) * (P `3_3) = 0. (GF p) by VECTSP_1:6;
rep_pt QQ = [0,1,0] by B2, C1, DefRepPoint;
then (rep_pt QQ) `3_3 = 0 by MCART_1:def 7;
then Q `3_3 = 0 by A5, ThRepPoint2
.= 0. (GF p) by EC_PF_1:11 ;
hence (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3) by C2, VECTSP_1:6; :: thesis: verum

end;

suppose C0: PP `3_3 <> 0 ; :: thesis: (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3)

then C1: PP `3_3 <> 0. (GF p) by EC_PF_1:11;
C3: rep_pt QQ = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by B2, C0, DefRepPoint;
then C4: (rep_pt QQ) `2_3 = (PP `2_3) * ((PP `3_3) ") by MCART_1:def 6;
C5: (rep_pt QQ) `3_3 <> 0 by C3, MCART_1:def 7;
then QQ `3_3 <> 0 by ThRepPoint3;
then C6: 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 C5, ThRepPoint3;
then (PP `2_3) * ((PP `3_3) ") = (QQ `2_3) * ((QQ `3_3) ") by C4, MCART_1:def 6;
hence (P `2_3) * (Q `3_3) = (Q `2_3) * (P `3_3) by A3, A5, C1, C6, ThGF12; :: thesis: verum

end;

end;