The relation and an order relation on pairs are given by formulas in the pair components, so membership reduces to a+d=b+c (resp. a+d<=b+c); reflexivity, symmetry and transitivity follow by natural-number arithmetic, and the quotient lemmas describe the quotient. Sum, product and negation maps are defined on pairs, shown compatible with the relation, and passed to the quotient by the compatibility lemma, which also gives uniqueness.
Membership. is a set by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, so is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set. By The Cartesian Product of Two Classes §product and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, the elements of are exactly the ordered pairs with . By The Components of an Ordered Pair §components, the components of such a pair are and ; in particular for every . Sums and products of natural numbers are natural numbers by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations. Hence the formulas and expressions below, built from components of elements of by sums, products and the order of natural numbers, quantify over sets only and use every defined set symbol properly for arguments in , and every pair of such sums and products lies in .
The relations and . Write for , as in Relations, Domain, Range, Inverse and Composition §relation. By Maps and Relations Given by Formulas §relation, applied to the set and the formula , there is exactly one relation on with if and only if , for all ; as every element of is a pair with components and , this is the relation of the statement, and for ,
In the same way, Maps and Relations Given by Formulas §relation, applied to and the formula , gives a relation on such that, for ,
The clause equivalence above. Let .
Reflexive: by Arithmetic and Order of the Natural Numbers §commutative, so by . Thus is reflexive.
Symmetric: if , then by , so by Arithmetic and Order of the Natural Numbers §commutative, that is, . Thus is symmetric.
Transitive: if and , then and by . Adding, ; rearranging by Arithmetic and Order of the Natural Numbers §commutative and Arithmetic and Order of the Natural Numbers §associative,
so by Arithmetic and Order of the Natural Numbers §cancellation, that is, . Thus is transitive.
Hence is an equivalence relation on the set by Equivalence Relations on a Set §equivalence.
The clause equal above. As is an equivalence relation on the set , the quotient is a set by Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §quotient-set. By The Quotient of a Set by an Equivalence Relation and the Canonical Projection §quotient, the elements of are exactly the classes with ; as the elements of are exactly the pairs with , these are exactly the classes with . For , if and only if , by Equivalence Classes Partition the Set: Cover, Disjointness and Representatives; the Quotient Is a Set and the Canonical Projection Is a Surjection §equal, that is, by , if and only if .
The clause operations above. Operations on . The expressions and lie in for all , so Maps and Relations Given by Formulas §binary, with domain and values in , gives maps , that is, binary operations on , with, in the notation of Binary Operations on a Set §notation,
Likewise Maps and Relations Given by Formulas §map, applied to , gives a map with .
Compatibility. Let , , and be elements of with and , that is, by ,
Sum: and . Rearranging by Arithmetic and Order of the Natural Numbers §commutative and Arithmetic and Order of the Natural Numbers §associative and using ,
so by .
Product: , and . First, : multiplying the first equation of by , and its reverse by , and expanding by Arithmetic and Order of the Natural Numbers §distributive and Arithmetic and Order of the Natural Numbers §commutative,
adding these and rearranging by Arithmetic and Order of the Natural Numbers §commutative and Arithmetic and Order of the Natural Numbers §associative,
which is by . Second, : multiplying the second equation of by , and its reverse by , and expanding in the same way,
adding these and rearranging,
which is by . As is transitive, .
Negation: and , and by , means , the first equation of reversed.
Order: by , means , and means . By Arithmetic and Order of the Natural Numbers §order, if and only if . Rearranging by Arithmetic and Order of the Natural Numbers §commutative and Arithmetic and Order of the Natural Numbers §associative and using (in the form ),
and . So if and only if , which by Arithmetic and Order of the Natural Numbers §order holds if and only if . Hence if and only if .
Passing to the quotient. By the compatibility of and Compatible Operations, Maps and Relations Pass to the Quotient §operation, there is exactly one binary operation on with for all . As and run through , runs through the pairs with , and ; so this condition says exactly that for all . Hence exists and is unique. In the same way, Compatible Operations, Maps and Relations Pass to the Quotient §operation applied to gives the unique with , and Compatible Operations, Maps and Relations Pass to the Quotient §map applied to gives the unique map with . Finally, Compatible Operations, Maps and Relations Pass to the Quotient §relation applied to gives a relation on with if and only if for all , that is, by , with if and only if for all ; and it is unique, since by every relation on with the latter property has the former, and the relation with the former property is unique by Compatible Operations, Maps and Relations Pass to the Quotient §relation.
Loading…