:: by Wojciech A. Trybulec and Micha{\l} J. Trybulec

::

:: Received October 3, 1991

:: Copyright (c) 1991-2012 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 )

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_{1} being Subgroup of A holds b_{1} is Subgroup of G
by GROUP_2:56;

end;
let A be Subgroup of G;

:: original: Subgroup

redefine mode Subgroup of A -> Subgroup of G;

coherence

for b

registration

let G be Group;

coherence

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

coherence

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

end;
coherence

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

coherence

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

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 )

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 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 ") )

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 )

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

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 )

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

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 ;

multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B

;

end;
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 #);

multMagma(# the carrier of M, the multF of M #) is strict normal Subgroup of B

proof end;

correctness ;

:: 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 #);

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 )

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

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

definition

let G be non empty 1-sorted ;

compatibility

( G is trivial iff ex x being set st the carrier of G = {x} )

end;
compatibility

( G is trivial iff ex x being set st the carrier of G = {x} )

proof 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} );

for G being non empty 1-sorted holds

( G is trivial iff ex x being set st the carrier of G = {x} );

registration
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 ) )

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

G is trivial ) )

proof end;

registration
end;

theorem Th13: :: GROUP_6:13

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 )

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 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 )

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

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;

ex b_{1} 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_{1} . (W1,W2) = A1 * A2

for b_{1}, b_{2} 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_{1} . (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_{2} . (W1,W2) = A1 * A2 ) holds

b_{1} = b_{2}

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

ex b

for W1, W2 being Element of Cosets N

for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds

b

proof end;

uniqueness for b

for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds

b

for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds

b

b

proof end;

:: deftheorem Def3 defines CosOp GROUP_6:def 3 :

for G being Group

for N being normal Subgroup of G

for b_{3} being BinOp of (Cosets N) holds

( b_{3} = 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_{3} . (W1,W2) = A1 * A2 );

for G being Group

for N being normal Subgroup of G

for b

( b

for A1, A2 being Subset of G st W1 = A1 & W2 = A2 holds

b

definition

let G be Group;

let N be normal Subgroup of G;

correctness

coherence

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

;

end;
let N be normal Subgroup of G;

correctness

coherence

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

;

:: 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) #);

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;

coherence

( G ./. N is strict & not G ./. N is empty ) ;

end;
let N be normal Subgroup of G;

coherence

( G ./. N is strict & not G ./. N is empty ) ;

theorem :: GROUP_6:17

theorem :: GROUP_6:18

definition

let G be Group;

let N be normal Subgroup of G;

let S be Element of (G ./. N);

coherence

S is Subset of G by Th15;

end;
let N be normal Subgroup of G;

let S be Element of (G ./. N);

coherence

S is Subset of G by Th15;

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

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

theorem :: GROUP_6:20

registration

let G be Group;

let N be normal Subgroup of G;

coherence

( G ./. N is associative & G ./. N is Group-like )

end;
let N be normal Subgroup of G;

coherence

( G ./. N is associative & G ./. N is Group-like )

proof end;

theorem :: GROUP_6:21

theorem :: GROUP_6:22

theorem Th23: :: GROUP_6:23

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 ) )

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

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

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

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

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

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 )

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;

end;
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);

for a, b being Element of G holds f . (a * b) = (f . a) * (f . b);

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

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;

ex b_{1} being Function of G,H st b_{1} is multiplicative

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

proof end;

registration

let G, H be Group;

for b_{1} being Homomorphism of G,H holds b_{1} is unity-preserving

end;
cluster Function-like quasi_total multiplicative -> unity-preserving for Element of bool [: the carrier of G, the carrier of H:];

coherence for b

proof 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) "

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)

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).]

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).]

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

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

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 Th39: :: GROUP_6:39

for G, H, I being Group

for h being Homomorphism of G,H

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

for h being Homomorphism of G,H

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

proof end;

registration

let G, H, I be Group;

let h be Homomorphism of G,H;

let h1 be Homomorphism of H,I;

coherence

for b_{1} being Function of G,I st b_{1} = h1 * h holds

b_{1} is multiplicative
by Th39;

end;
let h be Homomorphism of G,H;

let h1 be Homomorphism of H,I;

coherence

for b

b

definition

let G, H be Group;

ex b_{1} being Function of G,H st

for a being Element of G holds b_{1} . a = 1_ H

for b_{1}, b_{2} being Function of G,H st ( for a being Element of G holds b_{1} . a = 1_ H ) & ( for a being Element of G holds b_{2} . a = 1_ H ) holds

b_{1} = b_{2}

end;
func 1: (G,H) -> Function of G,H means :Def7: :: GROUP_6:def 7

