composites of ranges of subgroups

Johan G. F. Belinfante
2012 January 24

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

summary

The direct product of two groups  x  and  y  is the group  direct[x, y] = (x ⊗ y) ∘ TWIST.  The range of a subgroup of a direct product of two groups is a relation.  It is natural to ask whether constructions involving such relations yield ranges of other subgroups.  One such result has already been derived.   If  w  is the range of a subgroup of the direct product of groups  x  and  y, then  inverse[w]  is the range of a subgroup of the direct product of  y  and  x.

implies[
      and[member[x, GROUPS], member[y, GROUPS], 
        member[w, 
          image[IMAGE[SECOND], intersection[GROUPS, P[direct[x, y]]]]]], 
      member[inverse[w], 
        image[IMAGE[SECOND], 
          intersection[GROUPS, P[direct[y, x]]]]]]

In this notebook it is shown that if  u  is the range of a subgroup of the direct product of groups  y  and  z, and if  v  is the range of a subgroup of the direct product of groups  x  and  y, then the composite relation  u ∘ v  is the range of a subgroup of the direct product of  x  and  z.   One can think of this result as a generalization of the fact that the composite of two binary homomorphisms is a homomorphism.  Indeed, the set of binary homomorphisms from a group  x  to a group  y  is a subclass of the set of ranges of subgroups of the direct product of  x  and  y.

implies[and[member[x, GROUPS], member[y, GROUPS]], 
      subclass[binhom[x, y], 
        image[IMAGE[SECOND], 
          intersection[GROUPS, P[direct[x, y]]]]]]

a general result

The following general result says that ranges of substructures of direct products are relations.

Theorem.  The range  w  of a substructure of the direct product of  y  and  z  is a subclass of the cartesian product of the range of  y  and the range of  z.

SubstTest[implies, and[member[w, u], subclass[u, v]], 
        member[w, 
          v], {u -> image[IMAGE[SECOND], intersection[x, P[direct[y, z]]]], 
          v -> P[cart[range[y], range[z]]]}] // Reverse

or[not[
          member[w_, 
            image[IMAGE[SECOND], 
              intersection[x_, P[composite[cross[y_, z_], TWIST]]]]]], 
        subclass[w_, cart[range[y_], range[z_]]]] := True

For the special case  x = GROUPS, this theorem says that if  w  is the range of a subgroup of the direct product of  y  and  z, then w ⊂ range[y] × range[z].

binary closed

Theorem.  If  w  is the range of a subgroup of  gp[x], then  w  is binary closed under  gp[x].

SubstTest[implies, and[member[w, u], subclass[u, v]], 
        member[w, 
          v], {u -> image[IMAGE[SECOND], intersection[GROUPS, P[gp[x]]]], 
          v -> binclosed[gp[x]]}] // Reverse

or[not[
          member[w_, image[IMAGE[SECOND], intersection[GROUPS, P[gp[x_]]]]]], 
        subclass[image[gp[x_], cart[w_, w_]], w_]] := True

Corollary.  If  w  is the range of a subgroup of the direct product of  gp[x]  and  gp[y], then  w  is binary closed under  direct[gp[x], gp[y]].

SubstTest[implies, 
        member[w, image[IMAGE[SECOND], intersection[GROUPS, P[gp[z]]]]], 
        member[w, binclosed[gp[z]]], z -> direct[gp[x], gp[y]]] // 
      Reverse

or[not[
          member[w_, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, 
                P[composite[cross[gp[x_], gp[y_]], TWIST]]]]]], 
        subclass[composite[gp[y_], cross[w_, w_], inverse[gp[x_]]], w_]] := 
      True

The next step is to consider composites of ranges of subgroups of direct products.

Lemma.

(SubstTest[implies, subclass[p, q], 
            subclass[composite[r, p, z], 
              composite[r, q, z]], {r -> composite[gp[z], cross[u, u]], 
              p -> id[cart[t, t]], q -> composite[inverse[gp[y]], gp[y]], 
              z -> composite[cross[v, v], inverse[gp[x]]]}] // 
          Reverse) /. t -> range[gp[y]]

