Lemma·L43
Addition on integer representatives is well defined
Adding representative pairs coordinatewise 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 coordinatewise sums form equivalent pairs, representing the same sum.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1The hypotheses say (i) and (ii). By substitutivity, adding (i) and (ii):
- 2By commutativity and associativity, both sides are sums of the same four terms regrouped: the left is , the right is , so which is exactly by the defining equation of .
∎
Remarks
The engine behind D058. The proof is the same rearrangement trick used to prove transitivity of ∼ itself.