theorem LmCommutative2: :: EC_PF_3:18

for p being 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)
for d being Element of (GF p) st O = [0,1,0] & d <> 0. (GF p) & Q `1_3 = d * (P `1_3) & Q `2_3 = d * (P `2_3) & Q `3_3 = d * (P `3_3) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = (d |^ 6) * (PQ `1_3) & QP `2_3 = (d |^ 6) * (PQ `2_3) & QP `3_3 = (d |^ 6) * (PQ `3_3) )