let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for P1, P2, Q being 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)
let z be Element of EC_WParam p; for P1, P2, Q being 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)
let P1, P2, Q be Element of EC_SetProjCo ((z `1),(z `2),p); ( P1 _EQ_ P2 implies (addell_ProjCo (z,p)) . (P1,Q) _EQ_ (addell_ProjCo (z,p)) . (P2,Q) )
assume A1:
P1 _EQ_ P2
; (addell_ProjCo (z,p)) . (P1,Q) _EQ_ (addell_ProjCo (z,p)) . (P2,Q)
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
( P1 _EQ_ O or ( Q _EQ_ O & not P1 _EQ_ O ) or ( not P1 _EQ_ O & not Q _EQ_ O & not P1 _EQ_ Q ) or ( not P1 _EQ_ O & not Q _EQ_ O & P1 _EQ_ Q ) )
;
suppose B1:
(
Q _EQ_ O & not
P1 _EQ_ O )
;
(addell_ProjCo (z,p)) . (P1,Q) _EQ_ (addell_ProjCo (z,p)) . (P2,Q)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
(addell_ProjCo (z,p)) . (
P1,
Q)
_EQ_ (addell_ProjCo (z,p)) . (
P2,
Q)
by A1, B1, B2, EC_PF_2:def 9;
verum end; suppose B1:
( not
P1 _EQ_ O & not
Q _EQ_ O & not
P1 _EQ_ Q )
;
(addell_ProjCo (z,p)) . (P1,Q) _EQ_ (addell_ProjCo (z,p)) . (P2,Q)consider PP1 being
Element of
ProjCo (GF p) such that B2:
(
PP1 = P1 &
PP1 in EC_SetProjCo (
(z `1),
(z `2),
p) )
;
consider PP2 being
Element of
ProjCo (GF p) such that B3:
(
PP2 = P2 &
PP2 in EC_SetProjCo (
(z `1),
(z `2),
p) )
;
consider a being
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 =
(((((((Q `2_3) * (P1 `3_3)) - ((P1 `2_3) * (Q `3_3))) |^ 2) * (P1 `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P1 `3_3)) - ((P1 `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P1 `3_3)) - ((P1 `1_3) * (Q `3_3))) |^ 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 =
(((((((Q `2_3) * (P2 `3_3)) - ((P2 `2_3) * (Q `3_3))) |^ 2) * (P2 `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P2 `3_3)) - ((P2 `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P2 `3_3)) - ((P2 `1_3) * (Q `3_3))) |^ 2)) * (P2 `1_3)) * (Q `3_3));
reconsider gf1P1 =
((Q `2_3) * (P1 `3_3)) - ((P1 `2_3) * (Q `3_3)),
gf2P1 =
((Q `1_3) * (P1 `3_3)) - ((P1 `1_3) * (Q `3_3)),
gf3P1 =
(((((((Q `2_3) * (P1 `3_3)) - ((P1 `2_3) * (Q `3_3))) |^ 2) * (P1 `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P1 `3_3)) - ((P1 `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P1 `3_3)) - ((P1 `1_3) * (Q `3_3))) |^ 2)) * (P1 `1_3)) * (Q `3_3)),
gf1P2 =
((Q `2_3) * (P2 `3_3)) - ((P2 `2_3) * (Q `3_3)),
gf2P2 =
((Q `1_3) * (P2 `3_3)) - ((P2 `1_3) * (Q `3_3)),
gf3P2 =
(((((((Q `2_3) * (P2 `3_3)) - ((P2 `2_3) * (Q `3_3))) |^ 2) * (P2 `3_3)) * (Q `3_3)) - ((((Q `1_3) * (P2 `3_3)) - ((P2 `1_3) * (Q `3_3))) |^ 3)) - (((g2 * ((((Q `1_3) * (P2 `3_3)) - ((P2 `1_3) * (Q `3_3))) |^ 2)) * (P2 `1_3)) * (Q `3_3)) 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 being
Element of
ProjCo (GF p) such that BX1:
(
PP1Q = P1Q &
PP1Q in EC_SetProjCo (
(z `1),
(z `2),
p) )
;
consider PP2Q being
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
(addell_ProjCo (z,p)) . (
P1,
Q)
_EQ_ (addell_ProjCo (z,p)) . (
P2,
Q)
by B11, B12, B13, BX1, BX2, EC_PF_1:def 10;
verum end; suppose B1:
( not
P1 _EQ_ O & not
Q _EQ_ O &
P1 _EQ_ Q )
;
(addell_ProjCo (z,p)) . (P1,Q) _EQ_ (addell_ProjCo (z,p)) . (P2,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
(addell_ProjCo (z,p)) . (
P1,
Q)
_EQ_ (addell_ProjCo (z,p)) . (
P2,
Q)
by B4, EC_PF_1:44;
verum end;