composites of rationals

Johan G. F. Belinfante
2012 August 3

SetDirectory["l:"];  << goedel.12jul29a

summary

If  x  and  y  are rational numbers, then there exists a rational number  z  such that  x ∘ y ⊂ z.

derivation

Lemma.  An inclusion.

SubstTest[implies, subclass[r, s], 
        subclass[composite[q, r, t], 
          composite[q, s, t]], {q -> inverse[inttimes[u]], 
          r -> composite[inttimes[v], inverse[inttimes[x]]], 
          s -> composite[inverse[inttimes[x]], inttimes[v]], 
          t -> inttimes[y]}] // Reverse

subclass[
        composite[inverse[inttimes[u_]], inttimes[v_], inverse[inttimes[x_]], 
          inttimes[y_]], 
        composite[inverse[inttimes[intmul[u_, x_]]], 
          inttimes[intmul[v_, y_]]]] := True

Lemma.

SubstTest[implies, and[subclass[u, v], member[v, w]], 
        member[u, 
          image[inverse[S], w]], {u -> 
            composite[APPLY[RATIO, x], APPLY[RATIO, y]], 
          v -> composite[inverse[inttimes[first[x]]], 
              inverse[inttimes[first[y]]], inttimes[second[x]], 
              inttimes[second[y]]], w -> RATS}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p2, p3], p4], implies[p4, p5], 
          implies[and[p1, p5], p6], 
          not[implies[p1, p6]], {p1 -> 
              and[member[x, domain[RATIO]], member[y, domain[RATIO]]], 
            p2 -> 
              equal[APPLY[RATIO, x], 
                composite[inverse[inttimes[first[x]]], inttimes[second[x]]]], 
            p3 -> 
              equal[APPLY[RATIO, y], 
                composite[inverse[inttimes[first[y]]], inttimes[second[y]]]], 
            p4 -> 
              subclass[composite[APPLY[RATIO, x], APPLY[RATIO, y]], 
                composite[inverse[inttimes[first[x]]], inttimes[second[x]], 
                  inverse[inttimes[first[y]]], inttimes[second[y]]]], 
            p5 -> subclass[composite[APPLY[RATIO, x], APPLY[RATIO, y]], 
                composite[inverse[inttimes[first[x]]], 
                  inverse[inttimes[first[y]]], inttimes[second[x]], 
                  inttimes[second[y]]]], 
            p6 -> 
              member[composite[APPLY[RATIO, x], APPLY[RATIO, y]], 
                image[inverse[S], RATS]]}]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.  A membership rule.

(member[pair[x, y], composite[inverse[funpart[t]], z, funpart[t]]] // 
          AssertTest) /. t -> RATIO

member[pair[x_, y_], composite[inverse[RATIO], z_, RATIO]] := 
      and[member[first[x], Z], member[first[y], Z], 
        member[pair[APPLY[RATIO, x], APPLY[RATIO, y]], z], 
        member[second[x], Z], member[second[y], Z], 
        not[equal[first[x], id[omega]]], 
        not[equal[first[y], id[omega]]]]

Main Theorem. The composite of two rational numbers is a subset of a rational number.

Map[empty[composite[Id, complement[#]]] &, 
      SubstTest[class, pair[x, y], 
        implies[member[pair[x, y], u], 
          member[pair[x, y], v]], {u -> cartsq[domain[RATIO]], 
          v -> 
            image[inverse[composite[COMPOSE, cross[RATIO, RATIO]]], 
              image[inverse[S], RATS]]}]]

subclass[image[COMPOSE, cart[RATS, RATS]], image[inverse[S], RATS]] := 
      True