Lemma·L44
Multiplication on integer representatives is well defined
Multiplying representative pairs by the standard cross formula gives the same class no matter which representatives are chosen.
Let
with
and
(∼). Then
In words
For natural numbers a, b, c, d and a', b', c', d': if the pair (a, b) is equivalent to (a', b') and the pair (c, d) is equivalent to (c', d'), then the pairs built by the cross multiplication formula are equivalent as well, representing the same product.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Step 1: vary the first pair only. Suppose , i.e. **(*)**. Multiplying (*) by and by (substitutivity) gives Add to both sides of (A): The left side, reordered by commutativity/associativity, is . On the right side, (B) read as (symmetry) lets us substitute: Altogether which is exactly .
- 2Step 2: vary the second pair only. Suppose , i.e. . The identical computation, with the roles of and exchanged and using commutativity of multiplication to match the coordinate formula, gives
- 3Combine. By transitivity of ∼, steps 1 and 2 chain to give
∎
Remarks
The engine behind D060. As usual for a two-argument well-definedness proof, the pair of representatives is changed one coordinate-pair at a time and the two steps are chained by transitivity.