(% /. {u -> u_ , v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Lemma.  (Eliminating the factor  id[range[gp[y]]].)

SubstTest[implies, equal[t, range[gp[y]]], 
        subclass[
          composite[gp[z], 
            cross[composite[u, id[t], v], composite[u, id[t], v]], 
            inverse[gp[x]]], 
          composite[gp[z], cross[u, u], inverse[gp[y]], gp[y], cross[v, v], 
            inverse[gp[x]]]], t -> union[domain[u], range[gp[y]]]] // 
      Reverse

(% /. {u -> u_ , v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Lemma.

Map[not, 
        SubstTest[and, implies[and[p1, p2], p3], implies[p0, p4], 
          implies[and[p2, p3, p4], p5], 
          not[implies[and[p0, p1, p2], p5]], {p0 -> 
              subclass[domain[u], range[gp[y]]], 
            p1 -> subclass[composite[gp[z], cross[u, u], inverse[gp[y]]], u], 
            p2 -> subclass[composite[gp[y], cross[v, v], inverse[gp[x]]], 
                v], 
p3 -> 
              subclass[
                composite[gp[z], cross[u, u], inverse[gp[y]], gp[y], 
                  cross[v, v], inverse[gp[x]]], 
                composite[u, v]], 
p4 -> 
              subclass[
                composite[gp[z], cross[composite[u, v], composite[u, v]], 
                  inverse[gp[x]]], 
                composite[gp[z], cross[u, u], inverse[gp[y]], gp[y], 
                  cross[v, v], inverse[gp[x]]]], 
            p5 -> subclass[
                composite[gp[z], cross[composite[u, v], composite[u, v]], 
                  inverse[gp[x]]], composite[u, v]]}]] // Reverse

(% /. {u -> u_ , v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Theorem.  If  u  is the range of a subgroup of  direct[gp[y],  gp[z]]  and  v  is the range of a subgroup of  direct[gp[x], gp[y]], then  u ∘ v  is binary closed under  direct[gp[x], gp[z]].

\(Map[not, 
        SubstTest[
          and,  (*implies[p1, p3], implies[p2, p4], \ implies[p1, p5], *) \ 
          implies[p5, p6], implies[and[p3, p4, p6], p7], \ 
          not[implies[and[p1, p2], p7]], {p1 -> 
              member[u, 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[gp[y], gp[z]], TWIST]]]]], 

            p2 -> member[v, 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[gp[x], gp[y]], TWIST]]]]], 
            p3 -> subclass[composite[gp[z], cross[u, u], inverse[gp[y]]], u], 
            p4 -> subclass[composite[gp[y], cross[v, v], inverse[gp[x]]], 
                v], 
p5 -> 
              subclass[u, cart[range[gp[y]], range[gp[z]]]], 
            p6 -> subclass[domain[u], range[gp[y]]], 
            p7 -> subclass[
                composite[gp[z], cross[composite[u, v], composite[u, v]], 
                  inverse[gp[x]]], composite[u, v]]}]] // Reverse\)

(% /. {u -> u_, v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

images under inversion

Lemma.  If   w is the range of a subgroup of  gp[x],  then  image[inv[gp[x]], w] = w.

SubstTest[implies, and[member[w, u], subclass[u, v]], 
        member[w, 
          v], {u -> image[IMAGE[SECOND], intersection[GROUPS, P[gp[x]]]], 
          v -> fix[IMAGE[inv[gp[x]]]]}] // Reverse

or[equal[w_, image[inv[gp[x_]], w_]], 
        not[member[w_, 
            image[IMAGE[SECOND], intersection[GROUPS, P[gp[x_]]]]]]] := 
      True

Theorem.  If  w  is the range of a subgroup of direct[gp[x], gp[y]], then  w  is fixed under imaging with the inversion function for  direct[gp[x], gp[y]].

SubstTest[implies, 
        member[w, image[IMAGE[SECOND], intersection[GROUPS, P[gp[z]]]]], 
        member[w, fix[IMAGE[inv[gp[z]]]]], z -> direct[gp[x], gp[y]]] // 
      Reverse

or[equal[w_, composite[inv[gp[y_]], w_, inv[gp[x_]]]], 
        not[member[w_, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, 
                P[composite[cross[gp[x_], gp[y_]], TWIST]]]]]]] := 
      True

Lemma.

SubstTest[implies, and[equal[u, p], equal[v, q]], 
        equal[composite[u, v], 
          composite[p, q]], {p -> composite[inv[gp[z]], u, inv[gp[y]]], 
          q -> composite[inv[gp[y]], v, inv[gp[x]]]}] // Reverse

