THEOREM

*******

 

Introducing an equivalent definition of a group that defines an inverse function inv: G --> G

 

Given: Group(g) <=> ALL(a):ALL(b):[a e g & b e g => a*b e g]          (Previous result, link below)

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

       & EXIST(e):[e e g

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

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

 

Prove: Group(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)]

       & EXIST(e):[e e g

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

       & EXIST(inv):ALL(a):[a e g => inv(a) e g & a*inv(a)=e & inv(a)*a=e]]  <--- inv function on G

 

 

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

 

 

PREVIOUS RESULT

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

 

Definition of group with right and left identity and inverse elements    (See proof)

 

1     ALL(g):[Group(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)]

     & EXIST(e):[e e g

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

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

      Axiom

 

 

Suppose g is a set (used to construct inv function)

 

2     Set(g)

      Premise

 

    

     '=>'

    

     Suppose...

 

      3     Group(g)

            Premise

 

     Apply previous result

 

      4     Group(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)]

          & EXIST(e):[e e g

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

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

            U Spec, 1

 

      5     [Group(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)]

          & EXIST(e):[e e g

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

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

          & [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)]

          & EXIST(e):[e e g

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

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

            Iff-And, 4

 

      6     Group(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)]

          & EXIST(e):[e e g

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

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

            Split, 5

 

      7     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)]

          & EXIST(e):[e e g

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

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

            Split, 5

 

      8     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)]

          & EXIST(e):[e e g

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

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

            Detach, 6, 3

 

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

            Split, 8

 

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

            Split, 8

 

      11    EXIST(e):[e e g

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

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

            Split, 8

 

      12    e e g

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

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

            E Spec, 11

 

      13    e e g

            Split, 12

 

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

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

            Split, 12

 

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

            Split, 14

 

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

            Split, 14

 

    

     Construct g2

    

     Apply Cartesian Product Axiom

 

      17    ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]

            Cart Prod

 

      18    ALL(a2):[Set(g) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g & c2 e a2]]]

            U Spec, 17

 

      19    Set(g) & Set(g) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g & c2 e g]]

            U Spec, 18

 

      20    Set(g) & Set(g)

            Join, 2, 2

 

      21    EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e g & c2 e g]]

            Detach, 19, 20

 

      22    Set'(g2) & ALL(c1):ALL(c2):[(c1,c2) e g2 <=> c1 e g & c2 e g]

            E Spec, 21

 

    

     Define: g2

 

      23    Set'(g2)

            Split, 22

 

      24    ALL(c1):ALL(c2):[(c1,c2) e g2 <=> c1 e g & c2 e g]

            Split, 22

 

    

     Construct inv

    

     Apply Subset Axiom

 

      25    EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e g2 & a*b=e]]

            Subset, 23

 

      26    Set'(inv) & ALL(a):ALL(b):[(a,b) e inv <=> (a,b) e g2 & a*b=e]

            E Spec, 25

 

    

     Define: inv

 

      27    Set'(inv)

            Split, 26

 

      28    ALL(a):ALL(b):[(a,b) e inv <=> (a,b) e g2 & a*b=e]

            Split, 26

 

    

     Prove: inv is a function

    

     Apply Function Axiom

 

      29    ALL(f):ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]

          & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e f]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]

          => ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]]

            Function

 

      30    ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e inv => c e a & d e b]

          & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e inv]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]

          => ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]]

            U Spec, 29

 

      31    ALL(b):[ALL(c):ALL(d):[(c,d) e inv => c e g & d e b]

          & ALL(c):[c e g => EXIST(d):[d e b & (c,d) e inv]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]

          => ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]]

            U Spec, 30

 

    

     Sufficient: For functionality of inv

 

      32    ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]

          & ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]

          => ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]

            U Spec, 31

 

         

          Prove: ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]

         

          Suppose...

 

            33    (x,y) e inv

                  Premise

 

          Apply definition of inv

 

            34    ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]

                  U Spec, 28

 

            35    (x,y) e inv <=> (x,y) e g2 & x*y=e

                  U Spec, 34

 

            36    [(x,y) e inv => (x,y) e g2 & x*y=e]

              & [(x,y) e g2 & x*y=e => (x,y) e inv]

                  Iff-And, 35

 

            37    (x,y) e inv => (x,y) e g2 & x*y=e

                  Split, 36

 

            38    (x,y) e g2 & x*y=e => (x,y) e inv

                  Split, 36

 

            39    (x,y) e g2 & x*y=e

                  Detach, 37, 33

 

            40    (x,y) e g2

                  Split, 39

 

            41    x*y=e

                  Split, 39

 

          Apply definition of g2

 

            42    ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]

                  U Spec, 24

 

            43    (x,y) e g2 <=> x e g & y e g

                  U Spec, 42

 

            44    [(x,y) e g2 => x e g & y e g]

              & [x e g & y e g => (x,y) e g2]

                  Iff-And, 43

 

            45    (x,y) e g2 => x e g & y e g

                  Split, 44

 

            46    x e g & y e g => (x,y) e g2

                  Split, 44

 

            47    x e g & y e g

                  Detach, 45, 40

 

     Functionality, Part 1

    

     As Required:

 

      48    ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]

            4 Conclusion, 33

 

         

          Prove: ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]

         

          Suppose...

 

            49    x e g

                  Premise

 

          Apply premise

 

            50    x e g => EXIST(b):[b e g & [x*b=e & b*x=e]]

                  U Spec, 16

 

            51    EXIST(b):[b e g & [x*b=e & b*x=e]]

                  Detach, 50, 49

 

            52    x' e g & [x*x'=e & x'*x=e]

                  E Spec, 51

 

            53    x' e g

                  Split, 52

 

            54    x*x'=e & x'*x=e

                  Split, 52

 

            55    x*x'=e

                  Split, 54

 

            56    x'*x=e

                  Split, 54

 

          Apply definiton of inv

 

            57    ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]

                  U Spec, 28

 

            58    (x,x') e inv <=> (x,x') e g2 & x*x'=e

                  U Spec, 57

 

            59    [(x,x') e inv => (x,x') e g2 & x*x'=e]

              & [(x,x') e g2 & x*x'=e => (x,x') e inv]

                  Iff-And, 58

 

            60    (x,x') e inv => (x,x') e g2 & x*x'=e

                  Split, 59

 

            61    (x,x') e g2 & x*x'=e => (x,x') e inv

                  Split, 59

 

            62    ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]

                  U Spec, 24

 

          Apply definition of g2

 

            63    (x,x') e g2 <=> x e g & x' e g

                  U Spec, 62

 

            64    [(x,x') e g2 => x e g & x' e g]

              & [x e g & x' e g => (x,x') e g2]

                  Iff-And, 63

 

            65    (x,x') e g2 => x e g & x' e g

                  Split, 64

 

            66    x e g & x' e g => (x,x') e g2

                  Split, 64

 

            67    x e g & x' e g

                  Join, 49, 53

 

            68    (x,x') e g2

                  Detach, 66, 67

 

            69    (x,x') e g2 & x*x'=e

                  Join, 68, 55

 

            70    (x,x') e inv

                  Detach, 61, 69

 

            71    x' e g & (x,x') e inv

                  Join, 53, 70

 

     Functionality, Part 2

    

     As Required:

 

      72    ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]

            4 Conclusion, 49

 

         

          Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]

         

          Suppose...

 

            73    (x,y1) e inv & (x,y2) e inv

                  Premise

 

            74    (x,y1) e inv

                  Split, 73

 

            75    (x,y2) e inv

                  Split, 73

 

          Apply definition of inv

 

            76    ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]

                  U Spec, 28

 

            77    (x,y1) e inv <=> (x,y1) e g2 & x*y1=e

                  U Spec, 76

 

            78    [(x,y1) e inv => (x,y1) e g2 & x*y1=e]

              & [(x,y1) e g2 & x*y1=e => (x,y1) e inv]

                  Iff-And, 77

 

            79    (x,y1) e inv => (x,y1) e g2 & x*y1=e

                  Split, 78

 

            80    (x,y1) e g2 & x*y1=e => (x,y1) e inv

                  Split, 78

 

            81    (x,y1) e g2 & x*y1=e

                  Detach, 79, 74

 

            82    (x,y1) e g2

                  Split, 81

 

            83    x*y1=e

                  Split, 81

 

          Apply definition of g2

 

            84    ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]

                  U Spec, 24

 

            85    (x,y1) e g2 <=> x e g & y1 e g

                  U Spec, 84

 

            86    [(x,y1) e g2 => x e g & y1 e g]

              & [x e g & y1 e g => (x,y1) e g2]

                  Iff-And, 85

 

            87    (x,y1) e g2 => x e g & y1 e g

                  Split, 86

 

            88    x e g & y1 e g => (x,y1) e g2

                  Split, 86

 

            89    x e g & y1 e g

                  Detach, 87, 82

 

            90    x e g

                  Split, 89

 

            91    y1 e g

                  Split, 89

 

          Apply definition of inv

 

            92    (x,y2) e inv <=> (x,y2) e g2 & x*y2=e

                  U Spec, 76

 

            93    [(x,y2) e inv => (x,y2) e g2 & x*y2=e]

              & [(x,y2) e g2 & x*y2=e => (x,y2) e inv]

                  Iff-And, 92

 

            94    (x,y2) e inv => (x,y2) e g2 & x*y2=e

                  Split, 93

 

            95    (x,y2) e g2 & x*y2=e => (x,y2) e inv

                  Split, 93

 

            96    (x,y2) e g2 & x*y2=e

                  Detach, 94, 75

 

            97    (x,y2) e g2

                  Split, 96

 

            98    x*y2=e

                  Split, 96

 

          Apply definition of g2

 

            99    (x,y2) e g2 <=> x e g & y2 e g

                  U Spec, 84

 

            100  [(x,y2) e g2 => x e g & y2 e g]

              & [x e g & y2 e g => (x,y2) e g2]

                  Iff-And, 99

 

            101  (x,y2) e g2 => x e g & y2 e g

                  Split, 100

 

            102  x e g & y2 e g => (x,y2) e g2

                  Split, 100

 

            103  x e g & y2 e g

                  Detach, 101, 97

 

            104  x e g

                  Split, 103

 

            105  y2 e g

                  Split, 103

 

            106  x*y1=x*y2

                  Substitute, 98, 83

 

          Apply premise

 

            107  x e g => EXIST(b):[b e g & [x*b=e & b*x=e]]

                  U Spec, 16

 

            108  EXIST(b):[b e g & [x*b=e & b*x=e]]

                  Detach, 107, 90

 

            109  x' e g & [x*x'=e & x'*x=e]

                  E Spec, 108

 

            110  x' e g

                  Split, 109

 

            111  x*x'=e & x'*x=e

                  Split, 109

 

            112  x*x'=e

                  Split, 111

 

            113  x'*x=e

                  Split, 111

 

            114  x'*x*y1=x'*x*y1

                  Reflex

 

            115  e*y1=x'*x*y1

                  Substitute, 113, 114

 

          Apply premise

 

            116  y1 e g => y1*e=y1 & e*y1=y1

                  U Spec, 15

 

            117  y1*e=y1 & e*y1=y1

                  Detach, 116, 91

 

            118  y1*e=y1

                  Split, 117

 

            119  e*y1=y1

                  Split, 117

 

            120  y1=x'*x*y1

                  Substitute, 119, 115

 

          Apply associativity

 

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

                  U Spec, 10

 

            122  ALL(c):[x' e g & x e g & c e g => x'*x*c=x'*(x*c)]

                  U Spec, 121

 

            123  x' e g & x e g & y1 e g => x'*x*y1=x'*(x*y1)

                  U Spec, 122

 

            124  x' e g & x e g

                  Join, 110, 90

 

            125  x' e g & x e g & y1 e g

                  Join, 124, 91

 

            126  x'*x*y1=x'*(x*y1)

                  Detach, 123, 125

 

            127  y1=x'*(x*y1)

                  Substitute, 126, 120

 

            128  y1=x'*(x*y2)

                  Substitute, 106, 127

 

          Apply associativity

 

            129  x' e g & x e g & y2 e g => x'*x*y2=x'*(x*y2)

                  U Spec, 122

 

            130  x' e g & x e g & y2 e g

                  Join, 124, 105

 

            131  x'*x*y2=x'*(x*y2)

                  Detach, 129, 130

 

            132  y1=x'*x*y2

                  Substitute, 131, 128

 

            133  y1=e*y2

                  Substitute, 113, 132

 

            134  y2 e g => y2*e=y2 & e*y2=y2

                  U Spec, 15

 

            135  y2*e=y2 & e*y2=y2

                  Detach, 134, 105

 

            136  y2*e=y2

                  Split, 135

 

            137  e*y2=y2

                  Split, 135

 

            138  y1=y2

                  Substitute, 137, 133

 

     Functionality, Part 3

    

     As Required:

 

      139  ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]

            4 Conclusion, 73

 

     Joining results...

 

      140  ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]

          & ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]

            Join, 48, 72

 

      141  ALL(c):ALL(d):[(c,d) e inv => c e g & d e g]

          & ALL(c):[c e g => EXIST(d):[d e g & (c,d) e inv]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e inv & (c,d2) e inv => d1=d2]

            Join, 140, 139

 

    

     inv is a function

    

     As Required:

 

      142  ALL(c):ALL(d):[d=inv(c) <=> (c,d) e inv]

            Detach, 32, 141

 

         

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

         

          Suppose...

 

            143  x e g

                  Premise

 

          Apply premise

 

            144  x e g => EXIST(b):[b e g & [x*b=e & b*x=e]]

                  U Spec, 16

 

            145  EXIST(b):[b e g & [x*b=e & b*x=e]]

                  Detach, 144, 143

 

            146  x' e g & [x*x'=e & x'*x=e]

                  E Spec, 145

 

            147  x' e g

                  Split, 146

 

            148  x*x'=e & x'*x=e

                  Split, 146

 

            149  x*x'=e

                  Split, 148

 

            150  x'*x=e

                  Split, 148

 

          Apply definition inv

 

            151  ALL(b):[(x,b) e inv <=> (x,b) e g2 & x*b=e]

                  U Spec, 28

 

            152  (x,x') e inv <=> (x,x') e g2 & x*x'=e

                  U Spec, 151

 

            153  [(x,x') e inv => (x,x') e g2 & x*x'=e]

              & [(x,x') e g2 & x*x'=e => (x,x') e inv]

                  Iff-And, 152

 

            154  (x,x') e inv => (x,x') e g2 & x*x'=e

                  Split, 153

 

            155  (x,x') e g2 & x*x'=e => (x,x') e inv

                  Split, 153

 

          Apply definition of g2

 

            156  ALL(c2):[(x,c2) e g2 <=> x e g & c2 e g]

                  U Spec, 24

 

            157  (x,x') e g2 <=> x e g & x' e g

                  U Spec, 156

 

            158  [(x,x') e g2 => x e g & x' e g]

              & [x e g & x' e g => (x,x') e g2]

                  Iff-And, 157

 

            159  (x,x') e g2 => x e g & x' e g

                  Split, 158

 

            160  x e g & x' e g => (x,x') e g2

                  Split, 158

 

            161  x e g & x' e g

                  Join, 143, 147

 

            162  (x,x') e g2

                  Detach, 160, 161

 

            163  (x,x') e g2 & x*x'=e

                  Join, 162, 149

 

            164  (x,x') e inv

                  Detach, 155, 163

 

          Apply definition of inv

 

            165  ALL(b):[(x',b) e inv <=> (x',b) e g2 & x'*b=e]

                  U Spec, 28

 

            166  (x',x) e inv <=> (x',x) e g2 & x'*x=e

                  U Spec, 165

 

            167  [(x',x) e inv => (x',x) e g2 & x'*x=e]

              & [(x',x) e g2 & x'*x=e => (x',x) e inv]

                  Iff-And, 166

 

            168  (x',x) e inv => (x',x) e g2 & x'*x=e

                  Split, 167

 

            169  (x',x) e g2 & x'*x=e => (x',x) e inv

                  Split, 167

 

          Apply definition of g2

 

            170  ALL(c2):[(x',c2) e g2 <=> x' e g & c2 e g]

                  U Spec, 24

 

            171  (x',x) e g2 <=> x' e g & x e g

                  U Spec, 170

 

            172  [(x',x) e g2 => x' e g & x e g]

              & [x' e g & x e g => (x',x) e g2]

                  Iff-And, 171

 

            173  (x',x) e g2 => x' e g & x e g

                  Split, 172

 

            174  x' e g & x e g => (x',x) e g2

                  Split, 172

 

            175  x' e g & x e g

                  Join, 147, 143

 

            176  (x',x) e g2

                  Detach, 174, 175

 

            177  (x',x) e g2 & x'*x=e

                  Join, 176, 150

 

            178  (x',x) e inv

                  Detach, 169, 177

 

          Apply functionality of inv

 

            179  ALL(d):[d=inv(x) <=> (x,d) e inv]

                  U Spec, 142

 

            180  x'=inv(x) <=> (x,x') e inv

                  U Spec, 179

 

            181  [x'=inv(x) => (x,x') e inv]

              & [(x,x') e inv => x'=inv(x)]

                  Iff-And, 180

 

            182  x'=inv(x) => (x,x') e inv

                  Split, 181

 

            183  (x,x') e inv => x'=inv(x)

                  Split, 181

 

            184  x'=inv(x)

                  Detach, 183, 164

 

          Apply fuctionality of inv

 

            185  ALL(d):[d=inv(x') <=> (x',d) e inv]

                  U Spec, 142

 

            186  x=inv(x') <=> (x',x) e inv

                  U Spec, 185

 

            187  [x=inv(x') => (x',x) e inv]

              & [(x',x) e inv => x=inv(x')]

                  Iff-And, 186

 

            188  x=inv(x') => (x',x) e inv

                  Split, 187

 

            189  (x',x) e inv => x=inv(x')

                  Split, 187

 

            190  x=inv(x')

                  Detach, 189, 178

 

            191  x*inv(x)=e

                  Substitute, 184, 149

 

            192  inv(x)*x=e

                  Substitute, 184, 150

 

            193  inv(x) e g

                  Substitute, 184, 147

 

            194  inv(x) e g & x*inv(x)=e

                  Join, 193, 191

 

            195  inv(x) e g & x*inv(x)=e & inv(x)*x=e

                  Join, 194, 192

 

     As Required:

 

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

            4 Conclusion, 143

 

    

     Generalizing...

 

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

            E Gen, 196

 

     Joining results...

 

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

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

            Join, 15, 197

 

      199  e e g

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

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

            Join, 13, 198

 

     Generalizing...

 

      200  EXIST(e):[e e g

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

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

            E Gen, 199

 

     Joining results...

 

      201  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)]

            Join, 9, 10

 

      202  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)]

          & EXIST(e):[e e g

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

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

            Join, 201, 200

 

As Required:

 

203  Group(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)]

     & EXIST(e):[e e g

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

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

      4 Conclusion, 3

 

    

     '<='

    

     Prove: 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)]

            & EXIST(e):[e e g

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

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

            => Group(g)

    

     Suppose...

 

      204  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)]

          & EXIST(e):[e e g

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

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

            Premise

 

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

            Split, 204

 

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

            Split, 204

 

      207  EXIST(e):[e e g

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

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

            Split, 204

 

      208  e e g

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

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

            E Spec, 207

 

      209  e e g

            Split, 208

 

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

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

            Split, 208

 

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

            Split, 210

 

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

            Split, 210

 

     Apply premise

 

      213  Group(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)]

          & EXIST(e):[e e g

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

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

            U Spec, 1

 

      214  [Group(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)]

          & EXIST(e):[e e g

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

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

          & [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)]

          & EXIST(e):[e e g

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

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

            Iff-And, 213

 

      215  Group(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)]

          & EXIST(e):[e e g

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

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

            Split, 214

 

    

     Sufficient: For Group(g)

 

      216  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)]

          & EXIST(e):[e e g

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

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

            Split, 214

 

         

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

         

          Suppose...

 

            217  x e g

                  Premise

 

          Apply premise

 

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

                  E Spec, 212

 

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

                  U Spec, 218

 

            220  inv(x) e g & x*inv(x)=e & inv(x)*x=e

                  Detach, 219, 217

 

            221  inv(x) e g

                  Split, 220

 

            222  x*inv(x)=e

                  Split, 220

 

            223  inv(x)*x=e

                  Split, 220

 

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

                  Join, 222, 223

 

            225  inv(x) e g & [x*inv(x)=e & inv(x)*x=e]

                  Join, 221, 224

 

            226  EXIST(b):[b e g & [x*b=e & b*x=e]]

                  E Gen, 225

 

     As Required:

 

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

            4 Conclusion, 217

 

     Joining results...

 

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

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

            Join, 211, 227

 

      229  e e g

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

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

            Join, 209, 228

 

     Generalizing...

 

      230  EXIST(e):[e e g

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

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

            E Gen, 229

 

      231  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)]

            Join, 205, 206

 

      232  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)]

          & EXIST(e):[e e g

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

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

            Join, 231, 230

 

      233  Group(g)

            Detach, 216, 232

 

As Required:

 

234  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)]

     & EXIST(e):[e e g

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

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

     => Group(g)

      4 Conclusion, 204

 

Joining '=>' and '<=' to obtain '<=>'

 

235  [Group(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)]

     & EXIST(e):[e e g

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

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

     & [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)]

     & EXIST(e):[e e g

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

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

     => Group(g)]

      Join, 203, 234

 

As Required:

 

236  Group(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)]

     & EXIST(e):[e e g

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

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

      Iff-And, 235