Great! Still struggling to have Mathematica simplify matrix expressions though. See the very simple example below. How do I simplify A1.A2 + A1.A3 with A2+A3 == 0 to 0 (or a zero matrix)? How can I make Mathematica scour through a collection of matrix assumptions and have it simplify matrix expressions very much like it does so well for scalar expressions? Thank you!!

ass = {Element[A1, Matrices[{4, 4}]],
   Element[A2, Matrices[{4, 4}]], 
   Element[A3, Matrices[{4, 4}]],
   A2 + A3 == 0};
FullSimplify[A1.A2 + A1.A3, Assumptions -> ass]
Simplify[x y + x z, Assumptions -> {y + z == 0}]

Out[1836]= A1.A2 + A1.A3

Out[1837]= 0

Thank you Claudio, and I apologize for not catching the typo. I remain a little confused about how to robustly simplify matrix expressions, though.

Here are a few examples:

ClearAll[J, Jp, Z, Zp, Ib, V, Vp, ass, n];
n = 4;
ass = {
   Element[J, Matrices[{n, n}]],
   Element[Ib, Matrices[{n, n}]],
   Element[V, Matrices[{n, n}]],
   J - Ib.V == 0
   };
TensorReduce[Ib.V - J, Assumptions -> ass]
Simplify[TensorReduce[Ib.V - J, Assumptions -> ass]]
Simplify[Ib.V - J, Assumptions -> ass]

Out[314]= -J + Ib.V
Out[315]= -J + Ib.V
Out[316]= 0

Likewise,

ClearAll[J, Jp, Z, Zp, Ib, V, Vp, ass, n];
n = 4;
ass = {
   Element[J, Matrices[{n, n}]],
   Element[Ib, Matrices[{n, n}]],
   Element[V, Matrices[{n, n}]],
   J - Ib.V == 0
   };
TensorReduce[Transpose[V + J], Assumptions -> ass]
TensorReduce[Conjugate[V + J], Assumptions -> ass]
TensorReduce[ConjugateTranspose[V + J], Assumptions -> ass]

Out[324]= TensorTranspose[J, {2, 1}] + TensorTranspose[V, {2, 1}]
Out[325]= Conjugate[J] + Conjugate[V]
Out[326]= ConjugateTranspose[J + V]

For the last example, I guess I could add another rule to make it work... Though generally speaking, I wonder how robustly these simplifications are being applied and how to specify rules to make the process more robust.

Thank you for answering my beginners question!

I now have some followup questions. Still very basic.

ass = {Element[A1, Matrices[{4, 4}]],
  Element[A2, Matrices[{4, 4}]], 
  Element[A3, Matrices[{4, 4}]]
   Element[A4, Matrices[{4, 4}]]}
TensorReduce[Transpose[A1.A2] - Transpose[A2].Transpose[A1], 
 Assumptions -> ass]
TensorReduce[
 Transpose[A1.A2.A3] - Transpose[A3].Transpose[A2].Transpose[A1], 
 Assumptions -> ass]

The first simplification works. The second one fails...

Furthermore, I'd like to simplify expressions like

TensorReduce[ConjugateTranspose[A1.A2] - A4, Assumptions -> ass]...

where there is a relationship between A1, A2, and A4, and the matrices themselves exhibit some symmetries. For example, A4 could be self-adjoint, and A1.A2 == A4... in which case the reduction should produce 0...