(% /. {u -> u_, v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Lemma.   (Eliminating  id[range[gp[y]]].)

SubstTest[implies, equal[t, range[gp[y]]], 
        or[equal[composite[u, v], 
            composite[inv[gp[z]], u, id[t], v, inv[gp[x]]]], 
          not[equal[u, composite[inv[gp[z]], u, inv[gp[y]]]]], 
          not[equal[v, composite[inv[gp[y]], v, inv[gp[x]]]]]], 
        t -> union[domain[u], range[gp[y]]]] // Reverse

(% /. {u -> u_, v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Theorem.   If  u  is the range of a subgroup of  direct[gp[y],  gp[z]]  and  v  is the range of a subgroup of  direct[gp[x], gp[y]], then  u ∘ v  is fixed under imaging with the inversion function for  direct[gp[x], gp[z]].

\(Map[not, 
        SubstTest[
          and,  (*implies[p1, p3], implies[p2, p4], \ implies[p1, p5], *) \ 
          implies[p5, p6], implies[and[p3, p4, p6], p7], \ 
          not[implies[and[p1, p2], p7]], {p1 -> 
              member[u, 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[gp[y], gp[z]], TWIST]]]]], 

            p2 -> member[v, 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[gp[x], gp[y]], TWIST]]]]], 
            p3 -> equal[u, composite[inv[gp[z]], u, inv[gp[y]]]], 
            p4 -> equal[v, 
                composite[inv[gp[y]], v, 
                  inv[gp[x]]]], 
p5 -> 
              subclass[u, cart[range[gp[y]], range[gp[z]]]], 
            p6 -> subclass[domain[u], range[gp[y]]], 
            p7 -> equal[composite[u, v], 
                composite[inv[gp[z]], u, v, inv[gp[x]]]]}]] // 
      Reverse\)

(% /. {u -> u_, v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Lemma.

SubstTest[subclass, t, 
      intersection[u, v], {u -> binclosed[direct[gp[x], gp[y]]], 
        v -> fix[IMAGE[inv[direct[gp[x], gp[y]]]]]}]

and[subclass[t_, binclosed[composite[cross[gp[x_], gp[y_]], TWIST]]], 
        subclass[t_, fix[IMAGE[cross[inv[gp[x_]], inv[gp[y_]]]]]]] := 
      subclass[t, 
        union[image[IMAGE[SECOND], 
            intersection[GROUPS, P[composite[cross[gp[x], gp[y]], TWIST]]]], 
          set[0]]]

Lemma.

Map[
      implies[and[not[empty[t]], #], 
          member[t, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, 
                P[composite[cross[gp[x], gp[y]], TWIST]]]]]] &, 
      SubstTest[member, t, 
        intersection[u, v], {u -> binclosed[direct[gp[x], gp[y]]], 
          v -> fix[IMAGE[inv[direct[gp[x], gp[y]]]]]}]]

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

Lemma.

SubstTest[or, equal[0, t], 
        member[t, 
          image[IMAGE[SECOND], 
            intersection[GROUPS, P[composite[cross[gp[x], gp[y]], TWIST]]]]], 
        not[equal[t, composite[inv[gp[y]], t, inv[gp[x]]]]], 
        not[member[t, V]], 
        not[subclass[composite[gp[y], cross[t, t], inverse[gp[x]]], t]], 
        t -> composite[u, v]] // Reverse

(% /. {u -> u_, v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Lemma.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p0, p2, p3], p4], 
          not[implies[and[p0, p1], p4]], {p0 -> 
              and[member[composite[u, v], V], 
                not[disjoint[domain[u], range[v]]]], 
            p1 -> 
              and[member[u, 
                  image[IMAGE[SECOND], 
                    intersection[GROUPS, 
                      P[composite[cross[gp[y], gp[z]], TWIST]]]]], 
                member[v, 
                  image[IMAGE[SECOND], 
                    intersection[GROUPS, 
                      P[composite[cross[gp[x], gp[y]], TWIST]]]]]], 
            p2 -> subclass[
                composite[gp[z], cross[composite[u, v], composite[u, v]], 
                  inverse[gp[x]]], composite[u, v]], 
            p3 -> equal[composite[u, v], 
                composite[inv[gp[z]], u, v, inv[gp[x]]]], 
            p4 -> 
              member[composite[u, v], 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[gp[x], gp[z]], TWIST]]]]]}]] // 
      Reverse

(% /. {u -> u_, v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Lemma.  (Remove the wrappers.)

SubstTest[implies, 
          and[equal[x, gp[r]], equal[y, gp[s]], equal[z, gp[t]]], 
          or[equal[0, intersection[domain[u], range[v]]], 
            member[composite[u, v], 
              image[IMAGE[SECOND], 
                intersection[GROUPS, P[composite[cross[x, z], TWIST]]]]], 
            not[member[u, 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, P[composite[cross[y, z], TWIST]]]]]], 
            not[member[v, 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[x, y], TWIST]]]]]]], {r -> x, 
            s -> y, t -> z}] // MapNotNot // Reverse

