:: GROUP_6 semantic presentation

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 by GROUP_2:65;

end;

registration

let G be Group;
cluster (1). G -> normal ;
coherence by GROUP_3:137;
cluster (Omega). G -> normal ;
coherence 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: HGrStr(# the carrier of M,the mult of M #) is Subgroup of B ;
func B,M `*` -> strict normal Subgroup of B equals :Def1: :: GROUP_6:def 1
HGrStr(# the carrier of M,the mult of M #);
coherence

proof end;

correctness ;

end;

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

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

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 G being Group holds (1). G is trivial

proof end;

theorem Th12: :: GROUP_6:12

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

proof end;

theorem Th13: :: GROUP_6:13

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

proof end;

definition

let G be Group;
let N be normal Subgroup of G;
func Cosets N -> set equals :: GROUP_6:def 3
Left_Cosets N;
coherence ;

end;

:: deftheorem defines Cosets GROUP_6:def 3 :

registration

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

end;

theorem Th14: :: GROUP_6:14

for G being Group
for N being normal Subgroup of G holds
( Cosets N = Left_Cosets N & Cosets N = Right_Cosets N ) by GROUP_3:150;

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines CosOp GROUP_6:def 4 :

definition

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

end;

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

registration

let G be Group;
let N be normal Subgroup of G;
cluster G ./. N -> non empty strict ;
coherence ;

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 mult 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 by Th17;

end;

:: deftheorem defines @ GROUP_6:def 6 :

theorem Th24: :: 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 Th25: :: 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 Th24;

registration

let G be Group;
let N be normal Subgroup of G;
cluster G ./. N -> non empty strict Group-like associative ;
coherence

proof end;

end;

theorem Th26: :: 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 Th27: :: 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 Th31: :: GROUP_6:31

for G being Group
for N being normal Subgroup of G st Left_Cosets N is finite holds
G ./. N is finite by GROUP_1:def 14;

theorem :: GROUP_6:32

for G being Group
for N being normal Subgroup of G holds Ord (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
ord (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 HGrStr ;
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 :

registration

let G, H be Group;
cluster multiplicative M4(the carrier of G,the carrier of H);
existence

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;

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

end;

definition

let G, H be Group;
let g be Homomorphism of G,H;
:: original: rng
redefine func rng g -> Subset of H;
coherence by RELSET_1:12;

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

proof end;

uniqueness

proof end;

end;

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines nat_hom GROUP_6:def 9 :

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

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def10 defines Ker GROUP_6:def 10 :

registration

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

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

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def11 defines Image GROUP_6:def 11 :

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;

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 Ord (Image g) <=` Ord G

proof end;

theorem :: GROUP_6:62

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

proof end;

definition

let G, H be Group;
let h be Homomorphism of G,H;
attr h is being_monomorphism means :Def12: :: GROUP_6:def 12
h is one-to-one;
attr h is being_epimorphism means :Def13: :: GROUP_6:def 13
rng h = the carrier of H;

end;

:: deftheorem Def12 defines being_monomorphism GROUP_6:def 12 :

:: deftheorem Def13 defines being_epimorphism GROUP_6:def 13 :

notation

let G, H be Group;
let h be Homomorphism of G,H;
synonym h is_monomorphism for being_monomorphism h;
synonym h is_epimorphism for being_epimorphism h;

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_monomorphism & c in Image h holds
h . ((h " ) . c) = c

proof end;

theorem Th64: :: GROUP_6:64

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

proof end;

theorem Th65: :: GROUP_6:65

for H, G being Group
for h being Homomorphism of G,H st h is_monomorphism 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_monomorphism 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_epimorphism iff Image h = H )

proof end;

theorem Th68: :: GROUP_6:68

for G being Group
for H being strict Group
for h being Homomorphism of G,H st h is_epimorphism 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_epimorphism

proof end;

definition

let G, H be Group;
let h be Homomorphism of G,H;
attr h is being_isomorphism means :Def14: :: GROUP_6:def 14
( h is_epimorphism & h is_monomorphism );

end;

:: deftheorem Def14 defines being_isomorphism GROUP_6:def 14 :

notation

let G, H be Group;
let h be Homomorphism of G,H;
synonym h is_isomorphism for being_isomorphism h;

end;

theorem Th70: :: GROUP_6:70

for G, H being Group
for h being Homomorphism of G,H holds
( h is_isomorphism iff ( rng h = the carrier of H & h is one-to-one ) )

proof end;

theorem :: GROUP_6:71

for G, H being Group
for h being Homomorphism of G,H st h is_isomorphism holds
( dom h = the carrier of G & rng h = the carrier of H )

proof end;

theorem Th72: :: GROUP_6:72

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

proof end;

theorem Th73: :: GROUP_6:73

for H, G being Group
for h being Homomorphism of G,H
for g1 being Homomorphism of H,G st h is_isomorphism & g1 = h " holds
g1 is_isomorphism

proof end;

theorem Th74: :: GROUP_6:74

for G, H, I being Group
for h being Homomorphism of G,H
for h1 being Homomorphism of H,I st h is_isomorphism & h1 is_isomorphism holds
h1 * h is_isomorphism

proof end;

theorem Th75: :: GROUP_6:75

for G being Group holds nat_hom ((1). G) is_isomorphism

proof end;

definition

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

proof end;

end;

:: deftheorem Def15 defines are_isomorphic GROUP_6:def 15 :

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

proof end;

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
Ord G = Ord 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 Th86: :: GROUP_6:86

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

proof end;

theorem :: GROUP_6:87

for G, H being strict Group st G,H are_isomorphic & G is trivial 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 Group holds
H is commutative Group

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