:: GROUP_1 semantic presentation

definition

attr c₁ is strict;
struct HGrStr -> 1-sorted ;
aggr HGrStr(# carrier, mult #) -> HGrStr ;
sel mult c₁ -> BinOp of the carrier of c₁;

end;

registration

cluster non empty strict HGrStr ;
existence

proof end;

end;

definition

let S be non empty HGrStr ;
let x, y be Element of S;
func x * y -> Element of S equals :: GROUP_1:def 1
the mult of S . x,y;
coherence ;

end;

:: deftheorem defines * GROUP_1:def 1 :

registration

let A be non empty set ;
let m be BinOp of A;
cluster HGrStr(# A,m #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

Lm1: now

set G = HGrStr(# REAL ,addreal #);
A1: for h, g being Element of HGrStr(# REAL ,addreal #)
for A, B being Real st h = A & g = B holds
h * g = A + B by BINOP_2:def 9;
thus for h, g, f being Element of HGrStr(# REAL ,addreal #) holds (h * g) * f = h * (g * f) :: thesis:

proof

let h, g, f be Element of HGrStr(# REAL ,addreal #); :: thesis:
reconsider A = h, B = g, C = f as Real ;
A2: h * g = A + B by A1;
A3: g * f = B + C by A1;
thus (h * g) * f = (A + B) + C by A1, A2
.= A + (B + C)
.= h * (g * f) by A1, A3 ; :: thesis:

end;

reconsider e = 0 as Element of HGrStr(# REAL ,addreal #) ;
take e = e; :: thesis:
let h be Element of HGrStr(# REAL ,addreal #); :: thesis:
reconsider A = h as Real ;
thus h * e = A + 0 by A1
.= h ; :: thesis:
thus e * h = 0 + A by A1
.= h ; :: thesis:
reconsider g = - A as Element of HGrStr(# REAL ,addreal #) ;
take g = g; :: thesis:
thus h * g = A + (- A) by A1
.= e ; :: thesis:
thus g * h = (- A) + A by A1
.= e ; :: thesis:

end;

definition

let IT be non empty HGrStr ;
attr IT is unital means :Def2: :: GROUP_1:def 2
ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h );
attr IT is Group-like means :Def3: :: GROUP_1:def 3
ex e being Element of IT st
for h being Element of IT holds
( h * e = h & e * h = h & ex g being Element of IT st
( h * g = e & g * h = e ) );
attr IT is associative means :Def4: :: GROUP_1:def 4
for x, y, z being Element of IT holds (x * y) * z = x * (y * z);

end;

:: deftheorem Def2 defines unital GROUP_1:def 2 :

:: deftheorem Def3 defines Group-like GROUP_1:def 3 :

:: deftheorem Def4 defines associative GROUP_1:def 4 :

registration

cluster non empty Group-like -> non empty unital HGrStr ;
coherence

proof end;

end;

registration

cluster non empty strict unital Group-like associative HGrStr ;
existence

proof end;

end;

definition

mode Group is non empty Group-like associative HGrStr ;

end;

theorem :: GROUP_1:1

canceled;

theorem :: GROUP_1:2

canceled;

theorem :: GROUP_1:3

canceled;

theorem :: GROUP_1:4

canceled;

theorem :: GROUP_1:5

for S being non empty HGrStr st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ex t being Element of S st
for s1 being Element of S holds
( s1 * t = s1 & t * s1 = s1 & ex s2 being Element of S st
( s1 * s2 = t & s2 * s1 = t ) ) holds
S is Group by Def3, Def4;

theorem :: GROUP_1:6

for S being non empty HGrStr st ( for r, s, t being Element of S holds (r * s) * t = r * (s * t) ) & ( for r, s being Element of S holds
( ex t being Element of S st r * t = s & ex t being Element of S st t * r = s ) ) holds
( S is associative & S is Group-like )

proof end;

theorem Th7: :: GROUP_1:7

( HGrStr(# REAL ,addreal #) is associative & HGrStr(# REAL ,addreal #) is Group-like )

proof end;

definition

let G be non empty HGrStr ;
assume A1: G is unital ;
func 1. G -> Element of G means :Def5: :: GROUP_1:def 5
for h being Element of G holds
( h * it = h & it * h = h );
existence by A1, Def2;
uniqueness

proof end;

end;

:: deftheorem Def5 defines 1. GROUP_1:def 5 :

theorem :: GROUP_1:8

canceled;

theorem :: GROUP_1:9

canceled;

theorem :: GROUP_1:10

for G being non empty Group-like HGrStr
for e being Element of G st ( for h being Element of G holds
( h * e = h & e * h = h ) ) holds
e = 1. G by Def5;

definition

let G be Group;
let h be Element of G;
func h " -> Element of G means :Def6: :: GROUP_1:def 6
( h * it = 1. G & it * h = 1. G );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines " GROUP_1:def 6 :

theorem :: GROUP_1:11

canceled;

theorem :: GROUP_1:12

for G being Group
for h, g being Element of G st h * g = 1. G & g * h = 1. G holds
g = h " by Def6;

theorem :: GROUP_1:13

canceled;

theorem Th14: :: GROUP_1:14

for G being Group
for h, g, f being Element of G st ( h * g = h * f or g * h = f * h ) holds
g = f

proof end;

theorem :: GROUP_1:15

for G being Group
for h, g being Element of G st ( h * g = h or g * h = h ) holds
g = 1. G

proof end;

theorem Th16: :: GROUP_1:16

for G being Group holds (1. G) " = 1. G

proof end;

theorem Th17: :: GROUP_1:17

for G being Group
for h, g being Element of G st h " = g " holds
h = g

proof end;

theorem :: GROUP_1:18

for G being Group
for h being Element of G st h " = 1. G holds
h = 1. G

proof end;

theorem Th19: :: GROUP_1:19

for G being Group
for h being Element of G holds (h " ) " = h

proof end;

theorem Th20: :: GROUP_1:20

for G being Group
for h, g being Element of G st ( h * g = 1. G or g * h = 1. G ) holds
( h = g " & g = h " )

proof end;

theorem Th21: :: GROUP_1:21

for G being Group
for h, f, g being Element of G holds
( h * f = g iff f = (h " ) * g )

proof end;

theorem Th22: :: GROUP_1:22

for G being Group
for f, h, g being Element of G holds
( f * h = g iff f = g * (h " ) )

proof end;

theorem :: GROUP_1:23

for G being Group
for g, h being Element of G ex f being Element of G st g * f = h

proof end;

theorem :: GROUP_1:24

for G being Group
for g, h being Element of G ex f being Element of G st f * g = h

proof end;

theorem Th25: :: GROUP_1:25

for G being Group
for h, g being Element of G holds (h * g) " = (g " ) * (h " )

proof end;

theorem Th26: :: GROUP_1:26

for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g * h) " = (g " ) * (h " ) )

proof end;

theorem Th27: :: GROUP_1:27

for G being Group
for g, h being Element of G holds
( g * h = h * g iff (g " ) * (h " ) = (h " ) * (g " ) )

proof end;

theorem Th28: :: GROUP_1:28

for G being Group
for g, h being Element of G holds
( g * h = h * g iff g * (h " ) = (h " ) * g )

proof end;

definition

let G be Group;
func inverse_op G -> UnOp of the carrier of G means :Def7: :: GROUP_1:def 7
for h being Element of G holds it . h = h " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines inverse_op GROUP_1:def 7 :

theorem :: GROUP_1:29

canceled;

theorem :: GROUP_1:30

canceled;

theorem Th31: :: GROUP_1:31

for G being non empty associative HGrStr holds the mult of G is associative

proof end;

theorem Th32: :: GROUP_1:32

for G being non empty unital HGrStr holds 1. G is_a_unity_wrt the mult of G

proof end;

theorem Th33: :: GROUP_1:33

for G being non empty unital HGrStr holds the_unity_wrt the mult of G = 1. G

proof end;

theorem Th34: :: GROUP_1:34

for G being non empty unital HGrStr holds the mult of G has_a_unity

proof end;

theorem Th35: :: GROUP_1:35

for G being Group holds inverse_op G is_an_inverseOp_wrt the mult of G

proof end;

theorem Th36: :: GROUP_1:36

for G being Group holds the mult of G has_an_inverseOp

proof end;

theorem :: GROUP_1:37

for G being Group holds the_inverseOp_wrt the mult of G = inverse_op G

proof end;

definition

let G be non empty HGrStr ;
func power G -> Function of [:the carrier of G,NAT :],the carrier of G means :Def8: :: GROUP_1:def 8
for h being Element of G holds
( it . h,0 = 1. G & ( for n being Nat holds it . h,(n + 1) = (it . h,n) * h ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines power GROUP_1:def 8 :

definition

let G be Group;
let i be Integer;
let h be Element of G;
func h |^ i -> Element of G equals :Def9: :: GROUP_1:def 9
(power G) . h,(abs i) if 0 <= i
otherwise ((power G) . h,(abs i)) " ;
correctness ;

end;

:: deftheorem Def9 defines |^ GROUP_1:def 9 :

definition

let G be Group;
let n be Nat;
let h be Element of G;
redefine func h |^ n equals :: GROUP_1:def 10
(power G) . h,n;
compatibility

proof end;

end;

:: deftheorem defines |^ GROUP_1:def 10 :

Lm2: for n being Nat
for G being Group
for h being Element of G holds h |^ (n + 1) = (h |^ n) * h
by Def8;

Lm3: for G being Group
for h being Element of G holds h |^ 0 = 1. G
by Def8;

theorem :: GROUP_1:38

canceled;

theorem :: GROUP_1:39

canceled;

theorem :: GROUP_1:40

canceled;

theorem :: GROUP_1:41

canceled;

theorem Th42: :: GROUP_1:42

for n being Nat
for G being Group holds (1. G) |^ n = 1. G

proof end;

theorem :: GROUP_1:43

for G being Group
for h being Element of G holds h |^ 0 = 1. G by Lm3;

theorem Th44: :: GROUP_1:44

for G being Group
for h being Element of G holds h |^ 1 = h

proof end;

theorem Th45: :: GROUP_1:45

for G being Group
for h being Element of G holds h |^ 2 = h * h

proof end;

theorem :: GROUP_1:46

for G being Group
for h being Element of G holds h |^ 3 = (h * h) * h

proof end;

theorem :: GROUP_1:47

for G being Group
for h being Element of G holds
( h |^ 2 = 1. G iff h " = h )

proof end;

theorem Th48: :: GROUP_1:48

for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n + m) = (h |^ n) * (h |^ m)

proof end;

theorem Th49: :: GROUP_1:49

for n being Nat
for G being Group
for h being Element of G holds
( h |^ (n + 1) = (h |^ n) * h & h |^ (n + 1) = h * (h |^ n) )

proof end;

theorem Th50: :: GROUP_1:50

for n, m being Nat
for G being Group
for h being Element of G holds h |^ (n * m) = (h |^ n) |^ m

proof end;

theorem Th51: :: GROUP_1:51

for n being Nat
for G being Group
for h being Element of G holds (h " ) |^ n = (h |^ n) "

proof end;

theorem Th52: :: GROUP_1:52

for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ n) = (h |^ n) * g

proof end;

theorem Th53: :: GROUP_1:53

for n, m being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ m) = (h |^ m) * (g |^ n)

proof end;

theorem Th54: :: GROUP_1:54

for n being Nat
for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ n = (g |^ n) * (h |^ n)

proof end;

theorem Th55: :: GROUP_1:55

for i being Integer
for G being Group
for h being Element of G st 0 <= i holds
h |^ i = h |^ (abs i) by Def9;

theorem Th56: :: GROUP_1:56

for i being Integer
for G being Group
for h being Element of G st not 0 <= i holds
h |^ i = (h |^ (abs i)) " by Def9;

theorem :: GROUP_1:57

canceled;

theorem :: GROUP_1:58

canceled;

theorem :: GROUP_1:59

for i being Integer
for G being Group
for h being Element of G st i = 0 holds
h |^ i = 1. G by Lm3;

theorem Th60: :: GROUP_1:60

for i being Integer
for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "

proof end;

theorem :: GROUP_1:61

for i being Integer
for G being Group holds (1. G) |^ i = 1. G

proof end;

theorem Th62: :: GROUP_1:62

for G being Group
for h being Element of G holds h |^ (- 1) = h "

proof end;

Lm4: for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) "

proof end;

Lm5: for j being Integer holds
( j >= 1 or j = 0 or j < 0 )

proof end;

Lm6: for j being Integer
for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))

proof end;

Lm7: for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )

proof end;

Lm8: for j being Integer
for G being Group
for h being Element of G holds h |^ (j + 1) = (h |^ j) * (h |^ 1)

proof end;

theorem Th63: :: GROUP_1:63

for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i + j) = (h |^ i) * (h |^ j)

proof end;

theorem :: GROUP_1:64

for n being Nat
for j being Integer
for G being Group
for h being Element of G holds h |^ (n + j) = (h |^ n) * (h |^ j) by Th63;

theorem :: GROUP_1:65

for m being Nat
for i being Integer
for G being Group
for h being Element of G holds h |^ (i + m) = (h |^ i) * (h |^ m) by Th63;

theorem :: GROUP_1:66

for j being Integer
for G being Group
for h being Element of G holds
( h |^ (j + 1) = (h |^ j) * h & h |^ (j + 1) = h * (h |^ j) )

proof end;

Lm9: for i being Integer
for G being Group
for h being Element of G holds (h " ) |^ i = (h |^ i) "

proof end;

theorem Th67: :: GROUP_1:67

for i, j being Integer
for G being Group
for h being Element of G holds h |^ (i * j) = (h |^ i) |^ j

proof end;

theorem :: GROUP_1:68

for n being Nat
for j being Integer
for G being Group
for h being Element of G holds h |^ (n * j) = (h |^ n) |^ j by Th67;

theorem :: GROUP_1:69

for m being Nat
for i being Integer
for G being Group
for h being Element of G holds h |^ (i * m) = (h |^ i) |^ m by Th67;

theorem :: GROUP_1:70

for i being Integer
for G being Group
for h being Element of G holds h |^ (- i) = (h |^ i) " by Lm4;

theorem :: GROUP_1:71

for n being Nat
for G being Group
for h being Element of G holds h |^ (- n) = (h |^ n) " by Lm4;

theorem :: GROUP_1:72

for i being Integer
for G being Group
for h being Element of G holds (h " ) |^ i = (h |^ i) " by Lm9;

theorem Th73: :: GROUP_1:73

for i being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
(g * h) |^ i = (g |^ i) * (h |^ i)

proof end;

theorem Th74: :: GROUP_1:74

for i, j being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ i) * (h |^ j) = (h |^ j) * (g |^ i)

proof end;

theorem :: GROUP_1:75

for n being Nat
for j being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
(g |^ n) * (h |^ j) = (h |^ j) * (g |^ n) by Th74;

theorem :: GROUP_1:76

canceled;

theorem :: GROUP_1:77

for i being Integer
for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g

proof end;

definition

let G be Group;
let h be Element of G;
attr h is being_of_order_0 means :Def11: :: GROUP_1:def 11
for n being Nat st h |^ n = 1. G holds
n = 0;

end;

:: deftheorem Def11 defines being_of_order_0 GROUP_1:def 11 :

notation

let G be Group;
let h be Element of G;
antonym h is_not_of_order_0 for being_of_order_0 h;
synonym h is_of_order_0 for being_of_order_0 h;

end;

theorem :: GROUP_1:78

canceled;

theorem Th79: :: GROUP_1:79

for G being Group holds 1. G is_not_of_order_0

proof end;

definition

let G be Group;
let h be Element of G;
func ord h -> Nat means :Def12: :: GROUP_1:def 12
it = 0 if h is_of_order_0
otherwise ( h |^ it = 1. G & it <> 0 & ( for m being Nat st h |^ m = 1. G & m <> 0 holds
it <= m ) );
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def12 defines ord GROUP_1:def 12 :

theorem :: GROUP_1:80

canceled;

theorem :: GROUP_1:81

canceled;

theorem Th82: :: GROUP_1:82

for G being Group
for h being Element of G holds h |^ (ord h) = 1. G

proof end;

theorem :: GROUP_1:83

canceled;

theorem :: GROUP_1:84

for G being Group holds ord (1. G) = 1

proof end;

theorem :: GROUP_1:85

for G being Group
for h being Element of G st ord h = 1 holds
h = 1. G

proof end;

theorem :: GROUP_1:86

for n being Nat
for G being Group
for h being Element of G st h |^ n = 1. G holds
ord h divides n

proof end;

definition

let G be Group;
func Ord G -> Cardinal equals :: GROUP_1:def 13
Card the carrier of G;
correctness ;

end;

:: deftheorem defines Ord GROUP_1:def 13 :

definition

let S be 1-sorted ;
attr S is finite means :Def14: :: GROUP_1:def 14
the carrier of S is finite;

end;

:: deftheorem Def14 defines finite GROUP_1:def 14 :

notation

let S be 1-sorted ;
antonym infinite S for finite S;

end;

definition

let G be Group;
assume A1: G is finite ;
func ord G -> Nat means :Def15: :: GROUP_1:def 15
ex B being finite set st
( B = the carrier of G & it = card B );
existence

proof end;

correctness ;

end;

:: deftheorem Def15 defines ord GROUP_1:def 15 :

theorem :: GROUP_1:87

canceled;

theorem :: GROUP_1:88

canceled;

theorem :: GROUP_1:89

canceled;

theorem :: GROUP_1:90

for G being Group st G is finite holds
ord G >= 1

proof end;

reconsider G0 = HGrStr(# REAL ,addreal #) as Group by Th7;

definition

let IT be non empty HGrStr ;
attr IT is commutative means :Def16: :: GROUP_1:def 16
for x, y being Element of IT holds x * y = y * x;

end;

:: deftheorem Def16 defines commutative GROUP_1:def 16 :

registration

cluster strict commutative HGrStr ;
existence

proof end;

end;

definition

let FS be non empty commutative HGrStr ;
let x, y be Element of FS;
:: original: *
redefine func x * y -> Element of FS;
commutativity by Def16;

end;

theorem :: GROUP_1:91

canceled;

theorem :: GROUP_1:92

HGrStr(# REAL ,addreal #) is commutative Group

proof end;

theorem :: GROUP_1:93

canceled;

theorem :: GROUP_1:94

for A being commutative Group
for a, b being Element of A holds (a * b) " = (a " ) * (b " ) by Th25;

theorem :: GROUP_1:95

for n being Nat
for A being commutative Group
for a, b being Element of A holds (a * b) |^ n = (a |^ n) * (b |^ n) by Th54;

theorem :: GROUP_1:96

for i being Integer
for A being commutative Group
for a, b being Element of A holds (a * b) |^ i = (a |^ i) * (b |^ i) by Th73;

registration

let A be non empty set ;
let m be BinOp of A;
let u be Element of A;
cluster LoopStr(# A,m,u #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

theorem :: GROUP_1:97

for A being commutative Group holds
( LoopStr(# the carrier of A,the mult of A,(1. A) #) is Abelian & LoopStr(# the carrier of A,the mult of A,(1. A) #) is add-associative & LoopStr(# the carrier of A,the mult of A,(1. A) #) is right_zeroed & LoopStr(# the carrier of A,the mult of A,(1. A) #) is right_complementable )

proof end;