(% /. {u -> u_, v -> v_, x -> x_, y -> y_, 
            z -> z_}) /. Equal -> SetDelayed

Lemma.

SubstTest[implies, 
        and[member[t, image[IMAGE[SECOND], intersection[GROUPS, P[z]]]], 
          member[z, GROUPS]], member[e[z], t], 
        z -> direct[gp[x], gp[y]]] // Reverse

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

Theorem.  If  w  is the range of a subgroup of the direct product of groups  x  and  y, then  pair[e[x], e[y]] ∈ w.

SubstTest[implies, and[equal[x, gp[u]], equal[y, gp[v]]], 
          or[equal[0, x], equal[0, y], member[pair[e[x], e[y]], w], 
            not[member[w, 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[x, y], TWIST]]]]]]], {u -> x, 
            v -> y}] // Reverse // MapNotNot

or[member[pair[e[x_], e[y_]], w_], 
        not[member[w_, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[x_, y_], TWIST]]]]]], 
        not[member[x_, GROUPS]], not[member[y_, GROUPS]]] := True

Corollary 1.  If  w  is the range of a subgroup of the direct product of groups  x  and  y, then  e[x] ∈ domain[w].

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p2, p3], p4], 
          not[implies[p1, p4]], {p1 -> 
              and[member[x, GROUPS], member[y, GROUPS], 
                member[w, 
                  image[IMAGE[SECOND], 
                    intersection[GROUPS, 
                      P[composite[cross[x, y], 
                          TWIST]]]]]], 
p2 -> 
              member[pair[e[x], e[y]], w], 
            p3 -> subclass[w, cart[range[x], range[y]]], 
            p4 -> member[e[x], domain[w]]}]] // Reverse

or[member[e[x_], domain[w_]], 
        not[member[w_, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[x_, y_], TWIST]]]]]], 
        not[member[x_, GROUPS]], not[member[y_, GROUPS]]] := True

Corollary 2.  If  w  is the range of a subgroup of the direct product of groups  x  and  y, then  e[y] ∈ range[w].

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p2, p3], p4], 
          not[implies[p1, p4]], {p1 -> 
              and[member[x, GROUPS], member[y, GROUPS], 
                member[w, 
                  image[IMAGE[SECOND], 
                    intersection[GROUPS, 
                      P[composite[cross[x, y], 
                          TWIST]]]]]], 
p2 -> 
              member[pair[e[x], e[y]], w], 
            p3 -> subclass[w, cart[range[x], range[y]]], 
            p4 -> member[e[y], range[w]]}]] // Reverse

or[member[e[y_], range[w_]], 
        not[member[w_, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[x_, y_], TWIST]]]]]], 
        not[member[x_, GROUPS]], not[member[y_, GROUPS]]] := True

Main Theorem.  If  u  is the range of a subgroup of the direct product of groups  y  and  z, and if  v  is the range of a subgroup of the direct product of groups  x  and  y, then the composite relation  u ∘ v  is the range of a subgroup of the direct product of  x  and  z.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p2, p3], p4], implies[and[p1, p4], p5], 
          not[implies[p1, p5]], {p1 -> 
              and[member[u, 
                  image[IMAGE[SECOND], 
                    intersection[GROUPS, P[composite[cross[y, z], TWIST]]]]], 
                member[v, 
                  image[IMAGE[SECOND], 
                    intersection[GROUPS, P[composite[cross[x, y], TWIST]]]]], 
                member[x, GROUPS], member[y, GROUPS], member[z, GROUPS]], 
            p2 -> member[e[y], domain[u]], 
            p3 -> member[e[y], range[v]], 
            p4 -> not[disjoint[domain[u], range[v]]], 
            p5 -> member[composite[u, v], 
                image[IMAGE[SECOND], 
                  intersection[GROUPS, 
                    P[composite[cross[x, z], TWIST]]]]]}]] // 
      Reverse

or[member[composite[u_, v_], 
          image[IMAGE[SECOND], 
            intersection[GROUPS, P[composite[cross[x_, z_], TWIST]]]]], 
        not[member[u_, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[y_, z_], TWIST]]]]]], 
        not[member[v_, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[x_, y_], TWIST]]]]]], 
        not[member[x_, GROUPS]], not[member[y_, GROUPS]], 
        not[member[z_, GROUPS]]] := True

eliminating the variables u and v

In this section, the variables  u  and  v  are eliminated.

Theorem.

