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

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:56;

end;

registration

let G be Group;

cluster (1). G -> normal ;

coherence
(1). G is normal by GROUP_3:114;

cluster (Omega). G -> normal ;

coherence
(Omega). G is normal by GROUP_3:114;

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 Th5: :: GROUP_6:5

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 Th6: :: GROUP_6:6

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 Th7: :: GROUP_6:7

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 Th8: :: GROUP_6:8

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 Th9: :: GROUP_6:9

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 Th9;

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 Th9;

end;

definition

let G be non empty 1-sorted ;

redefine attr G is trivial means :Def2: :: GROUP_6:def 2
ex x being object st the carrier of G = {x};

compatibility
( G is trivial iff ex x being object 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 object st the carrier of G = {x} );

theorem Th10: :: GROUP_6:10

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 Th10;

end;

registration

cluster non empty trivial strict unital Group-like associative for multMagma ;

existence
ex b₁ being Group st
( b₁ is strict & b₁ is trivial )

proof end;

end;

theorem Th11: :: GROUP_6:11

( ( 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 Th12: :: GROUP_6:12

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:135;

end;

theorem Th13: :: GROUP_6:13

for G being Group
for x being object
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 Th14: :: GROUP_6:14

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 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
x is Subset of G ;

theorem Th16: :: GROUP_6:16

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

let G be Group;
let N be normal Subgroup of G;

func CosOp N -> BinOp of (Cosets N) means :Def3: :: GROUP_6:def 3
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 Def3 defines CosOp GROUP_6:def 3 :
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 4
multMagma(# (Cosets N),(CosOp N) #);

correctness
coherence
multMagma(# (Cosets N),(CosOp N) #) is multMagma ;
;

end;

:: deftheorem defines ./. GROUP_6:def 4 :
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:17

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

theorem :: GROUP_6:18

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 5
S;

coherence
S is Subset of G by Th15;

end;

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

theorem :: GROUP_6:19

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 Def3;

theorem :: GROUP_6:20

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 Def3;

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:21

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 Th13;

theorem :: GROUP_6:22

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 Th14, GROUP_2:135;

theorem Th23: :: GROUP_6:23

for G being Group
for x being object
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 ) ) by Th13, Th14;

theorem Th24: :: GROUP_6:24

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

proof end;

theorem Th25: :: GROUP_6:25

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:26

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

theorem :: GROUP_6:27

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 Th28: :: GROUP_6:28

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:29

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:30

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 non empty unital multMagma
for f being Function of G,H st ( for a being Element of G holds f . a = 1_ H ) holds
for a, b being Element of G 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 :Def6: :: GROUP_6:def 6
for a, b being Element of G holds f . (a * b) = (f . a) * (f . b);

end;

:: deftheorem Def6 defines multiplicative GROUP_6:def 6 :
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 non empty unital multMagma ;

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 for 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 Th31: :: GROUP_6:31

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 for Element of bool [: the carrier of G, the carrier of H:];

coherence
for b₁ being Homomorphism of G,H holds b₁ is unity-preserving by Th31;

end;

theorem Th32: :: GROUP_6:32

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 Th33: :: GROUP_6:33

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 Th34: :: GROUP_6:34

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:35

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 Th36: :: GROUP_6:36

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:37

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 Th38: :: GROUP_6:38

for G being non empty multMagma holds id the carrier of G is multiplicative ;

theorem Th39: :: GROUP_6:39

for G, H, I being non empty unital multMagma
for h being multiplicative Function of G,H
for h1 being multiplicative Function of H,I holds h1 * h is multiplicative

proof end;

registration

let G, H, I be non empty unital multMagma ;
let h be multiplicative Function of G,H;
let h1 be multiplicative Function of H,I;

cluster h * h1 -> multiplicative for Function of G,I;

coherence
for b₁ being Function of G,I st b₁ = h1 * h holds
b₁ is multiplicative by Th39;

end;

definition

let G, H be non empty multMagma ;

func 1: (G,H) -> Function of G,H equals :: GROUP_6:def 7
G --> (1_ H);

coherence
G --> (1_ H) is Function of G,H ;

end;

:: deftheorem defines 1: GROUP_6:def 7 :
for G, H being non empty multMagma holds 1: (G,H) = G --> (1_ H);

registration

let G, H be non empty unital multMagma ;

cluster 1: (G,H) -> multiplicative ;

coherence
1: (G,H) is multiplicative

proof end;

end;

theorem :: GROUP_6:40

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 -> Function of G,(G ./. N) means :Def8: :: GROUP_6:def 8
for a being Element of G holds it . a = a * N;

existence
ex b₁ being Function of G,(G ./. N) st
for a being Element of G holds b₁ . a = a * N

proof end;

uniqueness
for b₁, b₂ being Function 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 Def8 defines nat_hom GROUP_6:def 8 :
for G being Group
for N being normal Subgroup of G
for b₃ being Function of G,(G ./. N) holds
( b₃ = nat_hom N iff for a being Element of G holds b₃ . a = a * N );

registration

let G be Group;
let N be normal Subgroup of G;

cluster nat_hom N -> multiplicative ;

coherence
nat_hom N is multiplicative

proof end;

end;

definition

let G, H be Group;
let g be Homomorphism of G,H;

func Ker g -> strict Subgroup of G means :Def9: :: GROUP_6:def 9
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:59;

end;

:: deftheorem Def9 defines Ker GROUP_6:def 9 :
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 Th41: :: GROUP_6:41

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:42

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

proof end;

theorem Th43: :: GROUP_6:43

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 :Def10: :: GROUP_6:def 10
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:59;

end;

:: deftheorem Def10 defines Image GROUP_6:def 10 :
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 Th44: :: GROUP_6:44

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

proof end;

theorem Th45: :: GROUP_6:45

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

proof end;

theorem :: GROUP_6:46

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

proof end;

theorem :: GROUP_6:47

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

proof end;

theorem Th48: :: GROUP_6:48

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

proof end;

theorem Th49: :: GROUP_6:49

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

proof end;

theorem Th50: :: GROUP_6:50

for G, H 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 Th50;

end;

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

theorem :: GROUP_6:51

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

proof end;

theorem Th52: :: GROUP_6:52

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

proof end;

theorem :: GROUP_6:53

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:54

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:55

for G, H 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 Th56: :: GROUP_6:56

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

proof end;

theorem Th57: :: GROUP_6:57

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 Th58: :: GROUP_6:58

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 Th59: :: GROUP_6:59

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

proof end;

theorem :: GROUP_6:60

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 ) ) by FUNCT_2:def 3;

