MATH.7:4.4 - Derive the laws that the chosen structure retains

For each operation, substituting h(x_i) into its definition and cancelling r(h(x_i)) gives:

op_Y(h(x1),...,h(xn))=h(op_X(x1,...,xn)).

Any other receiving operation with this equality must coincide with the constructed one: every receiving input has the form h(x_i). Thus the source operation and h determine the transported operation uniquely on Y.

To carry an equation built from these operations, follow its expressions from the variables and constants through each operation. Variables are mapped by h, constants by their specified images, and the displayed equality carries each composite expression. This is an induction on the expression’s construction; MATH.4 supplies that form of argument.

For expressions s and t in one carrier, it yields:

s_Y(h(x1),...)=h(s_X(x1,...)) and t_Y(h(x1),...)=h(t_X(x1,...)).

An equality of the source expressions therefore gives equality of the receiving expressions. Conversely, h is injective, so equality of those receiving values gives equality of the source values. Surjectivity covers all assignments in Y. The same reasoning with the map for each sort treats operations with different input and output sets.

This transfers equational laws such as associativity, an identity law or distributivity for the operations actually carried. A further order, distance or other relation must use its own transported definition or an established compatibility result. For partial operations, compare the definedness of the compound expressions as well as their values.