THEOREM

*******

 

Suppose (g,*) is a group and h is a non-empty, finite subset of g. Then (h,*) is a subgroup of (g,*) if and only if * is closed on h.

 

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

 

 

DEFINITIONS

***********

 

Define: Group

 

Group(g,e,inv) means that (g,*) is a group with identity e and inverse operator inv

 

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

      Axiom

 

Define: Finite

 

A set is said to be finite if and only if there is no injective (1-to-1) function mapping n to s

 

2     ALL(s):[Set(s) => [Finite(s)

     <=> ALL(f):[ALL(a):[a e n => f(a) e s] => ~Injective(f,n,s)]]]

      Axiom

 

Define: Injective

 

Injective(f,a,b) means function f: a --> b is a injective, i.e. a 1-to-1 mapping from a to b

 

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

      Axiom

 

 

REQUIRED PROPERTIES OF N

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

 

4     Set(n)

      Axiom

 

5     1 e n

      Axiom

 

Required properties of + on n

 

6     ALL(a):ALL(b):[a e n & b e n => a+b e n]

      Axiom

 

7     ALL(a):[a e n => [~a=1 => EXIST(b):[b e n & a=b+1]]]

      Axiom

 

Required properties of < on n

 

8     ALL(a):ALL(b):[a e n & b e n => [~a=b => a<b | b<a]]

      Axiom

 

9     ALL(a):ALL(b):[a e n & b e n => [a<b => EXIST(c):[c e n & a+c=b]]]

      Axiom

 

Induction

 

10    ALL(a):[Set(a) & ALL(b):[b e a => b e n] => [1 e a & ALL(b):[b e a => b+1 e a] => ALL(b):[b e n => b e a]]]

      Axiom

 

 

PREVIOUS RESULTS USED

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

 

Lemma 1       Proof

*******

 

Establish the existence a power function such that:

 

   pow(x,1) = x

   pow(x,2) = x*x

   pow(x,3) = x*x*x

   and so on.

 

11    ALL(s):[Set(s)

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

     => EXIST(pow):[ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]

     & ALL(a):[a e s => pow(a,1)=a]

     & ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]]]

      Axiom

 

 

Lemma 2       Proof

*******

 

For each x0 in h, establish the existence of function f: n --> h such that f(x)=pow(x0,x)

 

   f(1) = x0

   f(2) = x0*x0

   f(3) = x0*x0*x0

   and so on.

 

12    ALL(s):ALL(pow):[Set(s)

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

     & ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]

     & ALL(a):[a e s => pow(a,1)=a]

     & ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]

     => ALL(a):[a e s => EXIST(f):[ALL(b):[b e n => f(b) e s]

     & ALL(b):[b e n => f(b)=pow(a,b)]]]]

      Axiom

 

 

Lemma 3       Proof

*******

 

The product of powers rule:  pow(x,y) * pow(x,z) = pow(x,y+z)

 

Analogous to x^y * x^z = x^(y+z)

 

13    ALL(s):ALL(pow):[Set(s)

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

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

     & ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]

     & ALL(a):[a e s => pow(a,1)=a]

     & ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]

     => ALL(a):ALL(b):ALL(c):[a e s & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]]

      Axiom

 

 

Lemma 4       Proof 

*******

 

