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) holds
( P _EQ_ Q iff (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q )
let z be Element of EC_WParam p; :: thesis: for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds
( P _EQ_ Q iff (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q )
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P _EQ_ Q iff (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q )
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;
set CP = (compell_ProjCo (z,p)) . P;
consider CPP being Element of ProjCo (GF p) such that
A6: ( CPP = (compell_ProjCo (z,p)) . P & CPP in EC_SetProjCo ((z `1),(z `2),p) ) ;
A7: ( CPP `1_3 = ((compell_ProjCo (z,p)) . P) `1_3 & CPP `2_3 = ((compell_ProjCo (z,p)) . P) `2_3 & CPP `3_3 = ((compell_ProjCo (z,p)) . P) `3_3 ) by A6, ThECSet2;
set CQ = (compell_ProjCo (z,p)) . Q;
consider CQQ being Element of ProjCo (GF p) such that
A8: ( CQQ = (compell_ProjCo (z,p)) . Q & CQQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
A9: ( CQQ `1_3 = ((compell_ProjCo (z,p)) . Q) `1_3 & CQQ `2_3 = ((compell_ProjCo (z,p)) . Q) `2_3 & CQQ `3_3 = ((compell_ProjCo (z,p)) . Q) `3_3 ) by A8, ThECSet2;

hereby :: thesis: ( (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q implies P _EQ_ Q )

assume B1: P _EQ_ Q ; :: thesis: (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q
B2: rep_pt P = rep_pt Q by B1, ThRepPoint4;

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

suppose C1: P `3_3 = 0 ; :: thesis: (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q

PP `3_3 = 0 by A2, C1, ThECSet2;
then rep_pt QQ = [0,1,0] by A2, A4, B2, DefRepPoint;
then (rep_pt QQ) `3_3 = 0 by MCART_1:def 7;
then C2: Q `3_3 = 0 by A5, ThRepPoint2;
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),0] by C1, DefCompEll;
then C3: CPP `3_3 = 0 by A7, DefZ;
(compell_ProjCo (z,p)) . Q = [(Q `1_3),(- (Q `2_3)),0] by C2, DefCompEll;
then CQQ `3_3 = 0 by A9, DefZ;
then rep_pt ((compell_ProjCo (z,p)) . Q) = [0,1,0] by A8, DefRepPoint
.= rep_pt ((compell_ProjCo (z,p)) . P) by A6, C3, DefRepPoint ;
hence (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q by ThRepPoint4; :: thesis: verum

end;

suppose C1: P `3_3 <> 0 ; :: thesis: (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q

rep_pt QQ = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by A2, A3, A4, B2, C1, DefRepPoint;
then C2: (rep_pt QQ) `3_3 <> 0 by MCART_1:def 7;
(compell_ProjCo (z,p)) . (rep_pt P) = rep_pt ((compell_ProjCo (z,p)) . Q) by A5, B2, C2, ThRepPoint3, ThCOMPELL2;
then rep_pt ((compell_ProjCo (z,p)) . P) = rep_pt ((compell_ProjCo (z,p)) . Q) by C1, ThCOMPELL2;
hence (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q by ThRepPoint4; :: thesis: verum

end;

end;

end;

assume B1: (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q ; :: thesis: P _EQ_ Q

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

suppose C1: P `3_3 = 0 ; :: thesis: P _EQ_ Q

(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),0] by C1, DefCompEll;
then CPP `3_3 = 0 by A7, DefZ;
then C3: rep_pt CPP = [0,1,0] by DefRepPoint;
rep_pt CQQ = [0,1,0] by A6, A8, B1, C3, ThRepPoint4;
then (rep_pt CQQ) `3_3 = 0 by MCART_1:def 7;
then C4: ((compell_ProjCo (z,p)) . Q) `3_3 = 0 by A9, ThRepPoint2;
(compell_ProjCo (z,p)) . Q = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] by DefCompEll;
then Q `3_3 = 0 by C4, DefZ;
then C5: rep_pt QQ = [0,1,0] by A5, DefRepPoint;
rep_pt PP = [0,1,0] by A3, C1, DefRepPoint;
hence P _EQ_ Q by A2, A4, C5, ThRepPoint4; :: thesis: verum

end;

suppose C1: P `3_3 <> 0 ; :: thesis: P _EQ_ Q

(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),(P `3_3)] by DefCompEll;
then C2: CPP `3_3 <> 0 by A7, C1, DefZ;
set RP = rep_pt P;
reconsider RP = rep_pt P as Element of EC_SetProjCo ((z `1),(z `2),p) by ThRepPoint1;
set RQ = rep_pt Q;
reconsider RQ = rep_pt Q as Element of EC_SetProjCo ((z `1),(z `2),p) by ThRepPoint1;
C3: rep_pt ((compell_ProjCo (z,p)) . P) = rep_pt ((compell_ProjCo (z,p)) . Q) by B1, ThRepPoint4;
rep_pt CPP = [((CPP `1_3) * ((CPP `3_3) ")),((CPP `2_3) * ((CPP `3_3) ")),1] by C2, DefRepPoint;
then (rep_pt CQQ) `3_3 <> 0 by A6, A8, C3, MCART_1:def 7;
then C4: ((compell_ProjCo (z,p)) . Q) `3_3 <> 0 by A9, ThRepPoint3;
(compell_ProjCo (z,p)) . Q = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] by DefCompEll;
then C5: Q `3_3 <> 0 by C4, DefZ;
C6: rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . RP by C1, ThCOMPELL2;
rep_pt ((compell_ProjCo (z,p)) . Q) = (compell_ProjCo (z,p)) . RQ by C5, ThCOMPELL2;
then RP = RQ by C3, C6, ThCOMPELL3;
hence P _EQ_ Q by ThRepPoint4; :: thesis: verum

end;

end;