/sci/ - Science & Math

How do i do a direct proof on
Vx(Px v Qx) -> Vx(Px) v Ex(Qx)
1. Vx(Px v Qx)
2. Pa v Qa //Universal elimination
and now i'm guessing:
3. Ex(Pa v Qx) ?? //this feels illegal skipping Pa
4. Pa v Ex(Qx) ??
5. Vx(Pa v Ex(Qx)) ??
6. Vx(Pa) v Ex(Qx) ??

i can do contrapositive i think:
~(Vx(Px) v Ex(Qx)) -> ~(Vx(Px v Qx))
1. ~(Vx(Px) v Ex(Qx))
2. ~Vx(Px) & ~Ex(Qx)
3. ~Vx(Px)
4. Ex~(Px)
5. ~Pa //existential elimination
6. ~Ex(Qx) //from 2
7. Vx~(Qx)
8. ~Qa //universal elimination
9. ~Pa & ~ Qa //from 5 and 8
10. Ex(~Px & ~ Qx)
11. Ex~(Px v Qx)
12. ~Vx(Px v Qx)

Am i doing any of this right? I am struggling especially with distributing both quantifiers over disjunctions