:: GROUP_6 semantic presentation

theorem Th1: :: GROUP_6:1

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂ holds
( b₃ is one-to-one iff for b₄, b₅ being Element of b₁ st b₃ . b₄ = b₃ . b₅ holds
b₄ = b₅ )

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
redefine mode Subgroup as Subgroup of c₂ -> Subgroup of a₁;
coherence by GROUP_2:65;

end;

registration

let c₁ be Group;
cluster (1). a₁ -> normal ;
coherence by GROUP_3:137;
cluster (Omega). a₁ -> normal ;
coherence by GROUP_3:137;

end;

theorem Th2: :: GROUP_6:2

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being Element of b₁
for b₄ being Subgroup of b₂
for b₅ being Element of b₂ st b₅ = b₃ holds
( b₅ * b₄ = b₃ * b₄ & b₄ * b₅ = b₄ * b₃ )

proof end;

theorem Th3: :: GROUP_6:3

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃, b₄ being Subgroup of b₂ holds b₃ /\ b₄ = b₃ /\ b₄

proof end;

theorem Th4: :: GROUP_6:4

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

proof end;

theorem Th5: :: GROUP_6:5

canceled;

theorem Th6: :: GROUP_6:6

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being Element of b₁ holds
( (b₃ * b₂) * b₂ = b₃ * b₂ & b₃ * (b₂ * b₂) = b₃ * b₂ & (b₂ * b₂) * b₃ = b₂ * b₃ & b₂ * (b₂ * b₃) = b₂ * b₃ )

proof end;

theorem Th7: :: GROUP_6:7

for b₁ being Group
for b₂ being Subset of b₁ st b₂ = { [.b₃,b₄.] where B is Element of b₁, B is Element of b₁ : verum } holds
b₁ ` = gr b₂

proof end;

theorem Th8: :: GROUP_6:8

for b₁ being strict Group
for b₂ being strict Subgroup of b₁ holds
( b₁ ` is Subgroup of b₂ iff for b₃, b₄ being Element of b₁ holds [.b₃,b₄.] in b₂ )

proof end;

