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) st P `3_3 <> 0 holds
rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P)
let z be Element of EC_WParam p; :: thesis: for P being Element of EC_SetProjCo ((z `1),(z `2),p) st P `3_3 <> 0 holds
rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P)
let P be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( P `3_3 <> 0 implies rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P) )
assume A1: P `3_3 <> 0 ; :: thesis: rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P)
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) ) ;
set CP = (compell_ProjCo (z,p)) . P;
(compell_ProjCo (z,p)) . P = [(P `1_3),(- (P `2_3)),(P `3_3)] by Def8;
then A3: ( ((compell_ProjCo (z,p)) . P) `1_3 = P `1_3 & ((compell_ProjCo (z,p)) . P) `2_3 = - (P `2_3) & ((compell_ProjCo (z,p)) . P) `3_3 = P `3_3 ) by Def3, Def4, Def5;
set RP = rep_pt PP;
reconsider RP = rep_pt PP as Element of EC_SetProjCo ((z `1),(z `2),p) by A2, Th36;
PP `3_3 <> 0 by A1, A2, Th32;
then RP = [((PP `1_3) * ((PP `3_3) ")),((PP `2_3) * ((PP `3_3) ")),1] by Def7;
then ( RP `1_3 = (PP `1_3) * ((PP `3_3) ") & RP `2_3 = (PP `2_3) * ((PP `3_3) ") & RP `3_3 = 1 ) by Def3, Def4, Def5;
then ( RP `1_3 = (P `1_3) * ((PP `3_3) ") & RP `2_3 = (P `2_3) * ((PP `3_3) ") & RP `3_3 = 1 ) by A2, Th32;
then A4: ( RP `1_3 = (P `1_3) * ((P `3_3) ") & RP `2_3 = (P `2_3) * ((P `3_3) ") & RP `3_3 = 1 ) by A2, Th32;
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) ) ;
set RCP = rep_pt CPP;
reconsider RCP = rep_pt CPP as Element of EC_SetProjCo ((z `1),(z `2),p) by A5, Th36;
CPP `3_3 <> 0 by A1, A3, A5, Th32;
then RCP = [((CPP `1_3) * ((CPP `3_3) ")),((CPP `2_3) * ((CPP `3_3) ")),1] by Def7;
then ( RCP `1_3 = (CPP `1_3) * ((CPP `3_3) ") & RCP `2_3 = (CPP `2_3) * ((CPP `3_3) ") & RCP `3_3 = 1 ) by Def3, Def4, Def5;
then ( RCP `1_3 = (((compell_ProjCo (z,p)) . P) `1_3) * ((CPP `3_3) ") & RCP `2_3 = (((compell_ProjCo (z,p)) . P) `2_3) * ((CPP `3_3) ") & RCP `3_3 = 1 ) by A5, Th32;
then ( RCP `1_3 = (((compell_ProjCo (z,p)) . P) `1_3) * ((((compell_ProjCo (z,p)) . P) `3_3) ") & RCP `2_3 = (((compell_ProjCo (z,p)) . P) `2_3) * ((((compell_ProjCo (z,p)) . P) `3_3) ") & RCP `3_3 = 1 ) by A5, Th32;
then A6: RCP = [((P `1_3) * ((P `3_3) ")),((- (P `2_3)) * ((P `3_3) ")),1] by A3, Th31;
set CRP = (compell_ProjCo (z,p)) . RP;
(compell_ProjCo (z,p)) . RP = [((P `1_3) * ((P `3_3) ")),(- ((P `2_3) * ((P `3_3) "))),1] by A4, Def8;
hence rep_pt ((compell_ProjCo (z,p)) . P) = (compell_ProjCo (z,p)) . (rep_pt P) by A2, A5, A6, VECTSP_1:9; :: thesis: verum