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) holds (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)
let z be Element of EC_WParam p; for P, Q being Element of EC_SetProjCo ((z `1),(z `2),p) holds (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)
let P, Q be Element of EC_SetProjCo ((z `1),(z `2),p); (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)
set O = [0,1,0];
reconsider O = [0,1,0] 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 being Element of ProjCo (GF p) such that
X1:
( PQQ = (addell_ProjCo (z,p)) . (P,Q) & PQQ in EC_SetProjCo ((z `1),(z `2),p) )
;
X2:
( PQQ `1_3 = ((addell_ProjCo (z,p)) . (P,Q)) `1_3 & PQQ `2_3 = ((addell_ProjCo (z,p)) . (P,Q)) `2_3 & PQQ `3_3 = ((addell_ProjCo (z,p)) . (P,Q)) `3_3 )
by X1, EC_PF_2:32;
consider QPP being Element of ProjCo (GF p) such that
X3:
( QPP = (addell_ProjCo (z,p)) . (Q,P) & QPP in EC_SetProjCo ((z `1),(z `2),p) )
;
X4:
( QPP `1_3 = ((addell_ProjCo (z,p)) . (Q,P)) `1_3 & QPP `2_3 = ((addell_ProjCo (z,p)) . (Q,P)) `2_3 & QPP `3_3 = ((addell_ProjCo (z,p)) . (Q,P)) `3_3 )
by X3, EC_PF_2:32;
per cases
( P _EQ_ O or ( Q _EQ_ O & not P _EQ_ O ) or ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q ) or ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q ) )
;
suppose A1:
( not
P _EQ_ O & not
Q _EQ_ O & not
P _EQ_ Q )
;
(addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)consider d being
Element of
(GF p) such that A2:
d = - (1. (GF p))
;
(
d * (((addell_ProjCo (z,p)) . (P,Q)) `1_3) = d * (- (((addell_ProjCo (z,p)) . (Q,P)) `1_3)) &
d * (((addell_ProjCo (z,p)) . (P,Q)) `2_3) = d * (- (((addell_ProjCo (z,p)) . (Q,P)) `2_3)) &
d * (((addell_ProjCo (z,p)) . (P,Q)) `3_3) = d * (- (((addell_ProjCo (z,p)) . (Q,P)) `3_3)) )
by A1, LmCommutative1;
then
(
d * (((addell_ProjCo (z,p)) . (P,Q)) `1_3) = (1. (GF p)) * (((addell_ProjCo (z,p)) . (Q,P)) `1_3) &
d * (((addell_ProjCo (z,p)) . (P,Q)) `2_3) = (1. (GF p)) * (((addell_ProjCo (z,p)) . (Q,P)) `2_3) &
d * (((addell_ProjCo (z,p)) . (P,Q)) `3_3) = (1. (GF p)) * (((addell_ProjCo (z,p)) . (Q,P)) `3_3) )
by A2, VECTSP_1:10;
then
(
QPP `1_3 = d * (((addell_ProjCo (z,p)) . (P,Q)) `1_3) &
QPP `2_3 = d * (((addell_ProjCo (z,p)) . (P,Q)) `2_3) &
QPP `3_3 = d * (((addell_ProjCo (z,p)) . (P,Q)) `3_3) )
by X3, EC_PF_2:32;
hence
(addell_ProjCo (z,p)) . (
P,
Q)
_EQ_ (addell_ProjCo (z,p)) . (
Q,
P)
by A2, X1, X2, X3, EC_PF_1:def 10, VECTSP_2:3;
verum end; suppose A1:
( not
P _EQ_ O & not
Q _EQ_ O &
P _EQ_ Q )
;
(addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)consider PP being
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 being
Element of
ProjCo (GF p) such that A4:
(
QQ = Q &
QQ in EC_SetProjCo (
(z `1),
(z `2),
p) )
;
consider d being
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 =
d |^ 6 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
(
((addell_ProjCo (z,p)) . (Q,P)) `1_3 = d6 * (((addell_ProjCo (z,p)) . (P,Q)) `1_3) &
((addell_ProjCo (z,p)) . (Q,P)) `2_3 = d6 * (((addell_ProjCo (z,p)) . (P,Q)) `2_3) &
((addell_ProjCo (z,p)) . (Q,P)) `3_3 = d6 * (((addell_ProjCo (z,p)) . (P,Q)) `3_3) )
by A1, A3, A6, LmCommutative2;
hence
(addell_ProjCo (z,p)) . (
P,
Q)
_EQ_ (addell_ProjCo (z,p)) . (
Q,
P)
by A8, X1, X2, X3, X4, EC_PF_1:def 10;
verum end; end;