let p be 5 _or_greater Prime; :: thesis: 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; :: thesis: 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); :: thesis: (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: P _EQ_ O ; :: thesis: (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)

then A2: (addell_ProjCo (z,p)) . (P,Q) _EQ_ Q by EC_PF_2:def 9;
(addell_ProjCo (z,p)) . (Q,P) _EQ_ Q

proof

per cases ( Q _EQ_ O or not Q _EQ_ O ) ;

suppose B1: Q _EQ_ O ; :: thesis: (addell_ProjCo (z,p)) . (Q,P) _EQ_ Q

then (addell_ProjCo (z,p)) . (Q,P) _EQ_ O by A1, EC_PF_2:def 9;
hence (addell_ProjCo (z,p)) . (Q,P) _EQ_ Q by B1, EC_PF_1:44; :: thesis: verum

end;

suppose not Q _EQ_ O ; :: thesis: (addell_ProjCo (z,p)) . (Q,P) _EQ_ Q

hence (addell_ProjCo (z,p)) . (Q,P) _EQ_ Q by A1, EC_PF_2:def 9; :: thesis: verum

end;

end;

end;

hence (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P) by A2, EC_PF_1:44; :: thesis: verum

end;

suppose A1: ( Q _EQ_ O & not P _EQ_ O ) ; :: thesis: (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P)

then (addell_ProjCo (z,p)) . (P,Q) _EQ_ P by EC_PF_2:def 9;
hence (addell_ProjCo (z,p)) . (P,Q) _EQ_ (addell_ProjCo (z,p)) . (Q,P) by A1, EC_PF_2:def 9; :: thesis: verum

end;

suppose A1: ( not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q ) ; :: thesis: (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; :: thesis: verum

end;

suppose A1: ( not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q ) ; :: thesis: (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; :: thesis: verum

end;

end;