What is the structure of matrix multiplication and minus? Please note I have only little background im mathematics and I am working on formalizing theorems with theorem provers. This is very much a beginner question.
Suppose I have matrices, where the elements of the matrix are from a commutative ring with 1 element (commonly called ring I guess).
I looked at the wikipedia entries of matrix multiplication and semi-ring.
My guess is that matrix multiplication together with plus (+) is a semi-ring.
But does multiplication together with minus form a semi-ring? Is it called something else?
The following lemmas are true: A ** (B - C) = A ** B - A ** C and (A - B) ** C = A ** C - B ** C where ** is the matrix multiplication.
 A: Let $R$ be a commutative ring with unit.  Let $M_n(R)$ be the set of $n \times n$ matrices with entries taken from $R$.  If $A = [A_{ij} \in M_n(R)$, then taking $-A = [-A_{ij}] \in M_n(R)$ yields a matrix $-A$ such that $A + (-A) = (-A) + A = 0 \in M_n(R)$.  According to this wikipedia page, we have shown $M_n(R)$ to be a ring, since we have demonstrated an additive inverse for each element.  Technically speaking, we should show $M_n(R)$ satisfies all the other ring axioms, but if one grants that $M_n(R)$ is a semi-ring, then that work is taken care of.  In any event, the existence of additive inverses is the distinguishing fact, and verification from scratch that $M_n(R)$ satisfies the other ring axioms is not a difficult matter, so I will leave it for my audience to work out.  Of course, if anyone needs more input in that matter, leaving a comment to that effect will beckon me to address this further, and I will be back to answer.
If the addtive operation is replaced by subtraction in any ring $S$, commutative or not, with or without a multiplative inverse, i.e. $a + b$ is replaced by $a - b =a + (-b)$ then we don't even have a semi-ring unless $a = -a$ for all $a \in S$ (or you may say $\text{char} S = 2$ if there exists $1_S \in S$ having  the usual property $1_S a = a 1_S$).  This is for the reason that, without $a = -a$, subtraction is neither commutative nor associative in general:  taking $b = 0$ yields 
$a - b = b - a \Rightarrow a = a - 0 = 0 - a = -a, \tag{1}$
and
$(a - b) - c = a - (b - c)  \Rightarrow (a - b) -c = a + (-(b - c)) = a + (-b + c)$
$= (a - b) + c \Rightarrow c = -c \; \text{for all} \; c \in S.  \tag{2}$
So in general, in the absence of the condition $a = -a$ for all $a \in S$, subtraction doesn't satisfy the necessary axioms, though $a(b - c) = ab - ac$ and $(a - b)c = ac - ab$ still apply.
Hope this helps.  Cheerio,
and as always,
Fiat Lux!!!
A: No. Subtraction is neither commutative nor associative. It's usually not considered as an operation in isolation without addition. With addition and subtraction, together with matrix multiplication, matrices form a ring.
