let p be 5 _or_greater Prime; 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; 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); ( O = [0,1,0] implies (addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ O )
assume A1:
O = [0,1,0]
; (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
;
(addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ Othen 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
;
(addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ Othen 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;
verum end; suppose C1:
not
P _EQ_ Q
;
(addell_ProjCo (z,p)) . (P,((compell_ProjCo (z,p)) . P)) _EQ_ Oreconsider 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;
verum end; end;