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 (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((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 (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))
reconsider O = [0,1,0] as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_1:42;
per cases ( P _EQ_ O or ( not P _EQ_ O & Q _EQ_ O ) or ( not P _EQ_ O & not Q _EQ_ O ) ) ;
suppose A1: P _EQ_ O ; :: thesis: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))
then A2: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) = (compell_ProjCo (z,p)) . Q by EC_PF_2:def 9;
(compell_ProjCo (z,p)) . P _EQ_ O by A1, ThCompellO;
hence (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q)) by A2, EC_PF_2:def 9; :: thesis: verum
end;
suppose A1: ( not P _EQ_ O & Q _EQ_ O ) ; :: thesis: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))
then A2: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) = (compell_ProjCo (z,p)) . P by EC_PF_2:def 9;
A3: not (compell_ProjCo (z,p)) . P _EQ_ O by A1, ThCompellO;
(compell_ProjCo (z,p)) . Q _EQ_ O by A1, ThCompellO;
hence (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q)) by A2, A3, EC_PF_2:def 9; :: thesis: verum
end;
suppose A1: ( not P _EQ_ O & not Q _EQ_ O ) ; :: thesis: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))
reconsider rP = rep_pt P, rQ = rep_pt Q as Element of EC_SetProjCo ((z `1),(z `2),p) by EC_PF_2:36;
(rep_pt P) `3_3 = 1 by A1, ThRepPoint7;
then A3: rP `3_3 = 1 by EC_PF_2:32;
(rep_pt Q) `3_3 = 1 by A1, ThRepPoint7;
then rQ `3_3 = 1 by EC_PF_2:32;
then A5: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (rP,rQ)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . rP),((compell_ProjCo (z,p)) . rQ)) by A3, LmCompAddCom;
( rP _EQ_ P & rQ _EQ_ Q ) by EC_PF_2:36;
then (addell_ProjCo (z,p)) . (rP,rQ) _EQ_ (addell_ProjCo (z,p)) . (P,Q) by ThAdd3;
then (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (rP,rQ)) _EQ_ (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) by EC_PF_2:46;
then A6: (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . rP),((compell_ProjCo (z,p)) . rQ)) by A5, EC_PF_1:44;
P `3_3 <> 0 by A1, ThEQO;
then A7: (compell_ProjCo (z,p)) . rP = rep_pt ((compell_ProjCo (z,p)) . P) by EC_PF_2:42;
Q `3_3 <> 0 by A1, ThEQO;
then A8: (compell_ProjCo (z,p)) . rQ = rep_pt ((compell_ProjCo (z,p)) . Q) by EC_PF_2:42;
A9: rep_pt ((compell_ProjCo (z,p)) . P) _EQ_ (compell_ProjCo (z,p)) . P by EC_PF_2:36;
rep_pt ((compell_ProjCo (z,p)) . Q) _EQ_ (compell_ProjCo (z,p)) . Q by EC_PF_2:36;
then (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . rP),((compell_ProjCo (z,p)) . rQ)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q)) by A7, A8, A9, ThAdd3;
hence (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q)) by A6, EC_PF_1:44; :: thesis: verum
end;
end;