Group Theory 3, Lemma 2

THEOREM

*******

For any x0 e s, there exists a function f mapping n to s such that f(x) = pow(x0,x)

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

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

REQUIRED PROPERTIES OF N

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

1 Set(n)

Axiom

2 1 e n

Axiom

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

Axiom

PROOF

*****

Suppose...

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

Premise

5 Set(s)

Split, 4

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

Split, 4

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

Split, 4

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

Split, 4

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

Split, 4

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

Suppose...

10 x0 e s

Premise

Construct the Cartesain of product of n and s

Apply the Cartesian Product Axiom

11 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

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

U Spec, 11

13 Set(n) & Set(s) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e s]]

U Spec, 12

14 Set(n) & Set(s)

Join, 1, 5

15 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e s]]

Detach, 13, 14

16 Set'(ns) & ALL(c1):ALL(c2):[(c1,c2) e ns <=> c1 e n & c2 e s]

E Spec, 15

Define: ns

The Cartesian product of n and s

17 Set'(ns)

Split, 16

18 ALL(c1):ALL(c2):[(c1,c2) e ns <=> c1 e n & c2 e s]

Split, 16

Construct a subset f of ns

Apply Subset Axiom

19 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e ns & b=pow(x0,a)]]

Subset, 17

20 Set'(f) & ALL(a):ALL(b):[(a,b) e f <=> (a,b) e ns & b=pow(x0,a)]

E Spec, 19

Define: f

21 Set'(f)

Split, 20

22 ALL(a):ALL(b):[(a,b) e f <=> (a,b) e ns & b=pow(x0,a)]

Split, 20

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

Suppose...

23 (x,y) e f

Premise

Apply definition of f

24 ALL(b):[(x,b) e f <=> (x,b) e ns & b=pow(x0,x)]

U Spec, 22

25 (x,y) e f <=> (x,y) e ns & y=pow(x0,x)

U Spec, 24

26 [(x,y) e f => (x,y) e ns & y=pow(x0,x)]

& [(x,y) e ns & y=pow(x0,x) => (x,y) e f]

Iff-And, 25

27 (x,y) e f => (x,y) e ns & y=pow(x0,x)

Split, 26

28 (x,y) e ns & y=pow(x0,x) => (x,y) e f

Split, 26

29 (x,y) e ns & y=pow(x0,x)

Detach, 27, 23

30 (x,y) e ns

Split, 29

31 y=pow(x0,x)

Split, 29

Apply definition of ns

32 ALL(c2):[(x,c2) e ns <=> x e n & c2 e s]

U Spec, 18

33 (x,y) e ns <=> x e n & y e s

U Spec, 32

34 [(x,y) e ns => x e n & y e s]

& [x e n & y e s => (x,y) e ns]

Iff-And, 33

35 (x,y) e ns => x e n & y e s

Split, 34

36 x e n & y e s => (x,y) e ns

Split, 34

37 x e n & y e s

Detach, 35, 30

As Required:

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

4 Conclusion, 23

Prove: ALL(a):ALL(b):[(a,b) e f => b=pow(x0,a)]

Suppose...

39 (x,y) e f

Premise

Apply definition of f

40 ALL(b):[(x,b) e f <=> (x,b) e ns & b=pow(x0,x)]

U Spec, 22

41 (x,y) e f <=> (x,y) e ns & y=pow(x0,x)

U Spec, 40

42 [(x,y) e f => (x,y) e ns & y=pow(x0,x)]

& [(x,y) e ns & y=pow(x0,x) => (x,y) e f]

Iff-And, 41

43 (x,y) e f => (x,y) e ns & y=pow(x0,x)

Split, 42

44 (x,y) e ns & y=pow(x0,x) => (x,y) e f

Split, 42

45 (x,y) e ns & y=pow(x0,x)

Detach, 43, 39

46 (x,y) e ns

Split, 45

47 y=pow(x0,x)

Split, 45

As Required:

48 ALL(a):ALL(b):[(a,b) e f => b=pow(x0,a)]

4 Conclusion, 39

Prove: f is a function

Apply Function Axiom

49 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

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

U Spec, 49

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

& ALL(c):[c e n => 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]]

U Spec, 50

Sufficient: For functionality of f

52 ALL(c):ALL(d):[(c,d) e f => c e n & d e s]

