Yes, A phi holds on every state that has no infinite path and for that reason this product structure is satisfied.

If there are some infinite paths in the product structure starting in state s, then we have to check ¬∃q.(K×KA,s×q) |= φI ∧ EφF, i.e., that there is no run q in the automaton that starts in the initial states and satisfies the acceptance condition.

The nasty thing the the examp problem is that we do not just check there A phi, but A(!a | phi) which is equivalent to !a | A phi. Hence, to check whether there is a state s such that s |= !a | A phi, we have to check that s |= !a or s |= A phi holds. The latter is what we discussed so far, but additionally, we should check also s |= !a for this exam problem.

About validity, we can also say the following: Validity of LTL can be reduced to LTL model checking in the structure that consists of all states that you can construct for the given variables V, i.e., the states are all the subsets of V, and transitions are between every pair of states. Then, this structure has all possible paths in it, and if we state that all states are also initial states, then checking whether this structure satisfies the LTL formula means checking that all paths are satisfying the LTL formula. While that Kripke structure seems to be enormously large (and in fact it is), its symbolic representation is just the formula true, so that is very small.