Map[empty[composite[Id, complement[#]]] &, 
      SubstTest[class, pair[u, v], 
        implies[and[member[x, r], member[y, r], member[z, r], 
            member[pair[u, v], s]], 
          member[pair[u, v], t]], {r -> GROUPS, 
          s -> cart[
              image[IMAGE[SECOND], 
                intersection[GROUPS, P[composite[cross[y, z], TWIST]]]], 
              image[IMAGE[SECOND], 
                intersection[GROUPS, P[composite[cross[x, y], TWIST]]]]], 
          t -> image[inverse[COMPOSE], 
              image[IMAGE[SECOND], 
                intersection[GROUPS, 
                  P[composite[cross[x, z], TWIST]]]]]}]]

or[not[member[x_, GROUPS]], not[member[y_, GROUPS]], 
        not[member[z_, GROUPS]], 
        subclass[
          image[COMPOSE, 
            cart[image[IMAGE[SECOND], 
                intersection[GROUPS, P[composite[cross[y_, z_], TWIST]]]], 
              image[IMAGE[SECOND], 
                intersection[GROUPS, P[composite[cross[x_, y_], TWIST]]]]]], 
          image[IMAGE[SECOND], 
            intersection[GROUPS, P[composite[cross[x_, z_], TWIST]]]]]] := 
      True

fractions as subgroups

Although rational numbers have not yet been formally defined in the GOEDEL program, it is perhaps apt to contemplate a possible (but non-standard) definition that would give the rationals some nice algebraic properties.  The concentional definition of integers as equivalence classes of a certain equivalence relation amounts to making rational numbers be linear functions in the plane  Z × Z  with the point at the origin forcibly removed.  Restoring that deleted point would make better algebraic sense.  

If  n  and  d  are integers  (with nonzero d),  it is natural to think of the fraction r = n/d  as a linear function that satisfies  n = r(d).   The graph of a linear function is the range of a subgroup of the direct product of INTADD with itself.  Thus the following lemma would then amount to the statement that one could consider any rational number as a certain subgroup of  direct[INTADD, INTADD].  A natural candidate for  n/d  is obtained by rewriting  n/d = (1/d) ∘ (n/1), and identifying  n/1 with  inttimes[n]  and  1/d   with the inverse of  d/1.  Thus:

                                            n/d = inverse[inttimes[d]] ∘ inttimes[n].

This proposed definition of rational numbers is also suggested by analogy with the construction of integers in terms of natural numbers.  In the latter case, an integer is a function in the plane  ω × ω  whose graph is a straight line with slope 1.  Such functions have the form  inverse[plus[a]] ∘ plus[b],  where  a  and  b  are natural numbers.  These lines are parallel to one another and are the equivalence classes of the equivalence relaton  EQUIDIFF.

Lemma.  If  x  and  y  are integers, then  inverse[inttimes[x]] ∘ inttimes[y]  is the range of a subgroup of the direct product of  INTADD with itself.

SubstTest[or, 
        member[composite[u, v], 
          image[IMAGE[SECOND], 
            intersection[GROUPS, P[composite[cross[r, t], TWIST]]]]], 
        not[member[u, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[s, t], TWIST]]]]]], 
        not[member[v, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[r, s], TWIST]]]]]], 
        not[member[r, GROUPS]], not[member[s, GROUPS]], 
        not[member[t, GROUPS]], {r -> INTADD, s -> INTADD, 
          t -> INTADD, u -> inverse[inttimes[x]], 
          v -> inttimes[y]}] // Reverse

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

Lemma.  The converse statement.

SubstTest[or, not[empty[w]], 
        not[member[w, 
            image[IMAGE[SECOND], 
              intersection[GROUPS, P[composite[cross[u, v], TWIST]]]]]], 
        not[member[u, GROUPS]], 
        not[member[v, GROUPS]], {u -> INTADD, v -> INTADD, 
          w -> composite[inverse[inttimes[x]], inttimes[y]]}] // 
      Reverse

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

Theorem.  The relation  inverse[inttimes[x]] ∘ inttimes[y]  is the range of a subgroup of the direct product of  INTADD with itself if and only if  x  and  y  are both integers.

equiv[
      member[composite[inverse[inttimes[x]], inttimes[y]], 
        image[IMAGE[SECOND], 
          intersection[GROUPS, P[composite[cross[INTADD, INTADD], TWIST]]]]], 
      and[member[x, Z], member[y, Z]]]

member[composite[inverse[inttimes[x_]], inttimes[y_]], 
        image[IMAGE[SECOND], 
          intersection[GROUPS, P[composite[cross[INTADD, INTADD], TWIST]]]]] := 
      and[member[x, Z], member[y, Z]]