theorem Th9: :: GROUP_6:9

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being normal Subgroup of b₁ st b₃ is Subgroup of b₂ holds
b₃ is normal Subgroup of b₂

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
let c₃ be normal Subgroup of c₁;
assume E8: HGrStr(# the carrier of c₃,the mult of c₃ #) is Subgroup of c₂ ;
func c₂,c₃ `*` -> strict normal Subgroup of a₂ equals :Def1: :: GROUP_6:def 1
HGrStr(# the carrier of a₃,the mult of a₃ #);
coherence

proof end;

correctness ;

end;

:: deftheorem Def1 defines `*` GROUP_6:def 1 :

theorem Th10: :: GROUP_6:10

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being normal Subgroup of b₁ holds
( b₂ /\ b₃ is normal Subgroup of b₂ & b₃ /\ b₂ is normal Subgroup of b₂ )

proof end;

definition

let c₁ be Group;
let c₂ be Subgroup of c₁;
let c₃ be normal Subgroup of c₁;
redefine func /\ as c₂ /\ c₃ -> strict normal Subgroup of a₂;
coherence by Th10;

end;

definition

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
let c₃ be Subgroup of c₁;
redefine func /\ as c₂ /\ c₃ -> strict normal Subgroup of a₃;
coherence by Th10;

end;

definition

let c₁ be non empty 1-sorted ;
redefine attr a₁ is trivial means :Def2: :: GROUP_6:def 2
ex b₁ being set st the carrier of a₁ = {b₁};
compatibility

proof end;

end;

:: deftheorem Def2 defines trivial GROUP_6:def 2 :

registration

cluster trivial HGrStr ;
existence

proof end;

end;

theorem Th11: :: GROUP_6:11

for b₁ being Group holds (1). b₁ is trivial

proof end;

theorem Th12: :: GROUP_6:12

for b₁ being Group holds
( b₁ is trivial iff ( ord b₁ = 1 & b₁ is finite ) )

proof end;

theorem Th13: :: GROUP_6:13

for b₁ being strict Group st b₁ is trivial holds
(1). b₁ = b₁

proof end;

definition

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
func Cosets c₂ -> set equals :: GROUP_6:def 3
Left_Cosets a₂;
coherence ;

end;

:: deftheorem Def3 defines Cosets GROUP_6:def 3 :

registration

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
cluster Cosets a₂ -> non empty ;
coherence by GROUP_2:165;

end;

theorem Th14: :: GROUP_6:14

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds
( Cosets b₂ = Left_Cosets b₂ & Cosets b₂ = Right_Cosets b₂ ) by GROUP_3:150;

theorem Th15: :: GROUP_6:15

for b₁ being Group
for b₂ being set
for b₃ being normal Subgroup of b₁ st b₂ in Cosets b₃ holds
ex b₄ being Element of b₁ st
( b₂ = b₄ * b₃ & b₂ = b₃ * b₄ )

proof end;

theorem Th16: :: GROUP_6:16

for b₁ being Group
for b₂ being Element of b₁
for b₃ being normal Subgroup of b₁ holds
( b₂ * b₃ in Cosets b₃ & b₃ * b₂ in Cosets b₃ )

proof end;

theorem Th17: :: GROUP_6:17

for b₁ being Group
for b₂ being set
for b₃ being normal Subgroup of b₁ st b₂ in Cosets b₃ holds
b₂ is Subset of b₁ ;

theorem Th18: :: GROUP_6:18

for b₁ being Group
for b₂, b₃ being Subset of b₁
for b₄ being normal Subgroup of b₁ st b₂ in Cosets b₄ & b₃ in Cosets b₄ holds
b₂ * b₃ in Cosets b₄

proof end;

definition

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
func CosOp c₂ -> BinOp of Cosets a₂ means :Def4: :: GROUP_6:def 4
for b₁, b₂ being Element of Cosets a₂
for b₃, b₄ being Subset of a₁ st b₁ = b₃ & b₂ = b₄ holds
a₃ . b₁,b₂ = b₃ * b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines CosOp GROUP_6:def 4 :

definition

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
func c₁ ./. c₂ -> HGrStr equals :: GROUP_6:def 5
HGrStr(# (Cosets a₂),(CosOp a₂) #);
correctness ;

end;

:: deftheorem Def5 defines ./. GROUP_6:def 5 :

registration

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
cluster a₁ ./. a₂ -> non empty strict ;
coherence ;

end;

theorem Th19: :: GROUP_6:19

canceled;

theorem Th20: :: GROUP_6:20

canceled;

theorem Th21: :: GROUP_6:21

canceled;

theorem Th22: :: GROUP_6:22

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds the carrier of (b₁ ./. b₂) = Cosets b₂ ;

theorem Th23: :: GROUP_6:23

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds the mult of (b₁ ./. b₂) = CosOp b₂ ;

definition

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
let c₃ be Element of (c₁ ./. c₂);
func @ c₃ -> Subset of a₁ equals :: GROUP_6:def 6
a₃;
coherence by Th17;

end;

:: deftheorem Def6 defines @ GROUP_6:def 6 :

theorem Th24: :: GROUP_6:24

for b₁ being Group
for b₂ being normal Subgroup of b₁
for b₃, b₄ being Element of (b₁ ./. b₂) holds (@ b₃) * (@ b₄) = b₃ * b₄ by Def4;

theorem Th25: :: GROUP_6:25

for b₁ being Group
for b₂ being normal Subgroup of b₁
for b₃, b₄ being Element of (b₁ ./. b₂) holds @ (b₃ * b₄) = (@ b₃) * (@ b₄) by Th24;

registration

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
cluster a₁ ./. a₂ -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem Th26: :: GROUP_6:26

for b₁ being Group
for b₂ being normal Subgroup of b₁
for b₃ being Element of (b₁ ./. b₂) ex b₄ being Element of b₁ st
( b₃ = b₄ * b₂ & b₃ = b₂ * b₄ ) by Th15;

theorem Th27: :: GROUP_6:27

for b₁ being Group
for b₂ being Element of b₁
for b₃ being normal Subgroup of b₁ holds
( b₃ * b₂ is Element of (b₁ ./. b₃) & b₂ * b₃ is Element of (b₁ ./. b₃) & carr b₃ is Element of (b₁ ./. b₃) ) by Th16, GROUP_2:165;

theorem Th28: :: GROUP_6:28

for b₁ being Group
for b₂ being set
for b₃ being normal Subgroup of b₁ holds
( b₂ in b₁ ./. b₃ iff ex b₄ being Element of b₁ st
( b₂ = b₄ * b₃ & b₂ = b₃ * b₄ ) )

proof end;

theorem Th29: :: GROUP_6:29

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds 1. (b₁ ./. b₂) = carr b₂

proof end;

theorem Th30: :: GROUP_6:30

for b₁ being Group
for b₂ being Element of b₁
for b₃ being normal Subgroup of b₁
for b₄ being Element of (b₁ ./. b₃) st b₄ = b₂ * b₃ holds
b₄ " = (b₂ " ) * b₃

proof end;

theorem Th31: :: GROUP_6:31

for b₁ being Group
for b₂ being normal Subgroup of b₁ st Left_Cosets b₂ is finite holds
b₁ ./. b₂ is finite by GROUP_1:def 14;

theorem Th32: :: GROUP_6:32

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds Ord (b₁ ./. b₂) = Index b₂ ;

theorem Th33: :: GROUP_6:33

for b₁ being Group
for b₂ being normal Subgroup of b₁ st Left_Cosets b₂ is finite holds
ord (b₁ ./. b₂) = index b₂

proof end;

theorem Th34: :: GROUP_6:34

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being strict normal Subgroup of b₁ st b₃ is Subgroup of b₂ holds
b₂ ./. (b₂,b₃ `*` ) is Subgroup of b₁ ./. b₃

proof end;

theorem Th35: :: GROUP_6:35

for b₁ being Group
for b₂, b₃ being strict normal Subgroup of b₁ st b₃ is Subgroup of b₂ holds
b₂ ./. (b₂,b₃ `*` ) is normal Subgroup of b₁ ./. b₃

proof end;

theorem Th36: :: GROUP_6:36

for b₁ being strict Group
for b₂ being strict normal Subgroup of b₁ holds
( b₁ ./. b₂ is commutative Group iff b₁ ` is Subgroup of b₂ )

proof end;

Lemma29: for b₁, b₂ being Group
for b₃, b₄ being Element of b₁
for b₅ being Function of the carrier of b₁,the carrier of b₂ st ( for b₆ being Element of b₁ holds b₅ . b₆ = 1. b₂ ) holds
b₅ . (b₃ * b₄) = (b₅ . b₃) * (b₅ . b₄)

proof end;

definition

let c₁, c₂ be non empty HGrStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is multiplicative means :Def7: :: GROUP_6:def 7
for b₁, b₂ being Element of a₁ holds a₃ . (b₁ * b₂) = (a₃ . b₁) * (a₃ . b₂);

end;

:: deftheorem Def7 defines multiplicative GROUP_6:def 7 :

registration

let c₁, c₂ be Group;
cluster multiplicative M4(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

definition

let c₁, c₂ be Group;
mode Homomorphism of a₁,a₂ is multiplicative Function of a₁,a₂;

end;

theorem Th37: :: GROUP_6:37

canceled;

theorem Th38: :: GROUP_6:38

canceled;

theorem Th39: :: GROUP_6:39

canceled;

theorem Th40: :: GROUP_6:40

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ holds b₃ . (1. b₁) = 1. b₂

proof end;

theorem Th41: :: GROUP_6:41

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

proof end;

theorem Th42: :: GROUP_6:42

for b₁, b₂ being Group
for b₃, b₄ being Element of b₁
for b₅ being Homomorphism of b₁,b₂ holds b₅ . (b₃ |^ b₄) = (b₅ . b₃) |^ (b₅ . b₄)

proof end;

theorem Th43: :: GROUP_6:43

for b₁, b₂ being Group
for b₃, b₄ being Element of b₁
for b₅ being Homomorphism of b₁,b₂ holds b₅ . [.b₃,b₄.] = [.(b₅ . b₃),(b₅ . b₄).]

proof end;

theorem Th44: :: GROUP_6:44

for b₁, b₂ being Group
for b₃, b₄, b₅ being Element of b₁
for b₆ being Homomorphism of b₁,b₂ holds b₆ . [.b₃,b₄,b₅.] = [.(b₆ . b₃),(b₆ . b₄),(b₆ . b₅).]

proof end;

theorem Th45: :: GROUP_6:45

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

proof end;

theorem Th46: :: GROUP_6:46

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

proof end;

theorem Th47: :: GROUP_6:47

for b₁ being Group holds id the carrier of b₁ is Homomorphism of b₁,b₁

proof end;

theorem Th48: :: GROUP_6:48

for b₁, b₂, b₃ being Group
for b₄ being Homomorphism of b₂,b₁
for b₅ being Homomorphism of b₁,b₃ holds b₅ * b₄ is Homomorphism of b₂,b₃

proof end;

definition

let c₁, c₂, c₃ be Group;
let c₄ be Homomorphism of c₁,c₂;
let c₅ be Homomorphism of c₂,c₃;
redefine func * as c₅ * c₄ -> Homomorphism of a₁,a₃;
coherence by Th48;

end;

definition

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
redefine func rng as rng c₃ -> Subset of a₂;
coherence by RELSET_1:12;

end;

definition

let c₁, c₂ be Group;
func 1: c₁,c₂ -> Homomorphism of a₁,a₂ means :Def8: :: GROUP_6:def 8
for b₁ being Element of a₁ holds a₃ . b₁ = 1. a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines 1: GROUP_6:def 8 :

theorem Th49: :: GROUP_6:49

for b₁, b₂, b₃ being Group
for b₄ being Homomorphism of b₁,b₂
for b₅ being Homomorphism of b₂,b₃ holds
( b₅ * (1: b₁,b₂) = 1: b₁,b₃ & (1: b₂,b₃) * b₄ = 1: b₁,b₃ )

proof end;

definition

let c₁ be Group;
let c₂ be normal Subgroup of c₁;
func nat_hom c₂ -> Homomorphism of a₁,(a₁ ./. a₂) means :Def9: :: GROUP_6:def 9
for b₁ being Element of a₁ holds a₃ . b₁ = b₁ * a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines nat_hom GROUP_6:def 9 :

definition

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
func Ker c₃ -> strict Subgroup of a₁ means :Def10: :: GROUP_6:def 10
the carrier of a₄ = { b₁ where B is Element of a₁ : a₃ . b₁ = 1. a₂ } ;
existence

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def10 defines Ker GROUP_6:def 10 :

registration

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
cluster Ker a₃ -> strict normal ;
coherence

proof end;

end;

theorem Th50: :: GROUP_6:50

for b₁, b₂ being Group
for b₃ being Element of b₁
for b₄ being Homomorphism of b₁,b₂ holds
( b₃ in Ker b₄ iff b₄ . b₃ = 1. b₂ )

proof end;

theorem Th51: :: GROUP_6:51

for b₁, b₂ being strict Group holds Ker (1: b₁,b₂) = b₁

proof end;

theorem Th52: :: GROUP_6:52

for b₁ being Group
for b₂ being strict normal Subgroup of b₁ holds Ker (nat_hom b₂) = b₂

proof end;

definition

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
func Image c₃ -> strict Subgroup of a₂ means :Def11: :: GROUP_6:def 11
the carrier of a₄ = a₃ .: the carrier of a₁;
existence

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def11 defines Image GROUP_6:def 11 :

theorem Th53: :: GROUP_6:53

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ holds rng b₃ = the carrier of (Image b₃)

proof end;

theorem Th54: :: GROUP_6:54

for b₁, b₂ being Group
for b₃ being set
for b₄ being Homomorphism of b₂,b₁ holds
( b₃ in Image b₄ iff ex b₅ being Element of b₂ st b₃ = b₄ . b₅ )

proof end;

theorem Th55: :: GROUP_6:55

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ holds Image b₃ = gr (rng b₃)

proof end;

theorem Th56: :: GROUP_6:56

for b₁, b₂ being Group holds Image (1: b₁,b₂) = (1). b₂

proof end;

theorem Th57: :: GROUP_6:57

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds Image (nat_hom b₂) = b₁ ./. b₂

proof end;

theorem Th58: :: GROUP_6:58

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ holds b₃ is Homomorphism of b₂,(Image b₃)

proof end;

theorem Th59: :: GROUP_6:59

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ st b₂ is finite holds
Image b₃ is finite

proof end;

Lemma49: for b₁ being commutative Group
for b₂, b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂
;

theorem Th60: :: GROUP_6:60

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ st b₂ is commutative Group holds
Image b₃ is commutative

proof end;

theorem Th61: :: GROUP_6:61

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ holds Ord (Image b₃) <=` Ord b₂

proof end;

theorem Th62: :: GROUP_6:62

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ st b₂ is finite holds
ord (Image b₃) <= ord b₂

proof end;

definition

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
attr a₃ is being_monomorphism means :Def12: :: GROUP_6:def 12
a₃ is one-to-one;
attr a₃ is being_epimorphism means :Def13: :: GROUP_6:def 13
rng a₃ = the carrier of a₂;

end;

:: deftheorem Def12 defines being_monomorphism GROUP_6:def 12 :

:: deftheorem Def13 defines being_epimorphism GROUP_6:def 13 :

notation

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
synonym c₃ is_monomorphism for being_monomorphism c₃;
synonym c₃ is_epimorphism for being_epimorphism c₃;

end;

theorem Th63: :: GROUP_6:63

for b₁, b₂ being Group
for b₃ being Element of b₂
for b₄ being Homomorphism of b₁,b₂ st b₄ is_monomorphism & b₃ in Image b₄ holds
b₄ . ((b₄ " ) . b₃) = b₃

proof end;

theorem Th64: :: GROUP_6:64

for b₁, b₂ being Group
for b₃ being Element of b₁
for b₄ being Homomorphism of b₁,b₂ st b₄ is_monomorphism holds
(b₄ " ) . (b₄ . b₃) = b₃

proof end;

theorem Th65: :: GROUP_6:65

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ st b₃ is_monomorphism holds
b₃ " is Homomorphism of (Image b₃),b₂

proof end;

theorem Th66: :: GROUP_6:66

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ holds
( b₃ is_monomorphism iff Ker b₃ = (1). b₂ )

proof end;

theorem Th67: :: GROUP_6:67

for b₁ being Group
for b₂ being strict Group
for b₃ being Homomorphism of b₁,b₂ holds
( b₃ is_epimorphism iff Image b₃ = b₂ )

proof end;

theorem Th68: :: GROUP_6:68

for b₁ being Group
for b₂ being strict Group
for b₃ being Homomorphism of b₁,b₂ st b₃ is_epimorphism holds
for b₄ being Element of b₂ ex b₅ being Element of b₁ st b₃ . b₅ = b₄

proof end;

theorem Th69: :: GROUP_6:69

for b₁ being Group
for b₂ being normal Subgroup of b₁ holds nat_hom b₂ is_epimorphism

proof end;

definition

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
attr a₃ is being_isomorphism means :Def14: :: GROUP_6:def 14
( a₃ is_epimorphism & a₃ is_monomorphism );

end;

:: deftheorem Def14 defines being_isomorphism GROUP_6:def 14 :

notation

let c₁, c₂ be Group;
let c₃ be Homomorphism of c₁,c₂;
synonym c₃ is_isomorphism for being_isomorphism c₃;

end;

theorem Th70: :: GROUP_6:70

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ holds
( b₃ is_isomorphism iff ( rng b₃ = the carrier of b₂ & b₃ is one-to-one ) )

proof end;

theorem Th71: :: GROUP_6:71

for b₁, b₂ being Group
for b₃ being Homomorphism of b₁,b₂ st b₃ is_isomorphism holds
( dom b₃ = the carrier of b₁ & rng b₃ = the carrier of b₂ )

proof end;

theorem Th72: :: GROUP_6:72

for b₁ being Group
for b₂ being strict Group
for b₃ being Homomorphism of b₁,b₂ st b₃ is_isomorphism holds
b₃ " is Homomorphism of b₂,b₁

proof end;

theorem Th73: :: GROUP_6:73

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁
for b₄ being Homomorphism of b₁,b₂ st b₃ is_isomorphism & b₄ = b₃ " holds
b₄ is_isomorphism

proof end;

theorem Th74: :: GROUP_6:74

for b₁, b₂, b₃ being Group
for b₄ being Homomorphism of b₁,b₂
for b₅ being Homomorphism of b₂,b₃ st b₄ is_isomorphism & b₅ is_isomorphism holds
b₅ * b₄ is_isomorphism

proof end;

theorem Th75: :: GROUP_6:75

for b₁ being Group holds nat_hom ((1). b₁) is_isomorphism

proof end;

definition

let c₁, c₂ be Group;
pred c₁,c₂ are_isomorphic means :Def15: :: GROUP_6:def 15
ex b₁ being Homomorphism of a₁,a₂ st b₁ is_isomorphism ;
reflexivity

proof end;

end;

:: deftheorem Def15 defines are_isomorphic GROUP_6:def 15 :

theorem Th76: :: GROUP_6:76

canceled;

theorem Th77: :: GROUP_6:77

for b₁, b₂ being strict Group st b₁,b₂ are_isomorphic holds
b₂,b₁ are_isomorphic

proof end;

definition

let c₁, c₂ be strict Group;
redefine pred are_isomorphic as c₁,c₂ are_isomorphic ;
symmetry by Th77;

end;

theorem Th78: :: GROUP_6:78

for b₁, b₂, b₃ being Group st b₁,b₂ are_isomorphic & b₂,b₃ are_isomorphic holds
b₁,b₃ are_isomorphic

proof end;

theorem Th79: :: GROUP_6:79

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ st b₃ is_monomorphism holds
b₂, Image b₃ are_isomorphic

proof end;

theorem Th80: :: GROUP_6:80

for b₁, b₂ being strict Group st b₁ is trivial & b₂ is trivial holds
b₁,b₂ are_isomorphic

proof end;

theorem Th81: :: GROUP_6:81

for b₁, b₂ being Group holds (1). b₁, (1). b₂ are_isomorphic

proof end;

theorem Th82: :: GROUP_6:82

for b₁ being strict Group holds b₁,b₁ ./. ((1). b₁) are_isomorphic

proof end;

theorem Th83: :: GROUP_6:83

for b₁ being Group holds b₁ ./. ((Omega). b₁) is trivial

proof end;

theorem Th84: :: GROUP_6:84

for b₁, b₂ being strict Group st b₁,b₂ are_isomorphic holds
Ord b₁ = Ord b₂

proof end;

theorem Th85: :: GROUP_6:85

for b₁, b₂ being Group st b₁,b₂ are_isomorphic & b₁ is finite holds
b₂ is finite

proof end;

theorem Th86: :: GROUP_6:86

for b₁, b₂ being strict Group st b₁,b₂ are_isomorphic & b₁ is finite holds
ord b₁ = ord b₂

proof end;

theorem Th87: :: GROUP_6:87

for b₁, b₂ being strict Group st b₁,b₂ are_isomorphic & b₁ is trivial holds
b₂ is trivial

proof end;

theorem Th88: :: GROUP_6:88

canceled;

theorem Th89: :: GROUP_6:89

for b₁ being Group
for b₂ being strict Group st b₁,b₂ are_isomorphic & b₁ is commutative Group holds
b₂ is commutative Group

proof end;

Lemma71: for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ holds
( b₂ ./. (Ker b₃), Image b₃ are_isomorphic & ex b₄ being Homomorphism of (b₂ ./. (Ker b₃)),(Image b₃) st
( b₄ is_isomorphism & b₃ = b₄ * (nat_hom (Ker b₃)) ) )

proof end;

theorem Th90: :: GROUP_6:90

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ holds b₂ ./. (Ker b₃), Image b₃ are_isomorphic by Lemma71;

theorem Th91: :: GROUP_6:91

for b₁, b₂ being Group
for b₃ being Homomorphism of b₂,b₁ ex b₄ being Homomorphism of (b₂ ./. (Ker b₃)),(Image b₃) st
( b₄ is_isomorphism & b₃ = b₄ * (nat_hom (Ker b₃)) ) by Lemma71;

theorem Th92: :: GROUP_6:92

for b₁ being Group
for b₂ being normal Subgroup of b₁
for b₃ being strict normal Subgroup of b₁
for b₄ being strict normal Subgroup of b₁ ./. b₃ st b₄ = b₂ ./. (b₂,b₃ `*` ) & b₃ is Subgroup of b₂ holds
(b₁ ./. b₃) ./. b₄,b₁ ./. b₂ are_isomorphic

proof end;

theorem Th93: :: GROUP_6:93

for b₁ being Group
for b₂ being Subgroup of b₁
for b₃ being strict normal Subgroup of b₁ holds (b₂ "\/" b₃) ./. ((b₂ "\/" b₃),b₃ `*` ),b₂ ./. (b₂ /\ b₃) are_isomorphic

proof end;