:: GROUP_7 semantic presentation

theorem Th1: :: GROUP_7:1

for b₁, b₂ being set st <*b₁*> = <*b₂*> holds
b₁ = b₂

proof end;

theorem Th2: :: GROUP_7:2

for b₁, b₂, b₃, b₄ being set st <*b₁,b₂*> = <*b₃,b₄*> holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th3: :: GROUP_7:3

for b₁, b₂, b₃, b₄, b₅, b₆ being set st <*b₁,b₂,b₃*> = <*b₄,b₅,b₆*> holds
( b₁ = b₄ & b₂ = b₅ & b₃ = b₆ )

proof end;

definition

let c₁ be Relation;
attr a₁ is HGrStr-yielding means :Def1: :: GROUP_7:def 1
for b₁ being set st b₁ in rng a₁ holds
b₁ is non empty HGrStr ;

end;

:: deftheorem Def1 defines HGrStr-yielding GROUP_7:def 1 :

registration

cluster HGrStr-yielding -> 1-sorted-yielding set ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster 1-sorted-yielding HGrStr-yielding ManySortedSet of a₁;
existence

proof end;

end;

registration

cluster 1-sorted-yielding HGrStr-yielding set ;
existence

proof end;

end;

definition

let c₁ be set ;
mode HGrStr-Family of a₁ is HGrStr-yielding ManySortedSet of a₁;

end;

definition

let c₁ be non empty set ;
let c₂ be HGrStr-Family of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> non empty HGrStr ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be HGrStr-Family of c₁;
cluster Carrier a₂ -> V2 ;
coherence

proof end;

end;

E3: now

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be HGrStr-yielding ManySortedSet of c₁;
let c₄ be Element of product (Carrier c₃);
E4: ex b₁ being 1-sorted st
( b₁ = c₃ . c₂ & (Carrier c₃) . c₂ = the carrier of b₁ ) by PRALG_1:def 13;
dom (Carrier c₃) = c₁ by PBOOLE:def 3;
hence c₄ . c₂ in the carrier of (c₃ . c₂) by E4, CARD_3:18;

end;

definition

