# Proof of symbolic matrix

For any n-order matrix A, B, H

$$[A, B] \stackrel{\text { def }}{=} A B-B A$$

Try to prove：

(1) $$\left[k_{1} \boldsymbol{A}+k_{2} \boldsymbol{B}, \boldsymbol{H}\right]=k_{1}[\boldsymbol{A}, \boldsymbol{H}]+k_{2}[\boldsymbol{B}, \boldsymbol{H}]$$

Clear["Global*"];
$$Assumptions = (A | B | H) \[Element] Matrices[{n, n}];$$Assumptions = Element[Subscript[k, 1] | Subscript[k, 2], Reals];
f[x_, y_] := x . y - y . x;
G = Subscript[k, 1]*A + Subscript[k, 2]*B;
TensorReduce[
f[G, H] == Subscript[k, 1]*f[A, H] + Subscript[k, 2]*f[B, H]]


$$-\mathrm{H} \cdot\left(\mathrm{A} \mathrm{k}_{1}+\mathrm{B} \mathrm{k}_{2}\right)+\left(\mathrm{A} \mathrm{k}_{1}+\mathrm{B} \mathrm{k}_{2}\right) \cdot \mathrm{H}==(\mathrm{A} \cdot \mathrm{H}-\mathrm{H} \cdot \mathrm{A}) \mathrm{k}_{1}+(\mathrm{B} \cdot \mathrm{H}-\mathrm{H} \cdot \mathrm{B}) \mathrm{k}_{2}$$

Failed.

(2) $$[A, B]=-[B, A]$$

Clear["Global*"];
$Assumptions = Element[A | B, Matrices[{n, n}]]; f[x_, y_] := x . y - y . x; TensorReduce[f[A, B] == -f[B, A]]  True (3) $$[A,[B, H]]+[B,[H, A]]+[H,[A, B]]=0$$ Clear["Global*"];$Assumptions = Element[A | B | H, Matrices[{n, n}]];
f[x_, y_] := x . y - y . x;
TensorReduce[f[A, f[B, H]] + f[B, f[H, A]] + f[H, f[A, B]] == 0]


True

How can I prove question (1)?

TensorExpand[
`