theorem :: GROUP_6:61

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 Th62: :: GROUP_6:62

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

proof end;

theorem Th63: :: GROUP_6:63

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 Th64: :: GROUP_6:64

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 Th65: :: GROUP_6:65

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

proof end;

definition

let G, H be Group;

pred G,H are_isomorphic means :Def11: :: GROUP_6:def 11
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 Def11 defines are_isomorphic GROUP_6:def 11 :
for G, H being Group holds
( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

theorem Th66: :: GROUP_6:66

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

proof end;

definition

let G, H be Group;
:: original: are_isomorphic
redefine pred G,H are_isomorphic ;
symmetry
for G, H being Group st (b₁,b₂) holds
(b₂,b₁) by Th66;

end;

theorem :: GROUP_6:67

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:68

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

proof end;

theorem Th69: :: GROUP_6:69

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

proof end;

theorem :: GROUP_6:70

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

theorem :: GROUP_6:71

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

proof end;

theorem :: GROUP_6:72

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

proof end;

theorem Th73: :: GROUP_6:73

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

proof end;

theorem Th74: :: GROUP_6:74

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

proof end;

theorem :: GROUP_6:75

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

theorem :: GROUP_6:76

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:77

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

proof end;

Lm3: for G, H 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:78

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

:: First isomorphism theorem for groups

theorem :: GROUP_6:79

for G, H 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;

:: Third isomorphism theorem for groups

theorem :: GROUP_6:80

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;

:: Second isomorphism theorem for groups

theorem :: GROUP_6:81

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;