let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
(compell_ProjCo (z,p)) . O _EQ_ O
let z be Element of EC_WParam p; :: thesis: for O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
(compell_ProjCo (z,p)) . O _EQ_ O
let O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies (compell_ProjCo (z,p)) . O _EQ_ O )
assume A1: O = [0,1,0] ; :: thesis: (compell_ProjCo (z,p)) . O _EQ_ O
set a = z `1 ;
set b = z `2 ;
A2: ( O `1_3 = 0 & O `2_3 = 1 & O `3_3 = 0 ) by A1, Def3, Def4, Def5;
consider OO being Element of ProjCo (GF p) such that
A3: ( OO = O & OO in EC_SetProjCo ((z `1),(z `2),p) ) ;
A4: ( OO `1_3 = 0 & OO `2_3 = 1 & OO `3_3 = 0 ) by A2, A3, Th32;
set CO = (compell_ProjCo (z,p)) . O;
consider COO being Element of ProjCo (GF p) such that
A5: ( COO = (compell_ProjCo (z,p)) . O & COO in EC_SetProjCo ((z `1),(z `2),p) ) ;
A6: ( COO `1_3 = ((compell_ProjCo (z,p)) . O) `1_3 & COO `2_3 = ((compell_ProjCo (z,p)) . O) `2_3 & COO `3_3 = ((compell_ProjCo (z,p)) . O) `3_3 ) by A5, Th32;
(compell_ProjCo (z,p)) . O = [(O `1_3),(- (O `2_3)),(O `3_3)] by Def8;
then COO `3_3 = 0 by A2, A6, Def5;
then A7: rep_pt ((compell_ProjCo (z,p)) . O) = [0,1,0] by A5, Def7;
rep_pt O = [0,1,0] by A3, A4, Def7;
hence (compell_ProjCo (z,p)) . O _EQ_ O by A7, Th39; :: thesis: verum