let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p
for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
(addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O
let z be Element of EC_WParam p; :: thesis: for P, O being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] holds
(addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O
set a = z `1 ;
set b = z `2 ;
let P, O be Element of EC_SetProjCo ((z `1),(z `2),p); :: thesis: ( O = [0,1,0] implies (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O )
assume A1: O = [0,1,0] ; :: thesis: (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O
set Q = (compell_ProjCo (z,p)) . P;
reconsider Q = (compell_ProjCo (z,p)) . P as Element of EC_SetProjCo ((z `1),(z `2),p) ;
consider OO being Element of ProjCo (GF p) such that
A3: ( OO = O & OO in EC_SetProjCo ((z `1),(z `2),p) ) ;

per cases ( P `3_3 = 0 or P `3_3 <> 0 ) ;

suppose B1: P `3_3 = 0 ; :: thesis: (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O

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 (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O by A1, B2, EC_PF_2:def 9; :: thesis: verum

end;

suppose B1: P `3_3 <> 0 ; :: thesis: (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O

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 ( P _EQ_ Q or not P _EQ_ Q ) ;

suppose C1: P _EQ_ Q ; :: thesis: (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O

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 = ((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)) * ((P `2_3) * (P `3_3));
set gf4 = ((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3))));
reconsider gf1 = ((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2)), gf2 = (P `2_3) * (P `3_3), gf3 = ((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)), gf4 = ((((z `1) * ((P `3_3) |^ 2)) + (g3 * ((P `1_3) |^ 2))) |^ 2) - (g8 * (((P `1_3) * (P `2_3)) * ((P `2_3) * (P `3_3)))) as Element of (GF p) ;
set R = (addell_ProjCo (z,p)) . (P,Q);
C7: (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, B2, B4, C1, EC_PF_2:def 9;
reconsider R = (addell_ProjCo (z,p)) . (P,Q) as Element of EC_SetProjCo ((z `1),(z `2),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 = R `2_3 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 being Element of ProjCo (GF p) such that
C23: ( RR = R & RR in EC_SetProjCo ((z `1),(z `2),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 (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O by A3, C15, C23, EC_PF_1:def 10, VECTSP_2:3; :: thesis: verum

end;

suppose C1: not P _EQ_ Q ; :: thesis: (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O

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 = (((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3));
reconsider gf1 = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)), gf2 = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)), gf3 = (((((((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3))) |^ 2) * (P `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3))) |^ 2)) * (P `1_3)) * (Q `3_3)) as Element of (GF p) ;
set R = (addell_ProjCo (z,p)) . (P,Q);
C3: (addell_ProjCo (z,p)) . (P,Q) = [(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: ((addell_ProjCo (z,p)) . (P,Q)) `2_3 <> 0 by C3, C10, EC_PF_2:def 4;
C13: ((addell_ProjCo (z,p)) . (P,Q)) `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 = ((addell_ProjCo (z,p)) . (P,Q)) `2_3 ;
reconsider d = ((addell_ProjCo (z,p)) . (P,Q)) `2_3 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) = ((addell_ProjCo (z,p)) . (P,Q)) `1_3 by C3, C5, C15, EC_PF_2:def 3;
C18: d * (OO `2_3) = d * (1. (GF p)) by C15
.= ((addell_ProjCo (z,p)) . (P,Q)) `2_3 ;
consider RR being Element of ProjCo (GF p) such that
C19: ( RR = (addell_ProjCo (z,p)) . (P,Q) & RR in EC_SetProjCo ((z `1),(z `2),p) ) ;
( RR `1_3 = ((addell_ProjCo (z,p)) . (P,Q)) `1_3 & RR `2_3 = ((addell_ProjCo (z,p)) . (P,Q)) `2_3 & RR `3_3 = ((addell_ProjCo (z,p)) . (P,Q)) `3_3 ) by C19, EC_PF_2:32;
hence (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O by A3, C6, C11, C13, C15, C16, C18, C19, EC_PF_1:def 10; :: thesis: verum

end;

end;

end;

end;