let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for P, Q being 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))
let z be Element of EC_WParam p; for P, Q being 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))
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); ( P `3_3 = 1 & Q `3_3 = 1 implies (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)) )
assume A3:
( P `3_3 = 1 & Q `3_3 = 1 )
; (compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))
reconsider 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
( not P _EQ_ Q or P _EQ_ Q )
;
suppose B1:
not
P _EQ_ Q
;
(compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))reconsider 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
(compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (
((compell_ProjCo (z,p)) . P),
((compell_ProjCo (z,p)) . Q))
by EC_PF_2:def 8;
verum end; suppose B1:
P _EQ_ Q
;
(compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (((compell_ProjCo (z,p)) . P),((compell_ProjCo (z,p)) . Q))reconsider 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)
hence
(compell_ProjCo (z,p)) . ((addell_ProjCo (z,p)) . (P,Q)) _EQ_ (addell_ProjCo (z,p)) . (
((compell_ProjCo (z,p)) . P),
((compell_ProjCo (z,p)) . Q))
by B13, B14, B15, ThEQX;
verum end;