let c₁ be set ;
let c₂ be HGrStr-Family of c₁;
func product c₂ -> strict HGrStr means :Def2: :: GROUP_7:def 2
( the carrier of a₃ = product (Carrier a₂) & ( for b₁, b₂ being Element of product (Carrier a₂)
for b₃ being set st b₃ in a₁ holds
ex b₄ being non empty HGrStr ex b₅ being Function st
( b₄ = a₂ . b₃ & b₅ = the mult of a₃ . b₁,b₂ & b₅ . b₃ = the mult of b₄ . (b₁ . b₃),(b₂ . b₃) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines product GROUP_7:def 2 :

registration

let c₁ be set ;
let c₂ be HGrStr-Family of c₁;
cluster product a₂ -> non empty strict constituted-Functions ;
coherence

proof end;

end;

theorem Th4: :: GROUP_7:4

for b₁, b₂ being set
for b₃, b₄, b₅ being Function
for b₆ being HGrStr-Family of b₁
for b₇ being non empty HGrStr
for b₈, b₉ being Element of (product b₆)
for b₁₀, b₁₁ being Element of b₇ st b₂ in b₁ & b₇ = b₆ . b₂ & b₃ = b₈ & b₄ = b₉ & b₅ = b₈ * b₉ & b₃ . b₂ = b₁₀ & b₄ . b₂ = b₁₁ holds
b₁₀ * b₁₁ = b₅ . b₂

proof end;

definition

let c₁ be set ;
let c₂ be HGrStr-Family of c₁;
attr a₂ is Group-like means :Def3: :: GROUP_7:def 3
for b₁ being set st b₁ in a₁ holds
ex b₂ being non empty Group-like HGrStr st b₂ = a₂ . b₁;
attr a₂ is associative means :Def4: :: GROUP_7:def 4
for b₁ being set st b₁ in a₁ holds
ex b₂ being non empty associative HGrStr st b₂ = a₂ . b₁;
attr a₂ is commutative means :Def5: :: GROUP_7:def 5
for b₁ being set st b₁ in a₁ holds
ex b₂ being non empty commutative HGrStr st b₂ = a₂ . b₁;

end;

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

:: deftheorem Def4 defines associative GROUP_7:def 4 :

:: deftheorem Def5 defines commutative GROUP_7:def 5 :

definition

let c₁ be non empty set ;
let c₂ be HGrStr-Family of c₁;
redefine attr a₂ is Group-like means :Def6: :: GROUP_7:def 6
for b₁ being Element of a₁ holds a₂ . b₁ is Group-like;
compatibility

proof end;

redefine attr a₂ is associative means :Def7: :: GROUP_7:def 7
for b₁ being Element of a₁ holds a₂ . b₁ is associative;
compatibility

proof end;

redefine attr a₂ is commutative means :: GROUP_7:def 8
for b₁ being Element of a₁ holds a₂ . b₁ is commutative;
compatibility

proof end;

end;

:: deftheorem Def6 defines Group-like GROUP_7:def 6 :

:: deftheorem Def7 defines associative GROUP_7:def 7 :

:: deftheorem Def8 defines commutative GROUP_7:def 8 :

registration

let c₁ be set ;
cluster Group-like associative commutative ManySortedSet of a₁;
existence

proof end;

end;

registration

let c₁ be set ;
let c₂ be Group-like HGrStr-Family of c₁;
cluster product a₂ -> non empty strict Group-like constituted-Functions ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be associative HGrStr-Family of c₁;
cluster product a₂ -> non empty strict associative constituted-Functions ;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be commutative HGrStr-Family of c₁;
cluster product a₂ -> non empty strict commutative constituted-Functions ;
coherence

proof end;

end;

theorem Th5: :: GROUP_7:5

for b₁, b₂ being set
for b₃ being HGrStr-Family of b₁
for b₄ being non empty HGrStr st b₂ in b₁ & b₄ = b₃ . b₂ & product b₃ is Group-like holds
b₄ is Group-like

proof end;

theorem Th6: :: GROUP_7:6

for b₁, b₂ being set
for b₃ being HGrStr-Family of b₁
for b₄ being non empty HGrStr st b₂ in b₁ & b₄ = b₃ . b₂ & product b₃ is associative holds
b₄ is associative

proof end;

theorem Th7: :: GROUP_7:7

for b₁, b₂ being set
for b₃ being HGrStr-Family of b₁
for b₄ being non empty HGrStr st b₂ in b₁ & b₄ = b₃ . b₂ & product b₃ is commutative holds
b₄ is commutative

proof end;

theorem Th8: :: GROUP_7:8

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being Group-like HGrStr-Family of b₁ st ( for b₄ being set st b₄ in b₁ holds
ex b₅ being non empty Group-like HGrStr st
( b₅ = b₃ . b₄ & b₂ . b₄ = 1. b₅ ) ) holds
b₂ = 1. (product b₃)

proof end;

theorem Th9: :: GROUP_7:9

for b₁, b₂ being set
for b₃ being Function
for b₄ being Group-like HGrStr-Family of b₁
for b₅ being non empty Group-like HGrStr st b₂ in b₁ & b₅ = b₄ . b₂ & b₃ = 1. (product b₄) holds
b₃ . b₂ = 1. b₅

proof end;

theorem Th10: :: GROUP_7:10

for b₁ being set
for b₂ being Function
for b₃ being ManySortedSet of b₁
for b₄ being Group-like associative HGrStr-Family of b₁
for b₅ being Element of (product b₄) st b₅ = b₂ & ( for b₆ being set st b₆ in b₁ holds
ex b₇ being Groupex b₈ being Element of b₇ st
( b₇ = b₄ . b₆ & b₃ . b₆ = b₈ " & b₈ = b₂ . b₆ ) ) holds
b₃ = b₅ "

proof end;

theorem Th11: :: GROUP_7:11

for b₁, b₂ being set
for b₃, b₄ being Function
for b₅ being Group-like associative HGrStr-Family of b₁
for b₆ being Element of (product b₅)
for b₇ being Group
for b₈ being Element of b₇ st b₂ in b₁ & b₇ = b₅ . b₂ & b₃ = b₆ & b₄ = b₆ " & b₃ . b₂ = b₈ holds
b₄ . b₂ = b₈ "

proof end;

definition

let c₁ be set ;
let c₂ be Group-like associative HGrStr-Family of c₁;
func sum c₂ -> strict Subgroup of product a₂ means :Def9: :: GROUP_7:def 9
for b₁ being set holds
( b₁ in the carrier of a₃ iff ex b₂ being Element of product (Carrier a₂)ex b₃ being finite Subset of a₁ex b₄ being ManySortedSet of b₃ st
( b₂ = 1. (product a₂) & b₁ = b₂ +* b₄ & ( for b₅ being set st b₅ in b₃ holds
ex b₆ being non empty Group-like HGrStr st
( b₆ = a₂ . b₅ & b₄ . b₅ in the carrier of b₆ & b₄ . b₅ <> 1. b₆ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines sum GROUP_7:def 9 :

registration

let c₁ be set ;
let c₂ be Group-like associative HGrStr-Family of c₁;
let c₃, c₄ be Element of (sum c₂);
cluster the mult of (sum a₂) . a₃,a₄ -> Relation-like Function-like ;
coherence

proof end;

end;

theorem Th12: :: GROUP_7:12

for b₁ being finite set
for b₂ being Group-like associative HGrStr-Family of b₁ holds product b₂ = sum b₂

proof end;

theorem Th13: :: GROUP_7:13

for b₁ being non empty HGrStr holds <*b₁*> is HGrStr-Family of {1}

proof end;

definition

let c₁ be non empty HGrStr ;
redefine func <* as <*c₁*> -> HGrStr-Family of {1};
coherence by Th13;

end;

theorem Th14: :: GROUP_7:14

for b₁ being non empty Group-like HGrStr holds <*b₁*> is Group-like HGrStr-Family of {1}

proof end;

definition

let c₁ be non empty Group-like HGrStr ;
redefine func <* as <*c₁*> -> Group-like HGrStr-Family of {1};
coherence by Th14;

end;

theorem Th15: :: GROUP_7:15

for b₁ being non empty associative HGrStr holds <*b₁*> is associative HGrStr-Family of {1}

proof end;

definition

let c₁ be non empty associative HGrStr ;
redefine func <* as <*c₁*> -> associative HGrStr-Family of {1};
coherence by Th15;

end;

theorem Th16: :: GROUP_7:16

for b₁ being non empty commutative HGrStr holds <*b₁*> is commutative HGrStr-Family of {1}

proof end;

definition

let c₁ be non empty commutative HGrStr ;
redefine func <* as <*c₁*> -> commutative HGrStr-Family of {1};
coherence by Th16;

end;

theorem Th17: :: GROUP_7:17

for b₁ being Group holds <*b₁*> is Group-like associative HGrStr-Family of {1}

proof end;

definition

let c₁ be Group;
redefine func <* as <*c₁*> -> Group-like associative HGrStr-Family of {1};
coherence by Th17;

end;

theorem Th18: :: GROUP_7:18

for b₁ being commutative Group holds <*b₁*> is Group-like associative commutative HGrStr-Family of {1}

proof end;

definition

let c₁ be commutative Group;
redefine func <* as <*c₁*> -> Group-like associative commutative HGrStr-Family of {1};
coherence by Th18;

end;

registration

let c₁ be non empty HGrStr ;
cluster -> FinSequence-like Element of product (Carrier <*a₁*>);
coherence

proof end;

end;

registration

let c₁ be non empty HGrStr ;
cluster -> FinSequence-like Element of the carrier of (product <*a₁*>);
coherence

proof end;

end;

definition

let c₁ be non empty HGrStr ;
let c₂ be Element of c₁;
redefine func <* as <*c₂*> -> Element of (product <*a₁*>);
coherence

proof end;

end;

theorem Th19: :: GROUP_7:19

for b₁, b₂ being non empty HGrStr holds <*b₁,b₂*> is HGrStr-Family of {1,2}

proof end;

definition

let c₁, c₂ be non empty HGrStr ;
redefine func <* as <*c₁,c₂*> -> HGrStr-Family of {1,2};
coherence by Th19;

end;

theorem Th20: :: GROUP_7:20

for b₁, b₂ being non empty Group-like HGrStr holds <*b₁,b₂*> is Group-like HGrStr-Family of {1,2}

proof end;

definition

let c₁, c₂ be non empty Group-like HGrStr ;
redefine func <* as <*c₁,c₂*> -> Group-like HGrStr-Family of {1,2};
coherence by Th20;

end;

theorem Th21: :: GROUP_7:21

for b₁, b₂ being non empty associative HGrStr holds <*b₁,b₂*> is associative HGrStr-Family of {1,2}

proof end;

definition

let c₁, c₂ be non empty associative HGrStr ;
redefine func <* as <*c₁,c₂*> -> associative HGrStr-Family of {1,2};
coherence by Th21;

end;

theorem Th22: :: GROUP_7:22

for b₁, b₂ being non empty commutative HGrStr holds <*b₁,b₂*> is commutative HGrStr-Family of {1,2}

proof end;

definition

let c₁, c₂ be non empty commutative HGrStr ;
redefine func <* as <*c₁,c₂*> -> commutative HGrStr-Family of {1,2};
coherence by Th22;

end;

theorem Th23: :: GROUP_7:23

for b₁, b₂ being Group holds <*b₁,b₂*> is Group-like associative HGrStr-Family of {1,2}

proof end;

definition

let c₁, c₂ be Group;
redefine func <* as <*c₁,c₂*> -> Group-like associative HGrStr-Family of {1,2};
coherence by Th23;

end;

theorem Th24: :: GROUP_7:24

for b₁, b₂ being commutative Group holds <*b₁,b₂*> is Group-like associative commutative HGrStr-Family of {1,2}

proof end;

definition

let c₁, c₂ be commutative Group;
redefine func <* as <*c₁,c₂*> -> Group-like associative commutative HGrStr-Family of {1,2};
coherence by Th24;

end;

registration

let c₁, c₂ be non empty HGrStr ;
cluster -> FinSequence-like Element of product (Carrier <*a₁,a₂*>);
coherence

proof end;

end;

registration

let c₁, c₂ be non empty HGrStr ;
cluster -> FinSequence-like Element of the carrier of (product <*a₁,a₂*>);
coherence

proof end;

end;

definition

let c₁, c₂ be non empty HGrStr ;
let c₃ be Element of c₁;
let c₄ be Element of c₂;
redefine func <* as <*c₃,c₄*> -> Element of (product <*a₁,a₂*>);
coherence

proof end;

end;

theorem Th25: :: GROUP_7:25

for b₁, b₂, b₃ being non empty HGrStr holds <*b₁,b₂,b₃*> is HGrStr-Family of {1,2,3}

proof end;

definition

let c₁, c₂, c₃ be non empty HGrStr ;
redefine func <* as <*c₁,c₂,c₃*> -> HGrStr-Family of {1,2,3};
coherence by Th25;

end;

theorem Th26: :: GROUP_7:26

for b₁, b₂, b₃ being non empty Group-like HGrStr holds <*b₁,b₂,b₃*> is Group-like HGrStr-Family of {1,2,3}

proof end;

definition

let c₁, c₂, c₃ be non empty Group-like HGrStr ;
redefine func <* as <*c₁,c₂,c₃*> -> Group-like HGrStr-Family of {1,2,3};
coherence by Th26;

end;

theorem Th27: :: GROUP_7:27

for b₁, b₂, b₃ being non empty associative HGrStr holds <*b₁,b₂,b₃*> is associative HGrStr-Family of {1,2,3}

proof end;

definition

let c₁, c₂, c₃ be non empty associative HGrStr ;
redefine func <* as <*c₁,c₂,c₃*> -> associative HGrStr-Family of {1,2,3};
coherence by Th27;

end;

theorem Th28: :: GROUP_7:28

for b₁, b₂, b₃ being non empty commutative HGrStr holds <*b₁,b₂,b₃*> is commutative HGrStr-Family of {1,2,3}

proof end;

definition

let c₁, c₂, c₃ be non empty commutative HGrStr ;
redefine func <* as <*c₁,c₂,c₃*> -> commutative HGrStr-Family of {1,2,3};
coherence by Th28;

end;

theorem Th29: :: GROUP_7:29

for b₁, b₂, b₃ being Group holds <*b₁,b₂,b₃*> is Group-like associative HGrStr-Family of {1,2,3}

proof end;

definition

let c₁, c₂, c₃ be Group;
redefine func <* as <*c₁,c₂,c₃*> -> Group-like associative HGrStr-Family of {1,2,3};
coherence by Th29;

end;

theorem Th30: :: GROUP_7:30

for b₁, b₂, b₃ being commutative Group holds <*b₁,b₂,b₃*> is Group-like associative commutative HGrStr-Family of {1,2,3}

proof end;

definition

let c₁, c₂, c₃ be commutative Group;
redefine func <* as <*c₁,c₂,c₃*> -> Group-like associative commutative HGrStr-Family of {1,2,3};
coherence by Th30;

end;

registration

let c₁, c₂, c₃ be non empty HGrStr ;
cluster -> FinSequence-like Element of product (Carrier <*a₁,a₂,a₃*>);
coherence

proof end;

end;

registration

let c₁, c₂, c₃ be non empty HGrStr ;
cluster -> FinSequence-like Element of the carrier of (product <*a₁,a₂,a₃*>);
coherence

proof end;

end;

definition

let c₁, c₂, c₃ be non empty HGrStr ;
let c₄ be Element of c₁;
let c₅ be Element of c₂;
let c₆ be Element of c₃;
redefine func <* as <*c₄,c₅,c₆*> -> Element of (product <*a₁,a₂,a₃*>);
coherence

proof end;

end;

theorem Th31: :: GROUP_7:31

for b₁ being non empty HGrStr
for b₂, b₃ being Element of b₁ holds <*b₂*> * <*b₃*> = <*(b₂ * b₃)*>

proof end;

theorem Th32: :: GROUP_7:32

for b₁, b₂ being non empty HGrStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ holds <*b₃,b₅*> * <*b₄,b₆*> = <*(b₃ * b₄),(b₅ * b₆)*>

proof end;

theorem Th33: :: GROUP_7:33

for b₁, b₂, b₃ being non empty HGrStr
for b₄, b₅ being Element of b₁
for b₆, b₇ being Element of b₂
for b₈, b₉ being Element of b₃ holds <*b₄,b₆,b₈*> * <*b₅,b₇,b₉*> = <*(b₄ * b₅),(b₆ * b₇),(b₈ * b₉)*>

proof end;

theorem Th34: :: GROUP_7:34

for b₁ being non empty Group-like HGrStr holds 1. (product <*b₁*>) = <*(1. b₁)*>

proof end;

theorem Th35: :: GROUP_7:35

for b₁, b₂ being non empty Group-like HGrStr holds 1. (product <*b₁,b₂*>) = <*(1. b₁),(1. b₂)*>

proof end;

theorem Th36: :: GROUP_7:36

for b₁, b₂, b₃ being non empty Group-like HGrStr holds 1. (product <*b₁,b₂,b₃*>) = <*(1. b₁),(1. b₂),(1. b₃)*>

proof end;

theorem Th37: :: GROUP_7:37

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

proof end;

theorem Th38: :: GROUP_7:38

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

proof end;

theorem Th39: :: GROUP_7:39

for b₁, b₂, b₃ being Group
for b₄ being Element of b₁
for b₅ being Element of b₂
for b₆ being Element of b₃ holds <*b₄,b₅,b₆*> " = <*(b₄ " ),(b₅ " ),(b₆ " )*>

proof end;

theorem Th40: :: GROUP_7:40

for b₁ being Group
for b₂ being Function of the carrier of b₁,the carrier of (product <*b₁*>) st ( for b₃ being Element of b₁ holds b₂ . b₃ = <*b₃*> ) holds
b₂ is Homomorphism of b₁,(product <*b₁*>)

proof end;

theorem Th41: :: GROUP_7:41

for b₁ being Group
for b₂ being Homomorphism of b₁,(product <*b₁*>) st ( for b₃ being Element of b₁ holds b₂ . b₃ = <*b₃*> ) holds
b₂ is_isomorphism

proof end;

theorem Th42: :: GROUP_7:42

for b₁ being Group holds b₁, product <*b₁*> are_isomorphic

proof end;