The Left Identity is the Right Identity

---------------------------------------

 

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

       where g is the underlying set that is closed under +

       '_' is the right inverse operator

       0 is the right identity

 

Outline:

 

Let x e g. Applying the axioms of group theory, we have:

 

0+x = x+_x+x    (Inverse)

    = x+(_x+x)  (Associativity)

    = x+0       (Previous Result)

    = x         (Identity)

 

 

Given The Group Axioms

----------------------

 

G1:

 

1     Set(g)

      Axiom

 

G2:

 

2     0 e g

      Axiom

 

G3: Closure

 

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

      Axiom

 

G4: Associativity

 

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

      Axiom

 

G5: Right Identity

 

5     ALL(a):[a e g => a+0=a]

      Axiom

 

G6:

 

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

      Axiom

 

G7: Right Inverse

 

7     ALL(a):[a e g => a+_a=0]

      Axiom

 

Previous result: The left inverse is the right inverse

 

8     ALL(a):[a e g => _a+a=0]

      Axiom

 

    

     Proof

     -----

    

     Suppose...

 

      9     x e g

            Premise

 

     Apply G6

 

      10    x e g => _x e g

            U Spec, 6

 

      11    _x e g

            Detach, 10, 9

 

     Apply G7

 

      12    x e g => x+_x=0

            U Spec, 7

 

      13    x+_x=0

            Detach, 12, 9

 

     Apply reflexivity

 

      14    0+x=0+x

            Reflex

 

      15    0+x=x+_x+x

            Substitute, 13, 14

 

     Apply G4

 

      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 & _x e g & c e g => x+_x+c=x+(_x+c)]

            U Spec, 16

 

      18    x e g & _x e g & x e g => x+_x+x=x+(_x+x)

            U Spec, 17

 

      19    x e g & _x e g

            Join, 9, 11

 

      20    x e g & _x e g & x e g

            Join, 19, 9

 

      21    x+_x+x=x+(_x+x)

            Detach, 18, 20

 

      22    0+x=x+(_x+x)

            Substitute, 21, 15

 

     Apply previous result

 

      23    x e g => _x+x=0

            U Spec, 8

 

      24    _x+x=0

            Detach, 23, 9

 

      25    0+x=x+0

            Substitute, 24, 22

 

     Apply G5

 

      26    x e g => x+0=x

            U Spec, 5

 

      27    x+0=x

            Detach, 26, 9

 

      28    0+x=x

            Substitute, 27, 25

 

As Required:

 

29    ALL(a):[a e g => 0+a=a]

      4 Conclusion, 9

 

     Prove: ALL(a):[a e g => a+0=a & 0+a=a]

    

     Suppose...

 

      30    x e g

            Premise

 

      31    x e g => x+0=x

            U Spec, 5

 

      32    x+0=x

            Detach, 31, 30

 

      33    x e g => 0+x=x

            U Spec, 29

 

      34    0+x=x

            Detach, 33, 30

 

      35    x+0=x & 0+x=x

            Join, 32, 34

 

As Required:

 

36    ALL(a):[a e g => a+0=a & 0+a=a]

      4 Conclusion, 30