ec_pf_3.miz



    begin

    reserve p for 5 _or_greater Prime;

    reserve z for Element of ( EC_WParam p);

    theorem :: EC_PF_3:1

    

     ThRepPoint5: for p be Prime, a,b be Element of ( GF p), P be Element of ( ProjCo ( GF p)) st (P = [ 0 , 1, 0 ] or (P `3_3 ) = 1) holds ( rep_pt P) = P

    proof

      let p be Prime, a,b be Element of ( GF p), P be Element of ( ProjCo ( GF p));

      

       A1: P = [ 0 , 1, 0 ] implies ( rep_pt P) = P

      proof

        assume

         B1: P = [ 0 , 1, 0 ];

        then (P `3_3 ) = 0 by MCART_1:def 7;

        hence ( rep_pt P) = P by B1, EC_PF_2:def 7;

      end;

      (P `3_3 ) = 1 implies ( rep_pt P) = P

      proof

        assume

         B1: (P `3_3 ) = 1;

        then ((P `3_3 ) " ) = ( 1. ( GF p)) by EC_PF_2: 2;

        

        hence ( rep_pt P) = [((P `1_3 ) * ( 1. ( GF p))), ((P `2_3 ) * ( 1. ( GF p))), 1] by B1, EC_PF_2:def 7

        .= P by B1, RECDEF_2: 3;

      end;

      hence thesis by A1;

    end;

    theorem :: EC_PF_3:2

    

     ThEQO: for p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st O = [ 0 , 1, 0 ] holds ((P `3_3 ) = 0 iff P _EQ_ O)

    proof

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A2: O = [ 0 , 1, 0 ];

      set a = (z `1 );

      set b = (z `2 );

      consider PP be Element of ( ProjCo ( GF p)) such that

       A3: PP = P & PP in ( EC_SetProjCo (a,b,p));

      hereby

        assume (P `3_3 ) = 0 ;

        then (PP `3_3 ) = 0 by A3, EC_PF_2: 32;

        then

         A5: ( rep_pt P) = [ 0 , 1, 0 ] by A3, EC_PF_2:def 7;

        ( rep_pt O) = [ 0 , 1, 0 ] by A2, ThRepPoint5;

        hence P _EQ_ O by A5, EC_PF_2: 39;

      end;

      assume P _EQ_ O;

      

      then ( rep_pt P) = ( rep_pt O) by EC_PF_2: 39

      .= O by A2, ThRepPoint5;

      then (( rep_pt PP) `3_3 ) = 0 by A2, A3, MCART_1:def 7;

      then (PP `3_3 ) = 0 by EC_PF_2: 37;

      hence thesis by A3, EC_PF_2: 32;

    end;

    theorem :: EC_PF_3:3

    

     ThEQCOMP4: for p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) holds ((P `3_3 ) = 0 implies P _EQ_ (( compell_ProjCo (z,p)) . P))

    proof

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      set a = (z `1 );

      set b = (z `2 );

      set O = [ 0 , 1, 0 ];

      reconsider O as Element of ( EC_SetProjCo (a,b,p)) by EC_PF_1: 42;

      assume

       A2: (P `3_3 ) = 0 ;

      

       A3: (( compell_ProjCo (z,p)) . O) _EQ_ O by EC_PF_2: 40;

      

       A4: P _EQ_ O by A2, ThEQO;

      then (( compell_ProjCo (z,p)) . P) _EQ_ (( compell_ProjCo (z,p)) . O) by EC_PF_2: 46;

      then (( compell_ProjCo (z,p)) . P) _EQ_ O by A3, EC_PF_1: 44;

      hence thesis by A4, EC_PF_1: 44;

    end;

    theorem :: EC_PF_3:4

    

     ThAddCompProjCo: for P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st O = [ 0 , 1, 0 ] holds (( addell_ProjCo (z,p)) . (P,(( compell_ProjCo (z,p)) . P))) _EQ_ O

    proof

      set a = (z `1 );

      set b = (z `2 );

      let P,O be Element of ( EC_SetProjCo (a,b,p)) such that

       A1: O = [ 0 , 1, 0 ];

      set Q = (( compell_ProjCo (z,p)) . P);

      reconsider Q as Element of ( EC_SetProjCo (a,b,p));

      consider OO be Element of ( ProjCo ( GF p)) such that

       A3: OO = O & OO in ( EC_SetProjCo (a,b,p));

      per cases ;

        suppose

         B1: (P `3_3 ) = 0 ;

        then

         B2: P _EQ_ O by A1, ThEQO;

        P _EQ_ Q by B1, ThEQCOMP4;

        then Q _EQ_ O by B2, EC_PF_1: 44;

        hence thesis by A1, B2, EC_PF_2:def 9;

      end;

        suppose

         B1: (P `3_3 ) <> 0 ;

        then

         B2: not P _EQ_ O by A1, ThEQO;

        then

         B3: not Q _EQ_ (( compell_ProjCo (z,p)) . O) by EC_PF_2: 46;

        (( compell_ProjCo (z,p)) . O) _EQ_ O by A1, EC_PF_2: 40;

        then

         B4: not Q _EQ_ O by B3, EC_PF_1: 44;

        per cases ;

          suppose

           C1: P _EQ_ Q;

          then

           C2: (P `2_3 ) = 0 by B1, EC_PF_2: 44;

          reconsider g2 = (2 mod p) as Element of ( GF p) by EC_PF_1: 14;

          reconsider g3 = (3 mod p) as Element of ( GF p) by EC_PF_1: 14;

          reconsider g4 = (4 mod p) as Element of ( GF p) by EC_PF_1: 14;

          reconsider g8 = (8 mod p) as Element of ( GF p) by EC_PF_1: 14;

          set gf1 = ((a * ((P `3_3 ) |^ 2)) + (g3 * ((P `1_3 ) |^ 2)));

          set gf2 = ((P `2_3 ) * (P `3_3 ));

          set gf3 = (((P `1_3 ) * (P `2_3 )) * gf2);

          set gf4 = ((gf1 |^ 2) - (g8 * gf3));

          reconsider gf1, gf2, gf3, gf4 as Element of ( GF p);

          set R = (( addell_ProjCo (z,p)) . (P,Q));

          

           C7: R = [((g2 * gf4) * gf2), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), (g8 * (gf2 |^ 3))] by A1, B2, B4, C1, EC_PF_2:def 9;

          reconsider R as Element of ( EC_SetProjCo (a,b,p));

          

           C12: gf1 <> 0 by B1, C2, EC_PF_2: 53;

          

           C13: gf1 <> ( 0. ( GF p)) by B1, C2, EC_PF_2: 53;

          gf4 = (gf1 |^ 2) by C2, VECTSP_1: 18;

          then gf4 <> 0 by C12, EC_PF_1: 25;

          then

           C14: gf4 <> ( 0. ( GF p)) by EC_PF_1: 11;

          (R `2_3 ) = ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))) by C7, EC_PF_2:def 4

          .= ((gf1 * ((g4 * ( 0. ( GF p))) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 * gf2))) by C2, EC_PF_1: 22

          .= ((gf1 * ( - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (( 0. ( GF p)) * ( 0. ( GF p))))) by C2, VECTSP_1: 18

          .= (gf1 * ( - gf4)) by VECTSP_1: 18

          .= ( - (gf1 * gf4)) by VECTSP_1: 8;

          then ( - (R `2_3 )) = (gf1 * gf4) by RLVECT_1: 17;

          then

           C15: ( - (R `2_3 )) <> ( 0. ( GF p)) by C13, C14, VECTSP_1: 12;

          

           C17: (gf2 |^ 3) = ( 0. ( GF p)) by C2, EC_PF_2: 5;

          set d = (R `2_3 );

          reconsider d as Element of ( GF p);

          

           C19: (OO `1_3 ) = 0 & (OO `2_3 ) = 1 & (OO `3_3 ) = 0 by A1, A3, MCART_1: 64;

          

           C20: (d * (OO `1_3 )) = (R `1_3 ) by C2, C7, C19, EC_PF_2:def 3;

          

           C21: (d * (OO `3_3 )) = (R `3_3 ) by C7, C17, C19, EC_PF_2:def 5;

          

           C22: (d * (OO `2_3 )) = (d * ( 1. ( GF p))) by C19

          .= (R `2_3 );

          consider RR be Element of ( ProjCo ( GF p)) such that

           C23: RR = R & RR in ( EC_SetProjCo (a,b,p));

          (RR `1_3 ) = (d * (OO `1_3 )) & (RR `2_3 ) = (d * (OO `2_3 )) & (RR `3_3 ) = (d * (OO `3_3 )) by C20, C21, C22, C23, EC_PF_2: 32;

          hence thesis by A3, C15, C23, EC_PF_1:def 10, VECTSP_2: 3;

        end;

          suppose

           C1: not P _EQ_ Q;

          reconsider g2 = (2 mod p) as Element of ( GF p) by EC_PF_1: 14;

          set gf1 = (((Q `2_3 ) * (P `3_3 )) - ((P `2_3 ) * (Q `3_3 )));

          set gf2 = (((Q `1_3 ) * (P `3_3 )) - ((P `1_3 ) * (Q `3_3 )));

          set gf3 = (((((gf1 |^ 2) * (P `3_3 )) * (Q `3_3 )) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3 )) * (Q `3_3 )));

          reconsider gf1, gf2, gf3 as Element of ( GF p);

          set R = (( addell_ProjCo (z,p)) . (P,Q));

          

           C3: R = [(gf2 * gf3), ((gf1 * ((((gf2 |^ 2) * (P `1_3 )) * (Q `3_3 )) - gf3)) - (((gf2 |^ 3) * (P `2_3 )) * (Q `3_3 ))), (((gf2 |^ 3) * (P `3_3 )) * (Q `3_3 ))] by A1, B2, B4, C1, EC_PF_2:def 9;

          Q = [(P `1_3 ), ( - (P `2_3 )), (P `3_3 )] by EC_PF_2:def 8;

          then

           C4: (Q `3_3 ) <> 0 by B1, EC_PF_2:def 5;

          then ((P `1_3 ) * (Q `3_3 )) = ((Q `1_3 ) * (P `3_3 )) by B1, EC_PF_2: 50;

          then

           C5: gf2 = ( 0. ( GF p)) by VECTSP_1: 19;

          then

           C6: (gf2 |^ 2) = ( 0. ( GF p)) & (gf2 |^ 3) = ( 0. ( GF p)) by EC_PF_2: 5;

          

           C7: gf1 <> ( 0. ( GF p)) by C1, EC_PF_2: 52, VECTSP_1: 19;

          then

           C8: (gf1 |^ 2) <> 0 by EC_PF_1: 25;

          

           C9: gf3 = ((((gf1 |^ 2) * (P `3_3 )) * (Q `3_3 )) - (( 0. ( GF p)) + (((g2 * ( 0. ( GF p))) * (P `1_3 )) * (Q `3_3 )))) by C6, VECTSP_1: 17

          .= ((((gf1 |^ 2) * (P `3_3 )) * (Q `3_3 )) - ( 0. ( GF p))) by ALGSTR_1: 7

          .= (((gf1 |^ 2) * (P `3_3 )) * (Q `3_3 )) by VECTSP_1: 18

          .= ((gf1 |^ 2) * ((P `3_3 ) * (Q `3_3 ))) by GROUP_1:def 3;

          ((P `3_3 ) * (Q `3_3 )) <> 0 by B1, C4, EC_PF_1: 20;

          then gf3 <> 0 by C8, C9, EC_PF_1: 20;

          then (gf1 * gf3) <> 0 by C7, EC_PF_1: 20;

          then (gf1 * gf3) <> ( 0. ( GF p)) by EC_PF_1: 11;

          then (gf1 * gf3) <> ( - ( 0. ( GF p))) by RLVECT_1: 12;

          then

           C10: ( - (gf1 * gf3)) <> 0 by EC_PF_2: 6;

          ((gf1 * ((((gf2 |^ 2) * (P `1_3 )) * (Q `3_3 )) - gf3)) - (((gf2 |^ 3) * (P `2_3 )) * (Q `3_3 ))) = (gf1 * (( 0. ( GF p)) - gf3)) by C6, VECTSP_1: 18

          .= (gf1 * ( - gf3)) by VECTSP_1: 18

          .= ( - (gf1 * gf3)) by VECTSP_1: 8;

          then

           C11: (R `2_3 ) <> 0 by C3, C10, EC_PF_2:def 4;

          

           C13: (R `3_3 ) = (((gf2 |^ 3) * (P `3_3 )) * (Q `3_3 )) by C3, EC_PF_2:def 5

          .= ((gf2 |^ 3) * ((P `3_3 ) * (Q `3_3 ))) by GROUP_1:def 3;

          set d = (R `2_3 );

          reconsider d as Element of ( GF p);

          

           C15: (OO `1_3 ) = 0 & (OO `2_3 ) = 1 & (OO `3_3 ) = 0 by A1, A3, MCART_1: 64;

          

           C16: (d * (OO `1_3 )) = (R `1_3 ) by C3, C5, C15, EC_PF_2:def 3;

          

           C18: (d * (OO `2_3 )) = (d * ( 1. ( GF p))) by C15

          .= (R `2_3 );

          consider RR be Element of ( ProjCo ( GF p)) such that

           C19: RR = R & RR in ( EC_SetProjCo (a,b,p));

          (RR `1_3 ) = (R `1_3 ) & (RR `2_3 ) = (R `2_3 ) & (RR `3_3 ) = (R `3_3 ) by C19, EC_PF_2: 32;

          hence thesis by A3, C6, C11, C13, C15, C16, C18, C19, EC_PF_1:def 10;

        end;

      end;

    end;

    definition

      let p be 5 _or_greater Prime;

      let z be Element of ( EC_WParam p);

      :: EC_PF_3:def1

      func EC_SetAffCo (z,p) -> non empty Subset of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) equals { P where P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) : (P `3_3 ) = 1 or P = [ 0 , 1, 0 ] };

      correctness

      proof

        set a = (z `1 );

        set b = (z `2 );

         A1:

        now

          let x be object;

          assume x in { P where P be Element of ( EC_SetProjCo (a,b,p)) : (P `3_3 ) = 1 or P = [ 0 , 1, 0 ] };

          then ex P be Element of ( EC_SetProjCo (a,b,p)) st x = P & ((P `3_3 ) = 1 or P = [ 0 , 1, 0 ]);

          hence x in ( EC_SetProjCo (a,b,p));

        end;

        reconsider O = [ 0 , 1, 0 ] as Element of ( EC_SetProjCo (a,b,p)) by EC_PF_1: 42;

        O in { P where P be Element of ( EC_SetProjCo (a,b,p)) : (P `3_3 ) = 1 or P = [ 0 , 1, 0 ] };

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: EC_PF_3:5

    

     ThAffCoZero: [ 0 , 1, 0 ] is Element of ( EC_SetAffCo (z,p))

    proof

       [ 0 , 1, 0 ] is Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) by EC_PF_1: 42;

      then [ 0 , 1, 0 ] in { P where P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) : (P `3_3 ) = 1 or P = [ 0 , 1, 0 ] };

      hence thesis;

    end;

    theorem :: EC_PF_3:6

    

     ThAffCo: for p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) holds ( rep_pt P) is Element of ( EC_SetAffCo (z,p))

    proof

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      set a = (z `1 );

      set b = (z `2 );

      consider PP be Element of ( ProjCo ( GF p)) such that

       A2: PP = P & PP in ( EC_SetProjCo (a,b,p));

      consider Q be Element of ( ProjCo ( GF p)) such that

       A3: Q = ( rep_pt P);

      reconsider Q as Element of ( EC_SetProjCo (a,b,p)) by A3, EC_PF_2: 36;

      per cases ;

        suppose (PP `3_3 ) = 0 ;

        then

         B1: Q = [ 0 , 1, 0 ] by A2, A3, EC_PF_2:def 7;

        Q in { QQ where QQ be Element of ( EC_SetProjCo (a,b,p)) : (QQ `3_3 ) = 1 or QQ = [ 0 , 1, 0 ] } by B1;

        hence thesis by A3;

      end;

        suppose (PP `3_3 ) <> 0 ;

        then ( rep_pt PP) = [((PP `1_3 ) * ((PP `3_3 ) " )), ((PP `2_3 ) * ((PP `3_3 ) " )), 1] by EC_PF_2:def 7;

        then

         B1: (Q `3_3 ) = 1 by A2, A3, EC_PF_2:def 5;

        Q in { QQ where QQ be Element of ( EC_SetProjCo (a,b,p)) : (QQ `3_3 ) = 1 or QQ = [ 0 , 1, 0 ] } by B1;

        hence thesis by A3;

      end;

    end;

    theorem :: EC_PF_3:7

    

     ThRepPoint6: for p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st P in ( EC_SetAffCo (z,p)) holds ( rep_pt P) = P

    proof

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      assume P in ( EC_SetAffCo (z,p));

      then

       X1: ex PP be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st P = PP & ((PP `3_3 ) = 1 or PP = [ 0 , 1, 0 ]);

      reconsider PP = P as Element of ( ProjCo ( GF p));

      PP = [ 0 , 1, 0 ] or (PP `3_3 ) = 1 by X1, EC_PF_2: 32;

      hence thesis by ThRepPoint5;

    end;

    theorem :: EC_PF_3:8

    

     ThRepPoint7: for P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st O = [ 0 , 1, 0 ] & not P _EQ_ O holds (( rep_pt P) `3_3 ) = 1

    proof

      let P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: O = [ 0 , 1, 0 ] & not P _EQ_ O;

      reconsider PP = P as Element of ( ProjCo ( GF p));

      (P `3_3 ) <> 0 by A1, ThEQO;

      then (PP `3_3 ) <> 0 by EC_PF_2: 32;

      then ( rep_pt PP) = [((PP `1_3 ) * ((PP `3_3 ) " )), ((PP `2_3 ) * ((PP `3_3 ) " )), 1] by EC_PF_2:def 7;

      hence thesis by MCART_1:def 7;

    end;

    theorem :: EC_PF_3:9

    for P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st O = [ 0 , 1, 0 ] & ( rep_pt P) _EQ_ O holds ( rep_pt P) = O & P _EQ_ O

    proof

      let P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: O = [ 0 , 1, 0 ] & ( rep_pt P) _EQ_ O;

      reconsider rP = ( rep_pt P) as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) by EC_PF_2: 36;

      (rP `3_3 ) = 0 by A1, ThEQO;

      then (( rep_pt P) `3_3 ) = 0 by EC_PF_2: 32;

      hence ( rep_pt P) = O by A1, EC_PF_2: 37;

      then ( rep_pt P) = ( rep_pt O) by A1, ThRepPoint5;

      hence thesis by EC_PF_2: 39;

    end;

    theorem :: EC_PF_3:10

    

     LmRepPoint9: for P be Element of ( ProjCo ( GF p)) holds ( rep_pt ( rep_pt P)) = ( rep_pt P)

    proof

      let P be Element of ( ProjCo ( GF p));

      set rP = ( rep_pt P);

      per cases ;

        suppose

         A1: (P `3_3 ) = 0 ;

        then ( rep_pt P) = [ 0 , 1, 0 ] by EC_PF_2:def 7;

        then (rP `3_3 ) = 0 by MCART_1:def 7;

        

        hence ( rep_pt ( rep_pt P)) = [ 0 , 1, 0 ] by EC_PF_2:def 7

        .= ( rep_pt P) by A1, EC_PF_2:def 7;

      end;

        suppose (P `3_3 ) <> 0 ;

        then ( rep_pt P) = [((P `1_3 ) * ((P `3_3 ) " )), ((P `2_3 ) * ((P `3_3 ) " )), 1] by EC_PF_2:def 7;

        then (rP `3_3 ) = 1 by MCART_1:def 7;

        hence thesis by ThRepPoint5;

      end;

    end;

    theorem :: EC_PF_3:11

    for P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st ( rep_pt P) _EQ_ ( rep_pt Q) holds ( rep_pt P) = ( rep_pt Q)

    proof

      let P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: ( rep_pt P) _EQ_ ( rep_pt 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 rP) = ( rep_pt rQ) by A1, EC_PF_2: 39

      .= ( rep_pt Q) by LmRepPoint9;

      hence thesis by LmRepPoint9;

    end;

    definition

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      :: EC_PF_3:def2

      func compell_AffCo (z,p) -> UnOp of ( EC_SetAffCo (z,p)) means

      : DefAffCompEll: for P be Element of ( EC_SetAffCo (z,p)) holds (it . P) = ( rep_pt (( compell_ProjCo (z,p)) . P));

      existence

      proof

        set a = (z `1 );

        set b = (z `2 );

        defpred P[ Element of ( EC_SetAffCo (z,p)), set] means $2 = ( rep_pt (( compell_ProjCo (z,p)) . $1));

        

         A2: for P be Element of ( EC_SetAffCo (z,p)) holds ex R be Element of ( EC_SetAffCo (z,p)) st P[P, R]

        proof

          let P be Element of ( EC_SetAffCo (z,p));

          set Q = (( compell_ProjCo (z,p)) . P);

          reconsider Q as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

          set R = ( rep_pt Q);

          reconsider R as Element of ( EC_SetAffCo (z,p)) by ThAffCo;

          take R;

          thus thesis;

        end;

        consider f be UnOp of ( EC_SetAffCo (z,p)) such that

         A3: for P be Element of ( EC_SetAffCo (z,p)) holds P[P, (f . P)] from FUNCT_2:sch 3( A2);

        take f;

        thus thesis by A3;

      end;

      uniqueness

      proof

        set a = (z `1 );

        set b = (z `2 );

        deffunc F( Element of ( EC_SetAffCo (z,p))) = ( rep_pt (( compell_ProjCo (z,p)) . $1));

        for f1,f2 be UnOp of ( EC_SetAffCo (z,p)) st (for x be Element of ( EC_SetAffCo (z,p)) holds (f1 . x) = F(x)) & (for x be Element of ( EC_SetAffCo (z,p)) holds (f2 . x) = F(x)) holds f1 = f2

        proof

          let f1,f2 be UnOp of ( EC_SetAffCo (z,p)) such that

           A2: for x be Element of ( EC_SetAffCo (z,p)) holds (f1 . x) = F(x) and

           A3: for x be Element of ( EC_SetAffCo (z,p)) holds (f2 . x) = F(x);

          now

            let x be Element of ( EC_SetAffCo (z,p));

            

            thus (f1 . x) = F(x) by A2

            .= (f2 . x) by A3;

          end;

          hence thesis by FUNCT_2: 63;

        end;

        hence thesis;

      end;

    end

    definition

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      let F be Function of ( EC_SetAffCo (z,p)), ( EC_SetAffCo (z,p));

      let P be Element of ( EC_SetAffCo (z,p));

      :: original: .

      redefine

      func F . P -> Element of ( EC_SetAffCo (z,p)) ;

      correctness

      proof

        (F . P) in ( EC_SetAffCo (z,p));

        hence thesis;

      end;

    end

    definition

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      :: EC_PF_3:def3

      func addell_AffCo (z,p) -> BinOp of ( EC_SetAffCo (z,p)) means

      : DefAffAddEll: for P,Q be Element of ( EC_SetAffCo (z,p)) holds (it . (P,Q)) = ( rep_pt (( addell_ProjCo (z,p)) . (P,Q)));

      existence

      proof

        defpred P[ Element of ( EC_SetAffCo (z,p)), Element of ( EC_SetAffCo (z,p)), set] means $3 = ( rep_pt (( addell_ProjCo (z,p)) . ($1,$2)));

        

         A1: for P,Q be Element of ( EC_SetAffCo (z,p)) holds ex R be Element of ( EC_SetAffCo (z,p)) st P[P, Q, R]

        proof

          let P,Q be Element of ( EC_SetAffCo (z,p));

          set R = ( rep_pt (( addell_ProjCo (z,p)) . (P,Q)));

          reconsider R as Element of ( EC_SetAffCo (z,p)) by ThAffCo;

          take R;

          thus thesis;

        end;

        consider f be Function of [:( EC_SetAffCo (z,p)), ( EC_SetAffCo (z,p)):], ( EC_SetAffCo (z,p)) such that

         A2: for P,Q be Element of ( EC_SetAffCo (z,p)) holds P[P, Q, (f . (P,Q))] from BINOP_1:sch 3( A1);

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        deffunc O( Element of ( EC_SetAffCo (z,p)), Element of ( EC_SetAffCo (z,p))) = ( rep_pt (( addell_ProjCo (z,p)) . ($1,$2)));

        for o1,o2 be BinOp of ( EC_SetAffCo (z,p)) st (for P,Q be Element of ( EC_SetAffCo (z,p)) holds (o1 . (P,Q)) = O(P,Q)) & (for P,Q be Element of ( EC_SetAffCo (z,p)) holds (o2 . (P,Q)) = O(P,Q)) holds o1 = o2 from BINOP_2:sch 2;

        hence thesis;

      end;

    end

    definition

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      let F be Function of [:( EC_SetAffCo (z,p)), ( EC_SetAffCo (z,p)):], ( EC_SetAffCo (z,p));

      let Q,R be Element of ( EC_SetAffCo (z,p));

      :: original: .

      redefine

      func F . (Q,R) -> Element of ( EC_SetAffCo (z,p)) ;

      correctness

      proof

        (F . (Q,R)) in ( EC_SetAffCo (z,p));

        hence thesis;

      end;

    end

    theorem :: EC_PF_3:12

    

     ThUnityProjCo: for P,O be 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

    proof

      let P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: O = [ 0 , 1, 0 ];

      (( addell_ProjCo (z,p)) . (P,O)) _EQ_ P

      proof

        per cases ;

          suppose

           B1: P _EQ_ O;

          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;

        end;

          suppose not P _EQ_ O;

          hence (( addell_ProjCo (z,p)) . (P,O)) _EQ_ P by A1, EC_PF_2:def 9;

        end;

      end;

      hence thesis by A1, EC_PF_2:def 9;

    end;

    theorem :: EC_PF_3:13

    

     ThLeftZeroedAffCo: for P,O be Element of ( EC_SetAffCo (z,p)) st O = [ 0 , 1, 0 ] holds (( addell_AffCo (z,p)) . (O,P)) = P

    proof

      let P,O be Element of ( EC_SetAffCo (z,p)) such that

       A1: O = [ 0 , 1, 0 ];

      consider PP be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       B1: PP = P & PP in ( EC_SetAffCo (z,p));

      (( addell_ProjCo (z,p)) . (O,PP)) _EQ_ PP by A1, ThUnityProjCo;

      

      then ( rep_pt (( addell_ProjCo (z,p)) . (O,PP))) = ( rep_pt PP) by EC_PF_2: 39

      .= PP by B1, ThRepPoint6;

      hence thesis by B1, DefAffAddEll;

    end;

    theorem :: EC_PF_3:14

    

     ThRightZeroedAffCo: for P,O be Element of ( EC_SetAffCo (z,p)) st O = [ 0 , 1, 0 ] holds (( addell_AffCo (z,p)) . (P,O)) = P

    proof

      let P,O be Element of ( EC_SetAffCo (z,p)) such that

       A1: O = [ 0 , 1, 0 ];

      consider PP be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       B1: PP = P & PP in ( EC_SetAffCo (z,p));

      (( addell_ProjCo (z,p)) . (PP,O)) _EQ_ PP by A1, ThUnityProjCo;

      

      then ( rep_pt (( addell_ProjCo (z,p)) . (PP,O))) = ( rep_pt PP) by EC_PF_2: 39

      .= PP by B1, ThRepPoint6;

      hence thesis by B1, DefAffAddEll;

    end;

    theorem :: EC_PF_3:15

    

     ThUnityAffCo: for O be Element of ( EC_SetAffCo (z,p)) st O = [ 0 , 1, 0 ] holds O is_a_unity_wrt ( addell_AffCo (z,p))

    proof

      let O be Element of ( EC_SetAffCo (z,p)) such that

       A1: O = [ 0 , 1, 0 ];

      for P be Element of ( EC_SetAffCo (z,p)) holds (( addell_AffCo (z,p)) . (O,P)) = P by A1, ThLeftZeroedAffCo;

      then

       A2: O is_a_left_unity_wrt ( addell_AffCo (z,p)) by BINOP_1:def 5;

      for P be Element of ( EC_SetAffCo (z,p)) holds (( addell_AffCo (z,p)) . (P,O)) = P by A1, ThRightZeroedAffCo;

      hence O is_a_unity_wrt ( addell_AffCo (z,p)) by A2, BINOP_1:def 6, BINOP_1:def 7;

    end;

    theorem :: EC_PF_3:16

    

     ThAddCompAffCo: for P,O be Element of ( EC_SetAffCo (z,p)) st O = [ 0 , 1, 0 ] holds (( addell_AffCo (z,p)) . (P,(( compell_AffCo (z,p)) . P))) = O

    proof

      let P,O be Element of ( EC_SetAffCo (z,p)) such that

       A1: O = [ 0 , 1, 0 ];

      set Q = (( compell_AffCo (z,p)) . P);

      reconsider Q as Element of ( EC_SetAffCo (z,p));

      consider PP be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A2: PP = P & PP in ( EC_SetAffCo (z,p));

      consider OO be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A4: OO = O & OO in ( EC_SetAffCo (z,p));

      per cases ;

        suppose

         B1: (P `3_3 ) <> 0 ;

        

         B2: (( compell_AffCo (z,p)) . P) = ( rep_pt (( compell_ProjCo (z,p)) . PP)) by A2, DefAffCompEll

        .= (( compell_ProjCo (z,p)) . ( rep_pt PP)) by A2, B1, EC_PF_2: 42

        .= (( compell_ProjCo (z,p)) . PP) by A2, ThRepPoint6;

        

         B3: ( rep_pt (( addell_ProjCo (z,p)) . (PP,(( compell_ProjCo (z,p)) . PP)))) = (( addell_AffCo (z,p)) . (P,(( compell_AffCo (z,p)) . P))) by A2, B2, DefAffAddEll;

        ( rep_pt OO) = (( addell_AffCo (z,p)) . (P,(( compell_AffCo (z,p)) . P))) by A1, A4, B3, ThAddCompProjCo, EC_PF_2: 39;

        hence (( addell_AffCo (z,p)) . (P,(( compell_AffCo (z,p)) . P))) = O by A4, ThRepPoint6;

      end;

        suppose (P `3_3 ) = 0 ;

        then

         B2: PP _EQ_ OO by A1, A2, A4, ThEQO;

        set COO = (( compell_ProjCo (z,p)) . OO);

        reconsider COO as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

        COO _EQ_ OO by A1, A4, EC_PF_2: 40;

        then COO _EQ_ PP by B2, EC_PF_1: 44;

        then (( compell_ProjCo (z,p)) . COO) _EQ_ (( compell_ProjCo (z,p)) . PP) by EC_PF_2: 46;

        then OO _EQ_ (( compell_ProjCo (z,p)) . PP) by EC_PF_2: 41;

        then ( rep_pt (( compell_ProjCo (z,p)) . PP)) = ( rep_pt OO) by EC_PF_2: 39;

        

        then

         B4: (( compell_AffCo (z,p)) . P) = ( rep_pt OO) by A2, DefAffCompEll

        .= OO by A4, ThRepPoint6;

        

         B5: (( addell_ProjCo (z,p)) . (PP,(( compell_AffCo (z,p)) . P))) = OO by A1, A4, B2, B4, EC_PF_2:def 9;

        

        thus (( addell_AffCo (z,p)) . (P,(( compell_AffCo (z,p)) . P))) = ( rep_pt (( addell_ProjCo (z,p)) . (PP,(( compell_AffCo (z,p)) . P)))) by A2, DefAffAddEll

        .= O by A4, B5, ThRepPoint6;

      end;

    end;

    begin

    theorem :: EC_PF_3:17

    

     LmCommutative1: for p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P,Q,O,PQ,QP be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st O = [ 0 , 1, 0 ] & not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q holds (PQ = (( addell_ProjCo (z,p)) . (P,Q)) & QP = (( addell_ProjCo (z,p)) . (Q,P))) implies (QP `1_3 ) = ( - (PQ `1_3 )) & (QP `2_3 ) = ( - (PQ `2_3 )) & (QP `3_3 ) = ( - (PQ `3_3 ))

    proof

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p), P,Q,O,PQ,QP be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A2: O = [ 0 , 1, 0 ] and

       A3: not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q;

      set a = (z `1 );

      set b = (z `2 );

      assume

       AS: PQ = (( addell_ProjCo (z,p)) . (P,Q)) & QP = (( addell_ProjCo (z,p)) . (Q,P));

      reconsider g2 = (2 mod p) as Element of ( GF p) by EC_PF_1: 14;

      set gf1PQ = (((Q `2_3 ) * (P `3_3 )) - ((P `2_3 ) * (Q `3_3 )));

      set gf2PQ = (((Q `1_3 ) * (P `3_3 )) - ((P `1_3 ) * (Q `3_3 )));

      set gf3PQ = (((((gf1PQ |^ 2) * (P `3_3 )) * (Q `3_3 )) - (gf2PQ |^ 3)) - (((g2 * (gf2PQ |^ 2)) * (P `1_3 )) * (Q `3_3 )));

      set gf1QP = (((P `2_3 ) * (Q `3_3 )) - ((Q `2_3 ) * (P `3_3 )));

      set gf2QP = (((P `1_3 ) * (Q `3_3 )) - ((Q `1_3 ) * (P `3_3 )));

      set gf3QP = (((((gf1QP |^ 2) * (Q `3_3 )) * (P `3_3 )) - (gf2QP |^ 3)) - (((g2 * (gf2QP |^ 2)) * (Q `1_3 )) * (P `3_3 )));

      reconsider gf1PQ, gf2PQ, gf3PQ, gf1QP, gf2QP, gf3QP as Element of ( GF p);

      

       A5: PQ = [(gf2PQ * gf3PQ), ((gf1PQ * ((((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 )) - gf3PQ)) - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 ))), (((gf2PQ |^ 3) * (P `3_3 )) * (Q `3_3 ))] by A2, A3, AS, EC_PF_2:def 9;

      

       A6: QP = [(gf2QP * gf3QP), ((gf1QP * ((((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )) - gf3QP)) - (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 ))), (((gf2QP |^ 3) * (Q `3_3 )) * (P `3_3 ))] by A2, A3, AS, EC_PF_2:def 9;

      

       A7: gf1QP = ( - gf1PQ) by VECTSP_1: 17;

      

       A8: gf2QP = ( - gf2PQ) by VECTSP_1: 17;

      

       A10: (gf2PQ |^ 2) = (gf2QP |^ 2) by A8, EC_PF_2: 1;

      

       A11: gf3QP = gf3PQ

      proof

        

         B1: (((g2 * (Q `1_3 )) * (P `3_3 )) - ((Q `1_3 ) * (P `3_3 ))) = ((g2 * ((Q `1_3 ) * (P `3_3 ))) - ((Q `1_3 ) * (P `3_3 ))) by GROUP_1:def 3

        .= ((Q `1_3 ) * (P `3_3 )) by EC_PF_2: 24;

        

         B2: (((g2 * (P `1_3 )) * (Q `3_3 )) - ((P `1_3 ) * (Q `3_3 ))) = ((g2 * ((P `1_3 ) * (Q `3_3 ))) - ((P `1_3 ) * (Q `3_3 ))) by GROUP_1:def 3

        .= ((P `1_3 ) * (Q `3_3 )) by EC_PF_2: 24;

        (gf2QP + ((g2 * (Q `1_3 )) * (P `3_3 ))) = (((P `1_3 ) * (Q `3_3 )) + (((g2 * (Q `1_3 )) * (P `3_3 )) + ( - ((Q `1_3 ) * (P `3_3 ))))) by ALGSTR_1: 7

        .= (((g2 * (P `1_3 )) * (Q `3_3 )) + (((Q `1_3 ) * (P `3_3 )) + ( - ((P `1_3 ) * (Q `3_3 ))))) by B1, B2, ALGSTR_1: 7

        .= (gf2PQ + ((g2 * (P `1_3 )) * (Q `3_3 )));

        

        then ((gf2QP + ((g2 * (Q `1_3 )) * (P `3_3 ))) * (gf2QP |^ 2)) = ((gf2PQ + ((g2 * (P `1_3 )) * (Q `3_3 ))) * (gf2PQ |^ 2)) by A8, EC_PF_2: 1

        .= ((gf2PQ * (gf2PQ |^ 2)) + (((g2 * (P `1_3 )) * (Q `3_3 )) * (gf2PQ |^ 2))) by VECTSP_1:def 3

        .= ((gf2PQ * (gf2PQ |^ 2)) + ((g2 * ((P `1_3 ) * (Q `3_3 ))) * (gf2PQ |^ 2))) by GROUP_1:def 3

        .= ((gf2PQ * (gf2PQ |^ 2)) + (g2 * (((P `1_3 ) * (Q `3_3 )) * (gf2PQ |^ 2)))) by GROUP_1:def 3

        .= ((gf2PQ |^ (2 + 1)) + (g2 * (((P `1_3 ) * (Q `3_3 )) * (gf2PQ |^ 2)))) by EC_PF_1: 24

        .= ((gf2PQ |^ 3) + ((g2 * (gf2PQ |^ 2)) * ((P `1_3 ) * (Q `3_3 )))) by GROUP_1:def 3

        .= ((gf2PQ |^ 3) + (((g2 * (gf2PQ |^ 2)) * (P `1_3 )) * (Q `3_3 ))) by GROUP_1:def 3;

        

        then

         B3: ((gf2PQ |^ 3) + (((g2 * (gf2PQ |^ 2)) * (P `1_3 )) * (Q `3_3 ))) = ((gf2QP * (gf2QP |^ 2)) + (((g2 * (Q `1_3 )) * (P `3_3 )) * (gf2QP |^ 2))) by VECTSP_1:def 3

        .= ((gf2QP * (gf2QP |^ 2)) + ((g2 * ((Q `1_3 ) * (P `3_3 ))) * (gf2QP |^ 2))) by GROUP_1:def 3

        .= ((gf2QP * (gf2QP |^ 2)) + (g2 * (((Q `1_3 ) * (P `3_3 )) * (gf2QP |^ 2)))) by GROUP_1:def 3

        .= ((gf2QP |^ (2 + 1)) + (g2 * (((Q `1_3 ) * (P `3_3 )) * (gf2QP |^ 2)))) by EC_PF_1: 24

        .= ((gf2QP |^ 3) + ((g2 * (gf2QP |^ 2)) * ((Q `1_3 ) * (P `3_3 )))) by GROUP_1:def 3

        .= ((gf2QP |^ 3) + (((g2 * (gf2QP |^ 2)) * (Q `1_3 )) * (P `3_3 ))) by GROUP_1:def 3;

        (((gf1QP |^ 2) * (Q `3_3 )) * (P `3_3 )) = ((gf1QP |^ 2) * ((Q `3_3 ) * (P `3_3 ))) by GROUP_1:def 3

        .= ((gf1PQ |^ 2) * ((Q `3_3 ) * (P `3_3 ))) by A7, EC_PF_2: 1

        .= (((gf1PQ |^ 2) * (P `3_3 )) * (Q `3_3 )) by GROUP_1:def 3;

        then ((((gf1QP |^ 2) * (Q `3_3 )) * (P `3_3 )) - ((gf2QP |^ 3) + (((g2 * (gf2QP |^ 2)) * (Q `1_3 )) * (P `3_3 )))) = gf3PQ by B3, VECTSP_1: 17;

        hence gf3PQ = gf3QP by VECTSP_1: 17;

      end;

      thus (QP `1_3 ) = ( - (PQ `1_3 ))

      proof

        ((PQ `1_3 ) + (QP `1_3 )) = ((gf2PQ * gf3PQ) + (QP `1_3 )) by A5, EC_PF_2:def 3

        .= ((gf2PQ * gf3PQ) + (( - gf2PQ) * gf3PQ)) by A6, A8, A11, EC_PF_2:def 3

        .= ((gf2PQ * gf3PQ) - (gf2PQ * gf3PQ)) by VECTSP_1: 9

        .= ( 0. ( GF p)) by VECTSP_1: 19;

        hence thesis by VECTSP_1: 16;

      end;

      thus (QP `2_3 ) = ( - (PQ `2_3 ))

      proof

        

         B1: (gf1PQ * gf3PQ) = (( - gf1QP) * gf3PQ) by VECTSP_1: 17

        .= ( - (gf1QP * gf3QP)) by A11, VECTSP_1: 9;

        (gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) = (( - gf1QP) * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) by VECTSP_1: 17

        .= ( - (gf1QP * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 )))) by VECTSP_1: 9

        .= ( - (gf1QP * ((gf2QP |^ 2) * ((P `1_3 ) * (Q `3_3 ))))) by A10, GROUP_1:def 3

        .= ( - (gf1QP * ((gf2QP |^ 2) * (((P `1_3 ) * (Q `3_3 )) + ( 0. ( GF p)))))) by ALGSTR_1: 7

        .= ( - (gf1QP * ((gf2QP |^ 2) * (((P `1_3 ) * (Q `3_3 )) + (((Q `1_3 ) * (P `3_3 )) - ((Q `1_3 ) * (P `3_3 ))))))) by VECTSP_1: 19

        .= ( - (gf1QP * ((gf2QP |^ 2) * (((Q `1_3 ) * (P `3_3 )) + (((P `1_3 ) * (Q `3_3 )) + ( - ((Q `1_3 ) * (P `3_3 )))))))) by ALGSTR_1: 7

        .= ( - (gf1QP * (((gf2QP |^ 2) * ((Q `1_3 ) * (P `3_3 ))) + ((gf2QP |^ 2) * gf2QP)))) by VECTSP_1:def 3

        .= ( - (gf1QP * (((gf2QP |^ 2) * ((Q `1_3 ) * (P `3_3 ))) + (gf2QP |^ (2 + 1))))) by EC_PF_1: 24

        .= ( - (gf1QP * (((gf2QP |^ 2) * ((Q `1_3 ) * (P `3_3 ))) + (gf2QP |^ 3))));

        then ((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * (((gf2QP |^ 2) * ((Q `1_3 ) * (P `3_3 ))) + (gf2QP |^ 3)))) = ( 0. ( GF p)) by VECTSP_1: 19;

        then ((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + ((gf1QP * ((gf2QP |^ 2) * ((Q `1_3 ) * (P `3_3 )))) + (gf1QP * (gf2QP |^ 3)))) = ( 0. ( GF p)) by VECTSP_1:def 3;

        then (((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * ((gf2QP |^ 2) * ((Q `1_3 ) * (P `3_3 ))))) + (gf1QP * (gf2QP |^ 3))) = ( 0. ( GF p)) by ALGSTR_1: 7;

        then ((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * ((gf2QP |^ 2) * ((Q `1_3 ) * (P `3_3 ))))) = ( - (gf1QP * (gf2QP |^ 3))) by VECTSP_1: 16;

        then

         B2: ((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * (((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )))) = ( - (gf1QP * (gf2QP |^ 3))) by GROUP_1:def 3;

        

         B3: ((((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )) + (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 ))) = (((gf2PQ |^ (2 + 1)) * ((P `2_3 ) * (Q `3_3 ))) + (((gf2QP |^ (2 + 1)) * (Q `2_3 )) * (P `3_3 ))) by GROUP_1:def 3

        .= (((gf2PQ |^ 3) * ((P `2_3 ) * (Q `3_3 ))) + ((((gf2QP |^ 2) * gf2QP) * (Q `2_3 )) * (P `3_3 ))) by EC_PF_1: 24

        .= (((gf2PQ |^ 3) * ((P `2_3 ) * (Q `3_3 ))) + ((((gf2PQ |^ 2) * ( - gf2PQ)) * (Q `2_3 )) * (P `3_3 ))) by A8, EC_PF_2: 1

        .= (((gf2PQ |^ 3) * ((P `2_3 ) * (Q `3_3 ))) + ((( - ((gf2PQ |^ 2) * gf2PQ)) * (Q `2_3 )) * (P `3_3 ))) by VECTSP_1: 8

        .= (((gf2PQ |^ 3) * ((P `2_3 ) * (Q `3_3 ))) + ((( - (gf2PQ |^ (2 + 1))) * (Q `2_3 )) * (P `3_3 ))) by EC_PF_1: 24

        .= (((gf2PQ |^ 3) * ((P `2_3 ) * (Q `3_3 ))) + (( - (gf2PQ |^ 3)) * ((Q `2_3 ) * (P `3_3 )))) by GROUP_1:def 3

        .= (((gf2PQ |^ 3) * ((P `2_3 ) * (Q `3_3 ))) + ( - ((gf2PQ |^ 3) * ((Q `2_3 ) * (P `3_3 ))))) by VECTSP_1: 9

        .= (((gf2PQ |^ 3) * ((P `2_3 ) * (Q `3_3 ))) + ((gf2PQ |^ 3) * ( - ((Q `2_3 ) * (P `3_3 ))))) by VECTSP_1: 8

        .= (gf1QP * (gf2PQ |^ (2 + 1))) by VECTSP_1:def 3

        .= (gf1QP * ((gf2PQ |^ 2) * gf2PQ)) by EC_PF_1: 24

        .= (gf1QP * ((gf2QP |^ 2) * gf2PQ)) by A8, EC_PF_2: 1

        .= (gf1QP * ((gf2QP |^ 2) * ( - gf2QP))) by VECTSP_1: 17

        .= (gf1QP * ( - ((gf2QP |^ 2) * gf2QP))) by VECTSP_1: 8

        .= ( - (gf1QP * ((gf2QP |^ 2) * gf2QP))) by VECTSP_1: 9

        .= ( - (gf1QP * (gf2QP |^ (2 + 1)))) by EC_PF_1: 24

        .= ( - (gf1QP * (gf2QP |^ 3)));

        ((((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * (((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )))) - ((((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )) + (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 )))) - ((gf1PQ * gf3PQ) + (gf1QP * gf3QP))) = ((( - (gf1QP * (gf2QP |^ 3))) - ( - (gf1QP * (gf2QP |^ 3)))) - ( 0. ( GF p))) by B1, B2, B3, VECTSP_1: 19

        .= (( - (gf1QP * (gf2QP |^ 3))) + ( - ( - (gf1QP * (gf2QP |^ 3))))) by VECTSP_1: 18

        .= ( 0. ( GF p)) by VECTSP_1: 19;

        

        then ( 0. ( GF p)) = (((((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * (((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )))) - ((((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )) + (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 )))) - (gf1QP * gf3QP)) - (gf1PQ * gf3PQ)) by VECTSP_1: 17

        .= (((((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * (((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )))) + (( - (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 ))) - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + ( - (gf1QP * gf3QP))) + ( - (gf1PQ * gf3PQ))) by VECTSP_1: 17

        .= ((((((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (gf1QP * (((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )))) + ( - (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 )))) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + ( - (gf1QP * gf3QP))) + ( - (gf1PQ * gf3PQ))) by ALGSTR_1: 7

        .= (((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + ((((gf1QP * (((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 ))) + ( - (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 )))) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + ( - (gf1QP * gf3QP)))) + ( - (gf1PQ * gf3PQ))) by EC_PF_2: 8

        .= (((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + ((((gf1QP * (((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 ))) - (gf1QP * gf3QP)) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + ( - (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 ))))) + ( - (gf1PQ * gf3PQ))) by EC_PF_2: 7

        .= (((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (((gf1QP * ((((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )) - gf3QP)) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + ( - (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 ))))) + ( - (gf1PQ * gf3PQ))) by VECTSP_1: 11

        .= (((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (((gf1QP * ((((gf2QP |^ 2) * (Q `1_3 )) * (P `3_3 )) - gf3QP)) + ( - (((gf2QP |^ 3) * (Q `2_3 )) * (P `3_3 )))) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 ))))) + ( - (gf1PQ * gf3PQ))) by ALGSTR_1: 8

        .= (((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + ((QP `2_3 ) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 ))))) + ( - (gf1PQ * gf3PQ))) by A6, EC_PF_2:def 4

        .= ((((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) + (QP `2_3 )) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + ( - (gf1PQ * gf3PQ))) by ALGSTR_1: 7

        .= ((((gf1PQ * (((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 ))) - (gf1PQ * gf3PQ)) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + (QP `2_3 )) by EC_PF_2: 7

        .= (((gf1PQ * ((((gf2PQ |^ 2) * (P `1_3 )) * (Q `3_3 )) - gf3PQ)) + ( - (((gf2PQ |^ 3) * (P `2_3 )) * (Q `3_3 )))) + (QP `2_3 )) by VECTSP_1: 11

        .= ((PQ `2_3 ) + (QP `2_3 )) by A5, EC_PF_2:def 4;

        hence thesis by VECTSP_1: 16;

      end;

      thus (QP `3_3 ) = ( - (PQ `3_3 ))

      proof

        ((gf2PQ |^ 2) * gf2PQ) = ((gf2QP |^ 2) * gf2PQ) by A8, EC_PF_2: 1

        .= ((gf2QP |^ 2) * ( - gf2QP)) by VECTSP_1: 17

        .= ( - ((gf2QP |^ 2) * gf2QP)) by VECTSP_1: 8

        .= ( - (gf2QP |^ (2 + 1))) by EC_PF_1: 24

        .= ( - (gf2QP |^ 3));

        

        then ( - (gf2QP |^ 3)) = (gf2PQ |^ (2 + 1)) by EC_PF_1: 24

        .= (gf2PQ |^ 3);

        

        then (((gf2PQ |^ 3) + (gf2QP |^ 3)) * ((P `3_3 ) * (Q `3_3 ))) = (( 0. ( GF p)) * ((P `3_3 ) * (Q `3_3 ))) by VECTSP_1: 19

        .= ( 0. ( GF p));

        then (((gf2PQ |^ 3) * ((P `3_3 ) * (Q `3_3 ))) + ((gf2QP |^ 3) * ((Q `3_3 ) * (P `3_3 )))) = ( 0. ( GF p)) by VECTSP_1:def 3;

        then ((((gf2PQ |^ 3) * (P `3_3 )) * (Q `3_3 )) + ((gf2QP |^ 3) * ((Q `3_3 ) * (P `3_3 )))) = ( 0. ( GF p)) by GROUP_1:def 3;

        then ((PQ `3_3 ) + ((gf2QP |^ 3) * ((Q `3_3 ) * (P `3_3 )))) = ( 0. ( GF p)) by A5, EC_PF_2:def 5;

        then ((PQ `3_3 ) + (((gf2QP |^ 3) * (Q `3_3 )) * (P `3_3 ))) = ( 0. ( GF p)) by GROUP_1:def 3;

        then ((PQ `3_3 ) + (QP `3_3 )) = ( 0. ( GF p)) by A6, EC_PF_2:def 5;

        hence thesis by VECTSP_1: 16;

      end;

    end;

    theorem :: EC_PF_3:18

    

     LmCommutative2: for P,Q,O,PQ,QP be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)), d be Element of ( GF p) st O = [ 0 , 1, 0 ] & d <> ( 0. ( GF p)) & (Q `1_3 ) = (d * (P `1_3 )) & (Q `2_3 ) = (d * (P `2_3 )) & (Q `3_3 ) = (d * (P `3_3 )) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = (( addell_ProjCo (z,p)) . (P,Q)) & QP = (( addell_ProjCo (z,p)) . (Q,P)) holds (QP `1_3 ) = ((d |^ 6) * (PQ `1_3 )) & (QP `2_3 ) = ((d |^ 6) * (PQ `2_3 )) & (QP `3_3 ) = ((d |^ 6) * (PQ `3_3 ))

    proof

      set a = (z `1 );

      set b = (z `2 );

      let P,Q,O,PQ,QP be Element of ( EC_SetProjCo (a,b,p)), d be Element of ( GF p) such that

       A0: O = [ 0 , 1, 0 ] and

       A1: d <> ( 0. ( GF p)) & (Q `1_3 ) = (d * (P `1_3 )) & (Q `2_3 ) = (d * (P `2_3 )) & (Q `3_3 ) = (d * (P `3_3 )) and

       A2: not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q and

       A3: PQ = (( addell_ProjCo (z,p)) . (P,Q)) and

       A4: QP = (( addell_ProjCo (z,p)) . (Q,P));

      reconsider g2 = (2 mod p) as Element of ( GF p) by EC_PF_1: 14;

      reconsider g3 = (3 mod p) as Element of ( GF p) by EC_PF_1: 14;

      reconsider g4 = (4 mod p) as Element of ( GF p) by EC_PF_1: 14;

      reconsider g8 = (8 mod p) as Element of ( GF p) by EC_PF_1: 14;

      set gf1P = ((a * ((P `3_3 ) |^ 2)) + (g3 * ((P `1_3 ) |^ 2)));

      set gf2P = ((P `2_3 ) * (P `3_3 ));

      set gf3P = (((P `1_3 ) * (P `2_3 )) * gf2P);

      set gf4P = ((gf1P |^ 2) - (g8 * gf3P));

      reconsider gf1P, gf2P, gf3P, gf4P as Element of ( GF p);

      

       A9: PQ = [((g2 * gf4P) * gf2P), ((gf1P * ((g4 * gf3P) - gf4P)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2P |^ 2))), (g8 * (gf2P |^ 3))] by A0, A2, A3, EC_PF_2:def 9;

      set gf1Q = ((a * ((Q `3_3 ) |^ 2)) + (g3 * ((Q `1_3 ) |^ 2)));

      set gf2Q = ((Q `2_3 ) * (Q `3_3 ));

      set gf3Q = (((Q `1_3 ) * (Q `2_3 )) * gf2Q);

      set gf4Q = ((gf1Q |^ 2) - (g8 * gf3Q));

      reconsider gf1Q, gf2Q, gf3Q, gf4Q as Element of ( GF p);

      

       A10: QP = [((g2 * gf4Q) * gf2Q), ((gf1Q * ((g4 * gf3Q) - gf4Q)) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))), (g8 * (gf2Q |^ 3))] by A0, A2, A4, EC_PF_2:def 9;

      

       A11: gf1Q = ((a * ((d |^ 2) * ((P `3_3 ) |^ 2))) + (g3 * ((d * (P `1_3 )) |^ 2))) by A1, BINOM: 9

      .= ((a * ((d |^ 2) * ((P `3_3 ) |^ 2))) + (g3 * ((d |^ 2) * ((P `1_3 ) |^ 2)))) by BINOM: 9

      .= (((a * (d |^ 2)) * ((P `3_3 ) |^ 2)) + (g3 * ((d |^ 2) * ((P `1_3 ) |^ 2)))) by GROUP_1:def 3

      .= (((a * (d |^ 2)) * ((P `3_3 ) |^ 2)) + ((g3 * (d |^ 2)) * ((P `1_3 ) |^ 2))) by GROUP_1:def 3

      .= (((d |^ 2) * (a * ((P `3_3 ) |^ 2))) + (((d |^ 2) * g3) * ((P `1_3 ) |^ 2))) by GROUP_1:def 3

      .= (((d |^ 2) * (a * ((P `3_3 ) |^ 2))) + ((d |^ 2) * (g3 * ((P `1_3 ) |^ 2)))) by GROUP_1:def 3

      .= ((d |^ 2) * gf1P) by VECTSP_1:def 3;

      

       A12: gf2Q = (d * (((P `2_3 ) * d) * (P `3_3 ))) by A1, GROUP_1:def 3

      .= (d * (d * ((P `2_3 ) * (P `3_3 )))) by GROUP_1:def 3

      .= ((d * d) * ((P `2_3 ) * (P `3_3 ))) by GROUP_1:def 3

      .= ((d |^ 2) * gf2P) by EC_PF_1: 22;

      

       A13: gf3Q = ((d * (((P `1_3 ) * d) * (P `2_3 ))) * gf2Q) by A1, GROUP_1:def 3

      .= ((d * (d * ((P `1_3 ) * (P `2_3 )))) * gf2Q) by GROUP_1:def 3

      .= (((d * d) * ((P `1_3 ) * (P `2_3 ))) * gf2Q) by GROUP_1:def 3

      .= (((d |^ 2) * ((P `1_3 ) * (P `2_3 ))) * gf2Q) by EC_PF_1: 22

      .= ((d |^ 2) * ((((P `1_3 ) * (P `2_3 )) * (d |^ 2)) * gf2P)) by A12, GROUP_1:def 3

      .= ((d |^ 2) * ((d |^ 2) * gf3P)) by GROUP_1:def 3

      .= (((d |^ 2) * (d |^ 2)) * gf3P) by GROUP_1:def 3

      .= (((d |^ 2) |^ 2) * gf3P) by EC_PF_1: 22

      .= ((d |^ (2 * 2)) * gf3P) by BINOM: 11

      .= ((d |^ 4) * gf3P);

      

       A14: gf4Q = ((((d |^ 2) |^ 2) * (gf1P |^ 2)) - (g8 * ((d |^ 4) * gf3P))) by A11, A13, BINOM: 9

      .= (((d |^ (2 * 2)) * (gf1P |^ 2)) - (g8 * ((d |^ 4) * gf3P))) by BINOM: 11

      .= (((d |^ 4) * (gf1P |^ 2)) - ((d |^ 4) * (g8 * gf3P))) by GROUP_1:def 3

      .= ((d |^ 4) * gf4P) by VECTSP_1: 11;

      

      thus (QP `1_3 ) = ((g2 * gf4Q) * gf2Q) by A10, EC_PF_2:def 3

      .= (g2 * (((d |^ 4) * gf4P) * ((d |^ 2) * gf2P))) by A12, A14, GROUP_1:def 3

      .= (g2 * ((d |^ 4) * (gf4P * ((d |^ 2) * gf2P)))) by GROUP_1:def 3

      .= (g2 * ((d |^ 4) * ((d |^ 2) * (gf4P * gf2P)))) by GROUP_1:def 3

      .= (g2 * (((d |^ 4) * (d |^ 2)) * (gf4P * gf2P))) by GROUP_1:def 3

      .= (g2 * ((d |^ (4 + 2)) * (gf4P * gf2P))) by BINOM: 10

      .= ((d |^ 6) * (g2 * (gf4P * gf2P))) by GROUP_1:def 3

      .= ((d |^ 6) * ((g2 * gf4P) * gf2P)) by GROUP_1:def 3

      .= ((d |^ 6) * (PQ `1_3 )) by A9, EC_PF_2:def 3;

      

      thus (QP `2_3 ) = ((gf1Q * ((g4 * gf3Q) - gf4Q)) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))) by A10, EC_PF_2:def 4

      .= ((gf1Q * (((d |^ 4) * (g4 * gf3P)) - ((d |^ 4) * gf4P))) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))) by A13, A14, GROUP_1:def 3

      .= ((gf1Q * ((d |^ 4) * ((g4 * gf3P) - gf4P))) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))) by VECTSP_1: 11

      .= (((gf1Q * (d |^ 4)) * ((g4 * gf3P) - gf4P)) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))) by GROUP_1:def 3

      .= (((((d |^ 2) * (d |^ 4)) * gf1P) * ((g4 * gf3P) - gf4P)) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))) by A11, GROUP_1:def 3

      .= ((((d |^ (2 + 4)) * gf1P) * ((g4 * gf3P) - gf4P)) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))) by BINOM: 10

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2Q |^ 2))) by GROUP_1:def 3

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((d |^ 2) * ((P `2_3 ) |^ 2))) * (((d |^ 2) * gf2P) |^ 2))) by A1, A12, BINOM: 9

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((d |^ 2) * ((P `2_3 ) |^ 2))) * (((d |^ 2) |^ 2) * (gf2P |^ 2)))) by BINOM: 9

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((g8 * ((d |^ 2) * ((P `2_3 ) |^ 2))) * ((d |^ (2 * 2)) * (gf2P |^ 2)))) by BINOM: 11

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - (((g8 * (d |^ 2)) * ((P `2_3 ) |^ 2)) * ((d |^ 4) * (gf2P |^ 2)))) by GROUP_1:def 3

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - (((((d |^ 2) * g8) * ((P `2_3 ) |^ 2)) * (gf2P |^ 2)) * (d |^ 4))) by GROUP_1:def 3

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ 4) * (((d |^ 2) * g8) * (((P `2_3 ) |^ 2) * (gf2P |^ 2))))) by GROUP_1:def 3

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ 4) * ((d |^ 2) * (g8 * (((P `2_3 ) |^ 2) * (gf2P |^ 2)))))) by GROUP_1:def 3

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ 4) * ((d |^ 2) * ((g8 * ((P `2_3 ) |^ 2)) * (gf2P |^ 2))))) by GROUP_1:def 3

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - (((d |^ 4) * (d |^ 2)) * ((g8 * ((P `2_3 ) |^ 2)) * (gf2P |^ 2)))) by GROUP_1:def 3

      .= (((d |^ 6) * (gf1P * ((g4 * gf3P) - gf4P))) - ((d |^ (4 + 2)) * ((g8 * ((P `2_3 ) |^ 2)) * (gf2P |^ 2)))) by BINOM: 10

      .= ((d |^ 6) * ((gf1P * ((g4 * gf3P) - gf4P)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2P |^ 2)))) by VECTSP_1: 11

      .= ((d |^ 6) * (PQ `2_3 )) by A9, EC_PF_2:def 4;

      

      thus (QP `3_3 ) = (g8 * (gf2Q |^ 3)) by A10, EC_PF_2:def 5

      .= (g8 * (((d |^ 2) |^ 3) * (gf2P |^ 3))) by A12, BINOM: 9

      .= (g8 * ((d |^ (2 * 3)) * (gf2P |^ 3))) by BINOM: 11

      .= ((d |^ 6) * (g8 * (gf2P |^ 3))) by GROUP_1:def 3

      .= ((d |^ 6) * (PQ `3_3 )) by A9, EC_PF_2:def 5;

    end;

    theorem :: EC_PF_3:19

    

     ThCommutativeProjCo: for P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) holds (( addell_ProjCo (z,p)) . (P,Q)) _EQ_ (( addell_ProjCo (z,p)) . (Q,P))

    proof

      let P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      set O = [ 0 , 1, 0 ];

      reconsider O as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) by EC_PF_1: 42;

      set PQ = (( addell_ProjCo (z,p)) . (P,Q));

      set QP = (( addell_ProjCo (z,p)) . (Q,P));

      consider PQQ be Element of ( ProjCo ( GF p)) such that

       X1: PQQ = PQ & PQQ in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      

       X2: (PQQ `1_3 ) = (PQ `1_3 ) & (PQQ `2_3 ) = (PQ `2_3 ) & (PQQ `3_3 ) = (PQ `3_3 ) by X1, EC_PF_2: 32;

      consider QPP be Element of ( ProjCo ( GF p)) such that

       X3: QPP = QP & QPP in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      

       X4: (QPP `1_3 ) = (QP `1_3 ) & (QPP `2_3 ) = (QP `2_3 ) & (QPP `3_3 ) = (QP `3_3 ) by X3, EC_PF_2: 32;

      per cases ;

        suppose

         A1: P _EQ_ O;

        then

         A2: PQ _EQ_ Q by EC_PF_2:def 9;

        QP _EQ_ Q

        proof

          per cases ;

            suppose

             B1: Q _EQ_ O;

            then QP _EQ_ O by A1, EC_PF_2:def 9;

            hence thesis by B1, EC_PF_1: 44;

          end;

            suppose not Q _EQ_ O;

            hence thesis by A1, EC_PF_2:def 9;

          end;

        end;

        hence thesis by A2, EC_PF_1: 44;

      end;

        suppose

         A1: Q _EQ_ O & not P _EQ_ O;

        then PQ _EQ_ P by EC_PF_2:def 9;

        hence thesis by A1, EC_PF_2:def 9;

      end;

        suppose

         A1: not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q;

        consider d be Element of ( GF p) such that

         A2: d = ( - ( 1. ( GF p)));

        (d * (PQ `1_3 )) = (d * ( - (QP `1_3 ))) & (d * (PQ `2_3 )) = (d * ( - (QP `2_3 ))) & (d * (PQ `3_3 )) = (d * ( - (QP `3_3 ))) by A1, LmCommutative1;

        then (d * (PQ `1_3 )) = (( 1. ( GF p)) * (QP `1_3 )) & (d * (PQ `2_3 )) = (( 1. ( GF p)) * (QP `2_3 )) & (d * (PQ `3_3 )) = (( 1. ( GF p)) * (QP `3_3 )) by A2, VECTSP_1: 10;

        then (QPP `1_3 ) = (d * (PQ `1_3 )) & (QPP `2_3 ) = (d * (PQ `2_3 )) & (QPP `3_3 ) = (d * (PQ `3_3 )) by X3, EC_PF_2: 32;

        hence thesis by A2, X1, X2, X3, EC_PF_1:def 10, VECTSP_2: 3;

      end;

        suppose

         A1: not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q;

        consider PP be Element of ( ProjCo ( GF p)) such that

         A2: PP = P & PP in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

        

         A3: (PP `1_3 ) = (P `1_3 ) & (PP `2_3 ) = (P `2_3 ) & (PP `3_3 ) = (P `3_3 ) by A2, EC_PF_2: 32;

        consider QQ be Element of ( ProjCo ( GF p)) such that

         A4: QQ = Q & QQ in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

        consider d be Element of ( GF p) such that

         A6: d <> ( 0. ( GF p)) and

         A7: (QQ `1_3 ) = (d * (PP `1_3 )) & (QQ `2_3 ) = (d * (PP `2_3 )) & (QQ `3_3 ) = (d * (PP `3_3 )) by A1, A2, A4, EC_PF_1:def 10;

        set d6 = (d |^ 6);

        reconsider d6 as Element of ( GF p);

        d6 <> 0 by A6, EC_PF_1: 25;

        then

         A8: d6 <> ( 0. ( GF p)) by EC_PF_1: 11;

        (Q `1_3 ) = (d * (PP `1_3 )) & (Q `2_3 ) = (d * (PP `2_3 )) & (Q `3_3 ) = (d * (PP `3_3 )) by A4, A7, EC_PF_2: 32;

        then (QP `1_3 ) = (d6 * (PQ `1_3 )) & (QP `2_3 ) = (d6 * (PQ `2_3 )) & (QP `3_3 ) = (d6 * (PQ `3_3 )) by A1, A3, A6, LmCommutative2;

        hence thesis by A8, X1, X2, X3, X4, EC_PF_1:def 10;

      end;

    end;

    theorem :: EC_PF_3:20

    

     ThCommutativeAffCo: for P,Q be Element of ( EC_SetAffCo (z,p)) holds (( addell_AffCo (z,p)) . (P,Q)) = (( addell_AffCo (z,p)) . (Q,P))

    proof

      let P,Q be Element of ( EC_SetAffCo (z,p));

      ( rep_pt (( addell_ProjCo (z,p)) . (P,Q))) = ( rep_pt (( addell_ProjCo (z,p)) . (Q,P))) by ThCommutativeProjCo, EC_PF_2: 39

      .= (( addell_AffCo (z,p)) . (Q,P)) by DefAffAddEll;

      hence thesis by DefAffAddEll;

    end;

    registration

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      cluster ( addell_AffCo (z,p)) -> non empty commutative having_a_unity;

      correctness

      proof

        reconsider O = [ 0 , 1, 0 ] as Element of ( EC_SetAffCo (z,p)) by ThAffCoZero;

        

         P1: O is_a_unity_wrt ( addell_AffCo (z,p)) by ThUnityAffCo;

        for P,Q be Element of ( EC_SetAffCo (z,p)) holds (( addell_AffCo (z,p)) . (P,Q)) = (( addell_AffCo (z,p)) . (Q,P)) by ThCommutativeAffCo;

        hence thesis by P1, BINOP_1:def 2, SETWISEO:def 2;

      end;

    end

    definition

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      :: EC_PF_3:def4

      func 0_EC (z,p) -> Element of ( EC_SetAffCo (z,p)) equals [ 0 , 1, 0 ];

      correctness by ThAffCoZero;

    end

    registration

      let p, z;

      cluster addMagma (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)) #) -> Abelian;

      coherence by ThCommutativeAffCo;

      cluster addLoopStr (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)), ( 0_EC (z,p)) #) -> left_zeroed right_zeroed;

      coherence

      proof

        set ECSTR = addLoopStr (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)), ( 0_EC (z,p)) #);

        for P be Element of ECSTR holds (( 0. ECSTR) + P) = P by ThLeftZeroedAffCo;

        hence thesis by ALGSTR_1:def 2, ThRightZeroedAffCo;

      end;

    end

    

     ThECSTRLeftComp: addLoopStr (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)), ( 0_EC (z,p)) #) is left_complementable

    proof

      set ECSTR = addLoopStr (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)), ( 0_EC (z,p)) #);

      for P be Element of ECSTR holds P is left_complementable

      proof

        let P be Element of ECSTR;

        ex Q be Element of ECSTR st (Q + P) = ( 0. ECSTR)

        proof

          set O = ( 0. ECSTR);

          set Q = (( compell_AffCo (z,p)) . P);

          reconsider Q as Element of ECSTR by FUNCT_2: 5;

          

           A2: (Q + P) = (( addell_AffCo (z,p)) . (P,Q)) by ThCommutativeAffCo

          .= O by ThAddCompAffCo;

          take Q;

          thus thesis by A2;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    

     ThECSTRRightComp: addLoopStr (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)), ( 0_EC (z,p)) #) is right_complementable

    proof

      set ECSTR = addLoopStr (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)), ( 0_EC (z,p)) #);

      for P be Element of ECSTR holds P is right_complementable

      proof

        let P be Element of ECSTR;

        ex Q be Element of ECSTR st (P + Q) = ( 0. ECSTR)

        proof

          set O = ( 0. ECSTR);

          set Q = (( compell_AffCo (z,p)) . P);

          reconsider Q as Element of ECSTR by FUNCT_2: 5;

          take Q;

          thus thesis by ThAddCompAffCo;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let p, z;

      cluster addLoopStr (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)), ( 0_EC (z,p)) #) -> complementable;

      coherence by ThECSTRLeftComp, ThECSTRRightComp;

    end

    registration

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      cluster multMagma (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)) #) -> unital;

      coherence

      proof

        set F = multMagma (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)) #);

        reconsider E = ( 0_EC (z,p)) as Element of F;

        now

          let h be Element of F;

          reconsider h1 = h as Element of ( EC_SetAffCo (z,p));

          

           X1: ( 0_EC (z,p)) is_a_unity_wrt ( addell_AffCo (z,p)) by ThUnityAffCo;

          hence (h * E) = h by BINOP_1:def 6, BINOP_1:def 7;

          thus (E * h) = h by X1, BINOP_1:def 5, BINOP_1:def 7;

        end;

        hence thesis by GROUP_1:def 1;

      end;

    end

    theorem :: EC_PF_3:21

    

     GP0: for p be 5 _or_greater Prime, z be Element of ( EC_WParam p) holds ( 1_ multMagma (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)) #)) = ( 0_EC (z,p))

    proof

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      set F = multMagma (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)) #);

      reconsider E = ( 0_EC (z,p)) as Element of F;

      for h be Element of F holds (h * E) = h & (E * h) = h

      proof

        let h be Element of F;

        reconsider h1 = h as Element of ( EC_SetAffCo (z,p));

        

         X1: ( 0_EC (z,p)) is_a_unity_wrt ( addell_AffCo (z,p)) by ThUnityAffCo;

        hence (h * E) = h by BINOP_1:def 6, BINOP_1:def 7;

        thus (E * h) = h by X1, BINOP_1:def 5, BINOP_1:def 7;

      end;

      hence thesis by GROUP_1:def 4;

    end;

    registration

      let p be 5 _or_greater Prime, z be Element of ( EC_WParam p);

      cluster multMagma (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)) #) -> commutative Group-like non empty;

      coherence

      proof

        set F = multMagma (# ( EC_SetAffCo (z,p)), ( addell_AffCo (z,p)) #);

        

         P1: for h be Element of F holds (h * ( 1_ F)) = h & (( 1_ F) * h) = h & ex g be Element of F st (h * g) = ( 1_ F) & (g * h) = ( 1_ F)

        proof

          let h be Element of F;

          thus (h * ( 1_ F)) = h & (( 1_ F) * h) = h by GROUP_1:def 4;

          reconsider h1 = h as Element of ( EC_SetAffCo (z,p));

          reconsider g1 = (( compell_AffCo (z,p)) . h1) as Element of ( EC_SetAffCo (z,p));

          reconsider g = g1 as Element of F;

          set O = [ 0 , 1, 0 ];

          reconsider O as Element of F by ThAffCoZero;

          take g;

          

          thus (h * g) = ( 0_EC (z,p)) by ThAddCompAffCo

          .= ( 1_ F) by GP0;

          

          thus (g * h) = (( addell_AffCo (z,p)) . (h1,g1)) by ThCommutativeAffCo

          .= ( 0_EC (z,p)) by ThAddCompAffCo

          .= ( 1_ F) by GP0;

        end;

        for x,y be Element of F holds (x * y) = (y * x) by BINOP_1:def 2;

        hence thesis by P1, GROUP_1:def 2, GROUP_1:def 12;

      end;

    end

    theorem :: EC_PF_3:22

    

     ThAdd1: for P1,P2,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st P1 _EQ_ P2 holds (( addell_ProjCo (z,p)) . (P1,Q)) _EQ_ (( addell_ProjCo (z,p)) . (P2,Q))

    proof

      let P1,P2,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: P1 _EQ_ P2;

      reconsider O = [ 0 , 1, 0 ] as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) by EC_PF_1: 42;

      reconsider P1Q = (( addell_ProjCo (z,p)) . (P1,Q)), P2Q = (( addell_ProjCo (z,p)) . (P2,Q)) as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      reconsider g2 = (2 mod p), g3 = (3 mod p), g4 = (4 mod p), g8 = (8 mod p) as Element of ( GF p) by EC_PF_1: 14;

      per cases ;

        suppose

         B1: P1 _EQ_ O;

        then

         B2: (( addell_ProjCo (z,p)) . (P1,Q)) = Q by EC_PF_2:def 9;

        P2 _EQ_ O by A1, B1, EC_PF_1: 44;

        hence thesis by B2, EC_PF_2:def 9;

      end;

        suppose

         B1: Q _EQ_ O & not P1 _EQ_ O;

        then

         B2: (( addell_ProjCo (z,p)) . (P1,Q)) = P1 by EC_PF_2:def 9;

         not P2 _EQ_ O by A1, B1, EC_PF_1: 44;

        hence thesis by A1, B1, B2, EC_PF_2:def 9;

      end;

        suppose

         B1: not P1 _EQ_ O & not Q _EQ_ O & not P1 _EQ_ Q;

        consider PP1 be Element of ( ProjCo ( GF p)) such that

         B2: PP1 = P1 & PP1 in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

        consider PP2 be Element of ( ProjCo ( GF p)) such that

         B3: PP2 = P2 & PP2 in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

        consider a be Element of ( GF p) such that

         B4: a <> ( 0. ( GF p)) & (PP1 `1_3 ) = (a * (PP2 `1_3 )) & (PP1 `2_3 ) = (a * (PP2 `2_3 )) & (PP1 `3_3 ) = (a * (PP2 `3_3 )) by A1, B2, B3, EC_PF_1:def 10;

        

         B5: (P1 `1_3 ) = (PP1 `1_3 ) & (P1 `2_3 ) = (PP1 `2_3 ) & (P1 `3_3 ) = (PP1 `3_3 ) by B2, EC_PF_2: 32;

        (P1 `1_3 ) = (a * (PP2 `1_3 )) & (P1 `2_3 ) = (a * (PP2 `2_3 )) & (P1 `3_3 ) = (a * (PP2 `3_3 )) by B2, B4, EC_PF_2: 32;

        then

         B51: (P1 `1_3 ) = (a * (P2 `1_3 )) & (P1 `2_3 ) = (a * (P2 `2_3 )) & (P1 `3_3 ) = (a * (P2 `3_3 )) by B3, EC_PF_2: 32;

        set gf1P1 = (((Q `2_3 ) * (P1 `3_3 )) - ((P1 `2_3 ) * (Q `3_3 )));

        set gf2P1 = (((Q `1_3 ) * (P1 `3_3 )) - ((P1 `1_3 ) * (Q `3_3 )));

        set gf3P1 = (((((gf1P1 |^ 2) * (P1 `3_3 )) * (Q `3_3 )) - (gf2P1 |^ 3)) - (((g2 * (gf2P1 |^ 2)) * (P1 `1_3 )) * (Q `3_3 )));

        set gf1P2 = (((Q `2_3 ) * (P2 `3_3 )) - ((P2 `2_3 ) * (Q `3_3 )));

        set gf2P2 = (((Q `1_3 ) * (P2 `3_3 )) - ((P2 `1_3 ) * (Q `3_3 )));

        set gf3P2 = (((((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 )) - (gf2P2 |^ 3)) - (((g2 * (gf2P2 |^ 2)) * (P2 `1_3 )) * (Q `3_3 )));

        reconsider gf1P1, gf2P1, gf3P1, gf1P2, gf2P2, gf3P2 as Element of ( GF p);

        

         B6: gf1P1 = (((Q `2_3 ) * (a * (P2 `3_3 ))) - ((P1 `2_3 ) * (Q `3_3 ))) by B3, B4, B5, EC_PF_2: 32

        .= (((Q `2_3 ) * (a * (P2 `3_3 ))) - ((a * (P2 `2_3 )) * (Q `3_3 ))) by B3, B4, B5, EC_PF_2: 32

        .= ((a * ((Q `2_3 ) * (P2 `3_3 ))) - ((a * (P2 `2_3 )) * (Q `3_3 ))) by GROUP_1:def 3

        .= ((a * ((Q `2_3 ) * (P2 `3_3 ))) - (a * ((P2 `2_3 ) * (Q `3_3 )))) by GROUP_1:def 3

        .= (a * gf1P2) by VECTSP_1: 11;

        

         B7: gf2P1 = (((Q `1_3 ) * (a * (P2 `3_3 ))) - ((P1 `1_3 ) * (Q `3_3 ))) by B3, B4, B5, EC_PF_2: 32

        .= (((Q `1_3 ) * (a * (P2 `3_3 ))) - ((a * (P2 `1_3 )) * (Q `3_3 ))) by B3, B4, B5, EC_PF_2: 32

        .= ((a * ((Q `1_3 ) * (P2 `3_3 ))) - ((a * (P2 `1_3 )) * (Q `3_3 ))) by GROUP_1:def 3

        .= ((a * ((Q `1_3 ) * (P2 `3_3 ))) - (a * ((P2 `1_3 ) * (Q `3_3 )))) by GROUP_1:def 3

        .= (a * gf2P2) by VECTSP_1: 11;

        

         B8: gf3P1 = ((((((a |^ 2) * (gf1P2 |^ 2)) * (a * (P2 `3_3 ))) * (Q `3_3 )) - ((a * gf2P2) |^ 3)) - (((g2 * ((a * gf2P2) |^ 2)) * (P1 `1_3 )) * (Q `3_3 ))) by B6, B7, B51, BINOM: 9

        .= ((((((a |^ 2) * (gf1P2 |^ 2)) * (a * (P2 `3_3 ))) * (Q `3_3 )) - ((a |^ 3) * (gf2P2 |^ 3))) - (((g2 * ((a * gf2P2) |^ 2)) * (P1 `1_3 )) * (Q `3_3 ))) by BINOM: 9

        .= (((((((a |^ 2) * (gf1P2 |^ 2)) * a) * (P2 `3_3 )) * (Q `3_3 )) - ((a |^ 3) * (gf2P2 |^ 3))) - (((g2 * ((a * gf2P2) |^ 2)) * (P1 `1_3 )) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((((((a |^ 2) * a) * (gf1P2 |^ 2)) * (P2 `3_3 )) * (Q `3_3 )) - ((a |^ 3) * (gf2P2 |^ 3))) - (((g2 * ((a * gf2P2) |^ 2)) * (P1 `1_3 )) * (Q `3_3 ))) by GROUP_1:def 3

        .= ((((((a |^ (2 + 1)) * (gf1P2 |^ 2)) * (P2 `3_3 )) * (Q `3_3 )) - ((a |^ 3) * (gf2P2 |^ 3))) - (((g2 * ((a * gf2P2) |^ 2)) * (P1 `1_3 )) * (Q `3_3 ))) by EC_PF_1: 24

        .= ((((((a |^ 3) * (gf1P2 |^ 2)) * (P2 `3_3 )) * (Q `3_3 )) - ((a |^ 3) * (gf2P2 |^ 3))) - (((g2 * ((a |^ 2) * (gf2P2 |^ 2))) * (a * (P2 `1_3 ))) * (Q `3_3 ))) by B51, BINOM: 9

        .= ((((a |^ 3) * (((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 ))) - ((a |^ 3) * (gf2P2 |^ 3))) - (((g2 * ((a |^ 2) * (gf2P2 |^ 2))) * (a * (P2 `1_3 ))) * (Q `3_3 ))) by EC_PF_2: 11

        .= (((a |^ 3) * ((((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 )) - (gf2P2 |^ 3))) - (((g2 * ((a |^ 2) * (gf2P2 |^ 2))) * (a * (P2 `1_3 ))) * (Q `3_3 ))) by VECTSP_1: 11

        .= (((a |^ 3) * ((((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 )) - (gf2P2 |^ 3))) - ((((g2 * (a |^ 2)) * (gf2P2 |^ 2)) * (a * (P2 `1_3 ))) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((a |^ 3) * ((((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 )) - (gf2P2 |^ 3))) - ((((((a |^ 2) * g2) * (gf2P2 |^ 2)) * a) * (P2 `1_3 )) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((a |^ 3) * ((((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 )) - (gf2P2 |^ 3))) - ((((((a |^ 2) * a) * g2) * (gf2P2 |^ 2)) * (P2 `1_3 )) * (Q `3_3 ))) by EC_PF_2: 11

        .= (((a |^ 3) * ((((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 )) - (gf2P2 |^ 3))) - (((((a |^ (2 + 1)) * g2) * (gf2P2 |^ 2)) * (P2 `1_3 )) * (Q `3_3 ))) by EC_PF_1: 24

        .= (((a |^ 3) * ((((gf1P2 |^ 2) * (P2 `3_3 )) * (Q `3_3 )) - (gf2P2 |^ 3))) - ((a |^ 3) * (((g2 * (gf2P2 |^ 2)) * (P2 `1_3 )) * (Q `3_3 )))) by EC_PF_2: 11

        .= ((a |^ 3) * gf3P2) by VECTSP_1: 11;

        

         B9: P1Q = [(gf2P1 * gf3P1), ((gf1P1 * ((((gf2P1 |^ 2) * (P1 `1_3 )) * (Q `3_3 )) - gf3P1)) - (((gf2P1 |^ 3) * (P1 `2_3 )) * (Q `3_3 ))), (((gf2P1 |^ 3) * (P1 `3_3 )) * (Q `3_3 ))] by B1, EC_PF_2:def 9;

         not P2 _EQ_ O & not P2 _EQ_ Q by A1, B1, EC_PF_1: 44;

        then

         B10: P2Q = [(gf2P2 * gf3P2), ((gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2)) - (((gf2P2 |^ 3) * (P2 `2_3 )) * (Q `3_3 ))), (((gf2P2 |^ 3) * (P2 `3_3 )) * (Q `3_3 ))] by B1, EC_PF_2:def 9;

        consider PP1Q be Element of ( ProjCo ( GF p)) such that

         BX1: PP1Q = P1Q & PP1Q in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

        consider PP2Q be Element of ( ProjCo ( GF p)) such that

         BX2: PP2Q = P2Q & PP2Q in ( EC_SetProjCo ((z `1 ),(z `2 ),p));

        

         B11: (PP1Q `1_3 ) = (P1Q `1_3 ) by BX1, EC_PF_2: 32

        .= ((a * gf2P2) * ((a |^ 3) * gf3P2)) by B7, B8, B9, EC_PF_2:def 3

        .= (((a * gf2P2) * (a |^ 3)) * gf3P2) by GROUP_1:def 3

        .= ((((a |^ 3) * a) * gf2P2) * gf3P2) by GROUP_1:def 3

        .= (((a |^ (3 + 1)) * gf2P2) * gf3P2) by EC_PF_1: 24

        .= ((a |^ 4) * (gf2P2 * gf3P2)) by GROUP_1:def 3

        .= ((a |^ 4) * (P2Q `1_3 )) by B10, EC_PF_2:def 3

        .= ((a |^ 4) * (PP2Q `1_3 )) by BX2, EC_PF_2: 32;

        

         B12: (PP1Q `3_3 ) = (P1Q `3_3 ) by BX1, EC_PF_2: 32

        .= (((gf2P1 |^ 3) * (P1 `3_3 )) * (Q `3_3 )) by B9, EC_PF_2:def 5

        .= ((((a * gf2P2) |^ 3) * (a * (P2 `3_3 ))) * (Q `3_3 )) by B3, B4, B5, B7, EC_PF_2: 32

        .= ((((a |^ 3) * (gf2P2 |^ 3)) * (a * (P2 `3_3 ))) * (Q `3_3 )) by BINOM: 9

        .= (((((a |^ 3) * (gf2P2 |^ 3)) * a) * (P2 `3_3 )) * (Q `3_3 )) by GROUP_1:def 3

        .= (((((a |^ 3) * a) * (gf2P2 |^ 3)) * (P2 `3_3 )) * (Q `3_3 )) by GROUP_1:def 3

        .= ((((a |^ (3 + 1)) * (gf2P2 |^ 3)) * (P2 `3_3 )) * (Q `3_3 )) by EC_PF_1: 24

        .= ((a |^ 4) * (((gf2P2 |^ 3) * (P2 `3_3 )) * (Q `3_3 ))) by EC_PF_2: 11

        .= ((a |^ 4) * (P2Q `3_3 )) by B10, EC_PF_2:def 5

        .= ((a |^ 4) * (PP2Q `3_3 )) by BX2, EC_PF_2: 32;

        

         B13: (PP1Q `2_3 ) = (P1Q `2_3 ) by BX1, EC_PF_2: 32

        .= (((a * gf1P2) * (((((a * gf2P2) |^ 2) * (a * (P2 `1_3 ))) * (Q `3_3 )) - ((a |^ 3) * gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by B51, B6, B7, B8, B9, EC_PF_2:def 4

        .= (((a * gf1P2) * (((((a |^ 2) * (gf2P2 |^ 2)) * (a * (P2 `1_3 ))) * (Q `3_3 )) - ((a |^ 3) * gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by BINOM: 9

        .= (((a * gf1P2) * ((((((a |^ 2) * (gf2P2 |^ 2)) * a) * (P2 `1_3 )) * (Q `3_3 )) - ((a |^ 3) * gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((a * gf1P2) * ((((((a |^ 2) * a) * (gf2P2 |^ 2)) * (P2 `1_3 )) * (Q `3_3 )) - ((a |^ 3) * gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((a * gf1P2) * (((((a |^ (2 + 1)) * (gf2P2 |^ 2)) * (P2 `1_3 )) * (Q `3_3 )) - ((a |^ 3) * gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by EC_PF_1: 24

        .= (((a * gf1P2) * (((a |^ 3) * (((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 ))) - ((a |^ 3) * gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by EC_PF_2: 11

        .= (((a * gf1P2) * ((a |^ 3) * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by VECTSP_1: 11

        .= ((((a * gf1P2) * (a |^ 3)) * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2)) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((((a |^ 3) * a) * gf1P2) * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2)) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by GROUP_1:def 3

        .= ((((a |^ (3 + 1)) * gf1P2) * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2)) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by EC_PF_1: 24

        .= (((a |^ 4) * (gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2))) - ((((a * gf2P2) |^ 3) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((a |^ 4) * (gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2))) - ((((a |^ 3) * (gf2P2 |^ 3)) * (a * (P2 `2_3 ))) * (Q `3_3 ))) by BINOM: 9

        .= (((a |^ 4) * (gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2))) - (((((a |^ 3) * (gf2P2 |^ 3)) * a) * (P2 `2_3 )) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((a |^ 4) * (gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2))) - (((((a |^ 3) * a) * (gf2P2 |^ 3)) * (P2 `2_3 )) * (Q `3_3 ))) by GROUP_1:def 3

        .= (((a |^ 4) * (gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2))) - ((((a |^ (3 + 1)) * (gf2P2 |^ 3)) * (P2 `2_3 )) * (Q `3_3 ))) by EC_PF_1: 24

        .= (((a |^ 4) * (gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2))) - ((a |^ 4) * (((gf2P2 |^ 3) * (P2 `2_3 )) * (Q `3_3 )))) by EC_PF_2: 11

        .= ((a |^ 4) * ((gf1P2 * ((((gf2P2 |^ 2) * (P2 `1_3 )) * (Q `3_3 )) - gf3P2)) - (((gf2P2 |^ 3) * (P2 `2_3 )) * (Q `3_3 )))) by VECTSP_1: 11

        .= ((a |^ 4) * (P2Q `2_3 )) by B10, EC_PF_2:def 4

        .= ((a |^ 4) * (PP2Q `2_3 )) by BX2, EC_PF_2: 32;

        (a |^ 4) <> 0 by B4, EC_PF_1: 25;

        then (a |^ 4) <> ( 0. ( GF p)) by EC_PF_1: 11;

        hence thesis by B11, B12, B13, BX1, BX2, EC_PF_1:def 10;

      end;

        suppose

         B1: not P1 _EQ_ O & not Q _EQ_ O & P1 _EQ_ Q;

        then

         B2: not P2 _EQ_ O & P2 _EQ_ Q by A1, EC_PF_1: 44;

        reconsider gf1 = (((z `1 ) * ((Q `3_3 ) |^ 2)) + (g3 * ((Q `1_3 ) |^ 2))), gf2 = ((Q `2_3 ) * (Q `3_3 )) as Element of ( GF p);

        reconsider gf3 = (((Q `1_3 ) * (Q `2_3 )) * gf2) as Element of ( GF p);

        reconsider gf4 = ((gf1 |^ 2) - (g8 * gf3)) as Element of ( GF p);

        (( addell_ProjCo (z,p)) . (Q,P1)) = [((g2 * gf4) * gf2), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((Q `2_3 ) |^ 2)) * (gf2 |^ 2))), (g8 * (gf2 |^ 3))] by B1, EC_PF_2:def 9

        .= (( addell_ProjCo (z,p)) . (Q,P2)) by B1, B2, EC_PF_2:def 9;

        then

         B4: P1Q _EQ_ (( addell_ProjCo (z,p)) . (Q,P2)) by ThCommutativeProjCo;

        P2Q _EQ_ (( addell_ProjCo (z,p)) . (Q,P2)) by ThCommutativeProjCo;

        hence thesis by B4, EC_PF_1: 44;

      end;

    end;

    theorem :: EC_PF_3:23

    

     ThAdd2: for P,Q1,Q2 be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st Q1 _EQ_ Q2 holds (( addell_ProjCo (z,p)) . (P,Q1)) _EQ_ (( addell_ProjCo (z,p)) . (P,Q2))

    proof

      let P,Q1,Q2 be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: Q1 _EQ_ Q2;

      

       A2: (( addell_ProjCo (z,p)) . (P,Q1)) _EQ_ (( addell_ProjCo (z,p)) . (Q1,P)) by ThCommutativeProjCo;

      (( addell_ProjCo (z,p)) . (Q1,P)) _EQ_ (( addell_ProjCo (z,p)) . (Q2,P)) by A1, ThAdd1;

      then

       A3: (( addell_ProjCo (z,p)) . (P,Q1)) _EQ_ (( addell_ProjCo (z,p)) . (Q2,P)) by A2, EC_PF_1: 44;

      (( addell_ProjCo (z,p)) . (Q2,P)) _EQ_ (( addell_ProjCo (z,p)) . (P,Q2)) by ThCommutativeProjCo;

      hence thesis by A3, EC_PF_1: 44;

    end;

    theorem :: EC_PF_3:24

    

     ThAdd3: for P1,P2,Q1,Q2 be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st P1 _EQ_ P2 & Q1 _EQ_ Q2 holds (( addell_ProjCo (z,p)) . (P1,Q1)) _EQ_ (( addell_ProjCo (z,p)) . (P2,Q2))

    proof

      let P1,P2,Q1,Q2 be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: P1 _EQ_ P2 & Q1 _EQ_ Q2;

      

       A2: (( addell_ProjCo (z,p)) . (P1,Q1)) _EQ_ (( addell_ProjCo (z,p)) . (P2,Q1)) by A1, ThAdd1;

      (( addell_ProjCo (z,p)) . (P2,Q1)) _EQ_ (( addell_ProjCo (z,p)) . (P2,Q2)) by A1, ThAdd2;

      hence thesis by A2, EC_PF_1: 44;

    end;

    theorem :: EC_PF_3:25

    

     ThCompellO: for P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st O = [ 0 , 1, 0 ] holds P _EQ_ O iff (( compell_ProjCo (z,p)) . P) _EQ_ O

    proof

      let P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: O = [ 0 , 1, 0 ];

      hereby

        assume P _EQ_ O;

        then

         B2: (( compell_ProjCo (z,p)) . P) _EQ_ (( compell_ProjCo (z,p)) . O) by EC_PF_2: 46;

        (( compell_ProjCo (z,p)) . O) _EQ_ O by A1, EC_PF_2: 40;

        hence (( compell_ProjCo (z,p)) . P) _EQ_ O by B2, EC_PF_1: 44;

      end;

      assume (( compell_ProjCo (z,p)) . P) _EQ_ O;

      then

       B2: P _EQ_ (( compell_ProjCo (z,p)) . O) by EC_PF_2: 47;

      (( compell_ProjCo (z,p)) . O) _EQ_ O by A1, EC_PF_2: 40;

      hence P _EQ_ O by B2, EC_PF_1: 44;

    end;

    theorem :: EC_PF_3:26

    

     ThEQX: for P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)), a be Element of ( GF p) st a <> ( 0. ( GF p)) & (P `1_3 ) = (a * (Q `1_3 )) & (P `2_3 ) = (a * (Q `2_3 )) & (P `3_3 ) = (a * (Q `3_3 )) holds P _EQ_ Q

    proof

      let P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)), a be Element of ( GF p) such that

       A1: a <> ( 0. ( GF p)) and

       A2: (P `1_3 ) = (a * (Q `1_3 )) & (P `2_3 ) = (a * (Q `2_3 )) & (P `3_3 ) = (a * (Q `3_3 ));

      reconsider PP = P, QQ = Q as Element of ( ProjCo ( GF p));

      

       A3: (PP `1_3 ) = (a * (Q `1_3 )) by A2, EC_PF_2: 32

      .= (a * (QQ `1_3 )) by EC_PF_2: 32;

      

       A4: (PP `2_3 ) = (a * (Q `2_3 )) by A2, EC_PF_2: 32

      .= (a * (QQ `2_3 )) by EC_PF_2: 32;

      (PP `3_3 ) = (a * (Q `3_3 )) by A2, EC_PF_2: 32

      .= (a * (QQ `3_3 )) by EC_PF_2: 32;

      hence thesis by A1, A3, A4, EC_PF_1:def 10;

    end;

    theorem :: EC_PF_3:27

    

     LmAddEll1: for P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)), g2,gf1,gf2,gf3 be Element of ( GF p) st not P _EQ_ Q & (P `3_3 ) = 1 & (Q `3_3 ) = 1 & g2 = (2 mod p) & gf1 = ((Q `2_3 ) - (P `2_3 )) & gf2 = ((Q `1_3 ) - (P `1_3 )) & gf3 = (((gf1 |^ 2) - (gf2 |^ 3)) - ((g2 * (gf2 |^ 2)) * (P `1_3 ))) holds (( addell_ProjCo (z,p)) . (P,Q)) = [(gf2 * gf3), ((gf1 * (((gf2 |^ 2) * (P `1_3 )) - gf3)) - ((gf2 |^ 3) * (P `2_3 ))), (gf2 |^ 3)]

    proof

      let P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)), g2,gf1,gf2,gf3 be Element of ( GF p) such that

       A1: not P _EQ_ Q & (P `3_3 ) = 1 & (Q `3_3 ) = 1 and

       A2: g2 = (2 mod p) and

       A3: gf1 = ((Q `2_3 ) - (P `2_3 )) & gf2 = ((Q `1_3 ) - (P `1_3 )) & gf3 = (((gf1 |^ 2) - (gf2 |^ 3)) - ((g2 * (gf2 |^ 2)) * (P `1_3 )));

      reconsider O = [ 0 , 1, 0 ] as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) by EC_PF_1: 42;

      

       A4: not P _EQ_ O by A1, ThEQO;

      

       A5: not Q _EQ_ O by A1, ThEQO;

      

       A6: (((Q `2_3 ) * (P `3_3 )) - ((P `2_3 ) * (Q `3_3 ))) = ((Q `2_3 ) - ((P `2_3 ) * ( 1. ( GF p)))) by A1

      .= gf1 by A3;

      

       A7: (((Q `1_3 ) * (P `3_3 )) - ((P `1_3 ) * (Q `3_3 ))) = ((Q `1_3 ) - ((P `1_3 ) * ( 1. ( GF p)))) by A1

      .= gf2 by A3;

      (((((gf1 |^ 2) * (P `3_3 )) * (Q `3_3 )) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3 )) * (Q `3_3 ))) = (((gf1 |^ 2) - (gf2 |^ 3)) - (((g2 * (gf2 |^ 2)) * (P `1_3 )) * ( 1. ( GF p)))) by A1

      .= gf3 by A3;

      

      hence (( addell_ProjCo (z,p)) . (P,Q)) = [(gf2 * gf3), ((gf1 * ((((gf2 |^ 2) * (P `1_3 )) * ( 1. ( GF p))) - gf3)) - (((gf2 |^ 3) * (P `2_3 )) * (Q `3_3 ))), (((gf2 |^ 3) * (P `3_3 )) * (Q `3_3 ))] by A1, A2, A4, A5, A6, A7, EC_PF_2:def 9

      .= [(gf2 * gf3), ((gf1 * (((gf2 |^ 2) * (P `1_3 )) - gf3)) - ((gf2 |^ 3) * (P `2_3 ))), (gf2 |^ 3)] by A1;

    end;

    theorem :: EC_PF_3:28

    

     LmAddEll2: for P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)), g2,g3,g4,g8,gf1,gf2,gf3,gf4 be Element of ( GF p) st P _EQ_ Q & (P `3_3 ) = 1 & (Q `3_3 ) = 1 & g2 = (2 mod p) & g3 = (3 mod p) & g4 = (4 mod p) & g8 = (8 mod p) & gf1 = ((z `1 ) + (g3 * ((P `1_3 ) |^ 2))) & gf2 = (P `2_3 ) & gf3 = (((P `1_3 ) * (P `2_3 )) * gf2) & gf4 = ((gf1 |^ 2) - (g8 * gf3)) holds (( addell_ProjCo (z,p)) . (P,Q)) = [((g2 * gf4) * gf2), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), (g8 * (gf2 |^ 3))]

    proof

      let P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)), g2,g3,g4,g8,gf1,gf2,gf3,gf4 be Element of ( GF p) such that

       A1: P _EQ_ Q & (P `3_3 ) = 1 & (Q `3_3 ) = 1 and

       A2: g2 = (2 mod p) & g3 = (3 mod p) & g4 = (4 mod p) & g8 = (8 mod p) and

       A3: gf1 = ((z `1 ) + (g3 * ((P `1_3 ) |^ 2))) & gf2 = (P `2_3 ) & gf3 = (((P `1_3 ) * (P `2_3 )) * gf2) & gf4 = ((gf1 |^ 2) - (g8 * gf3));

      reconsider O = [ 0 , 1, 0 ] as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) by EC_PF_1: 42;

      

       A4: not P _EQ_ O by A1, ThEQO;

      

       A5: not Q _EQ_ O by A1, ThEQO;

      

       A6: (((z `1 ) * ((P `3_3 ) |^ 2)) + (g3 * ((P `1_3 ) |^ 2))) = (((z `1 ) * ((P `3_3 ) * (P `3_3 ))) + (g3 * ((P `1_3 ) |^ 2))) by EC_PF_1: 22

      .= (((z `1 ) * ( 1. ( GF p))) + (g3 * ((P `1_3 ) |^ 2))) by A1

      .= gf1 by A3;

      ((P `2_3 ) * (P `3_3 )) = ((P `2_3 ) * ( 1. ( GF p))) by A1

      .= gf2 by A3;

      hence (( addell_ProjCo (z,p)) . (P,Q)) = [((g2 * gf4) * gf2), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), (g8 * (gf2 |^ 3))] by A1, A2, A3, A4, A5, A6, EC_PF_2:def 9;

    end;

    theorem :: EC_PF_3:29

    

     LmCompAddCom: for P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st (P `3_3 ) = 1 & (Q `3_3 ) = 1 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)))

    proof

      let P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A3: (P `3_3 ) = 1 & (Q `3_3 ) = 1;

      reconsider CP = (( compell_ProjCo (z,p)) . P), CQ = (( compell_ProjCo (z,p)) . Q) as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      

       A4: CP = [(P `1_3 ), ( - (P `2_3 )), (P `3_3 )] & CQ = [(Q `1_3 ), ( - (Q `2_3 )), (Q `3_3 )] by EC_PF_2:def 8;

      then

       A5: (CP `3_3 ) = 1 & (CQ `3_3 ) = 1 by A3, EC_PF_2:def 5;

      

       A6: (CP `1_3 ) = (P `1_3 ) & (CP `2_3 ) = ( - (P `2_3 )) by A4, EC_PF_2: 33;

      

       A7: (CQ `1_3 ) = (Q `1_3 ) & (CQ `2_3 ) = ( - (Q `2_3 )) by A4, EC_PF_2: 33;

      reconsider PQ = (( addell_ProjCo (z,p)) . (P,Q)) as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      reconsider CP = (( compell_ProjCo (z,p)) . P), CQ = (( compell_ProjCo (z,p)) . Q) as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      per cases ;

        suppose

         B1: not P _EQ_ Q;

        reconsider g2 = (2 mod p) as Element of ( GF p) by EC_PF_1: 14;

        reconsider gf1 = ((Q `2_3 ) - (P `2_3 )) as Element of ( GF p);

        reconsider gf2 = ((Q `1_3 ) - (P `1_3 )) as Element of ( GF p);

        reconsider gf3 = (((gf1 |^ 2) - (gf2 |^ 3)) - ((g2 * (gf2 |^ 2)) * (P `1_3 ))) as Element of ( GF p);

        reconsider gf1C = ((CQ `2_3 ) - (CP `2_3 )) as Element of ( GF p);

        reconsider gf2C = ((CQ `1_3 ) - (CP `1_3 )) as Element of ( GF p);

        reconsider gf3C = (((gf1C |^ 2) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3 ))) as Element of ( GF p);

        

         B2: gf1C = (( - (Q `2_3 )) - ( - (P `2_3 ))) by A4, A7, EC_PF_2: 33

        .= ( - (( - (P `2_3 )) + (Q `2_3 ))) by RLVECT_1: 31

        .= ( - gf1);

        

         B3: gf2C = ((Q `1_3 ) - (CP `1_3 )) by A4, EC_PF_2: 33

        .= gf2 by A4, EC_PF_2: 33;

        

         B4: gf3C = (((gf1C * gf1C) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3 ))) by EC_PF_1: 22

        .= (((gf1 * gf1) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3 ))) by B2, EC_PF_1: 26

        .= (((gf1 |^ 2) - (gf2C |^ 3)) - ((g2 * (gf2C |^ 2)) * (CP `1_3 ))) by EC_PF_1: 22

        .= gf3 by A4, B3, EC_PF_2: 33;

        

         B5: PQ = [(gf2 * gf3), ((gf1 * (((gf2 |^ 2) * (P `1_3 )) - gf3)) - ((gf2 |^ 3) * (P `2_3 ))), (gf2 |^ 3)] by A3, B1, LmAddEll1;

        (( addell_ProjCo (z,p)) . (CP,CQ)) = [(gf2C * gf3C), ((gf1C * (((gf2C |^ 2) * (CP `1_3 )) - gf3C)) - ((gf2C |^ 3) * (CP `2_3 ))), (gf2C |^ 3)] by A5, B1, LmAddEll1, EC_PF_2: 46

        .= [(gf2 * gf3), ((( - gf1) * (((gf2 |^ 2) * (P `1_3 )) - gf3)) - ( - ((gf2 |^ 3) * (P `2_3 )))), (gf2 |^ 3)] by A6, B2, B3, B4, VECTSP_1: 8

        .= [(gf2 * gf3), (( - (gf1 * (((gf2 |^ 2) * (P `1_3 )) - gf3))) - ( - ((gf2 |^ 3) * (P `2_3 )))), (gf2 |^ 3)] by VECTSP_1: 8

        .= [(gf2 * gf3), ( - ((gf1 * (((gf2 |^ 2) * (P `1_3 )) - gf3)) + ( - ((gf2 |^ 3) * (P `2_3 ))))), (gf2 |^ 3)] by RLVECT_1: 31

        .= [(PQ `1_3 ), ( - ((gf1 * (((gf2 |^ 2) * (P `1_3 )) - gf3)) - ((gf2 |^ 3) * (P `2_3 )))), (gf2 |^ 3)] by B5, EC_PF_2: 33

        .= [(PQ `1_3 ), ( - (PQ `2_3 )), (gf2 |^ 3)] by B5, EC_PF_2: 33

        .= [(PQ `1_3 ), ( - (PQ `2_3 )), (PQ `3_3 )] by B5, EC_PF_2: 33;

        hence thesis by EC_PF_2:def 8;

      end;

        suppose

         B1: P _EQ_ Q;

        reconsider g2 = (2 mod p), g3 = (3 mod p), g4 = (4 mod p), g8 = (8 mod p) as Element of ( GF p) by EC_PF_1: 14;

        reconsider gf1 = ((z `1 ) + (g3 * ((P `1_3 ) |^ 2))), gf2 = (P `2_3 ) as Element of ( GF p);

        reconsider gf3 = (((P `1_3 ) * (P `2_3 )) * gf2) as Element of ( GF p);

        reconsider gf4 = ((gf1 |^ 2) - (g8 * gf3)) as Element of ( GF p);

        reconsider gf1C = ((z `1 ) + (g3 * ((CP `1_3 ) |^ 2))), gf2C = (CP `2_3 ) as Element of ( GF p);

        reconsider gf3C = (((CP `1_3 ) * (CP `2_3 )) * gf2C) as Element of ( GF p);

        reconsider gf4C = ((gf1C |^ 2) - (g8 * gf3C)) as Element of ( GF p);

        

         B2: gf1C = gf1 by A4, EC_PF_2: 33;

        

         B3: gf2C = ( - gf2) by A4, EC_PF_2: 33;

        

         B4: gf3C = ((P `1_3 ) * (( - (P `2_3 )) * ( - gf2))) by A6, GROUP_1:def 3

        .= ((P `1_3 ) * ((P `2_3 ) * gf2)) by VECTSP_1: 10

        .= gf3 by GROUP_1:def 3;

        

         B6: (gf2C |^ 2) = (gf2C * gf2C) by EC_PF_1: 22

        .= (gf2 * gf2) by B3, EC_PF_1: 26

        .= (gf2 |^ 2) by EC_PF_1: 22;

        

         B7: ((CP `2_3 ) |^ 2) = ((CP `2_3 ) * (CP `2_3 )) by EC_PF_1: 22

        .= ((P `2_3 ) * (P `2_3 )) by A6, EC_PF_1: 26

        .= ((P `2_3 ) |^ 2) by EC_PF_1: 22;

        

         B8: (gf2C |^ 3) = (gf2C |^ (2 + 1))

        .= ((gf2C |^ 2) * gf2C) by EC_PF_1: 24

        .= ( - ((gf2 |^ 2) * gf2)) by B3, B6, VECTSP_1: 8

        .= ( - (gf2 |^ (2 + 1))) by EC_PF_1: 24

        .= ( - (gf2 |^ 3));

        

         B9: PQ = [((g2 * gf4) * gf2), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), (g8 * (gf2 |^ 3))] by A3, B1, LmAddEll2;

        

         B11: (( addell_ProjCo (z,p)) . (CP,CQ)) = [((g2 * gf4C) * gf2C), ((gf1C * ((g4 * gf3C) - gf4C)) - ((g8 * ((CP `2_3 ) |^ 2)) * (gf2C |^ 2))), (g8 * (gf2C |^ 3))] by A5, B1, LmAddEll2, EC_PF_2: 46

        .= [( - ((g2 * gf4) * gf2)), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), (g8 * ( - (gf2 |^ 3)))] by B2, B3, B4, B7, B8, VECTSP_1: 8

        .= [( - ((g2 * gf4) * gf2)), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), ( - (g8 * (gf2 |^ 3)))] by VECTSP_1: 8

        .= [( - (PQ `1_3 )), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), ( - (g8 * (gf2 |^ 3)))] by B9, EC_PF_2: 33

        .= [( - (PQ `1_3 )), (PQ `2_3 ), ( - (g8 * (gf2 |^ 3)))] by B9, EC_PF_2: 33

        .= [( - (PQ `1_3 )), (PQ `2_3 ), ( - (PQ `3_3 ))] by B9, EC_PF_2: 33;

        

         B12: (( compell_ProjCo (z,p)) . PQ) = [(PQ `1_3 ), ( - (PQ `2_3 )), (PQ `3_3 )] by EC_PF_2:def 8;

        

         B13: ((( addell_ProjCo (z,p)) . (CP,CQ)) `1_3 ) = ( - (( 1. ( GF p)) * (PQ `1_3 ))) by B11, EC_PF_2: 33

        .= (( - ( 1. ( GF p))) * (PQ `1_3 )) by VECTSP_1: 9

        .= (( - ( 1. ( GF p))) * ((( compell_ProjCo (z,p)) . PQ) `1_3 )) by B12, EC_PF_2: 33;

        

         B14: ((( addell_ProjCo (z,p)) . (CP,CQ)) `2_3 ) = (( 1. ( GF p)) * (PQ `2_3 )) by B11, EC_PF_2: 33

        .= (( - ( 1. ( GF p))) * ( - (PQ `2_3 ))) by VECTSP_1: 10

        .= (( - ( 1. ( GF p))) * ((( compell_ProjCo (z,p)) . PQ) `2_3 )) by B12, EC_PF_2: 33;

        

         B15: ((( addell_ProjCo (z,p)) . (CP,CQ)) `3_3 ) = ( - (( 1. ( GF p)) * (PQ `3_3 ))) by B11, EC_PF_2: 33

        .= (( - ( 1. ( GF p))) * (PQ `3_3 )) by VECTSP_1: 9

        .= (( - ( 1. ( GF p))) * ((( compell_ProjCo (z,p)) . PQ) `3_3 )) by B12, EC_PF_2: 33;

        ( - ( 1. ( GF p))) <> ( 0. ( GF p))

        proof

          assume ( - ( 1. ( GF p))) = ( 0. ( GF p));

          then (( 1. ( GF p)) - ( 1. ( GF p))) = ( 1. ( GF p)) by RLVECT_1: 4;

          then ( 0. ( GF p)) = ( 1. ( GF p)) by RLVECT_1: 15;

          hence contradiction;

        end;

        hence thesis by B13, B14, B15, ThEQX;

      end;

    end;

    theorem :: EC_PF_3:30

    for P,Q be 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)))

    proof

      let P,Q be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p));

      reconsider O = [ 0 , 1, 0 ] as Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) by EC_PF_1: 42;

      per cases ;

        suppose

         A1: P _EQ_ O;

        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 thesis by A2, EC_PF_2:def 9;

      end;

        suppose

         A1: not P _EQ_ O & Q _EQ_ O;

        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 thesis by A2, A3, EC_PF_2:def 9;

      end;

        suppose

         A1: not P _EQ_ O & not Q _EQ_ O;

        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 thesis by A6, EC_PF_1: 44;

      end;

    end;

    theorem :: EC_PF_3:31

    for P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) st O = [ 0 , 1, 0 ] & not P _EQ_ O holds ((P `2_3 ) = ( 0. ( GF p)) iff (( addell_ProjCo (z,p)) . (P,P)) _EQ_ O)

    proof

      let P,O be Element of ( EC_SetProjCo ((z `1 ),(z `2 ),p)) such that

       A1: O = [ 0 , 1, 0 ] and

       A2: not P _EQ_ O;

      reconsider g2 = (2 mod p), g3 = (3 mod p), g4 = (4 mod p), g8 = (8 mod p) as Element of ( GF p) by EC_PF_1: 14;

      set gf1 = (((z `1 ) * ((P `3_3 ) |^ 2)) + (g3 * ((P `1_3 ) |^ 2)));

      set gf2 = ((P `2_3 ) * (P `3_3 ));

      set gf3 = (((P `1_3 ) * (P `2_3 )) * gf2);

      set gf4 = ((gf1 |^ 2) - (g8 * gf3));

      

       A3: (( addell_ProjCo (z,p)) . (P,P)) = [((g2 * gf4) * gf2), ((gf1 * ((g4 * gf3) - gf4)) - ((g8 * ((P `2_3 ) |^ 2)) * (gf2 |^ 2))), (g8 * (gf2 |^ 3))] by A1, A2, EC_PF_2:def 9;

      hereby

        assume (P `2_3 ) = ( 0. ( GF p));

        

        then (g8 * (gf2 |^ 3)) = (g8 * (( 0. ( GF p)) |^ (2 + 1)))

        .= (g8 * ((( 0. ( GF p)) |^ 2) * ( 0. ( GF p)))) by EC_PF_1: 24

        .= ( 0. ( GF p));

        

        then ((( addell_ProjCo (z,p)) . (P,P)) `3_3 ) = ( 0. ( GF p)) by A3, EC_PF_2:def 5

        .= 0 by EC_PF_1: 11;

        hence (( addell_ProjCo (z,p)) . (P,P)) _EQ_ O by A1, ThEQO;

      end;

      assume (( addell_ProjCo (z,p)) . (P,P)) _EQ_ O;

      

      then

       B1: ((( addell_ProjCo (z,p)) . (P,P)) `3_3 ) = 0 by A1, ThEQO

      .= ( 0. ( GF p)) by EC_PF_1: 11;

      

       B2: ((( addell_ProjCo (z,p)) . (P,P)) `3_3 ) = (g8 * (gf2 |^ 3)) by A3, EC_PF_2:def 5;

      g8 <> ( 0. ( GF p))

      proof

        

         C1: (g2 |^ 3) = ((2 |^ (2 + 1)) mod p) by EC_PF_1: 23

        .= (((2 |^ (1 + 1)) * 2) mod p) by NEWTON: 6

        .= ((((2 |^ 1) * 2) * 2) mod p) by NEWTON: 6

        .= g8;

        p >= (3 + 2) by EC_PF_2:def 1;

        then p > 2 by XXREAL_0: 2;

        hence thesis by C1, EC_PF_2: 28;

      end;

      

      then (gf2 |^ 3) = ( 0. ( GF p)) by B1, B2, VECTSP_1: 12

      .= 0 by EC_PF_1: 11;

      then

       B4: gf2 = ( 0. ( GF p)) by EC_PF_1: 25;

      (P `3_3 ) <> 0 by A1, A2, ThEQO;

      then (P `3_3 ) <> ( 0. ( GF p)) by EC_PF_1: 11;

      hence (P `2_3 ) = ( 0. ( GF p)) by B4, VECTSP_1: 12;

    end;