How do I simplify a vector expression?

If you have Mathematica Version 9, you can use Vectors and TensorReduce:

Assuming[(x | y) \[Element] Vectors[n] , TensorReduce[Dot[x, y] - Dot[y, x]]]
(* 0 *)
TensorReduce[Dot[x, y] - Dot[y, x], Assumptions -> (x | y) \[Element] Vectors[n]]
(* 0 *)
TensorReduce[Cross[x + y, z],  Assumptions -> (x | y | z) \[Element] Vectors[n]]
(* x\[Cross]z + y\[Cross]z *)
Distribute[Cross[x + y, z]] (* this should work in all previous versions *)
(* x\[Cross]z + y\[Cross]z *)

Here is a way to do all the things you asked for automatically, independently of Mathematica version. The approach relies on a special symbol to identify when we're dealing with a vector: Instead of using things like x, y etc. for vectors, the convention now is that vectors are written as vec[x], vec[y], etc.

You could also define the wrapper OverVector[x] for this purpose because it displays as $\vec{x}$. But for this post I want to keep it simple, and the arrows wouldn't display easily in the source code below.

ClearAll[scalarProduct, vec]; 
SetAttributes[scalarProduct, {Orderless}]
vec /: Dot[vec[x_], vec[y_]] := scalarProduct[vec[x], vec[y]]
vec /: Cross[vec[x_], HoldPattern[Plus[y__]]] := 
 Map[Cross[vec[x], #] &, Plus[y]]
vec /: Cross[HoldPattern[Plus[y__]], vec[x_]] := 
 Map[Cross[#, vec[x]] &, Plus[y]]
scalarProduct /: MakeBoxes[scalarProduct[x_, y_], _] := 
 RowBox[{ToBoxes[x], ".", ToBoxes[y]}]

vec[x].vec[y]

(* ==> vec[x].vec[y] *)

vec[x].vec[y] == vec[y].vec[x]

(* ==> True *)

Cross[vec[x], vec[a] + vec[b]]

(* ==> vec[x]\[Cross]vec[a] + vec[x]\[Cross]vec[b] *)

Cross[vec[a] + vec[b], vec[x]]

(* ==> vec[a]\[Cross]vec[x] + vec[b]\[Cross]vec[x] *)

For the Dot product, I defined the behavior of vec such that it gets evaluated as a new function scalarProduct whose only algebraic property is that it's Orderless as you were expecting for the dot product of vectors. Of course this is only true for Euclidean dot products, so this assumption is implicit here. For more information on how this definition works, look up TagSetDelayed.

In addition, scalarProduct is given a customized display format by defining that it should again display as if it were a dot product when it appears in the low-level formatting function MakeBoxes.

For the distributive property of the cross product, I give vec the additional property that when it appears in Cross together with an expression of head Plus, the sum is expanded. Here the TagSetDelayed definitions are done for both orders, and contain a HoldPattern to prevent Plus from being evaluated too early in the definition.

Now you may come back with many more wishes: e.g., what about multiplicative scalars in the dot or cross product, and what about matrices. However, that's a wide field that opens up a can of worms, so I would say just implement the bare minimum of features you can get away with symbolically, then proceed with a concrete working basis so that you can write vectors as lists instead.

Another approach would be to define a new symbol for a custom dot product. That is done in this question.

Using OverVector

As mentioned above, you can replace vec by Overvector everywhere in the above source code, to get a better formatted result. Assuming you have done that (I won't bother to repeat the definitions with that change), here are some examples:

To enter these vector expressions, refer to the Basic Math assistant palette. The cross product can be entered as EsccrossEsc.

Another thing you asked for is to use the antisymmetry of the cross product in simplifications. That's actually done already if you invoke FullSimplify: