:: GROUP_1 semantic presentation

definition

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

end;

registration

cluster non empty strict HGrStr ;
existence

proof end;

end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be Element of c₁;
func c₂ * c₃ -> Element of a₁ equals :: GROUP_1:def 1
the mult of a₁ . a₂,a₃;
coherence ;

end;

:: deftheorem Def1 defines * GROUP_1:def 1 :

registration

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
cluster HGrStr(# a₁,a₂ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

E1: now

set c₁ = HGrStr(# REAL ,addreal #);
E2: for b₁, b₂ being Element of HGrStr(# REAL ,addreal #)
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ + b₄ by BINOP_2:def 9;
thus for b₁, b₂, b₃ being Element of HGrStr(# REAL ,addreal #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)

proof

let c₂, c₃, c₄ be Element of HGrStr(# REAL ,addreal #);
reconsider c₅ = c₂, c₆ = c₃, c₇ = c₄ as Real ;
E3: c₂ * c₃ = c₅ + c₆ by E2;
E4: c₃ * c₄ = c₆ + c₇ by E2;
thus (c₂ * c₃) * c₄ = (c₅ + c₆) + c₇ by E2, E3
.= c₅ + (c₆ + c₇)
.= c₂ * (c₃ * c₄) by E2, E4 ;

end;

reconsider c₂ = 0 as Element of HGrStr(# REAL ,addreal #) ;
take c₃ = c₂;
let c₄ be Element of HGrStr(# REAL ,addreal #);
reconsider c₅ = c₄ as Real ;
thus c₄ * c₃ = c₅ + 0 by E2
.= c₄ ;
thus c₃ * c₄ = 0 + c₅ by E2
.= c₄ ;
reconsider c₆ = - c₅ as Element of HGrStr(# REAL ,addreal #) ;
take c₇ = c₆;
thus c₄ * c₇ = c₅ + (- c₅) by E2
.= c₃ ;
thus c₇ * c₄ = (- c₅) + c₅ by E2
.= c₃ ;

end;

definition

let c₁ be non empty HGrStr ;
attr a₁ is unital means :Def2: :: GROUP_1:def 2
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds
( b₂ * b₁ = b₂ & b₁ * b₂ = b₂ );
attr a₁ is Group-like means :Def3: :: GROUP_1:def 3
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds
( b₂ * b₁ = b₂ & b₁ * b₂ = b₂ & ex b₃ being Element of a₁ st
( b₂ * b₃ = b₁ & b₃ * b₂ = b₁ ) );
attr a₁ is associative means :Def4: :: GROUP_1:def 4
for b₁, b₂, b₃ being Element of a₁ holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃);

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 Th1: :: GROUP_1:1

canceled;

theorem Th2: :: GROUP_1:2

canceled;

theorem Th3: :: GROUP_1:3

canceled;

theorem Th4: :: GROUP_1:4

canceled;

theorem Th5: :: GROUP_1:5

for b₁ being non empty HGrStr st ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ex b₂ being Element of b₁ st
for b₃ being Element of b₁ holds
( b₃ * b₂ = b₃ & b₂ * b₃ = b₃ & ex b₄ being Element of b₁ st
( b₃ * b₄ = b₂ & b₄ * b₃ = b₂ ) ) holds
b₁ is Group by Def3, Def4;

theorem Th6: :: GROUP_1:6

for b₁ being non empty HGrStr st ( for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) ) & ( for b₂, b₃ being Element of b₁ holds
( ex b₄ being Element of b₁ st b₂ * b₄ = b₃ & ex b₄ being Element of b₁ st b₄ * b₂ = b₃ ) ) holds
( b₁ is associative & b₁ 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 c₁ be non empty HGrStr ;
assume E6: c₁ is unital ;
func 1. c₁ -> Element of a₁ means :Def5: :: GROUP_1:def 5
for b₁ being Element of a₁ holds
( b₁ * a₂ = b₁ & a₂ * b₁ = b₁ );
existence by E6, Def2;
uniqueness

proof end;

end;

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

theorem Th8: :: GROUP_1:8

canceled;

theorem Th9: :: GROUP_1:9

canceled;

theorem Th10: :: GROUP_1:10

for b₁ being non empty Group-like HGrStr
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds
( b₃ * b₂ = b₃ & b₂ * b₃ = b₃ ) ) holds
b₂ = 1. b₁ by Def5;

definition

let c₁ be Group;
let c₂ be Element of c₁;
func c₂ " -> Element of a₁ means :Def6: :: GROUP_1:def 6
( a₂ * a₃ = 1. a₁ & a₃ * a₂ = 1. a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines " GROUP_1:def 6 :

theorem Th11: :: GROUP_1:11

canceled;

theorem Th12: :: GROUP_1:12

for b₁ being Group
for b₂, b₃ being Element of b₁ st b₂ * b₃ = 1. b₁ & b₃ * b₂ = 1. b₁ holds
b₃ = b₂ " by Def6;

theorem Th13: :: GROUP_1:13

canceled;

theorem Th14: :: GROUP_1:14

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ st ( b₂ * b₃ = b₂ * b₄ or b₃ * b₂ = b₄ * b₂ ) holds
b₃ = b₄

proof end;

theorem Th15: :: GROUP_1:15

for b₁ being Group
for b₂, b₃ being Element of b₁ st ( b₂ * b₃ = b₂ or b₃ * b₂ = b₂ ) holds
b₃ = 1. b₁

proof end;

theorem Th16: :: GROUP_1:16

for b₁ being Group holds (1. b₁) " = 1. b₁

proof end;

theorem Th17: :: GROUP_1:17

for b₁ being Group
for b₂, b₃ being Element of b₁ st b₂ " = b₃ " holds
b₂ = b₃

proof end;

theorem Th18: :: GROUP_1:18

for b₁ being Group
for b₂ being Element of b₁ st b₂ " = 1. b₁ holds
b₂ = 1. b₁

proof end;

theorem Th19: :: GROUP_1:19

for b₁ being Group
for b₂ being Element of b₁ holds (b₂ " ) " = b₂

proof end;

theorem Th20: :: GROUP_1:20

for b₁ being Group
for b₂, b₃ being Element of b₁ st ( b₂ * b₃ = 1. b₁ or b₃ * b₂ = 1. b₁ ) holds
( b₂ = b₃ " & b₃ = b₂ " )

proof end;

theorem Th21: :: GROUP_1:21

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ * b₃ = b₄ iff b₃ = (b₂ " ) * b₄ )

proof end;

theorem Th22: :: GROUP_1:22

for b₁ being Group
for b₂, b₃, b₄ being Element of b₁ holds
( b₂ * b₃ = b₄ iff b₂ = b₄ * (b₃ " ) )

proof end;

theorem Th23: :: GROUP_1:23

for b₁ being Group
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₂ * b₄ = b₃

proof end;

theorem Th24: :: GROUP_1:24

for b₁ being Group
for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₄ * b₂ = b₃

proof end;

theorem Th25: :: GROUP_1:25

for b₁ being Group
for b₂, b₃ being Element of b₁ holds (b₂ * b₃) " = (b₃ " ) * (b₂ " )

proof end;

theorem Th26: :: GROUP_1:26

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂ * b₃ = b₃ * b₂ iff (b₂ * b₃) " = (b₂ " ) * (b₃ " ) )

proof end;

theorem Th27: :: GROUP_1:27

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂ * b₃ = b₃ * b₂ iff (b₂ " ) * (b₃ " ) = (b₃ " ) * (b₂ " ) )

proof end;

theorem Th28: :: GROUP_1:28

for b₁ being Group
for b₂, b₃ being Element of b₁ holds
( b₂ * b₃ = b₃ * b₂ iff b₂ * (b₃ " ) = (b₃ " ) * b₂ )

proof end;

definition

let c₁ be Group;
func inverse_op c₁ -> UnOp of the carrier of a₁ means :Def7: :: GROUP_1:def 7
for b₁ being Element of a₁ holds a₂ . b₁ = b₁ " ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines inverse_op GROUP_1:def 7 :

theorem Th29: :: GROUP_1:29

canceled;

theorem Th30: :: GROUP_1:30

canceled;

theorem Th31: :: GROUP_1:31

for b₁ being non empty associative HGrStr holds the mult of b₁ is associative

proof end;

theorem Th32: :: GROUP_1:32

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

proof end;

theorem Th33: :: GROUP_1:33

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

proof end;

theorem Th34: :: GROUP_1:34

for b₁ being non empty unital HGrStr holds the mult of b₁ has_a_unity

proof end;

theorem Th35: :: GROUP_1:35

for b₁ being Group holds inverse_op b₁ is_an_inverseOp_wrt the mult of b₁

proof end;

theorem Th36: :: GROUP_1:36

for b₁ being Group holds the mult of b₁ has_an_inverseOp

proof end;

theorem Th37: :: GROUP_1:37

for b₁ being Group holds the_inverseOp_wrt the mult of b₁ = inverse_op b₁

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines power GROUP_1:def 8 :

definition

let c₁ be Group;
let c₂ be Integer;
let c₃ be Element of c₁;
func c₃ |^ c₂ -> Element of a₁ equals :Def9: :: GROUP_1:def 9
(power a₁) . a₃,(abs a₂) if 0 <= a₂
otherwise ((power a₁) . a₃,(abs a₂)) " ;
correctness ;

end;

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

definition

let c₁ be Group;
let c₂ be Nat;
let c₃ be Element of c₁;
redefine func c₃ |^ c₂ -> Element of a₁ equals :: GROUP_1:def 10
(power a₁) . a₃,a₂;
compatibility

proof end;

end;

:: deftheorem Def10 defines |^ GROUP_1:def 10 :

Lemma28: for b₁ being Nat
for b₂ being Group
for b₃ being Element of b₂ holds b₃ |^ (b₁ + 1) = (b₃ |^ b₁) * b₃
by Def8;

Lemma29: for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ 0 = 1. b₁
by Def8;

theorem Th38: :: GROUP_1:38

canceled;

theorem Th39: :: GROUP_1:39

canceled;

theorem Th40: :: GROUP_1:40

canceled;

theorem Th41: :: GROUP_1:41

canceled;

theorem Th42: :: GROUP_1:42

for b₁ being Nat
for b₂ being Group holds (1. b₂) |^ b₁ = 1. b₂

proof end;

theorem Th43: :: GROUP_1:43

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ 0 = 1. b₁ by Lemma29;

theorem Th44: :: GROUP_1:44

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ 1 = b₂

proof end;

theorem Th45: :: GROUP_1:45

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ 2 = b₂ * b₂

proof end;

theorem Th46: :: GROUP_1:46

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ 3 = (b₂ * b₂) * b₂

proof end;

theorem Th47: :: GROUP_1:47

for b₁ being Group
for b₂ being Element of b₁ holds
( b₂ |^ 2 = 1. b₁ iff b₂ " = b₂ )

proof end;

theorem Th48: :: GROUP_1:48

for b₁, b₂ being Nat
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₁ + b₂) = (b₄ |^ b₁) * (b₄ |^ b₂)

proof end;

theorem Th49: :: GROUP_1:49

for b₁ being Nat
for b₂ being Group
for b₃ being Element of b₂ holds
( b₃ |^ (b₁ + 1) = (b₃ |^ b₁) * b₃ & b₃ |^ (b₁ + 1) = b₃ * (b₃ |^ b₁) )

proof end;

theorem Th50: :: GROUP_1:50

for b₁, b₂ being Nat
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₁ * b₂) = (b₄ |^ b₁) |^ b₂

proof end;

theorem Th51: :: GROUP_1:51

for b₁ being Nat
for b₂ being Group
for b₃ being Element of b₂ holds (b₃ " ) |^ b₁ = (b₃ |^ b₁) "

proof end;

theorem Th52: :: GROUP_1:52

for b₁ being Nat
for b₂ being Group
for b₃, b₄ being Element of b₂ st b₃ * b₄ = b₄ * b₃ holds
b₃ * (b₄ |^ b₁) = (b₄ |^ b₁) * b₃

proof end;

theorem Th53: :: GROUP_1:53

for b₁, b₂ being Nat
for b₃ being Group
for b₄, b₅ being Element of b₃ st b₄ * b₅ = b₅ * b₄ holds
(b₄ |^ b₁) * (b₅ |^ b₂) = (b₅ |^ b₂) * (b₄ |^ b₁)

proof end;

theorem Th54: :: GROUP_1:54

for b₁ being Nat
for b₂ being Group
for b₃, b₄ being Element of b₂ st b₃ * b₄ = b₄ * b₃ holds
(b₃ * b₄) |^ b₁ = (b₃ |^ b₁) * (b₄ |^ b₁)

proof end;

theorem Th55: :: GROUP_1:55

for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ st 0 <= b₁ holds
b₃ |^ b₁ = b₃ |^ (abs b₁) by Def9;

theorem Th56: :: GROUP_1:56

for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ st not 0 <= b₁ holds
b₃ |^ b₁ = (b₃ |^ (abs b₁)) " by Def9;

theorem Th57: :: GROUP_1:57

canceled;

theorem Th58: :: GROUP_1:58

canceled;

theorem Th59: :: GROUP_1:59

for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ st b₁ = 0 holds
b₃ |^ b₁ = 1. b₂ by Lemma29;

theorem Th60: :: GROUP_1:60

for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ st b₁ <= 0 holds
b₃ |^ b₁ = (b₃ |^ (abs b₁)) "

proof end;

theorem Th61: :: GROUP_1:61

for b₁ being Integer
for b₂ being Group holds (1. b₂) |^ b₁ = 1. b₂

proof end;

theorem Th62: :: GROUP_1:62

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ (- 1) = b₂ "

proof end;

Lemma44: for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ holds b₃ |^ (- b₁) = (b₃ |^ b₁) "

proof end;

Lemma45: for b₁ being Integer holds
( b₁ >= 1 or b₁ = 0 or b₁ < 0 )

proof end;

Lemma46: for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ holds b₃ |^ (b₁ - 1) = (b₃ |^ b₁) * (b₃ |^ (- 1))

proof end;

Lemma47: for b₁ being Integer holds
( b₁ >= 0 or b₁ = - 1 or b₁ < - 1 )

proof end;

Lemma48: for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ holds b₃ |^ (b₁ + 1) = (b₃ |^ b₁) * (b₃ |^ 1)

proof end;

theorem Th63: :: GROUP_1:63

for b₁, b₂ being Integer
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₁ + b₂) = (b₄ |^ b₁) * (b₄ |^ b₂)

proof end;

theorem Th64: :: GROUP_1:64

for b₁ being Nat
for b₂ being Integer
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₁ + b₂) = (b₄ |^ b₁) * (b₄ |^ b₂) by Th63;

theorem Th65: :: GROUP_1:65

for b₁ being Nat
for b₂ being Integer
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₂ + b₁) = (b₄ |^ b₂) * (b₄ |^ b₁) by Th63;

theorem Th66: :: GROUP_1:66

for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ holds
( b₃ |^ (b₁ + 1) = (b₃ |^ b₁) * b₃ & b₃ |^ (b₁ + 1) = b₃ * (b₃ |^ b₁) )

proof end;

Lemma50: for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ holds (b₃ " ) |^ b₁ = (b₃ |^ b₁) "

proof end;

theorem Th67: :: GROUP_1:67

for b₁, b₂ being Integer
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₁ * b₂) = (b₄ |^ b₁) |^ b₂

proof end;

theorem Th68: :: GROUP_1:68

for b₁ being Nat
for b₂ being Integer
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₁ * b₂) = (b₄ |^ b₁) |^ b₂ by Th67;

theorem Th69: :: GROUP_1:69

for b₁ being Nat
for b₂ being Integer
for b₃ being Group
for b₄ being Element of b₃ holds b₄ |^ (b₂ * b₁) = (b₄ |^ b₂) |^ b₁ by Th67;

theorem Th70: :: GROUP_1:70

for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ holds b₃ |^ (- b₁) = (b₃ |^ b₁) " by Lemma44;

theorem Th71: :: GROUP_1:71

for b₁ being Nat
for b₂ being Group
for b₃ being Element of b₂ holds b₃ |^ (- b₁) = (b₃ |^ b₁) " by Lemma44;

theorem Th72: :: GROUP_1:72

for b₁ being Integer
for b₂ being Group
for b₃ being Element of b₂ holds (b₃ " ) |^ b₁ = (b₃ |^ b₁) " by Lemma50;

theorem Th73: :: GROUP_1:73

for b₁ being Integer
for b₂ being Group
for b₃, b₄ being Element of b₂ st b₃ * b₄ = b₄ * b₃ holds
(b₃ * b₄) |^ b₁ = (b₃ |^ b₁) * (b₄ |^ b₁)

proof end;

theorem Th74: :: GROUP_1:74

for b₁, b₂ being Integer
for b₃ being Group
for b₄, b₅ being Element of b₃ st b₄ * b₅ = b₅ * b₄ holds
(b₄ |^ b₁) * (b₅ |^ b₂) = (b₅ |^ b₂) * (b₄ |^ b₁)

proof end;

theorem Th75: :: GROUP_1:75

for b₁ being Nat
for b₂ being Integer
for b₃ being Group
for b₄, b₅ being Element of b₃ st b₄ * b₅ = b₅ * b₄ holds
(b₄ |^ b₁) * (b₅ |^ b₂) = (b₅ |^ b₂) * (b₄ |^ b₁) by Th74;

theorem Th76: :: GROUP_1:76

canceled;

theorem Th77: :: GROUP_1:77

for b₁ being Integer
for b₂ being Group
for b₃, b₄ being Element of b₂ st b₃ * b₄ = b₄ * b₃ holds
b₃ * (b₄ |^ b₁) = (b₄ |^ b₁) * b₃

proof end;

definition

let c₁ be Group;
let c₂ be Element of c₁;
attr a₂ is being_of_order_0 means :Def11: :: GROUP_1:def 11
for b₁ being Nat st a₂ |^ b₁ = 1. a₁ holds
b₁ = 0;

end;

:: deftheorem Def11 defines being_of_order_0 GROUP_1:def 11 :

notation

let c₁ be Group;
let c₂ be Element of c₁;
antonym c₂ is_not_of_order_0 for being_of_order_0 c₂;
synonym c₂ is_of_order_0 for being_of_order_0 c₂;

end;

theorem Th78: :: GROUP_1:78

canceled;

theorem Th79: :: GROUP_1:79

for b₁ being Group holds 1. b₁ is_not_of_order_0

proof end;

definition

let c₁ be Group;
let c₂ be Element of c₁;
func ord c₂ -> Nat means :Def12: :: GROUP_1:def 12
a₃ = 0 if a₂ is_of_order_0
otherwise ( a₂ |^ a₃ = 1. a₁ & a₃ <> 0 & ( for b₁ being Nat st a₂ |^ b₁ = 1. a₁ & b₁ <> 0 holds
a₃ <= b₁ ) );
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def12 defines ord GROUP_1:def 12 :

theorem Th80: :: GROUP_1:80

canceled;

theorem Th81: :: GROUP_1:81

canceled;

theorem Th82: :: GROUP_1:82

for b₁ being Group
for b₂ being Element of b₁ holds b₂ |^ (ord b₂) = 1. b₁

proof end;

theorem Th83: :: GROUP_1:83

canceled;

theorem Th84: :: GROUP_1:84

for b₁ being Group holds ord (1. b₁) = 1

proof end;

theorem Th85: :: GROUP_1:85

for b₁ being Group
for b₂ being Element of b₁ st ord b₂ = 1 holds
b₂ = 1. b₁

proof end;

theorem Th86: :: GROUP_1:86

for b₁ being Nat
for b₂ being Group
for b₃ being Element of b₂ st b₃ |^ b₁ = 1. b₂ holds
ord b₃ divides b₁

proof end;

definition

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

end;

:: deftheorem Def13 defines Ord GROUP_1:def 13 :

definition

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

end;

:: deftheorem Def14 defines finite GROUP_1:def 14 :

notation

let c₁ be 1-sorted ;
antonym infinite c₁ for finite c₁;

end;

definition

let c₁ be Group;
assume E59: c₁ is finite ;
func ord c₁ -> Nat means :Def15: :: GROUP_1:def 15
ex b₁ being finite set st
( b₁ = the carrier of a₁ & a₂ = card b₁ );
existence

proof end;

correctness ;

end;

:: deftheorem Def15 defines ord GROUP_1:def 15 :

theorem Th87: :: GROUP_1:87

canceled;

theorem Th88: :: GROUP_1:88

canceled;

theorem Th89: :: GROUP_1:89

canceled;

theorem Th90: :: GROUP_1:90

for b₁ being Group st b₁ is finite holds
ord b₁ >= 1

proof end;

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

definition

let c₂ be non empty HGrStr ;
attr a₁ is commutative means :Def16: :: GROUP_1:def 16
for b₁, b₂ being Element of a₁ holds b₁ * b₂ = b₂ * b₁;

end;

:: deftheorem Def16 defines commutative GROUP_1:def 16 :

registration

cluster strict commutative HGrStr ;
existence

proof end;

end;

definition

let c₂ be non empty commutative HGrStr ;
let c₃, c₄ be Element of c₂;
redefine func * as c₂ * c₃ -> Element of a₁;
commutativity by Def16;

end;

theorem Th91: :: GROUP_1:91

canceled;

theorem Th92: :: GROUP_1:92

HGrStr(# REAL ,addreal #) is commutative Group

proof end;

theorem Th93: :: GROUP_1:93

canceled;

theorem Th94: :: GROUP_1:94

for b₁ being commutative Group
for b₂, b₃ being Element of b₁ holds (b₂ * b₃) " = (b₂ " ) * (b₃ " ) by Th25;

theorem Th95: :: GROUP_1:95

for b₁ being Nat
for b₂ being commutative Group
for b₃, b₄ being Element of b₂ holds (b₃ * b₄) |^ b₁ = (b₃ |^ b₁) * (b₄ |^ b₁) by Th54;

theorem Th96: :: GROUP_1:96

for b₁ being Integer
for b₂ being commutative Group
for b₃, b₄ being Element of b₂ holds (b₃ * b₄) |^ b₁ = (b₃ |^ b₁) * (b₄ |^ b₁) by Th73;

registration

let c₂ be non empty set ;
let c₃ be BinOp of c₂;
let c₄ be Element of c₂;
cluster LoopStr(# a₁,a₂,a₃ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

theorem Th97: :: GROUP_1:97

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

proof end;