Proving a group isomorphism from $(S,+)$ to $(S,+')$

Let $S$ be a set with an element $O$ and a composition law $*$ satisfying the following two conditions:

1. $P*Q=Q*P$ for all $P,Q\in S$
2. $P*(P*Q)=Q$ for all $P,Q\in S$.

Define an operation $+$ on $S$ by $P+Q=O*(P*Q)$, and assume that $+$ is associative, which is equivalent to the condition that

$P*(O*(R*Q))=R*(O*(Q*P))$ for all $P,Q,R\in S$.

This makes (S,+) into a group. Now define a new operation $+'$ on $S$ which is also associative, but with $O'$ in place of $O$. Prove that the function $F:(S,+)\rightarrow (S,+')$ defined by $P\mapsto O*(O'*P)$ is a group isomorphism.

Whew! That was a lot to write down. Ok so bijectivity is easy, but I'm unable to prove the homomorphism part. I have:

$F(P+Q)=F(O*(P*Q))=O*(O'*(O*(P*Q)))$

Now the only non trivial move I can see to make at this point is to use the associativity condition to write this as:

$(P*Q)*(O'*(O*O))$

From here I can't find anything more to do despite a lot of trying, and I certainly can't make it look even close to:

$F(P)+'F(Q)=O'*[(O*(O'*P))*(O*(O'*Q))]$

-
Where does this come from? Is this related to the group law on an elliptic curve? –  DonAntonio Jan 30 '13 at 5:09
@DonAntonio: yup, it's from Rational Points on Elliptic Curves by Silverman –  cactuar Jan 30 '13 at 5:10
No wonder it rang so loudly a bell...:) . If I can remember I'll try something later, right now's too late. –  DonAntonio Jan 30 '13 at 5:12
@DonAntonio: Ok thanks –  cactuar Jan 30 '13 at 5:13

Sure we can prove this. But first, a lemma from our sponsors:

Note that $P+Q = O*(P*Q) = O*(O'*(O'*(P*Q)) = (P+'Q)+O'$, hence: $P+'Q = (P+Q) - O'$. Also note that $F(P) = P+O'$.

It then follows that:

$F(P+Q) = (P+Q)+O' = (P+Q) + [(O'+O') - O']$

$= ((P+O') + (Q+O')) - O'$ (by associativity and commutativity of +)

$= (P+O')+'(Q+O') = F(P) +' F(Q)$.

-
Damn, I don't know if I could have ever figured this out using just the composition law, it would have been really complex. Thanks. –  cactuar Jan 30 '13 at 21:19