[Logic] Negating Quantifiers in an Implication

Say I have a statement like this ∀ x ∈ Z, ∀ y ∈ Z x+y -> y+x, Is this essentially P -> Q? So the quantifiers are contained within P? (That doesn't make sense to me because the quantifiers apply to both sides of the implication)

Let's say I want to find the contradiction/negation and the contrapositive. How do I go about this? I think it should be as follows

Contradiction/negation

~(∀ x ∈ Z, ∀ y ∈ Z x+y ) \/ y+x - Get rid of implication

(∀ x ∈ Z, ∀ y ∈ Z x+y ) /\ y+x - Demorgans

Contrapositive

~(y+x) -> ~(∀ x ∈ Z, ∀ y ∈ Z x+y)

​

Or are the quantifiers separate from the actual implication so they are not affected by the negation or contrapositive?

​