THEOREM

*******

 

Elementary propositions in group theory:

 

  1. Right cancellation of *              Line 9

  2. Left cancellation of *               Line 54

  3. Determine identity (right)           Line 210

  4. Determine identity (left)            Line 238

  5. Determine inverse (right & left)     Line 135

  6. inv(e)=e                             Line 199

  7. inv(inv(x)) = x                      Line 95

  8. inv(x*y) = inv(y)*inv(x)             Line 265

 

 

This fomral proof was written and machine-verified with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com

 

    

     Suppose (g,*) is group with identity e and inverse operator inv

 

      1     Set(g)

          & ALL(a):ALL(b):[a e g & b e g => a*b e g]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]

          & e e g

          & ALL(a):[a e g => a*e=a & e*a=a]

          & ALL(a):[a e g => inv(a) e g]

          & ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]

            Premise

 

    

     Define: g

 

      2     Set(g)

            Split, 1

 

    

     Define: *

 

      3     ALL(a):ALL(b):[a e g & b e g => a*b e g]9

            Split, 1

 

      4     ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]

            Split, 1

 

    

     Define: e

 

      5     e e g

            Split, 1

 

      6     ALL(a):[a e g => a*e=a & e*a=a]

            Split, 1

 

    

     Define: inv

 

      7     ALL(a):[a e g => inv(a) e g]

            Split, 1

 

      8     ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]

            Split, 1

 

         

          Right cancellation

          ******************

         

          Prove: ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

         

          Suppose...

 

            9     x e g & y e g & z e g

                  Premise

 

            10    x e g

                  Split, 9

 

            11    y e g

                  Split, 9

 

            12    z e g

                  Split, 9

 

             

              Prove: x*y=z*y => x=z

             

              Suppose...

 

                  13    x*y=z*y

                        Premise

 

                  14    x*y*inv(y)=x*y*inv(y)

                        Reflex

 

                  15    x*y*inv(y)=z*y*inv(y)

                        Substitute, 13, 14

 

              Apply associativity

 

                  16    ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]

                        U Spec, 4

 

                  17    ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]

                        U Spec, 16

 

                  18    x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))

                        U Spec, 17

 

                  19    y e g => inv(y) e g

                        U Spec, 7

 

                  20    inv(y) e g

                        Detach, 19, 11

 

                  21    x e g & y e g

                        Join, 10, 11

 

                  22    x e g & y e g & inv(y) e g

                        Join, 21, 20

 

                  23    x*y*inv(y)=x*(y*inv(y))

                        Detach, 18, 22

 

                  24    x*(y*inv(y))=z*y*inv(y)

                        Substitute, 23, 15

 

              Apply definition of inv

 

                  25    y e g => y*inv(y)=e & inv(y)*y=e

                        U Spec, 8

 

                  26    y*inv(y)=e & inv(y)*y=e

                        Detach, 25, 11

 

                  27    y*inv(y)=e

                        Split, 26

 

                  28    inv(y)*y=e

                        Split, 26

 

                  29    x*e=z*y*inv(y)

                        Substitute, 27, 24

 

                  30    x e g => x*e=x & e*x=x

                        U Spec, 6

 

                  31    x*e=x & e*x=x

                        Detach, 30, 10

 

                  32    x*e=x

                        Split, 31

 

                  33    e*x=x

                        Split, 31

 

                  34    x=z*y*inv(y)

                        Substitute, 32, 29

 

              Apply associativity

 

                  35    ALL(b):ALL(c):[z e g & b e g & c e g => z*b*c=z*(b*c)]

                        U Spec, 4

 

                  36    ALL(c):[z e g & y e g & c e g => z*y*c=z*(y*c)]

                        U Spec, 35

 

                  37    z e g & y e g & inv(y) e g => z*y*inv(y)=z*(y*inv(y))

                        U Spec, 36

 

                  38    z e g & y e g

                        Join, 12, 11

 

                  39    z e g & y e g & inv(y) e g

                        Join, 38, 20

 

                  40    z*y*inv(y)=z*(y*inv(y))

                        Detach, 37, 39

 

                  41    x=z*(y*inv(y))

                        Substitute, 40, 34

 

                  42    y e g => y*inv(y)=e & inv(y)*y=e

                        U Spec, 8

 

                  43    y*inv(y)=e & inv(y)*y=e

                        Detach, 42, 11

 

                  44    y*inv(y)=e

                        Split, 43

 

                  45    inv(y)*y=e

                        Split, 43

 

                  46    x=z*e

                        Substitute, 44, 41

 

                  47    z e g => z*e=z & e*z=z

                        U Spec, 6

 

                  48    z*e=z & e*z=z

                        Detach, 47, 12

 

                  49    z*e=z

                        Split, 48

 

                  50    e*z=z

                        Split, 48

 

                  51    x=z

                        Substitute, 49, 46

 

          As Required:

 

            52    x*y=z*y => x=z

                  4 Conclusion, 13

 

    

     As Required:

 

      53    ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

            4 Conclusion, 9

 

         

          Left cancellation

          *****************

         

          Prove: ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

         

          Suppose...

 

            54    x e g & y e g & z e g

                  Premise

 

            55    x e g

                  Split, 54

 

            56    y e g

                  Split, 54

 

            57    z e g

                  Split, 54

 

             

              Prove: x*y=x*z => y=z

             

              Suppose...

 

                  58    x*y=x*z

                        Premise

 

                  59    inv(x)*(x*y)=inv(x)*(x*y)

                        Reflex

 

                  60    inv(x)*(x*y)=inv(x)*(x*z)

                        Substitute, 58, 59

 

              Apply associativity

 

                  61    ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]

                        U Spec, 4

 

                  62    ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]

                        U Spec, 61

 

                  63    inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)

                        U Spec, 62

 

                  64    x e g => inv(x) e g

                        U Spec, 7

 

                  65    inv(x) e g

                        Detach, 64, 55

 

                  66    inv(x) e g & x e g

                        Join, 65, 55

 

                  67    inv(x) e g & x e g & y e g

                        Join, 66, 56

 

                  68    inv(x)*x*y=inv(x)*(x*y)

                        Detach, 63, 67

 

                  69    inv(x)*x*y=inv(x)*(x*z)

                        Substitute, 68, 60

 

                  70    x e g => x*inv(x)=e & inv(x)*x=e

                        U Spec, 8

 

                  71    x*inv(x)=e & inv(x)*x=e

                        Detach, 70, 55

 

                  72    x*inv(x)=e

                        Split, 71

 

                  73    inv(x)*x=e

                        Split, 71

 

                  74    e*y=inv(x)*(x*z)

                        Substitute, 73, 69

 

                  75    y e g => y*e=y & e*y=y

                        U Spec, 6

 

                  76    y*e=y & e*y=y

                        Detach, 75, 56

 

                  77    y*e=y

                        Split, 76

 

                  78    e*y=y

                        Split, 76

 

                  79    y=inv(x)*(x*z)

                        Substitute, 78, 74

 

              Apply associativity

 

                  80    ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]

                        U Spec, 4

 

                  81    ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]

                        U Spec, 80

 

                  82    inv(x) e g & x e g & z e g => inv(x)*x*z=inv(x)*(x*z)

                        U Spec, 81

 

                  83    inv(x) e g & x e g

                        Join, 65, 55

 

                  84    inv(x) e g & x e g & z e g

                        Join, 83, 57

 

                  85    inv(x)*x*z=inv(x)*(x*z)

                        Detach, 82, 84

 

                  86    y=inv(x)*x*z

                        Substitute, 85, 79

 

                  87    y=e*z

                        Substitute, 73, 86

 

                  88    z e g => z*e=z & e*z=z

                        U Spec, 6

 

                  89    z*e=z & e*z=z

                        Detach, 88, 57

 

                  90    z*e=z

                        Split, 89

 

                  91    e*z=z

                        Split, 89

 

                  92    y=z

                        Substitute, 91, 87

 

            93    x*y=x*z => y=z

                  4 Conclusion, 58

 

     As Required:

 

      94    ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

            4 Conclusion, 54

 

         

          inv(inv(x))=x

          *************

         

          Prove: ALL(a):[a e g => inv(inv(a))=a]

         

          Suppose...

 

            95    x e g

                  Premise

 

          Apply definition of inv

 

            96    x e g => x*inv(x)=e & inv(x)*x=e

                  U Spec, 8

 

            97    x*inv(x)=e & inv(x)*x=e

                  Detach, 96, 95

 

            98    x*inv(x)=e

                  Split, 97

 

            99    inv(x)*x=e

                  Split, 97

 

          Apply definition of inv

 

            100  inv(x) e g => inv(x)*inv(inv(x))=e & inv(inv(x))*inv(x)=e

                  U Spec, 8

 

            101  x e g => inv(x) e g

                  U Spec, 7

 

            102  inv(x) e g

                  Detach, 101, 95

 

            103  inv(x)*inv(inv(x))=e & inv(inv(x))*inv(x)=e

                  Detach, 100, 102

 

            104  inv(x)*inv(inv(x))=e

                  Split, 103

 

            105  inv(inv(x))*inv(x)=e

                  Split, 103

 

            106  e*x=e*x

                  Reflex

 

            107  inv(inv(x))*inv(x)*x=e*x

                  Substitute, 105, 106

 

          Apply associativity

 

            108  ALL(b):ALL(c):[inv(inv(x)) e g & b e g & c e g => inv(inv(x))*b*c=inv(inv(x))*(b*c)]

                  U Spec, 4

 

            109  ALL(c):[inv(inv(x)) e g & inv(x) e g & c e g => inv(inv(x))*inv(x)*c=inv(inv(x))*(inv(x)*c)]

                  U Spec, 108

 

            110  inv(inv(x)) e g & inv(x) e g & x e g => inv(inv(x))*inv(x)*x=inv(inv(x))*(inv(x)*x)

                  U Spec, 109

 

            111  inv(x) e g => inv(inv(x)) e g

                  U Spec, 7

 

            112  x e g => inv(x) e g

                  U Spec, 7

 

            113  inv(x) e g

                  Detach, 112, 95

 

            114  inv(inv(x)) e g

                  Detach, 111, 113

 

            115  inv(inv(x)) e g & inv(x) e g

                  Join, 114, 113

 

            116  inv(inv(x)) e g & inv(x) e g & x e g

                  Join, 115, 95

 

            117  inv(inv(x))*inv(x)*x=inv(inv(x))*(inv(x)*x)

                  Detach, 110, 116

 

            118  inv(inv(x))*(inv(x)*x)=e*x

                  Substitute, 117, 107

 

          Apply definition of inv

 

            119  x e g => x*inv(x)=e & inv(x)*x=e

                  U Spec, 8

 

            120  x*inv(x)=e & inv(x)*x=e

                  Detach, 119, 95

 

            121  x*inv(x)=e

                  Split, 120

 

            122  inv(x)*x=e

                  Split, 120

 

            123  inv(inv(x))*e=e*x

                  Substitute, 122, 118

 

          Apply definition of e

 

            124  inv(inv(x)) e g => inv(inv(x))*e=inv(inv(x)) & e*inv(inv(x))=inv(inv(x))

                  U Spec, 6

 

            125  inv(inv(x))*e=inv(inv(x)) & e*inv(inv(x))=inv(inv(x))

                  Detach, 124, 114

 

            126  inv(inv(x))*e=inv(inv(x))

                  Split, 125

 

            127  e*inv(inv(x))=inv(inv(x))

                  Split, 125

 

            128  inv(inv(x))=e*x

                  Substitute, 126, 123

 

            129  x e g => x*e=x & e*x=x

                  U Spec, 6

 

            130  x*e=x & e*x=x

                  Detach, 129, 95

 

            131  x*e=x

                  Split, 130

 

            132  e*x=x

                  Split, 130

 

            133  inv(inv(x))=x

                  Substitute, 132, 128

 

     As Required:

 

      134  ALL(a):[a e g => inv(inv(a))=a]

            4 Conclusion, 95

 

         

          Determine inverse (right & left)

          ********************************

         

          Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]

         

          Suppose...

 

            135  x e g & y e g

                  Premise

 

            136  x e g

                  Split, 135

 

            137  y e g

                  Split, 135

 

             

              Prove: x*y=e => inv(x)=y & inv(y)=x

             

              Suppose

 

                  138  x*y=e

                        Premise

 

              Apply definition of inv

 

                  139  x e g => x*inv(x)=e & inv(x)*x=e

                        U Spec, 8

 

                  140  x*inv(x)=e & inv(x)*x=e

                        Detach, 139, 136

 

                  141  x*inv(x)=e

                        Split, 140

 

                  142  inv(x)*x=e

                        Split, 140

 

                  143  inv(x)*x*y=inv(x)*x*y

                        Reflex

 

                  144  e*y=inv(x)*x*y

                        Substitute, 142, 143

 

              Apply definition of e

 

                  145  y e g => y*e=y & e*y=y

                        U Spec, 6

 

                  146  y*e=y & e*y=y

                        Detach, 145, 137

 

                  147  y*e=y

                        Split, 146

 

                  148  e*y=y

                        Split, 146

 

                  149  y=inv(x)*x*y

                        Substitute, 148, 144

 

              Apply associativity

 

                  150  ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]

                        U Spec, 4

 

                  151  ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]

                        U Spec, 150

 

                  152  inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)

                        U Spec, 151

 

                  153  x e g => inv(x) e g

                        U Spec, 7

 

                  154  inv(x) e g

                        Detach, 153, 136

 

                  155  inv(x) e g & x e g

                        Join, 154, 136

 

                  156  inv(x) e g & x e g & y e g

                        Join, 155, 137

 

                  157  inv(x)*x*y=inv(x)*(x*y)

                        Detach, 152, 156

 

                  158  y=inv(x)*(x*y)

                        Substitute, 157, 149

 

                  159  y=inv(x)*e

                        Substitute, 138, 158

 

                  160  inv(x) e g => inv(x)*e=inv(x) & e*inv(x)=inv(x)

                        U Spec, 6

 

                  161  inv(x)*e=inv(x) & e*inv(x)=inv(x)

                        Detach, 160, 154

 

                  162  inv(x)*e=inv(x)

                        Split, 161

 

                  163  e*inv(x)=inv(x)

                        Split, 161

 

              As Required:

 

                  164  y=inv(x)

                        Substitute, 162, 159

 

                  165  y e g => y*inv(y)=e & inv(y)*y=e

                        U Spec, 8

 

                  166  y*inv(y)=e & inv(y)*y=e

                        Detach, 165, 137

 

                  167  y*inv(y)=e

                        Split, 166

 

                  168  inv(y)*y=e

                        Split, 166

 

                  169  x*y*inv(y)=x*y*inv(y)

                        Reflex

 

                  170  e*inv(y)=x*y*inv(y)

                        Substitute, 138, 169

 

              Apply definition of e

 

                  171  inv(y) e g => inv(y)*e=inv(y) & e*inv(y)=inv(y)

                        U Spec, 6

 

                  172  y e g => inv(y) e g

                        U Spec, 7

 

                  173  inv(y) e g

                        Detach, 172, 137

 

                  174  inv(y)*e=inv(y) & e*inv(y)=inv(y)

                        Detach, 171, 173

 

                  175  inv(y)*e=inv(y)

                        Split, 174

 

                  176  e*inv(y)=inv(y)

                        Split, 174

 

                  177  inv(y)=x*y*inv(y)

                        Substitute, 176, 170

 

              Apply associativity

 

                  178  ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]

                        U Spec, 4

 

                  179  ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]

                        U Spec, 178

 

                  180  x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))

                        U Spec, 179

 

                  181  x e g & y e g

                        Join, 136, 137

 

                  182  x e g & y e g & inv(y) e g

                        Join, 181, 173

 

                  183  x*y*inv(y)=x*(y*inv(y))

                        Detach, 180, 182

 

                  184  inv(y)=x*(y*inv(y))

                        Substitute, 183, 177

 

                  185  y e g => y*inv(y)=e & inv(y)*y=e

                        U Spec, 8

 

                  186  y*inv(y)=e & inv(y)*y=e

                        Detach, 185, 137

 

                  187  y*inv(y)=e

                        Split, 186

 

                  188  inv(y)*y=e

                        Split, 186

 

                  189  inv(y)=x*e

                        Substitute, 187, 184

 

                  190  x e g => x*e=x & e*x=x

                        U Spec, 6

 

                  191  x*e=x & e*x=x

                        Detach, 190, 136

 

                  192  x*e=x

                        Split, 191

 

                  193  e*x=x

                        Split, 191

 

              As Required:

 

                  194  inv(y)=x

                        Substitute, 192, 189

 

                  195  inv(x)=y

                        Sym, 164

 

                  196  inv(x)=y & inv(y)=x

                        Join, 195, 194

 

          As Required:

 

            197  x*y=e => inv(x)=y & inv(y)=x

                  4 Conclusion, 138

 

     As Required:

 

      198  ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]

            4 Conclusion, 135

 

    

     inv(e)=e

     ********

 

     Prove: inv(e)=e

    

     Apply previous result

 

      199  ALL(b):[e e g & b e g => [e*b=e => inv(e)=b & inv(b)=e]]

            U Spec, 198

 

      200  e e g & e e g => [e*e=e => inv(e)=e & inv(e)=e]

            U Spec, 199

 

      201  e e g & e e g

            Join, 5, 5

 

      202  e*e=e => inv(e)=e & inv(e)=e

            Detach, 200, 201

 

      203  e e g => e*e=e & e*e=e

            U Spec, 6

 

      204  e*e=e & e*e=e

            Detach, 203, 5

 

      205  e*e=e

            Split, 204

 

      206  e*e=e

            Split, 204

 

      207  inv(e)=e & inv(e)=e

            Detach, 202, 206

 

      208  inv(e)=e

            Split, 207

 

     As Required:

 

      209  inv(e)=e

            Split, 207

 

         

          Determine identity (right)

          **************************

         

          Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

         

          Suppose...

 

            210  x e g & y e g

                  Premise

 

            211  x e g

                  Split, 210

 

            212  y e g

                  Split, 210

 

             

              Prove: x*y=x => y=e

             

              Suppose...

 

                  213  x*y=x

                        Premise

 

                  214  inv(x)*x=inv(x)*x

                        Reflex

 

                  215  inv(x)*(x*y)=inv(x)*x

                        Substitute, 213, 214

 

              Apply definition of inv

 

                  216  x e g => x*inv(x)=e & inv(x)*x=e

                        U Spec, 8

 

                  217  x*inv(x)=e & inv(x)*x=e

                        Detach, 216, 211

 

                  218  x*inv(x)=e

                        Split, 217

 

                  219  inv(x)*x=e

                        Split, 217

 

                  220  inv(x)*(x*y)=e

                        Substitute, 219, 215

 

              Apply associativity

 

                  221  ALL(b):ALL(c):[inv(x) e g & b e g & c e g => inv(x)*b*c=inv(x)*(b*c)]

                        U Spec, 4

 

                  222  ALL(c):[inv(x) e g & x e g & c e g => inv(x)*x*c=inv(x)*(x*c)]

                        U Spec, 221

 

                  223  inv(x) e g & x e g & y e g => inv(x)*x*y=inv(x)*(x*y)

                        U Spec, 222

 

                  224  x e g => inv(x) e g

                        U Spec, 7

 

                  225  inv(x) e g

                        Detach, 224, 211

 

                  226  inv(x) e g & x e g

                        Join, 225, 211

 

                  227  inv(x) e g & x e g & y e g

                        Join, 226, 212

 

                  228  inv(x)*x*y=inv(x)*(x*y)

                        Detach, 223, 227

 

                  229  inv(x)*x*y=inv(x)*x

                        Substitute, 228, 215

 

                  230  e*y=e

                        Substitute, 219, 229

 

              Apply defintion of e

 

                  231  y e g => y*e=y & e*y=y

                        U Spec, 6

 

                  232  y*e=y & e*y=y

                        Detach, 231, 212

 

                  233  y*e=y

                        Split, 232

 

                  234  e*y=y

                        Split, 232

 

                  235  y=e

                        Substitute, 234, 230

 

          As Required:

 

            236  x*y=x => y=e

                  4 Conclusion, 213

 

     As Required:

 

      237  ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

            4 Conclusion, 210

 

         

          Determine identity (left)

          *************************

         

          Prove: ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

         

          Suppose

 

            238  x e g & y e g

                  Premise

 

            239  x e g

                  Split, 238

 

            240  y e g

                  Split, 238

 

             

              Prove: x*y=y => x=e

             

              Suppose...

 

                  241  x*y=y

                        Premise

 

                  242  y*inv(y)=y*inv(y)

                        Reflex

 

                  243  x*y*inv(y)=y*inv(y)

                        Substitute, 241, 242

 

              Apply definition of inv

 

                  244  y e g => y*inv(y)=e & inv(y)*y=e

                        U Spec, 8

 

                  245  y*inv(y)=e & inv(y)*y=e

                        Detach, 244, 240

 

                  246  y*inv(y)=e

                        Split, 245

 

                  247  inv(y)*y=e

                        Split, 245

 

                  248  x*y*inv(y)=e

                        Substitute, 246, 243

 

              Apply associativity

 

                  249  ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]

                        U Spec, 4

 

                  250  ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]

                        U Spec, 249

 

                  251  x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))

                        U Spec, 250

 

                  252  y e g => inv(y) e g

                        U Spec, 7

 

                  253  inv(y) e g

                        Detach, 252, 240

 

                  254  x e g & y e g & inv(y) e g

                        Join, 238, 253

 

                  255  x*y*inv(y)=x*(y*inv(y))

                        Detach, 251, 254

 

                  256  x*(y*inv(y))=e

                        Substitute, 255, 248

 

                  257  x*e=e

                        Substitute, 246, 256

 

                  258  x e g => x*e=x & e*x=x

                        U Spec, 6

 

                  259  x*e=x & e*x=x

                        Detach, 258, 239

 

                  260  x*e=x

                        Split, 259

 

                  261  e*x=x

                        Split, 259

 

                  262  x=e

                        Substitute, 260, 257

 

          As Required:

 

            263  x*y=y => x=e

                  4 Conclusion, 241

 

     As Required:

 

      264  ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

            4 Conclusion, 238

 

 

          inv(x*y) = inv(y)*inv(x)

          ************************

         

          Prove: ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]

         

          Suppose...

 

            265  x e g & y e g

                  Premise

 

            266  x e g

                  Split, 265

 

            267  y e g

                  Split, 265

 

          Apply definition of inv

 

            268  x e g => inv(x) e g

                  U Spec, 7

 

            269  inv(x) e g

                  Detach, 268, 266

 

            270  y e g => inv(y) e g

                  U Spec, 7

 

            271  inv(y) e g

                  Detach, 270, 267

 

            272  x*y*(inv(y)*inv(x))=x*y*(inv(y)*inv(x))

                  Reflex

 

          Apply associativity of *

 

            273  ALL(b):ALL(c):[x*y e g & b e g & c e g => x*y*b*c=x*y*(b*c)]

                  U Spec, 4

 

            274  ALL(c):[x*y e g & inv(y) e g & c e g => x*y*inv(y)*c=x*y*(inv(y)*c)]

                  U Spec, 273

 

            275  x*y e g & inv(y) e g & inv(x) e g => x*y*inv(y)*inv(x)=x*y*(inv(y)*inv(x))

                  U Spec, 274

 

            276  ALL(b):[x e g & b e g => x*b e g]

                  U Spec, 3

 

            277  x e g & y e g => x*y e g

                  U Spec, 276

 

            278  x*y e g

                  Detach, 277, 265

 

            279  x*y e g & inv(y) e g

                  Join, 278, 271

 

            280  x*y e g & inv(y) e g & inv(x) e g

                  Join, 279, 269

 

            281  x*y*inv(y)*inv(x)=x*y*(inv(y)*inv(x))

                  Detach, 275, 280

 

            282  x*y*(inv(y)*inv(x))=x*y*inv(y)*inv(x)

                  Substitute, 281, 272

 

          Apply associativity of *

 

            283  ALL(b):ALL(c):[x e g & b e g & c e g => x*b*c=x*(b*c)]

                  U Spec, 4

 

            284  ALL(c):[x e g & y e g & c e g => x*y*c=x*(y*c)]

                  U Spec, 283

 

            285  x e g & y e g & inv(y) e g => x*y*inv(y)=x*(y*inv(y))

                  U Spec, 284

 

            286  x e g & y e g & inv(y) e g

                  Join, 265, 271

 

            287  x*y*inv(y)=x*(y*inv(y))

                  Detach, 285, 286

 

            288  x*y*(inv(y)*inv(x))=x*(y*inv(y))*inv(x)

                  Substitute, 287, 282

 

            289  y e g => y*inv(y)=e & inv(y)*y=e

                  U Spec, 8

 

            290  y*inv(y)=e & inv(y)*y=e

                  Detach, 289, 267

 

            291  y*inv(y)=e

                  Split, 290

 

            292  inv(y)*y=e

                  Split, 290

 

            293  x*y*(inv(y)*inv(x))=x*e*inv(x)

                  Substitute, 291, 288

 

            294  x e g => x*e=x & e*x=x

                  U Spec, 6

 

            295  x*e=x & e*x=x

                  Detach, 294, 266

 

            296  x*e=x

                  Split, 295

 

            297  e*x=x

                  Split, 295

 

            298  x*y*(inv(y)*inv(x))=x*inv(x)

                  Substitute, 296, 293

 

          Apply definition of inv

 

            299  x e g => x*inv(x)=e & inv(x)*x=e

                  U Spec, 8

 

            300  x*inv(x)=e & inv(x)*x=e

                  Detach, 299, 266

 

            301  x*inv(x)=e

                  Split, 300

 

            302  inv(x)*x=e

                  Split, 300

 

            303  x*y*(inv(y)*inv(x))=e

                  Substitute, 301, 298

 

          Apply previous result

 

            304  ALL(b):[x*y e g & b e g => [x*y*b=e => inv(x*y)=b & inv(b)=x*y]]

                  U Spec, 198

 

            305  x*y e g & inv(y)*inv(x) e g => [x*y*(inv(y)*inv(x))=e => inv(x*y)=inv(y)*inv(x) & inv(inv(y)*inv(x))=x*y]

                  U Spec, 304

 

            306  ALL(b):[inv(y) e g & b e g => inv(y)*b e g]

                  U Spec, 3

 

            307  inv(y) e g & inv(x) e g => inv(y)*inv(x) e g

                  U Spec, 306

 

            308  inv(y) e g & inv(x) e g

                  Join, 271, 269

 

            309  inv(y)*inv(x) e g

                  Detach, 307, 308

 

            310  x*y e g & inv(y)*inv(x) e g

                  Join, 278, 309

 

            311  x*y*(inv(y)*inv(x))=e => inv(x*y)=inv(y)*inv(x) & inv(inv(y)*inv(x))=x*y

                  Detach, 305, 310

 

            312  inv(x*y)=inv(y)*inv(x) & inv(inv(y)*inv(x))=x*y

                  Detach, 311, 303

 

            313  inv(x*y)=inv(y)*inv(x)

                  Split, 312

 

     As Required:

 

      314  ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]

            4 Conclusion, 265

 

      315  ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

            Join, 53, 94

 

      316  ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

            Join, 315, 237

 

      317  ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

            Join, 316, 264

 

      318  ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]

            Join, 317, 198

 

      319  ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]

          & inv(e)=e

            Join, 318, 209

 

      320  ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]

          & inv(e)=e

          & ALL(a):[a e g => inv(inv(a))=a]

            Join, 319, 134

 

      321  ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

          & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

          & ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]

          & inv(e)=e

          & ALL(a):[a e g => inv(inv(a))=a]

          & ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]

            Join, 320, 314

 

As Required:

 

322  ALL(g):ALL(e):ALL(inv):[Set(g)

     & ALL(a):ALL(b):[a e g & b e g => a*b e g]

     & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => a*b*c=a*(b*c)]

     & e e g

     & ALL(a):[a e g => a*e=a & e*a=a]

     & ALL(a):[a e g => inv(a) e g]

     & ALL(a):[a e g => a*inv(a)=e & inv(a)*a=e]

     => ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=c*b => a=c]]

     & ALL(a):ALL(b):ALL(c):[a e g & b e g & c e g => [a*b=a*c => b=c]]

     & ALL(a):ALL(b):[a e g & b e g => [a*b=a => b=e]]

     & ALL(a):ALL(b):[a e g & b e g => [a*b=b => a=e]]

     & ALL(a):ALL(b):[a e g & b e g => [a*b=e => inv(a)=b & inv(b)=a]]

     & inv(e)=e

     & ALL(a):[a e g => inv(inv(a))=a]

     & ALL(a):ALL(b):[a e g & b e g => inv(a*b)=inv(b)*inv(a)]]

      4 Conclusion, 1