for a being Element of G holds it . a = 1_ H;

existence for a being Element of G holds it . a = 1_ H;

ex b

for a being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines 1: GROUP_6:def 7 :

for G, H being Group

for b_{3} being Function of G,H holds

( b_{3} = 1: (G,H) iff for a being Element of G holds b_{3} . a = 1_ H );

for G, H being Group

for b

( b

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) )

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;

ex b_{1} being Function of G,(G ./. N) st

for a being Element of G holds b_{1} . a = a * N

for b_{1}, b_{2} being Function of G,(G ./. N) st ( for a being Element of G holds b_{1} . a = a * N ) & ( for a being Element of G holds b_{2} . a = a * N ) holds

b_{1} = b_{2}

end;
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 for a being Element of G holds it . a = a * N;

ex b

for a being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines nat_hom GROUP_6:def 8 :

for G being Group

for N being normal Subgroup of G

for b_{3} being Function of G,(G ./. N) holds

( b_{3} = nat_hom N iff for a being Element of G holds b_{3} . a = a * N );

for G being Group

for N being normal Subgroup of G

for b

( b

registration
end;

definition

let G, H be Group;

let g be Homomorphism of G,H;

ex b_{1} being strict Subgroup of G st the carrier of b_{1} = { a where a is Element of G : g . a = 1_ H }

for b_{1}, b_{2} being strict Subgroup of G st the carrier of b_{1} = { a where a is Element of G : g . a = 1_ H } & the carrier of b_{2} = { a where a is Element of G : g . a = 1_ H } holds

b_{1} = b_{2}
by GROUP_2:59;

end;
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 the carrier of it = { a where a is Element of G : g . a = 1_ H } ;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines Ker GROUP_6:def 9 :

for G, H being Group

for g being Homomorphism of G,H

for b_{4} being strict Subgroup of G holds

( b_{4} = Ker g iff the carrier of b_{4} = { a where a is Element of G : g . a = 1_ H } );

for G, H being Group

for g being Homomorphism of G,H

for b

( b

registration
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 )

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;

definition

let G, H be Group;

let g be Homomorphism of G,H;

ex b_{1} being strict Subgroup of H st the carrier of b_{1} = g .: the carrier of G

for b_{1}, b_{2} being strict Subgroup of H st the carrier of b_{1} = g .: the carrier of G & the carrier of b_{2} = g .: the carrier of G holds

b_{1} = b_{2}
by GROUP_2:59;

end;
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 the carrier of it = g .: the carrier of G;

ex b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines Image GROUP_6:def 10 :

for G, H being Group

for g being Homomorphism of G,H

for b_{4} being strict Subgroup of H holds

( b_{4} = Image g iff the carrier of b_{4} = g .: the carrier of G );

for G, H being Group

for g being Homomorphism of G,H

for b

( b

theorem Th45: :: GROUP_6:45

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 )

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;

registration

let G be finite Group;

let H be Group;

let g be Homomorphism of G,H;

coherence

Image g is finite by Th50;

end;
let H be Group;

let g be Homomorphism of G,H;

coherence

Image g is finite by Th50;

Lm2: for A being commutative Group

for a, b being Element of A holds a * b = b * a

;

theorem :: GROUP_6:51

for H, G being Group

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

Image g is commutative

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

Image g is commutative

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

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

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

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

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

h " is Homomorphism of (Image h),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 )

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

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 Th60: :: 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 ) )

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

theorem Th62: :: GROUP_6:62

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

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

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

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;

definition

let G, H be Group;

for G being Group ex h being Homomorphism of G,G st h is bijective

end;
pred G,H are_isomorphic means :Def11: :: GROUP_6:def 11

ex h being Homomorphism of G,H st h is bijective ;

reflexivity ex h being Homomorphism of G,H st h is bijective ;

for G being Group ex h being Homomorphism of G,G st h is bijective

proof 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 );

for G, H being Group holds

( G,H are_isomorphic iff ex h being Homomorphism of G,H st h is bijective );

definition

let G, H be strict Group;

:: original: are_isomorphic

redefine pred G,H are_isomorphic ;

symmetry

for G, H being strict Group st (b_{1},b_{2}) holds

(b_{2},b_{1})
by Th66;

end;
:: original: are_isomorphic

redefine pred G,H are_isomorphic ;

symmetry

for G, H being strict Group st (b

(b

theorem :: GROUP_6:68

for H, G being Group

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

G, Image h are_isomorphic

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

G, Image h are_isomorphic

proof end;

theorem :: GROUP_6:75

theorem :: GROUP_6:77

for G being Group

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

H is commutative

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

for H, G being Group

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

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

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

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

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;