let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )
let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )
let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies ( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P ) )
assume A1: O = [0,1,0] ; :: thesis: ( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P )
(addell_ProjCo (z,p)) . (P,O) _EQ_ P
proof
per cases ( P _EQ_ O or not P _EQ_ O ) ;
suppose B1: P _EQ_ O ; :: thesis: (addell_ProjCo (z,p)) . (P,O) _EQ_ P
then (addell_ProjCo (z,p)) . (P,O) = O by A1, EC_PF_2:def 9;
hence (addell_ProjCo (z,p)) . (P,O) _EQ_ P by B1; :: thesis: verum
end;
end;
end;
hence ( (addell_ProjCo (z,p)) . (P,O) _EQ_ P & (addell_ProjCo (z,p)) . (O,P) _EQ_ P ) by A1, EC_PF_2:def 9; :: thesis: verum