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
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;
set CP = (compell_ProjCo (z,p)) . P;
consider CPP being Element of ProjCo (GF p) such that
A5: ( CPP = (compell_ProjCo (z,p)) . P & CPP in EC_SetProjCo ((z `1),(z `2),p) ) ;
A6: ( 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 A5, Th32;
set CQ = (compell_ProjCo (z,p)) . Q;
consider CQQ being Element of ProjCo (GF p) such that
A7: ( CQQ = (compell_ProjCo (z,p)) . Q & CQQ in EC_SetProjCo ((z `1),(z `2),p) ) ;
A8: ( 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 A7, Th32;
hereby :: thesis: ( (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q implies P _EQ_ Q )
assume A9: P _EQ_ Q ; :: thesis: (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q
A10: rep_pt P = rep_pt Q by A9, Th39;
per cases ( P `3_3 = 0 or P `3_3 <> 0 ) ;
suppose A11: P `3_3 = 0 ; :: thesis: (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q
PP `3_3 = 0 by A1, A11, Th32;
then rep_pt QQ = [0,1,0] by A1, A3, A10, Def7;
then (rep_pt QQ) `3_3 = 0 ;
then A12: Q `3_3 = 0 by A4, Th37;
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),0] by A11, Def8;
then A13: CPP `3_3 = 0 by A6, Def5;
(compell_ProjCo (z,p)) . Q = [(Q `1_3),(- (Q `2_3)),0] by A12, Def8;
then CQQ `3_3 = 0 by A8, Def5;
then rep_pt ((compell_ProjCo (z,p)) . Q) = [0,1,0] by A7, Def7
.= rep_pt ((compell_ProjCo (z,p)) . P) by A5, A13, Def7 ;
hence (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q by Th39; :: thesis: verum
end;
suppose A14: 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 A1, A2, A3, A10, A14, Def7;
then A15: (rep_pt QQ) `3_3 <> 0 ;
(compell_ProjCo (z,p)) . (rep_pt P) = rep_pt ((compell_ProjCo (z,p)) . Q) by A4, A10, A15, Th38, Th42;
then rep_pt ((compell_ProjCo (z,p)) . P) = rep_pt ((compell_ProjCo (z,p)) . Q) by A14, Th42;
hence (compell_ProjCo (z,p)) . P _EQ_ (compell_ProjCo (z,p)) . Q by Th39; :: thesis: verum
end;
end;
end;
assume A16: (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 A17: P `3_3 = 0 ; :: thesis: P _EQ_ Q
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),0] by A17, Def8;
then CPP `3_3 = 0 by A6, Def5;
then A18: rep_pt CPP = [0,1,0] by Def7;
rep_pt CQQ = [0,1,0] by A5, A7, A16, A18, Th39;
then (rep_pt CQQ) `3_3 = 0 ;
then A19: ((compell_ProjCo (z,p)) . Q) `3_3 = 0 by A8, Th37;
(compell_ProjCo (z,p)) . Q = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] by Def8;
then Q `3_3 = 0 by A19, Def5;
then A20: rep_pt QQ = [0,1,0] by A4, Def7;
rep_pt PP = [0,1,0] by A2, A17, Def7;
hence P _EQ_ Q by A1, A3, A20, Th39; :: thesis: verum
end;
suppose A21: P `3_3 <> 0 ; :: thesis: P _EQ_ Q
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),(P `3_3)] by Def8;
then A22: CPP `3_3 <> 0 by A6, A21, Def5;
set RP = rep_pt P;
reconsider RP = rep_pt P as Element of EC_SetProjCo ((z `1),(z `2),p) by Th36;
set RQ = rep_pt Q;
reconsider RQ = rep_pt Q as Element of EC_SetProjCo ((z `1),(z `2),p) by Th36;
A23: rep_pt ((compell_ProjCo (z,p)) . P) = rep_pt ((compell_ProjCo (z,p)) . Q) by A16, Th39;
rep_pt CPP = [((CPP `1_3) * ((CPP `3_3) ")),((CPP `2_3) * ((CPP `3_3) ")),1] by A22, Def7;
then (rep_pt CQQ) `3_3 <> 0 by A5, A7, A23;
then A24: ((compell_ProjCo (z,p)) . Q) `3_3 <> 0 by A8, Th38;
(compell_ProjCo (z,p)) . Q = [(Q `1_3),(- (Q `2_3)),(Q `3_3)] by Def8;
then A25: Q `3_3 <> 0 by A24, Def5;
A26: rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . RP by A21, Th42;
rep_pt ((compell_ProjCo (z,p)) . Q) = (compell_ProjCo (z,p)) . RQ by A25, Th42;
then RP = RQ by A23, A26, Th43;
hence P _EQ_ Q by Th39; :: thesis: verum
end;
end;