:: Homomorphisms and Isomorphisms of Groups. Quotient Group
:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec
::
:: Received October 3, 1991
:: Copyright (c) 1991-2011 Association of Mizar Users

begin

theorem Th1: :: GROUP_6:1

for A, B being non empty set
for f being Function of A,B holds
( f is one-to-one iff for a, b being Element of A st f . a = f . b holds
a = b )

proof end;

definition

let G be Group;
let A be Subgroup of G;
:: original: Subgroup
redefine mode Subgroup of A -> Subgroup of G;
coherence
for b₁ being Subgroup of A holds b₁ is Subgroup of G by GROUP_2:65;

end;

registration

let G be Group;
cluster (1). G -> normal ;
coherence
(1). G is normal by GROUP_3:137;
cluster (Omega). G -> normal ;
coherence
(Omega). G is normal by GROUP_3:137;

end;

theorem Th2: :: GROUP_6:2

for G being Group
for A being Subgroup of G
for a being Element of G
for X being Subgroup of A
for x being Element of A st x = a holds
( x * X = a * X & X * x = X * a )

proof end;

theorem :: GROUP_6:3

for G being Group
for A being Subgroup of G
for X, Y being Subgroup of A holds X /\ Y = X /\ Y

proof end;

theorem Th4: :: GROUP_6:4

for G being Group
for a, b being Element of G holds
( (a * b) * (a ") = b |^ (a ") & a * (b * (a ")) = b |^ (a ") )

proof end;

theorem :: GROUP_6:5

canceled;

theorem Th6: :: GROUP_6:6

for G being Group
for A being Subgroup of G
for a being Element of G holds
( (a * A) * A = a * A & a * (A * A) = a * A & (A * A) * a = A * a & A * (A * a) = A * a )

proof end;

theorem Th7: :: GROUP_6:7

for G being Group
for A1 being Subset of G st A1 = { [.a,b.] where a, b is Element of G : verum } holds
G ` = gr A1

proof end;

theorem Th8: :: GROUP_6:8

for G being strict Group
for B being strict Subgroup of G holds
( G ` is Subgroup of B iff for a, b being Element of G holds [.a,b.] in B )

proof end;

theorem Th9: :: GROUP_6:9

for G being Group
for B being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of B holds
N is normal Subgroup of B

proof end;

definition