Elementary results from group theory.  

 

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

      Axiom

 

    

     PROOF

     *****

    

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

 

      15    Group(g,e,inv)

            Premise

 

     Apply definition of Group

 

      16    ALL(e):ALL(inv):[Group(g,e,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]]

            U Spec, 1

 

      17    ALL(inv):[Group(g,e,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]]

            U Spec, 16

 

      18    Group(g,e,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]

            U Spec, 17

 

      19    [Group(g,e,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]]

          & [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] => Group(g,e,inv)]

            Iff-And, 18

 

      20    Group(g,e,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]

            Split, 19

 

      21    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] => Group(g,e,inv)

            Split, 19

 

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

            Detach, 20, 15

 

     Splitting out each statement...

    

     Define: g

 

      23    Set(g)

            Split, 22

 

    

     Define: *

 

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

            Split, 22

 

     * is associative

 

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

            Split, 22

 

    

     Define: e

 

      26    e e g

            Split, 22

 

     e is the identity element

 

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

            Split, 22

 

    

     Define: inv

 

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

            Split, 22

 

     inv(x) is the inverse of x

 

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

            Split, 22

 

    

     Apply Lemma 4

 

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

            U Spec, 14

 

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

            U Spec, 30

 

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

            U Spec, 31

 

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

            Detach, 32, 22

 

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

            Split, 33

 

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

            Split, 33

 

      36    inv(e)=e

            Split, 33

 

         

          Suppose h is a non-empty, finite subset of g

 

            37    Set(h)

              & EXIST(a):a e h

              & Finite(h)

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

                  Premise

 

          Splitting this premise...

 

            38    Set(h)

                  Split, 37

 

            39    EXIST(a):a e h

                  Split, 37

 

            40    Finite(h)

                  Split, 37

 

            41    ALL(a):[a e h => a e g]

                  Split, 37

 

             

              '=>'

             

              Prove: Group(h,e,inv) => ALL(a):ALL(b):[aeh & beh => a*b e h

               

              Suppose...

 

                  42    Group(h,e,inv)

                        Premise

 

              Apply the definition Group

 

                  43    ALL(e):ALL(inv):[Group(h,e,inv) <=> Set(h)

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

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

                   & e e h

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

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

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

                        U Spec, 1

 

                  44    ALL(inv):[Group(h,e,inv) <=> Set(h)

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

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

                   & e e h

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

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

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

                        U Spec, 43

 

                  45    Group(h,e,inv) <=> Set(h)

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

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

                   & e e h

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

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

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

                        U Spec, 44

 

                  46    [Group(h,e,inv) => Set(h)

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

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

                   & e e h

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

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

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

                   & [Set(h)

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

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

                   & e e h

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

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

                   & ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)]

                        Iff-And, 45

 

                  47    Group(h,e,inv) => Set(h)

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

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

                   & e e h

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

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

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

                        Split, 46

 

                  48    Set(h)

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

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

                   & e e h

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

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

                   & ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)

                        Split, 46

 

                  49    Set(h)

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

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

                   & e e h

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

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

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

                        Detach, 47, 42

 

                  50    Set(h)

                        Split, 49

 

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

                        Split, 49

 

          As Required:

 

            52    Group(h,e,inv)

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

                  4 Conclusion, 42

 

             

              '<='

             

              Prove: ALL(a):ALL(b):[a e h & b e h => a*b e h] => Group(h,e,inv)

             

               Suppose...

 

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

                        Premise

 

              Apply the definition of Group

 

                  54    ALL(e):ALL(inv):[Group(h,e,inv) <=> Set(h)

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

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

                   & e e h

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

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

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

                        U Spec, 1

 

                  55    ALL(inv):[Group(h,e,inv) <=> Set(h)

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

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

                   & e e h

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

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

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

                        U Spec, 54

 

                  56    Group(h,e,inv) <=> Set(h)

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

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

                   & e e h

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

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

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

                        U Spec, 55

 

                  57    [Group(h,e,inv) => Set(h)

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

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

                   & e e h

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

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

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

                   & [Set(h)

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

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

                   & e e h

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

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

                   & ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)]

                        Iff-And, 56

 

                  58    Group(h,e,inv) => Set(h)

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

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

                   & e e h

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

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

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

                        Split, 57

 

              Sufficient: For Group(h,e,inv)

 

                  59    Set(h)

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

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

                   & e e h

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

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

                   & ALL(a):[a e h => a*inv(a)=e & inv(a)*a=e] => Group(h,e,inv)

                        Split, 57

 

                  

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

                  

                   Suppose...

 

                        60    x e h & y e h & z e h

                              Premise

 

                        61    x e h

                              Split, 60

 

                        62    y e h

                              Split, 60

 

                        63    z e h

                              Split, 60

 

                   Apply associtativity of * on g

 

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

                              U Spec, 25

 

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

                              U Spec, 64

 

                        66    x e g & y e g & z e g => x*y*z=x*(y*z)

                              U Spec, 65

 

                        67    x e h => x e g

                              U Spec, 41

 

                        68    x e g

                              Detach, 67, 61

 

                        69    y e h => y e g

                              U Spec, 41

 

                        70    y e g

                              Detach, 69, 62

 

                        71    z e h => z e g

                              U Spec, 41

 

                        72    z e g

                              Detach, 71, 63

 

                        73    x e g & y e g

                              Join, 68, 70

 

                        74    x e g & y e g & z e g

                              Join, 73, 72

 

                        75    x*y*z=x*(y*z)

                              Detach, 66, 74

 

              As Required:

 

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

                        4 Conclusion, 60

 

                  

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

                  

                   Suppose...

 

                        77    x e h

                              Premise

 

                   Apply definition of e on g

 

                        78    x e g => x*e=x & e*x=x

                              U Spec, 27

 

                        79    x e h => x e g

                              U Spec, 41

 

                        80    x e g

                              Detach, 79, 77

 

                        81    x*e=x & e*x=x

                              Detach, 78, 80

 

              As Required:

 

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

                        4 Conclusion, 77

 

                  

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

                  

                   Suppose...

 

                        83    x e h

                              Premise

 

                   Apply the definition of inv

 

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

                              U Spec, 29

 

                        85    x e h => x e g

                              U Spec, 41

 

                        86    x e g

                              Detach, 85, 83

 

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

                              Detach, 84, 86

 

              As Required:

 

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

                        4 Conclusion, 83

 

             

              Apply Lemma 1

 

                  89    Set(g)

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

                   => EXIST(pow):[ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]]

                        U Spec, 11

 

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

                        Join, 23, 24

 

                  91    EXIST(pow):[ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]]

                        Detach, 89, 90

 

                  92    ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                        E Spec, 91

 

             

              Define: pow function

 

                  93    ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                        Split, 92

 

                  94    ALL(a):[a e g => pow(a,1)=a]

                        Split, 92

 

                  95    ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                        Split, 92

 

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

                        Join, 23, 24

 

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

                        Join, 96, 25

 

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                        Join, 97, 93

 

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                        Join, 98, 94

 

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                        Join, 99, 95

 

             

              Apply Lemma 2

 

                  101  ALL(pow):[Set(g)

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                   => ALL(a):[a e g => EXIST(f):[ALL(b):[b e n => f(b) e g]

                   & ALL(b):[b e n => f(b)=pow(a,b)]]]]

                        U Spec, 12

 

                  102  Set(g)

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                   => ALL(a):[a e g => EXIST(f):[ALL(b):[b e n => f(b) e g]

                   & ALL(b):[b e n => f(b)=pow(a,b)]]]

                        U Spec, 101

 

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

                        Join, 23, 24

 

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                        Join, 103, 93

 

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                        Join, 104, 94

 

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

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                   & ALL(a):[a e g => pow(a,1)=a]

                   & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                        Join, 105, 95

 

                  107  ALL(a):[a e g => EXIST(f):[ALL(b):[b e n => f(b) e g]

                   & ALL(b):[b e n => f(b)=pow(a,b)]]]

                        Detach, 102, 106

 

                  

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

                  

                   Suppose...

 

                        108  x e h

                              Premise

 

                   Apply the definition of h

 

                        109  x e h => x e g

                              U Spec, 41

 

                        110  x e g

                              Detach, 109, 108

 

                   Apply previous result

 

                        111  x e g => EXIST(f):[ALL(b):[b e n => f(b) e g]

                        & ALL(b):[b e n => f(b)=pow(x,b)]]

                              U Spec, 107

 

                        112  EXIST(f):[ALL(b):[b e n => f(b) e g]

                        & ALL(b):[b e n => f(b)=pow(x,b)]]

                              Detach, 111, 110

 

                        113  ALL(b):[b e n => f(b) e g]

                        & ALL(b):[b e n => f(b)=pow(x,b)]

                              E Spec, 112

 

                  

                   Define: f

 

                        114  ALL(b):[b e n => f(b) e g]

                              Split, 113

 

                        115  ALL(b):[b e n => f(b)=pow(x,b)]

                              Split, 113

 

                        116  Set(h) => [Finite(h)

                        <=> ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]]

                              U Spec, 2

 

                        117  Finite(h)

                        <=> ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]

                              Detach, 116, 38

 

                        118  [Finite(h) => ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]]

                        & [ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)] => Finite(h)]

                              Iff-And, 117

 

                        119  Finite(h) => ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]

                              Split, 118

 

                        120  ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)] => Finite(h)

                              Split, 118

 

                        121  ALL(f):[ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)]

                              Detach, 119, 40

 

                        122  ALL(a):[a e n => f(a) e h] => ~Injective(f,n,h)

                              U Spec, 121

 

                  

                   Prove by induction that * is closed on h

                  

                   Apply Subset Axiom

 

                        123  EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & f(a) e h]]

                              Subset, 4

 

                        124  Set(p1) & ALL(a):[a e p1 <=> a e n & f(a) e h]

                              E Spec, 123

 

                   Define: p1

                  

                   The subset of n on which f is closed

 

                        125  Set(p1)

                              Split, 124

 

                        126  ALL(a):[a e p1 <=> a e n & f(a) e h]

                              Split, 124

 

                   Apply induction axiom

 

                        127  Set(p1) & ALL(b):[b e p1 => b e n] => [1 e p1 & ALL(b):[b e p1 => b+1 e p1] => ALL(b):[b e n => b e p1]]

                              U Spec, 10

 

                       

                        Prove that p1 is a subset of n

                       

                        Suppose...

 

                              128  y e p1

                                    Premise

 

                        Apply the definition p1

 

                              129  y e p1 <=> y e n & f(y) e h

                                    U Spec, 126

 

                              130  [y e p1 => y e n & f(y) e h]

                             & [y e n & f(y) e h => y e p1]

                                    Iff-And, 129

 

                              131  y e p1 => y e n & f(y) e h

                                    Split, 130

 

                              132  y e n & f(y) e h => y e p1

                                    Split, 130

 

                              133  y e n & f(y) e h

                                    Detach, 131, 128

 

                              134  y e n

                                    Split, 133

 

                   As Required:

 

                        135  ALL(b):[b e p1 => b e n]

                              4 Conclusion, 128

 

                        136  Set(p1) & ALL(b):[b e p1 => b e n]

                              Join, 125, 135

 

                  

                   Sufficient: ALL(b):[b e n => b e p1]

 

                        137  1 e p1 & ALL(b):[b e p1 => b+1 e p1] => ALL(b):[b e n => b e p1]

                              Detach, 127, 136

 

                  

                   Base Case

                   *********

                  

                   Prove: 1 e p1

                  

                   Apply the definition of p1

 

                        138  1 e p1 <=> 1 e n & f(1) e h

                              U Spec, 126

 

                        139  [1 e p1 => 1 e n & f(1) e h]

                        & [1 e n & f(1) e h => 1 e p1]

                              Iff-And, 138

 

                        140  1 e p1 => 1 e n & f(1) e h

                              Split, 139

 

                        141  1 e n & f(1) e h => 1 e p1

                              Split, 139

 

                   Apply definition of f

 

                        142  1 e n => f(1)=pow(x,1)

                              U Spec, 115

 

                        143  f(1)=pow(x,1)

                              Detach, 142, 5

 

                        144  x e g => pow(x,1)=x

                              U Spec, 94

 

                        145  pow(x,1)=x

                              Detach, 144, 110

 

                        146  f(1)=x

                              Substitute, 143, 145

 

                        147  f(1) e h

                              Substitute, 146, 108

 

                        148  1 e n & f(1) e h

                              Join, 5, 147

 

                   As Required:

 

                        149  1 e p1

                              Detach, 141, 148

 

                       

                        Inductive Step

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

                       

                        Prove: ALL(b):[b e p1 => b+1 e p1]

                       

                        Suppose...

 

                              150  y e p1

                                    Premise

 

                        Apply definition of p1

 

                              151  y e p1 <=> y e n & f(y) e h

                                    U Spec, 126

 

                              152  [y e p1 => y e n & f(y) e h]

                             & [y e n & f(y) e h => y e p1]

                                    Iff-And, 151

 

                              153  y e p1 => y e n & f(y) e h

                                    Split, 152

 

                              154  y e n & f(y) e h => y e p1

                                    Split, 152

 

                              155  y e n & f(y) e h

                                    Detach, 153, 150

 

                              156  y e n

                                    Split, 155

 

                              157  f(y) e h

                                    Split, 155

 

                        Apply definition of f

 

                              158  y e n => f(y)=pow(x,y)

                                    U Spec, 115

 

                              159  f(y)=pow(x,y)

                                    Detach, 158, 156

 

                              160  pow(x,y) e h

                                    Substitute, 159, 157

 

                        Apply definition of p1

 

                              161  y+1 e p1 <=> y+1 e n & f(y+1) e h

                                    U Spec, 126

 

                              162  [y+1 e p1 => y+1 e n & f(y+1) e h]

                             & [y+1 e n & f(y+1) e h => y+1 e p1]

                                    Iff-And, 161

 

                              163  y+1 e p1 => y+1 e n & f(y+1) e h

                                    Split, 162

 

                        Sufficient:

 

                              164  y+1 e n & f(y+1) e h => y+1 e p1

                                    Split, 162

 

                        Apply definition of + on n

 

                              165  ALL(b):[y e n & b e n => y+b e n]

                                    U Spec, 6

 

                              166  y e n & 1 e n => y+1 e n

                                    U Spec, 165

 

                              167  y e n & 1 e n

                                    Join, 156, 5

 

                              168  y+1 e n

                                    Detach, 166, 167

 

                        Apply definiton of f

 

                              169  y+1 e n => f(y+1)=pow(x,y+1)

                                    U Spec, 115

 

                              170  f(y+1)=pow(x,y+1)

                                    Detach, 169, 168

 

                              171  ALL(b):[x e g & b e n => pow(x,b+1)=pow(x,b)*x]

                                    U Spec, 95

 

                              172  x e g & y e n => pow(x,y+1)=pow(x,y)*x

                                    U Spec, 171

 

                              173  x e g & y e n

                                    Join, 110, 156

 

                              174  pow(x,y+1)=pow(x,y)*x

                                    Detach, 172, 173

 

                        Apply definition of * on g

 

                              175  ALL(b):[pow(x,y) e h & b e h => pow(x,y)*b e h]

                                    U Spec, 53

 

                              176  pow(x,y) e h & x e h => pow(x,y)*x e h

                                    U Spec, 175

 

                              177  pow(x,y) e h & x e h

                                    Join, 160, 108

 

                              178  pow(x,y)*x e h

                                    Detach, 176, 177

 

                              179  pow(x,y+1) e h

                                    Substitute, 174, 178

 

                              180  f(y+1) e h

                                    Substitute, 170, 179

 

                              181  y+1 e n & f(y+1) e h

                                    Join, 168, 180

 

                              182  y+1 e p1

                                    Detach, 164, 181

 

                   As Required:

 

                        183  ALL(b):[b e p1 => b+1 e p1]

                              4 Conclusion, 150

 

                   Joining results from base case and inductive step...

 

                        184  1 e p1 & ALL(b):[b e p1 => b+1 e p1]

                              Join, 149, 183

 

                   By induction, we have...

 

                        185  ALL(b):[b e n => b e p1]

                              Detach, 137, 184

 

                       

                        Prove: ALL(a):[a e n => f(a) e h]

                       

                        Suppose...

 

                              186  y e n

                                    Premise

 

                        Apply previous result

 

                              187  y e n => y e p1

                                    U Spec, 185

 

                              188  y e p1

                                    Detach, 187, 186

 

                        Apply definition of p1

 

                              189  y e p1 <=> y e n & f(y) e h

                                    U Spec, 126

 

                              190  [y e p1 => y e n & f(y) e h]

                             & [y e n & f(y) e h => y e p1]

                                    Iff-And, 189

 

                              191  y e p1 => y e n & f(y) e h

                                    Split, 190

 

                              192  y e n & f(y) e h => y e p1

                                    Split, 190

 

                              193  y e n & f(y) e h

                                    Detach, 191, 188

 

                              194  y e n

                                    Split, 193

 

                              195  f(y) e h

                                    Split, 193

 

                  

                   f is closed on h

                  

                   As Required:

 

                        196  ALL(a):[a e n => f(a) e h]

                              4 Conclusion, 186

 

                   Since h is finite, we must have:

 

                        197  ~Injective(f,n,h)

                              Detach, 122, 196

 

                   Apply the definition of Injective

 

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

                              U Spec, 3

 

                        199  ALL(b):[Injective(f,n,b) <=> ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]]

                              U Spec, 198

 

                        200  Injective(f,n,h) <=> ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]

                              U Spec, 199

 

                        201  [Injective(f,n,h) => ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]]

                        & [ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]] => Injective(f,n,h)]

                              Iff-And, 200

 

                        202  Injective(f,n,h) => ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]

                              Split, 201

 

                        203  ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]] => Injective(f,n,h)

                              Split, 201

 

                        204  ~Injective(f,n,h) => ~ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]

                              Contra, 203

 

                        205  ~ALL(c):ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]

                              Detach, 204, 197

 

                        206  ~~EXIST(c):~ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]

                              Quant, 205

 

                        207  EXIST(c):~ALL(d):[c e n & d e n => [f(c)=f(d) => c=d]]

                              Rem DNeg, 206

 

                        208  EXIST(c):~~EXIST(d):~[c e n & d e n => [f(c)=f(d) => c=d]]

                              Quant, 207

 

                        209  EXIST(c):EXIST(d):~[c e n & d e n => [f(c)=f(d) => c=d]]

                              Rem DNeg, 208

 

                        210  EXIST(c):EXIST(d):~~[c e n & d e n & ~[f(c)=f(d) => c=d]]

                              Imply-And, 209

 

                        211  EXIST(c):EXIST(d):[c e n & d e n & ~[f(c)=f(d) => c=d]]

                              Rem DNeg, 210

 

                        212  EXIST(c):EXIST(d):[c e n & d e n & ~~[f(c)=f(d) & ~c=d]]

                              Imply-And, 211

 

                        213  EXIST(c):EXIST(d):[c e n & d e n & [f(c)=f(d) & ~c=d]]

                              Rem DNeg, 212

 

                        214  EXIST(d):[t e n & d e n & [f(t)=f(d) & ~t=d]]

                              E Spec, 213

 

                        215  t e n & u e n & [f(t)=f(u) & ~t=u]

                              E Spec, 214

 

                  

                   Define: t, u

                  

                   Where f(t) = f(u)

 

                        216  t e n

                              Split, 215

 

                        217  u e n

                              Split, 215

 

                        218  f(t)=f(u) & ~t=u

                              Split, 215

 

                        219  f(t)=f(u)

                              Split, 218

 

                        220  ~t=u

                              Split, 218

 

                   Apply definiton of < on n

 

                        221  ALL(b):[t e n & b e n => [~t=b => t<b | b<t]]

                              U Spec, 8

 

                        222  t e n & u e n => [~t=u => t<u | u<t]

                              U Spec, 221

 

                        223  t e n & u e n

                              Join, 216, 217

 

                        224  ~t=u => t<u | u<t

                              Detach, 222, 223

 

                   Two cases to consider

                  

                   (In an informal proof at this point, you might we would say something hand-wavey like

                   "without loss of generality, let t < u." Or "by symmetry, we have...." Unfortunately,

                   such arguments are not allowed in formal proofs.)

 

                        225  t<u | u<t

                              Detach, 224, 220

 

                       

                        Prove: ALL(a):ALL(b):[a e n & b e n

                               => [f(a)=f(b) => [a<b => e e h & inv(x) e h]]]

                       

                        (This sub-proof will be used to make the formal equilavent of a symmetry argument.)

                       

                        Suppose...

 

                              226  v e n & w e n

                                    Premise

 

                              227  v e n

                                    Split, 226

 

                              228  w e n

                                    Split, 226

 

                            

                             Prove: f(v)=f(w) => [v<w => e e h & inv(x) e h

                            

                             Suppose...

 

                                    229  f(v)=f(w)

                                          Premise

 

                                 

                                  Prove: v<w => e e h & inv(x) e h

                                 

                                  Suppose...

 

                                          230  v<w

                                                Premise

 

                                  Apply definition of < on n

 

                                          231  ALL(b):[v e n & b e n => [v<b => EXIST(c):[c e n & v+c=b]]]

                                                U Spec, 9

 

                                          232  v e n & w e n => [v<w => EXIST(c):[c e n & v+c=w]]

                                                U Spec, 231

 

                                          233  v<w => EXIST(c):[c e n & v+c=w]

                                                Detach, 232, 226

 

                                          234  EXIST(c):[c e n & v+c=w]

                                                Detach, 233, 230

 

                                          235  y e n & v+y=w

                                                E Spec, 234

 

                                  Define: y

                                 

                                  The difference between v and w

 

                                          236  y e n

                                                Split, 235

 

                                          237  v+y=w

                                                Split, 235

 

                                          238  f(v)=f(v+y)

                                                Substitute, 237, 229

 

                                  Apply definition of f

 

                                          239  v e n => f(v)=pow(x,v)

                                                U Spec, 115

 

                                          240  f(v)=pow(x,v)

                                                Detach, 239, 227

 

                                          241  pow(x,v)=f(v+y)

                                                Substitute, 240, 238

 

                                  Apply definition of f

 

                                          242  v+y e n => f(v+y)=pow(x,v+y)

                                                U Spec, 115

 

                                          243  ALL(b):[v e n & b e n => v+b e n]

                                                U Spec, 6

 

                                          244  v e n & y e n => v+y e n

                                                U Spec, 243

 

                                          245  v e n & y e n

                                                Join, 227, 236

 

                                          246  v+y e n

                                                Detach, 244, 245

 

                                          247  f(v+y)=pow(x,v+y)

                                                Detach, 242, 246

 

                                          248  pow(x,v)=pow(x,v+y)

                                                Substitute, 247, 241

 

                                  Establish equivalent of Product of Powers Rule for (g,*)

                                 

                                  Apply Lemma 3

 

                                          249  ALL(pow):[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)]

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                                      & ALL(a):[a e g => pow(a,1)=a]

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                                      => ALL(a):ALL(b):ALL(c):[a e g & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]]

                                                U Spec, 13

 

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

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                                      & ALL(a):[a e g => pow(a,1)=a]

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                                      => ALL(a):ALL(b):ALL(c):[a e g & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]

                                                U Spec, 249

 

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

                                                Join, 23, 24

 

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

                                                Join, 251, 25

 

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

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                                                Join, 252, 93

 

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

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                                      & ALL(a):[a e g => pow(a,1)=a]

                                                Join, 253, 94

 

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

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b) e g]

                                      & ALL(a):[a e g => pow(a,1)=a]

                                      & ALL(a):ALL(b):[a e g & b e n => pow(a,b+1)=pow(a,b)*a]

                                                Join, 254, 95

 

                                  Product of Powers Rule

 

                                          256  ALL(a):ALL(b):ALL(c):[a e g & b e n & c e n => pow(a,b)*pow(a,c)=pow(a,b+c)]

                                                Detach, 250, 255

 

                                  Apply Product of Powers Rule

 

                                          257  ALL(b):ALL(c):[x e g & b e n & c e n => pow(x,b)*pow(x,c)=pow(x,b+c)]

                                                U Spec, 256

 

                                          258  ALL(c):[x e g & v e n & c e n => pow(x,v)*pow(x,c)=pow(x,v+c)]

                                                U Spec, 257

 

                                          259  x e g & v e n & y e n => pow(x,v)*pow(x,y)=pow(x,v+y)

                                                U Spec, 258

 

                                          260  x e g & v e n

                                                Join, 110, 227

 

                                          261  x e g & v e n & y e n

                                                Join, 260, 236

 

                                          262  pow(x,v)*pow(x,y)=pow(x,v+y)

                                                Detach, 259, 261

 

                                          263  pow(x,v)=pow(x,v)*pow(x,y)

                                                Substitute, 262, 248

 

                                  Apply previous result

 

                                          264  ALL(b):[pow(x,v) e g & b e g => [pow(x,v)*b=pow(x,v) => b=e]]

                                                U Spec, 34

 

                                          265  pow(x,v) e g & pow(x,y) e g => [pow(x,v)*pow(x,y)=pow(x,v) => pow(x,y)=e]

                                                U Spec, 264

 

                                          266  ALL(b):[x e g & b e n => pow(x,b) e g]

                                                U Spec, 93

 

                                          267  x e g & v e n => pow(x,v) e g

                                                U Spec, 266

 

                                          268  x e g & v e n

                                                Join, 110, 227

 

                                          269  pow(x,v) e g

                                                Detach, 267, 268

 

                                  Apply definition of pow

 

                                          270  x e g & y e n => pow(x,y) e g

                                                U Spec, 266

 

                                          271  x e g & y e n

                                                Join, 110, 236

 

                                          272  pow(x,y) e g

                                                Detach, 270, 271

 

                                          273  pow(x,v) e g & pow(x,y) e g

                                                Join, 269, 272

 

                                          274  pow(x,v)*pow(x,y)=pow(x,v) => pow(x,y)=e

                                                Detach, 265, 273

 

                                          275  pow(x,v)*pow(x,y)=pow(x,v)

                                                Sym, 263

 

                                          276  pow(x,y)=e

                                                Detach, 274, 275

 

                                  Apply previous result

 

                                          277  y e n => f(y) e h

                                                U Spec, 196

 

                                          278  f(y) e h

                                                Detach, 277, 236

 

                                          279  y e n => f(y)=pow(x,y)

                                                U Spec, 115

 

                                          280  f(y)=pow(x,y)

                                                Detach, 279, 236

 

                                          281  pow(x,y) e h

                                                Substitute, 280, 278

 

                                  As Required:

 

                                          282  e e h

                                                Substitute, 276, 281

 

                                  Apply definition of inv on g

 

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

                                                U Spec, 28

 

                                          284  inv(x) e g

                                                Detach, 283, 110

 

                                 Apply definition of inv

 

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

                                                U Spec, 29

 

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

                                                Detach, 285, 110

 

                                          287  x*inv(x)=e

                                                Split, 286

 

                                          288  inv(x)*x=e

                                                Split, 286

 

                                 

                                  Two sub-cases to consider:

 

                                          289  y=1 | ~y=1

                                                Or Not

 

                                     

                                      Sub-case 1

                                     

                                      Prove: y=1 => inv(x) e h

                                     

                                      Suppose...

 

                                                290  y=1

                                                      Premise

 

                                                291  pow(x,1)=e

                                                      Substitute, 290, 276

 

                                      Apply definition of pow

 

                                                292  x e g => pow(x,1)=x

                                                      U Spec, 94

 

                                                293  pow(x,1)=x

                                                      Detach, 292, 110

 

                                                294  x=e

                                                      Substitute, 293, 291

 

                                                295  inv(x)=e

                                                      Substitute, 294, 36

 

                                                296  inv(x) e h

                                                      Substitute, 295, 282

 

                                  As Required:

 

                                          297  y=1 => inv(x) e h

                                                4 Conclusion, 290

 

                                     

                                      Sub-case 2

                                     

                                      Prove: ~y=1 => inv(x) e h

                                     

                                      Suppose...

 

                                                298  ~y=1

                                                      Premise

 

                                      Apply property of + on n

 

                                                299  y e n => [~y=1 => EXIST(b):[b e n & y=b+1]]

                                                      U Spec, 7

 

                                                300  ~y=1 => EXIST(b):[b e n & y=b+1]

                                                      Detach, 299, 236

 

                                                301  EXIST(b):[b e n & y=b+1]

                                                      Detach, 300, 298

 

                                                302  z e n & y=z+1

                                                      E Spec, 301

 

                                      Define: z 

                                     

                                      The predecessor of y

 

                                                303  z e n

                                                      Split, 302

 

                                                304  y=z+1

                                                      Split, 302

 

                                                305  pow(x,z+1)=e

                                                      Substitute, 304, 276

 

                                      Apply definition of pow

 

                                                306  ALL(b):[x e g & b e n => pow(x,b+1)=pow(x,b)*x]

                                                      U Spec, 95

 

                                                307  x e g & z e n => pow(x,z+1)=pow(x,z)*x

                                                      U Spec, 306

 

                                                308  x e g & z e n

                                                      Join, 110, 303

 

                                                309  pow(x,z+1)=pow(x,z)*x

                                                      Detach, 307, 308

 

                                                310  pow(x,z)*x=e

                                                      Substitute, 309, 305

 

                                      Apply previous result

 

                                                311  ALL(b):[pow(x,z) e g & b e g => [pow(x,z)*b=e => inv(pow(x,z))=b & inv(b)=pow(x,z)]]

                                                      U Spec, 35

 

                                                312  pow(x,z) e g & x e g => [pow(x,z)*x=e => inv(pow(x,z))=x & inv(x)=pow(x,z)]

                                                      U Spec, 311

 

                                                313  ALL(b):[x e g & b e n => pow(x,b) e g]

                                                      U Spec, 93

 

                                                314  x e g & z e n => pow(x,z) e g

                                                      U Spec, 313

 

                                                315  x e g & z e n

                                                      Join, 110, 303

 

                                                316  pow(x,z) e g

                                                      Detach, 314, 315

 

                                                317  pow(x,z) e g & x e g

                                                      Join, 316, 110

 

                                                318  pow(x,z)*x=e => inv(pow(x,z))=x & inv(x)=pow(x,z)

                                                      Detach, 312, 317

 

                                                319  inv(pow(x,z))=x & inv(x)=pow(x,z)

                                                      Detach, 318, 310

 

                                                320  inv(pow(x,z))=x

                                                      Split, 319

 

                                                321  inv(x)=pow(x,z)

                                                      Split, 319

 

                                                322  z e n => f(z) e h

                                                      U Spec, 196

 

                                                323  f(z) e h

                                                      Detach, 322, 303

 

                                      Apply definition of f

 

                                                324  z e n => f(z)=pow(x,z)

                                                      U Spec, 115

 

                                                325  f(z)=pow(x,z)

                                                      Detach, 324, 303

 

                                                326  pow(x,z) e h

                                                      Substitute, 325, 323

 

                                                327  inv(x) e h

                                                      Substitute, 321, 326

 

                                  As Required:

 

                                          328  ~y=1 => inv(x) e h

                                                4 Conclusion, 298

 

                                  Joining results for Cases Rule...

 

                                          329  [y=1 => inv(x) e h] & [~y=1 => inv(x) e h]

                                                Join, 297, 328

 

                                          330  inv(x) e h

                                                Cases, 289, 329

 

                                          331  e e h & inv(x) e h

                                                Join, 282, 330

 

                             As Required:

 

                                    332  v<w => e e h & inv(x) e h

                                          4 Conclusion, 230

 

                        As Required:

 

                              333  f(v)=f(w) => [v<w => e e h & inv(x) e h]

                                    4 Conclusion, 229

 

                   As Required:

 

                        334  ALL(a):ALL(b):[a e n & b e n

                        => [f(a)=f(b) => [a<b => e e h & inv(x) e h]]]

                              4 Conclusion, 226

 

                       

                        Prove: u<t => e e h & inv(x) e h

                       

                        Suppose...

 

                              335  t<u

                                    Premise

 

                              336  ALL(b):[t e n & b e n

                             => [f(t)=f(b) => [t<b => e e h & inv(x) e h]]]

                                    U Spec, 334

 

                              337  t e n & u e n

                             => [f(t)=f(u) => [t<u => e e h & inv(x) e h]]

                                    U Spec, 336

 

                              338  t e n & u e n

                                    Join, 216, 217

 

                              339  f(t)=f(u) => [t<u => e e h & inv(x) e h]

                                    Detach, 337, 338

 

                              340  t<u => e e h & inv(x) e h

                                    Detach, 339, 219

 

                              341  e e h & inv(x) e h

                                    Detach, 340, 335

 

                   As Required:

 

                        342  t<u => e e h & inv(x) e h

                              4 Conclusion, 335

 

                       

                        Prove: u<t => e e h & inv(x) e h

                       

                        Suppose...

 

                              343  u<t

                                    Premise

 

                              344  ALL(b):[u e n & b e n

                             => [f(u)=f(b) => [u<b => e e h & inv(x) e h]]]

                                    U Spec, 334

 

                              345  u e n & t e n

                             => [f(u)=f(t) => [u<t => e e h & inv(x) e h]]

                                    U Spec, 344

 

                              346  u e n & t e n

                                    Join, 217, 216

 

                              347  f(u)=f(t) => [u<t => e e h & inv(x) e h]

                                    Detach, 345, 346

 

                              348  f(t)=f(u) => [u<t => e e h & inv(x) e h]

                                    Sym, 347

 

                              349  u<t => e e h & inv(x) e h

                                    Detach, 348, 219

 

                              350  e e h & inv(x) e h

                                    Detach, 349, 343

 

                   As Required:

 

                        351  u<t => e e h & inv(x) e h

                              4 Conclusion, 343

 

                        352  [t<u => e e h & inv(x) e h]

                        & [u<t => e e h & inv(x) e h]

                              Join, 342, 351

 

                   By "symmetry"...

 

                        353  e e h & inv(x) e h

                              Cases, 225, 352

 

              As Required:

 

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

                        4 Conclusion, 108

 

              Apply definition of h

 

                  355  h0 e h

                        E Spec, 39

 

                  356  h0 e h => e e h & inv(h0) e h

                        U Spec, 354

 

                  357  e e h & inv(h0) e h

                        Detach, 356, 355

 

              As Required:

 

                  358  e e h

                        Split, 357

 

                  359  inv(h0) e h

                        Split, 357

 

                  

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

                  

                   Suppose...

 

                        360  x e h

                              Premise

 

                   Apply previous result

 

                        361  x e h => e e h & inv(x) e h

                              U Spec, 354

 

                        362  e e h & inv(x) e h

                              Detach, 361, 360

 

                        363  e e h

                              Split, 362

 

                        364  inv(x) e h

                              Split, 362

 

              As Required:

 

                  365  ALL(a):[a e h => inv(a) e h]

                        4 Conclusion, 360

 

              Joining results...

 

                  366  Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]

                        Join, 38, 53

 

                  367  Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]

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

                        Join, 366, 76

 

                  368  Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]

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

                   & e e h

                        Join, 367, 358

 

                  369  Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]

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

                   & e e h

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

                        Join, 368, 82

 

                  370  Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]

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

                   & e e h

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

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

                        Join, 369, 365

 

                  371  Set(h) & ALL(a):ALL(b):[a e h & b e h => a*b e h]

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

                   & e e h

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

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

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

                        Join, 370, 88

 

                  372  Group(h,e,inv)

                        Detach, 59, 371

 

          As Required:

 

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

              => Group(h,e,inv)

                  4 Conclusion, 53

 

          Joining results for Iff-And Rule

 

            374  [Group(h,e,inv)

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

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

              => Group(h,e,inv)]

                  Join, 52, 373

 

            375  Group(h,e,inv)

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

                  Iff-And, 374

 

     As Required:

 

      376  ALL(h):[Set(h)

          & EXIST(a):a e h

          & Finite(h)

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

          => [Group(h,e,inv)

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

            4 Conclusion, 37

 

As Required:

 

377  ALL(g):ALL(e):ALL(inv):[Group(g,e,inv)

     => ALL(h):[Set(h)

     & EXIST(a):a e h

     & Finite(h)

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

     => [Group(h,e,inv)

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

      4 Conclusion, 15