The first step is driving in the negation, as you wrote. The second step does not tell you that AGA=G holds, instead, consider A!a which holds in a state where all outgoing paths must satisfy !a. Hence, that is nothing else than (A false) | !a, so that we get AG(A!a) = AG((A false) | !a). A false only holds in states with no infinite paths which are ignored by AG, so that the latter is equivalent to AG!a.

Then, we have A(AG!a & A![Fb SU !c]) where we can pull out the A quantifier and get AA(G!a & ![Fb SU !c]) which is the same as A(G!a & ![Fb SU !c]).

It is a common mistake to consider some of these replacements are equivalences that should be generally valid. However, they appear in a context and are only valid in that context. For instance, A!a is not equivalent to !a only, but in the context above, it is so, since the other disjunction A false is wiped out.