Is there a mathematical notation for applying an axiom using substitution?

Question

Given an axiom like:

commute(a,b): a.b=b.a

And an expression

(x+y).z+k

I want to show, using the commute axiom, that this is equal to $z.(x+y)+k$.

I could write this in words. e.g. "Using $commute(x+y,z)$ and substituting this into the expression $(x+y).z+k$ we find that this equals $z.(x+y)+k$"

But is there a meta-mathematical language of substitution that one can use to write an entire proof in mathematical symbols. I have seen somewhere the proof is written as a list of an expression and which axiom is being used and some numbers which seem to indicate where this axiom is being used in the expression but this seems kind of ugly. Is there a standard way to write the whole proof as a single mathematical entity? And then verifying the proof would be some simple repeated simplification of the proof?

Edit: I'm thinking if instead the axiom has an extra function parameter:

commute(a,b,f): f(a.b)=f(b.a)

Then we can write $commute(x+y,z,p\rightarrow p+k)$ which gives $z.(x+y)+k = (x+y).z+k$. Not sure if that helps much in general.

I suppose you could then apply list of axioms: {axiom1(..), axiom2(..), axiom1(..),..} which would give you a chain $(a_1=a_2) \land (a_2=a_3) \land (a_3=a_4)$. Then you might need a meta-axiom that $(A=B) \land (B=C)$ can be replaced with $A=C$.

Answer 1

The substitution into mathematical expressions is governed by logical axioms for equality :

$t_1=t_2 \to f(t_1, \ldots)=f(t_2,\ldots)$.

In your example, we have the two terms $(x+y) \cdot z$ and $z \cdot (x+y)$ and the commutative axiom : $(x+y) \cdot z = z \cdot (x+y)$.

This is the part $t_1=t_2$.

We use it with the term $t + k$ that is built up with binary function symbol ("operation") : $+$.