& ALL(c):[c e n => EXIST(d):[d e s & (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]

U Spec, 51

Prove: ALL(c):[c e n => EXIST(d):[d e s & (c,d) e f]]

Suppose...

53 x e n

Premise

Apply definition of f

54 ALL(b):[(x,b) e f <=> (x,b) e ns & b=pow(x0,x)]

U Spec, 22

55 (x,pow(x0,x)) e f <=> (x,pow(x0,x)) e ns & pow(x0,x)=pow(x0,x)

U Spec, 54

56 [(x,pow(x0,x)) e f => (x,pow(x0,x)) e ns & pow(x0,x)=pow(x0,x)]

& [(x,pow(x0,x)) e ns & pow(x0,x)=pow(x0,x) => (x,pow(x0,x)) e f]

Iff-And, 55

57 (x,pow(x0,x)) e f => (x,pow(x0,x)) e ns & pow(x0,x)=pow(x0,x)

Split, 56

58 (x,pow(x0,x)) e ns & pow(x0,x)=pow(x0,x) => (x,pow(x0,x)) e f

Split, 56

Apply definition of ns

59 ALL(c2):[(x,c2) e ns <=> x e n & c2 e s]

U Spec, 18

60 (x,pow(x0,x)) e ns <=> x e n & pow(x0,x) e s

U Spec, 59

61 [(x,pow(x0,x)) e ns => x e n & pow(x0,x) e s]

& [x e n & pow(x0,x) e s => (x,pow(x0,x)) e ns]

Iff-And, 60

62 (x,pow(x0,x)) e ns => x e n & pow(x0,x) e s

Split, 61

63 x e n & pow(x0,x) e s => (x,pow(x0,x)) e ns

Split, 61

Apply definiton of pow

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

U Spec, 7

65 x0 e s & x e n => pow(x0,x) e s

U Spec, 64

66 x0 e s & x e n

Join, 10, 53

67 pow(x0,x) e s

Detach, 65, 66

68 x e n & pow(x0,x) e s

Join, 53, 67

69 (x,pow(x0,x)) e ns

Detach, 63, 68

70 pow(x0,x)=pow(x0,x)

Reflex

71 (x,pow(x0,x)) e ns & pow(x0,x)=pow(x0,x)

Join, 69, 70

72 (x,pow(x0,x)) e f

Detach, 58, 71

73 pow(x0,x) e s & (x,pow(x0,x)) e f

Join, 67, 72

Generalizing...

74 EXIST(d):[d e s & (x,d) e f]

E Gen, 73

Functionality, Part 2

75 ALL(c):[c e n => EXIST(d):[d e s & (c,d) e f]]

4 Conclusion, 53

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

Suppose...

76 (x,y1) e f & (x,y2) e f

Premise

77 (x,y1) e f

Split, 76

78 (x,y2) e f

Split, 76

Apply previous result

79 ALL(b):[(x,b) e f => b=pow(x0,x)]

U Spec, 48

80 (x,y1) e f => y1=pow(x0,x)

U Spec, 79

81 y1=pow(x0,x)

Detach, 80, 77

82 (x,y2) e f => y2=pow(x0,x)

U Spec, 79

83 y2=pow(x0,x)

Detach, 82, 78

84 y1=y2

Substitute, 83, 81

Functionality, Part 3

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

4 Conclusion, 76

Joining results...

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

& ALL(c):[c e n => EXIST(d):[d e s & (c,d) e f]]

Join, 38, 75

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

& ALL(c):[c e n => EXIST(d):[d e s & (c,d) e f]]

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

Join, 86, 85

f is a function

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

Detach, 52, 87

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

Suppose...

89 x e n

Premise

Apply previous result

90 x e n => EXIST(d):[d e s & (x,d) e f]

U Spec, 75

91 EXIST(d):[d e s & (x,d) e f]

Detach, 90, 89

92 y e s & (x,y) e f

E Spec, 91

93 y e s

Split, 92

94 (x,y) e f

Split, 92

Apply functionality of f

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

U Spec, 88

96 y=f(x) <=> (x,y) e f

U Spec, 95

97 [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]

Iff-And, 96

98 y=f(x) => (x,y) e f

Split, 97

99 (x,y) e f => y=f(x)

Split, 97

100 y=f(x)

Detach, 99, 94

101 f(x) e s

Substitute, 100, 93

As Required:

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

4 Conclusion, 89

Prove: ALL(b):[b e n => f(b)=pow(x0,b)]

Suppose...

103 x e n

Premise

Apply previous result

104 x e n => EXIST(d):[d e s & (x,d) e f]

U Spec, 75

105 EXIST(d):[d e s & (x,d) e f]

Detach, 104, 103

106 y e s & (x,y) e f

E Spec, 105

107 y e s

Split, 106

108 (x,y) e f

Split, 106

Apply functionality of f

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

U Spec, 88

110 y=f(x) <=> (x,y) e f

U Spec, 109

111 [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]

Iff-And, 110

112 y=f(x) => (x,y) e f

Split, 111

113 (x,y) e f => y=f(x)

Split, 111

114 y=f(x)

Detach, 113, 108

Apply previous result

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

U Spec, 48

116 (x,y) e f => y=pow(x0,x)

U Spec, 115

117 y=pow(x0,x)

Detach, 116, 108

118 f(x)=pow(x0,x)

Substitute, 114, 117

As Required:

119 ALL(b):[b e n => f(b)=pow(x0,b)]

4 Conclusion, 103

Joining results...

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

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

Join, 102, 119

As Required:

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

4 Conclusion, 10

As Required:

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

4 Conclusion, 4