let p be 5 _or_greater Prime; 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; 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); ( 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
; 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; verum