let G be Group;
let B be Subgroup of G;
let M be normal Subgroup of G;
assume A1: multMagma(# the carrier of M, the multF of M #) is Subgroup of B ;
func (B,M) `*` -> strict normal Subgroup of B equals :Def1: :: GROUP_6:def 1
multMagma(# the carrier of M, the multF of M #);
coherence
multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B

proof end;

correctness
;

end;

:: deftheorem Def1 defines `*` GROUP_6:def 1 :
for G being Group
for B being Subgroup of G
for M being normal Subgroup of G st multMagma(# the carrier of M, the multF of M #) is Subgroup of B holds
(B,M) `*` = multMagma(# the carrier of M, the multF of M #);

theorem Th10: :: GROUP_6:10

for G being Group
for B being Subgroup of G
for N being normal Subgroup of G holds
( B /\ N is normal Subgroup of B & N /\ B is normal Subgroup of B )

proof end;

definition

let G be Group;
let B be Subgroup of G;
let N be normal Subgroup of G;
:: original: /\
redefine func B /\ N -> strict normal Subgroup of B;
coherence
B /\ N is strict normal Subgroup of B by Th10;

end;

definition

let G be Group;
let N be normal Subgroup of G;
let B be Subgroup of G;
:: original: /\
redefine func N /\ B -> strict normal Subgroup of B;
coherence
N /\ B is strict normal Subgroup of B by Th10;

end;

definition

let G be non empty 1-sorted ;
redefine attr G is trivial means :Def2: :: GROUP_6:def 2
ex x being set st the carrier of G = {x};
compatibility
( G is trivial iff ex x being set st the carrier of G = {x} )

proof end;

end;

:: deftheorem Def2 defines trivial GROUP_6:def 2 :
for G being non empty 1-sorted holds
( G is trivial iff ex x being set st the carrier of G = {x} );

theorem Th11: :: GROUP_6:11

for G being Group holds (1). G is trivial

proof end;

registration

let G be Group;
cluster (1). G -> trivial ;
coherence
(1). G is trivial by Th11;

end;

registration

cluster non empty trivial strict unital Group-like associative multMagma ;
existence
ex b₁ being Group st
( b₁ is strict & b₁ is trivial )

proof end;

end;

theorem Th12: :: GROUP_6:12

( ( for G being trivial Group holds
( card G = 1 & G is finite ) ) & ( for G being finite Group st card G = 1 holds
G is trivial ) )

proof end;

theorem Th13: :: GROUP_6:13

for G being trivial strict Group holds (1). G = G

proof end;

notation

let G be Group;
let N be normal Subgroup of G;
synonym Cosets N for Left_Cosets N;

end;

registration

let G be Group;
let N be normal Subgroup of G;
cluster Cosets N -> non empty ;
coherence
not Cosets N is empty by GROUP_2:165;

end;

theorem :: GROUP_6:14

canceled;

theorem Th15: :: GROUP_6:15

for G being Group
for x being set
for N being normal Subgroup of G st x in Cosets N holds
ex a being Element of G st
( x = a * N & x = N * a )

proof end;

theorem Th16: :: GROUP_6:16

for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( a * N in Cosets N & N * a in Cosets N )

proof end;

theorem Th17: :: GROUP_6:17

for G being Group
for x being set
for N being normal Subgroup of G st x in Cosets N holds
x is Subset of G ;

theorem Th18: :: GROUP_6:18

for G being Group
for A1, A2 being Subset of G
for N being normal Subgroup of G st A1 in Cosets N & A2 in Cosets N holds
A1 * A2 in Cosets N

proof end;

definition

canceled;
let G be Group;
let N be normal Subgroup of G;
func CosOp N -> BinOp of (Cosets N) means :Def4: :: GROUP_6:def 4
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
it . (W1,W2) = A1 * A2;
existence
ex b₁ being BinOp of (Cosets N) st
for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b₁ . (W1,W2) = A1 * A2

proof end;

uniqueness
for b₁, b₂ being BinOp of (Cosets N) st ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b₁ . (W1,W2) = A1 * A2 ) & ( for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b₂ . (W1,W2) = A1 * A2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem GROUP_6:def 3 :
canceled;

:: deftheorem Def4 defines CosOp GROUP_6:def 4 :
for G being Group
for N being normal Subgroup of G
for b₃ being BinOp of (Cosets N) holds
( b₃ = CosOp N iff for W1, W2 being Element of Cosets N
for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds
b₃ . (W1,W2) = A1 * A2 );

definition

let G be Group;
let N be normal Subgroup of G;
func G ./. N -> multMagma equals :: GROUP_6:def 5
multMagma(# (Cosets N),(CosOp N) #);
correctness
coherence
multMagma(# (Cosets N),(CosOp N) #) is multMagma ;
;

end;

:: deftheorem defines ./. GROUP_6:def 5 :
for G being Group
for N being normal Subgroup of G holds G ./. N = multMagma(# (Cosets N),(CosOp N) #);

registration

let G be Group;
let N be normal Subgroup of G;
cluster G ./. N -> non empty strict ;
coherence
( G ./. N is strict & not G ./. N is empty ) ;

end;

theorem :: GROUP_6:19

canceled;

theorem :: GROUP_6:20

canceled;

theorem :: GROUP_6:21

canceled;

theorem :: GROUP_6:22

for G being Group
for N being normal Subgroup of G holds the carrier of (G ./. N) = Cosets N ;

theorem :: GROUP_6:23

for G being Group
for N being normal Subgroup of G holds the multF of (G ./. N) = CosOp N ;

definition

let G be Group;
let N be normal Subgroup of G;
let S be Element of (G ./. N);
func @ S -> Subset of G equals :: GROUP_6:def 6
S;
coherence
S is Subset of G by Th17;

end;

:: deftheorem defines @ GROUP_6:def 6 :
for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) holds @ S = S;

theorem :: GROUP_6:24

for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds (@ T1) * (@ T2) = T1 * T2 by Def4;

theorem :: GROUP_6:25

for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds @ (T1 * T2) = (@ T1) * (@ T2) by Def4;

registration

let G be Group;
let N be normal Subgroup of G;
cluster G ./. N -> Group-like associative ;
coherence
( G ./. N is associative & G ./. N is Group-like )

proof end;

end;

theorem :: GROUP_6:26

for G being Group
for N being normal Subgroup of G
for S being Element of (G ./. N) ex a being Element of G st
( S = a * N & S = N * a ) by Th15;

theorem :: GROUP_6:27

for G being Group
for a being Element of G
for N being normal Subgroup of G holds
( N * a is Element of (G ./. N) & a * N is Element of (G ./. N) & carr N is Element of (G ./. N) ) by Th16, GROUP_2:165;

theorem Th28: :: GROUP_6:28

for G being Group
for x being set
for N being normal Subgroup of G holds
( x in G ./. N iff ex a being Element of G st
( x = a * N & x = N * a ) )

proof end;

theorem Th29: :: GROUP_6:29

for G being Group
for N being normal Subgroup of G holds 1_ (G ./. N) = carr N

proof end;

theorem Th30: :: GROUP_6:30

for G being Group
for a being Element of G
for N being normal Subgroup of G
for S being Element of (G ./. N) st S = a * N holds
S " = (a ") * N

proof end;

theorem :: GROUP_6:31

canceled;

theorem :: GROUP_6:32

for G being Group
for N being normal Subgroup of G holds card (G ./. N) = Index N ;

theorem :: GROUP_6:33

for G being Group
for N being normal Subgroup of G st Left_Cosets N is finite holds
card (G ./. N) = index N

proof end;

theorem Th34: :: GROUP_6:34

for G being Group
for B being Subgroup of G
for M being strict normal Subgroup of G st M is Subgroup of B holds
B ./. ((B,M) `*`) is Subgroup of G ./. M

proof end;

theorem :: GROUP_6:35

for G being Group
for N, M being strict normal Subgroup of G st M is Subgroup of N holds
N ./. ((N,M) `*`) is normal Subgroup of G ./. M

proof end;

theorem :: GROUP_6:36

for G being strict Group
for N being strict normal Subgroup of G holds
( G ./. N is commutative Group iff G ` is Subgroup of N )

proof end;

Lm1: for G, H being Group
for a, b being Element of G
for f being Function of the carrier of G, the carrier of H st ( for a being Element of G holds f . a = 1_ H ) holds
f . (a * b) = (f . a) * (f . b)

proof end;

definition

let G, H be non empty multMagma ;
let f be Function of G,H;
attr f is multiplicative means :Def7: :: GROUP_6:def 7
for a, b being Element of G holds f . (a * b) = (f . a) * (f . b);

end;

:: deftheorem Def7 defines multiplicative GROUP_6:def 7 :
for G, H being non empty multMagma
for f being Function of G,H holds
( f is multiplicative iff for a, b being Element of G holds f . (a * b) = (f . a) * (f . b) );

registration

let G, H be Group;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty V22( the carrier of G) quasi_total multiplicative Element of bool [: the carrier of G, the carrier of H:];
existence
ex b₁ being Function of G,H st b₁ is multiplicative

proof end;

end;

definition

let G, H be Group;
mode Homomorphism of G,H is multiplicative Function of G,H;

end;

theorem :: GROUP_6:37

canceled;

theorem :: GROUP_6:38

canceled;

theorem :: GROUP_6:39

canceled;

theorem Th40: :: GROUP_6:40

for G, H being Group
for g being Homomorphism of G,H holds g . (1_ G) = 1_ H

proof end;

registration

let G, H be Group;
cluster Function-like quasi_total multiplicative -> unity-preserving Element of bool [: the carrier of G, the carrier of H:];
coherence
for b₁ being Homomorphism of G,H holds b₁ is unity-preserving

proof end;

end;

theorem Th41: :: GROUP_6:41

for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a ") = (g . a) "

proof end;

theorem Th42: :: GROUP_6:42

for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . (a |^ b) = (g . a) |^ (g . b)

proof end;

theorem Th43: :: GROUP_6:43

for G, H being Group
for a, b being Element of G
for g being Homomorphism of G,H holds g . [.a,b.] = [.(g . a),(g . b).]

proof end;

theorem :: GROUP_6:44

for G, H being Group
for a1, a2, a3 being Element of G
for g being Homomorphism of G,H holds g . [.a1,a2,a3.] = [.(g . a1),(g . a2),(g . a3).]

proof end;

theorem Th45: :: GROUP_6:45

for n being Element of NAT
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n

proof end;

theorem :: GROUP_6:46

for i being Integer
for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i

proof end;

theorem Th47: :: GROUP_6:47

for G being Group holds id the carrier of G is Homomorphism of G,G

proof end;

theorem Th48: :: GROUP_6:48

for H, G, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I

proof end;

definition

let G, H, I be Group;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
:: original: *
redefine func h1 * h -> Homomorphism of G,I;
coherence
h * h1 is Homomorphism of G,I by Th48;

end;

definition

let G, H be Group;
func 1: (G,H) -> Homomorphism of G,H means :Def8: :: GROUP_6:def 8
for a being Element of G holds it . a = 1_ H;
existence
ex b₁ being Homomorphism of G,H st
for a being Element of G holds b₁ . a = 1_ H

proof end;

uniqueness
for b₁, b₂ being Homomorphism of G,H st ( for a being Element of G holds b₁ . a = 1_ H ) & ( for a being Element of G holds b₂ . a = 1_ H ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines 1: GROUP_6:def 8 :
for G, H being Group
for b₃ being Homomorphism of G,H holds
( b₃ = 1: (G,H) iff for a being Element of G holds b₃ . a = 1_ H );

theorem :: GROUP_6:49

for G, H, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I holds
( h1 * (1: (G,H)) = 1: (G,I) & (1: (H,I)) * h = 1: (G,I) )

proof end;

definition

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

proof end;

uniqueness
for b₁, b₂ being Homomorphism of G,(G ./. N) st ( for a being Element of G holds b₁ . a = a * N ) & ( for a being Element of G holds b₂ . a = a * N ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines nat_hom GROUP_6:def 9 :
for G being Group
for N being normal Subgroup of G
for b₃ being Homomorphism of G,(G ./. N) holds
( b₃ = nat_hom N iff for a being Element of G holds b₃ . a = a * N );

definition

let G, H be Group;
let g be Homomorphism of G,H;
func Ker g -> strict Subgroup of G means :Def10: :: GROUP_6:def 10
the carrier of it = { a where a is Element of G : g . a = 1_ H } ;
existence
ex b₁ being strict Subgroup of G st the carrier of b₁ = { a where a is Element of G : g . a = 1_ H }

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = { a where a is Element of G : g . a = 1_ H } & the carrier of b₂ = { a where a is Element of G : g . a = 1_ H } holds
b₁ = b₂ by GROUP_2:68;

end;

:: deftheorem Def10 defines Ker GROUP_6:def 10 :
for G, H being Group
for g being Homomorphism of G,H
for b₄ being strict Subgroup of G holds
( b₄ = Ker g iff the carrier of b₄ = { a where a is Element of G : g . a = 1_ H } );

registration

let G, H be Group;
let g be Homomorphism of G,H;
cluster Ker g -> strict normal ;
coherence
Ker g is normal

proof end;

end;

theorem Th50: :: GROUP_6:50

for G, H being Group
for a being Element of G
for h being Homomorphism of G,H holds
( a in Ker h iff h . a = 1_ H )

proof end;

theorem :: GROUP_6:51

for G, H being strict Group holds Ker (1: (G,H)) = G

proof end;

theorem Th52: :: GROUP_6:52

for G being Group
for N being strict normal Subgroup of G holds Ker (nat_hom N) = N

proof end;

definition

let G, H be Group;
let g be Homomorphism of G,H;
func Image g -> strict Subgroup of H means :Def11: :: GROUP_6:def 11
the carrier of it = g .: the carrier of G;
existence
ex b₁ being strict Subgroup of H st the carrier of b₁ = g .: the carrier of G

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of H st the carrier of b₁ = g .: the carrier of G & the carrier of b₂ = g .: the carrier of G holds
b₁ = b₂ by GROUP_2:68;

end;

:: deftheorem Def11 defines Image GROUP_6:def 11 :
for G, H being Group
for g being Homomorphism of G,H
for b₄ being strict Subgroup of H holds
( b₄ = Image g iff the carrier of b₄ = g .: the carrier of G );

theorem Th53: :: GROUP_6:53

for G, H being Group
for g being Homomorphism of G,H holds rng g = the carrier of (Image g)

proof end;

theorem Th54: :: GROUP_6:54

for H, G being Group
for x being set
for g being Homomorphism of G,H holds
( x in Image g iff ex a being Element of G st x = g . a )

proof end;

theorem :: GROUP_6:55

for G, H being Group
for g being Homomorphism of G,H holds Image g = gr (rng g)

proof end;

theorem :: GROUP_6:56

for G, H being Group holds Image (1: (G,H)) = (1). H

proof end;

theorem Th57: :: GROUP_6:57

for G being Group
for N being normal Subgroup of G holds Image (nat_hom N) = G ./. N

proof end;

theorem Th58: :: GROUP_6:58

for H, G being Group
for h being Homomorphism of G,H holds h is Homomorphism of G,(Image h)

proof end;

theorem Th59: :: GROUP_6:59

for H, G being Group
for g being Homomorphism of G,H st G is finite holds
Image g is finite

proof end;

registration

let G be finite Group;
let H be Group;
let g be Homomorphism of G,H;
cluster Image g -> finite strict ;
coherence
Image g is finite by Th59;

end;

Lm2: for A being commutative Group
for a, b being Element of A holds a * b = b * a
;

theorem :: GROUP_6:60

for H, G being Group
for g being Homomorphism of G,H st G is commutative Group holds
Image g is commutative

proof end;

theorem Th61: :: GROUP_6:61

for H, G being Group
for g being Homomorphism of G,H holds card (Image g) c= card G

proof end;

theorem :: GROUP_6:62

for G being finite Group
for H being Group
for g being Homomorphism of G,H holds card (Image g) <= card G

proof end;

theorem :: GROUP_6:63

for G, H being Group
for c being Element of H
for h being Homomorphism of G,H st h is one-to-one & c in Image h holds
h . ((h ") . c) = c

proof end;

theorem :: GROUP_6:64

canceled;

theorem Th65: :: GROUP_6:65

for H, G being Group
for h being Homomorphism of G,H st h is one-to-one holds
h " is Homomorphism of (Image h),G

proof end;

theorem Th66: :: GROUP_6:66

for H, G being Group
for h being Homomorphism of G,H holds
( h is one-to-one iff Ker h = (1). G )

proof end;

theorem Th67: :: GROUP_6:67

for G being Group
for H being strict Group
for h being Homomorphism of G,H holds
( h is onto iff Image h = H )

proof end;

theorem Th68: :: GROUP_6:68

for G, H being non empty set
for h being Function of G,H st h is onto holds
for c being Element of H ex a being Element of G st h . a = c

proof end;

theorem Th69: :: GROUP_6:69

for G being Group
for N being normal Subgroup of G holds nat_hom N is onto

proof end;

theorem Th70: :: GROUP_6:70

for G, H being set
for h being Function of G,H holds
( h is bijective iff ( rng h = H & h is one-to-one ) )

proof end;

theorem :: GROUP_6:71

for G being set
for H being non empty set
for h being Function of G,H st h is bijective holds
( dom h = G & rng h = H ) by FUNCT_2:def 1, FUNCT_2:def 3;

theorem Th72: :: GROUP_6:72

for G being Group
for H being strict Group
for h being Homomorphism of G,H st h is bijective holds
h " is Homomorphism of H,G

proof end;

theorem Th73: :: GROUP_6:73

for G being set
for H being non empty set
for h being Function of G,H
for g1 being Function of H,G st h is bijective & g1 = h " holds
g1 is bijective

proof end;

theorem Th74: :: GROUP_6:74

for G being set
for H, I being non empty set
for h being Function of G,H
for h1 being Function of H,I st h is bijective & h1 is bijective holds
h1 * h is bijective

proof end;

theorem Th75: :: GROUP_6:75

for G being Group holds nat_hom ((1). G) is bijective

proof end;

definition

let G, H be Group;
canceled;
canceled;
canceled;
pred G,H are_isomorphic means :Def15: :: GROUP_6:def 15
ex h being Homomorphism of G,H st h is bijective ;
reflexivity
for G being Group ex h being Homomorphism of G,G st h is bijective

proof end;

end;

:: deftheorem GROUP_6:def 12 :
canceled;

:: deftheorem GROUP_6:def 13 :
canceled;

:: deftheorem GROUP_6:def 14 :
canceled;

:: deftheorem Def15 defines are_isomorphic GROUP_6:def 15 :
for G, H being Group holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

theorem :: GROUP_6:76

canceled;

theorem Th77: :: GROUP_6:77

for G, H being strict Group st G,H are_isomorphic holds
H,G are_isomorphic

proof end;

definition

let G, H be strict Group;
:: original: are_isomorphic
redefine pred G,H are_isomorphic ;
symmetry
for G, H being strict Group st G,H are_isomorphic holds
H,G are_isomorphic by Th77;

end;

theorem :: GROUP_6:78

for G, H, I being Group st G,H are_isomorphic & H,I are_isomorphic holds
G,I are_isomorphic

proof end;

theorem :: GROUP_6:79

for H, G being Group
for h being Homomorphism of G,H st h is one-to-one holds
G, Image h are_isomorphic

proof end;

theorem Th80: :: GROUP_6:80

for G, H being strict Group st G is trivial & H is trivial holds
G,H are_isomorphic

proof end;

theorem :: GROUP_6:81

for G, H being Group holds (1). G, (1). H are_isomorphic by Th80;

theorem :: GROUP_6:82

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

proof end;

theorem :: GROUP_6:83

for G being Group holds G ./. ((Omega). G) is trivial

proof end;

theorem Th84: :: GROUP_6:84

for G, H being strict Group st G,H are_isomorphic holds
card G = card H

proof end;

theorem Th85: :: GROUP_6:85

for G, H being Group st G,H are_isomorphic & G is finite holds
H is finite

proof end;

theorem :: GROUP_6:86

for G, H being strict Group st G,H are_isomorphic & G is finite holds
card G = card H by Th84;

theorem :: GROUP_6:87

for G being trivial strict Group
for H being strict Group st G,H are_isomorphic holds
H is trivial

proof end;

theorem :: GROUP_6:88

canceled;

theorem :: GROUP_6:89

for G being Group
for H being strict Group st G,H are_isomorphic & G is commutative holds
H is commutative

proof end;

Lm3: for H, G being Group
for g being Homomorphism of G,H holds
( G ./. (Ker g), Image g are_isomorphic & ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) )

proof end;

theorem :: GROUP_6:90

for H, G being Group
for g being Homomorphism of G,H holds G ./. (Ker g), Image g are_isomorphic by Lm3;

theorem :: GROUP_6:91

for H, G being Group
for g being Homomorphism of G,H ex h being Homomorphism of (G ./. (Ker g)),(Image g) st
( h is bijective & g = h * (nat_hom (Ker g)) ) by Lm3;

theorem :: GROUP_6:92

for G being Group
for N being normal Subgroup of G
for M being strict normal Subgroup of G
for J being strict normal Subgroup of G ./. M st J = N ./. ((N,M) `*`) & M is Subgroup of N holds
(G ./. M) ./. J,G ./. N are_isomorphic

proof end;

theorem :: GROUP_6:93

for G being Group
for B being Subgroup of G
for N being strict normal Subgroup of G holds (B "\/" N) ./. (((B "\/" N),N) `*`),B ./. (B /\ N) are_isomorphic

proof end;