If you just want to verify some identities of Dirac gamma matrices in some certain representations. FeynCalc is not a necessity. Actually your choice of Dirac matrices is just the Weyl (chiral) representation:

$$ \gamma^\mu = \left( \begin{array}{ll} 0 & \sigma^\mu \\ \overline{\sigma}^\mu & 0 \end{array}\right), $$

which specifically are

$$ \begin{align} \gamma^0 &= \ \tau_1\otimes\sigma^0, \\ \gamma^i &= \mathrm i \tau_2\otimes\sigma^i. \end{align} $$

So according to the above equations, we can define the Dirac gamma matrices ourselves in the Wolfram language:

Clear[γ] SetAttributes[γ, Listable] γ[μ_] := If[μ == 0, KroneckerProduct @@ PauliMatrix[{1, μ}], I KroneckerProduct @@ PauliMatrix[{2, μ}] ] 

Then that codes below return True means your first three identities are verified:

With[{commutator = #.#2 - #2.# &, γList = γ@Range[0, 3]}, 2 TensorProduct[DiagonalMatrix[{1, -1, -1, -1}], γ[0].γ[0]] + Outer[commutator, γList, γList, 1] == 2 Outer[Dot, γList, γList, 1] ] 

True 

As for the last two, it is easy to see:

Table[Dot @@ γ[{0, i, 0, i}], {i, 3}] == -Table[Dot @@ γ[{0, i, i, 0}], {i, 3}] == ConstantArray[IdentityMatrix[4], 3] 

True 

Bonus

To verify what speaks of the Clifford algebra, also the defining features of Dirac gamma matrices

$$ \{\gamma^\mu, \gamma^\nu\} = 2\eta^{\mu\nu}, $$

one can compare the outcomes of the two pieces of codes:

With[{anticommutator = #.#2 + #2.# &, γList = γ[Range[0, 3]]}, Outer[anticommutator, γList, γList, 1] // MatrixForm ] 2 DiagonalMatrix[{1, -1, -1, -1}]~TensorProduct~IdentityMatrix[4] // MatrixForm 

If you just want to verify some identities of Dirac gamma matrices in some certain representations. FeynCalc is not a necessity. Actually your choice of Dirac matrices is just the Weyl (chiral) representation:

$$ \gamma^\mu = \left( \begin{array}{ll} 0 & \sigma^\mu \\ \overline{\sigma}^\mu & 0 \end{array}\right), $$

which specifically are

$$ \begin{align} \gamma^0 &= \ \tau_1\otimes\sigma^0, \\ \gamma^i &= \mathrm i \tau_2\otimes\sigma^i. \end{align} $$

So according to the above equations, we can define the Dirac gamma matrices ourselves in the Wolfram language:

Clear[γ] SetAttributes[γ, Listable] γ[μ_] := If[μ == 0, KroneckerProduct @@ PauliMatrix[{1, μ}], I KroneckerProduct @@ PauliMatrix[{2, μ}] ] 

Then that codes below return True means your first three identities are verified:

With[{commutator = #.#2 - #2.# &, γList = γ@Range[0, 3]}, 2 TensorProduct[DiagonalMatrix[{1, -1, -1, -1}], γ[0].γ[0]] + Outer[commutator, γList, γList, 1] == 2 Outer[Dot, γList, γList, 1] ] 

True 

As for the last two, it is easy to see:

Table[Dot @@ γ[{0, i, 0, i}], {i, 3}] == -Table[Dot @@ γ[{0, i, i, 0}], {i, 3}] == ConstantArray[IdentityMatrix[4], 3] 

True 

Bonus

To verify what speaks of the Clifford algebra, also the defining features of Dirac gamma matrices

$$ \{\gamma^\mu, \gamma^\nu\} = 2\eta^{\mu\nu}I_4, $$

one can compare the outcomes of the two pieces of codes:

With[{anticommutator = #.#2 + #2.# &, γList = γ[Range[0, 3]]}, Outer[anticommutator, γList, γList, 1] // MatrixForm ] 2 DiagonalMatrix[{1, -1, -1, -1}]~TensorProduct~IdentityMatrix[4] // MatrixForm 

If you just want to verify some identities of Dirac gamma matrices in some certain representations. FeynCalc is not a necessity. Actually your choice of Dirac matrices is just the Weyl (chiral) representation:

$$ \gamma^\mu = \left( \begin{array}{ll} 0 & \sigma^\mu \\ \overline{\sigma}^\mu & 0 \end{array}\right), $$

which specifically are

$$ \begin{align} \gamma^0 &= \ \tau_1\otimes\sigma^0, \\ \gamma^i &= \mathrm i \tau_2\otimes\sigma^i. \end{align} $$

So according to the above equations, we can define the Dirac gamma matrices ourselves in the Wolfram language:

Clear[γ] SetAttributes[γ, Listable] γ[μ_] := If[μ == 0, KroneckerProduct @@ PauliMatrix[{1, μ}], I KroneckerProduct @@ PauliMatrix[{2, μ}] ] 

Then that codes below return True means your first three identities are verified:

With[{commutator = #.#2 - #2.# &, γList = γ@Range[0, 3]}, 2 TensorProduct[DiagonalMatrix[{1, -1, -1, -1}], γ[0].γ[0]] + Outer[commutator, γList, γList, 1] == 2 Outer[Dot, γList, γList, 1] ] 

True 

As for the last two, it is easy to see:

Table[Dot @@ γ[{0, i, 0, i}], {i, 3}] == -Table[Dot @@ γ[{0, i, i, 0}], {i, 3}] == ConstantArray[IdentityMatrix[4], 3] 

True 

If you just want to verify some identities of Dirac gamma matrices in some certain representations. FeynCalc is not a necessity. Actually your choice of Dirac matrices is just the Weyl (chiral) representation:

$$ \gamma^\mu = \left( \begin{array}{ll} 0 & \sigma^\mu \\ \overline{\sigma}^\mu & 0 \end{array}\right), $$

which specifically are

$$ \begin{align} \gamma^0 &= \ \tau_1\otimes\sigma^0, \\ \gamma^i &= \mathrm i \tau_2\otimes\sigma^i. \end{align} $$

So according to the above equations, we can define the Dirac gamma matrices ourselves in the Wolfram language:

Clear[γ] SetAttributes[γ, Listable] γ[μ_] := If[μ == 0, KroneckerProduct @@ PauliMatrix[{1, μ}], I KroneckerProduct @@ PauliMatrix[{2, μ}] ] 

Then that codes below return True means your first three identities are verified:

With[{commutator = #.#2 - #2.# &, γList = γ@Range[0, 3]}, 2 TensorProduct[DiagonalMatrix[{1, -1, -1, -1}], γ[0].γ[0]] + Outer[commutator, γList, γList, 1] == 2 Outer[Dot, γList, γList, 1] ] 

True 

As for the last two, it is easy to see:

Table[Dot @@ γ[{0, i, 0, i}], {i, 3}] == -Table[Dot @@ γ[{0, i, i, 0}], {i, 3}] == ConstantArray[IdentityMatrix[4], 3] 

True 

Bonus

To verify what speaks of the Clifford algebra, also the defining features of Dirac gamma matrices

$$ \{\gamma^\mu, \gamma^\nu\} = 2\eta^{\mu\nu}, $$

one can compare the outcomes of the two pieces of codes:

With[{anticommutator = #.#2 + #2.# &, γList = γ[Range[0, 3]]}, Outer[anticommutator, γList, γList, 1] // MatrixForm ] 2 DiagonalMatrix[{1, -1, -1, -1}]~TensorProduct~IdentityMatrix[4] // MatrixForm