let p be 5 _or_greater Prime; for z being Element of EC_WParam p
for P, Q, O, PQ, QP being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = - (PQ `1_3) & QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) )
let z be Element of EC_WParam p; for P, Q, O, PQ, QP being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = - (PQ `1_3) & QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) )
let P, Q, O, PQ, QP be Element of EC_SetProjCo ((z `1),(z `2),p); ( O = [0,1,0] & not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) implies ( QP `1_3 = - (PQ `1_3) & QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) ) )
assume that
A2:
O = [0,1,0]
and
A3:
( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q )
; ( not PQ = (addell_ProjCo (z,p)) . (P,Q) or not QP = (addell_ProjCo (z,p)) . (Q,P) or ( QP `1_3 = - (PQ `1_3) & QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) ) )
set a = z `1 ;
set b = z `2 ;
assume AS:
( PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) )
; ( QP `1_3 = - (PQ `1_3) & QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) )
reconsider g2 = 2 mod p as Element of (GF p) by EC_PF_1:14;
set gf1PQ = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3));
set gf2PQ = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3));
set gf3PQ = (((((((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));
set gf1QP = ((P `2_3) * (Q `3_3)) - ((Q `2_3) * (P `3_3));
set gf2QP = ((P `1_3) * (Q `3_3)) - ((Q `1_3) * (P `3_3));
set gf3QP = (((((((P `2_3) * (Q `3_3)) - ((Q `2_3) * (P `3_3))) |^ 2) * (Q `3_3)) * (P `3_3)) - ((((P `1_3) * (Q `3_3)) - ((Q `1_3) * (P `3_3))) |^ 3)) - (((g2 * ((((P `1_3) * (Q `3_3)) - ((Q `1_3) * (P `3_3))) |^ 2)) * (Q `1_3)) * (P `3_3));
reconsider gf1PQ = ((Q `2_3) * (P `3_3)) - ((P `2_3) * (Q `3_3)), gf2PQ = ((Q `1_3) * (P `3_3)) - ((P `1_3) * (Q `3_3)), gf3PQ = (((((((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)), gf1QP = ((P `2_3) * (Q `3_3)) - ((Q `2_3) * (P `3_3)), gf2QP = ((P `1_3) * (Q `3_3)) - ((Q `1_3) * (P `3_3)), gf3QP = (((((((P `2_3) * (Q `3_3)) - ((Q `2_3) * (P `3_3))) |^ 2) * (Q `3_3)) * (P `3_3)) - ((((P `1_3) * (Q `3_3)) - ((Q `1_3) * (P `3_3))) |^ 3)) - (((g2 * ((((P `1_3) * (Q `3_3)) - ((Q `1_3) * (P `3_3))) |^ 2)) * (Q `1_3)) * (P `3_3)) as Element of (GF p) ;
A5:
PQ = [(gf2PQ * gf3PQ),((gf1PQ * ((((gf2PQ |^ 2) * (P `1_3)) * (Q `3_3)) - gf3PQ)) - (((gf2PQ |^ 3) * (P `2_3)) * (Q `3_3))),(((gf2PQ |^ 3) * (P `3_3)) * (Q `3_3))]
by A2, A3, AS, EC_PF_2:def 9;
A6:
QP = [(gf2QP * gf3QP),((gf1QP * ((((gf2QP |^ 2) * (Q `1_3)) * (P `3_3)) - gf3QP)) - (((gf2QP |^ 3) * (Q `2_3)) * (P `3_3))),(((gf2QP |^ 3) * (Q `3_3)) * (P `3_3))]
by A2, A3, AS, EC_PF_2:def 9;
A7:
gf1QP = - gf1PQ
by VECTSP_1:17;
A8:
gf2QP = - gf2PQ
by VECTSP_1:17;
A10:
gf2PQ |^ 2 = gf2QP |^ 2
by A8, EC_PF_2:1;
A11:
gf3QP = gf3PQ
thus
QP `1_3 = - (PQ `1_3)
( QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) )
thus
QP `2_3 = - (PQ `2_3)
QP `3_3 = - (PQ `3_3)
thus
QP `3_3 = - (PQ `3_3)
verum