GROUP_9: The {J}ordan-H\"older Theorem

:: The {J}ordan-H\"older Theorem
:: by Marco Riccardi
::
:: Received April 20, 2007
:: Copyright (c) 2007-2011 Association of Mizar Users

begin

definition

let O, E be set ;
let A be Action of O,E;
let IT be set ;
pred IT is_stable_under_the_action_of A means :Def1: :: GROUP_9:def 1
for o being Element of O
for f being Function of E,E st o in O & f = A . o holds
f .: IT c= IT;

end;

:: deftheorem Def1 defines is_stable_under_the_action_of GROUP_9:def 1 :

Lm1: for O, E being set
for A being Action of O,E holds [#] E is_stable_under_the_action_of A

proof end;

definition

let O, E be set ;
let A be Action of O,E;
let X be Subset of E;
func the_stable_subset_generated_by (X,A) -> Subset of E means :Def2: :: GROUP_9:def 2
( X c= it & it is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds
it c= Y ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines the_stable_subset_generated_by GROUP_9:def 2 :

definition

let O, E be set ;
let A be Action of O,E;
let F be FinSequence of O;
func Product (F,A) -> Function of E,E means :Def3: :: GROUP_9:def 3
it = id E if len F = 0
otherwise ex PF being FinSequence of Funcs (E,E) st
( it = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds
ex f, g being Function of E,E st
( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) );
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def3 defines Product GROUP_9:def 3 :

definition

let O be set ;
let G be Group;
let IT be Action of O, the carrier of G;
attr IT is distributive means :Def4: :: GROUP_9:def 4
for o being Element of O st o in O holds
IT . o is Homomorphism of G,G;

end;

:: deftheorem Def4 defines distributive GROUP_9:def 4 :

definition

let O be set ;
attr c₂ is strict ;
struct HGrWOpStr of O -> multMagma ;
aggr HGrWOpStr(# carrier, multF, action #) -> HGrWOpStr of O;
sel action c₂ -> Action of O, the carrier of c₂;

end;

registration

let O be set ;
cluster non empty HGrWOpStr of O;
existence

proof end;

end;

definition

let O be set ;
let IT be non empty HGrWOpStr of O;
attr IT is distributive means :Def5: :: GROUP_9:def 5
for G being Group
for a being Action of O, the carrier of G st a = the action of IT & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of IT, the multF of IT #) holds
a is distributive ;

end;

:: deftheorem Def5 defines distributive GROUP_9:def 5 :

Lm2: for O, E being set holds [:O,{(id E)}:] is Action of O,E

proof end;

Lm3: for O being set
for G being strict Group ex H being non empty HGrWOpStr of O st
( H is strict & H is distributive & H is Group-like & H is associative & G = multMagma(# the carrier of H, the multF of H #) )

proof end;

registration

let O be set ;
cluster non empty Group-like associative strict distributive HGrWOpStr of O;
existence

proof end;

end;

definition

let O be set ;
mode GroupWithOperators of O is non empty Group-like associative distributive HGrWOpStr of O;

end;

definition

let O be set ;
let G be GroupWithOperators of O;
let o be Element of O;
func G ^ o -> Homomorphism of G,G equals :Def6: :: GROUP_9:def 6
the action of G . o if o in O
otherwise id the carrier of G;
correctness

proof end;

end;

:: deftheorem Def6 defines ^ GROUP_9:def 6 :

definition

let O be set ;
let G be GroupWithOperators of O;
mode StableSubgroup of G -> non empty Group-like associative distributive HGrWOpStr of O means :Def7: :: GROUP_9:def 7
( it is Subgroup of G & ( for o being Element of O holds it ^ o = (G ^ o) | the carrier of it ) );
correctness

proof end;

end;

:: deftheorem Def7 defines StableSubgroup GROUP_9:def 7 :

Lm4: for O being set
for G being GroupWithOperators of O holds HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G

proof end;

registration

let O be set ;
let G be GroupWithOperators of O;
cluster non empty unital Group-like associative strict distributive StableSubgroup of G;
correctness

proof end;

end;

Lm5: for O being set
for G being GroupWithOperators of O
for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
H1 = H2

proof end;

definition

let O be set ;
let G be GroupWithOperators of O;
func (1). G -> strict StableSubgroup of G means :Def8: :: GROUP_9:def 8
the carrier of it = {(1_ G)};
existence

proof end;

uniqueness by Lm5;

end;

:: deftheorem Def8 defines (1). GROUP_9:def 8 :

definition

let O be set ;
let G be GroupWithOperators of O;
func (Omega). G -> strict StableSubgroup of G equals :: GROUP_9:def 9
HGrWOpStr(# the carrier of G, the multF of G, the action of G #);
correctness by Lm4;

end;

:: deftheorem defines (Omega). GROUP_9:def 9 :

definition

let O be set ;
let G be GroupWithOperators of O;
let IT be StableSubgroup of G;
attr IT is normal means :Def10: :: GROUP_9:def 10
for H being strict Subgroup of G st H = multMagma(# the carrier of IT, the multF of IT #) holds
H is normal ;

end;

:: deftheorem Def10 defines normal GROUP_9:def 10 :

registration

let O be set ;
let G be GroupWithOperators of O;
cluster non empty unital Group-like associative strict distributive normal StableSubgroup of G;
existence

proof end;

end;

registration

let O be set ;
let G be GroupWithOperators of O;
let H be StableSubgroup of G;
cluster non empty unital Group-like associative distributive normal StableSubgroup of H;
existence

proof end;

end;

registration

let O be set ;
let G be GroupWithOperators of O;
cluster (1). G -> strict normal ;
correctness

proof end;

cluster (Omega). G -> strict normal ;
correctness

proof end;

end;

definition

let O be set ;
let G be GroupWithOperators of O;
func the_stable_subgroups_of G -> set means :Def11: :: GROUP_9:def 11
for x being set holds
( x in it iff x is strict StableSubgroup of G );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines the_stable_subgroups_of GROUP_9:def 11 :

registration

let O be set ;
let G be GroupWithOperators of O;
cluster the_stable_subgroups_of G -> non empty ;
correctness

proof end;

end;

definition

let IT be Group;
attr IT is simple means :Def12: :: GROUP_9:def 12
( not IT is trivial & ( for H being strict normal Subgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) );

end;

:: deftheorem Def12 defines simple GROUP_9:def 12 :

Lm6: Group_of_Perm 2 is simple

proof end;

registration

cluster non empty strict unital Group-like associative simple multMagma ;
existence by Lm6;

end;

definition

let O be set ;
let IT be GroupWithOperators of O;
attr IT is simple means :Def13: :: GROUP_9:def 13
( not IT is trivial & ( for H being strict normal StableSubgroup of IT holds
( not H <> (Omega). IT or not H <> (1). IT ) ) );

end;

:: deftheorem Def13 defines simple GROUP_9:def 13 :

Lm7: for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G

proof end;

Lm8: for G1, G2 being Group
for A1 being Subset of G1
for A2 being Subset of G2
for H1 being strict Subgroup of G1
for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 holds
( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 )

proof end;

registration

let O be set ;
cluster non empty unital Group-like associative strict distributive simple HGrWOpStr of O;
existence

proof end;

end;

definition

let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func Cosets N -> set means :Def14: :: GROUP_9:def 14
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
it = Cosets H;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Cosets GROUP_9:def 14 :

definition

let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func CosOp N -> BinOp of (Cosets N) means :Def15: :: GROUP_9:def 15
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
it = CosOp H;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines CosOp GROUP_9:def 15 :

Lm9: for G being Group
for N being normal Subgroup of G
for A being Element of Cosets N
for g being Element of G holds
( g in A iff A = g * N )

proof end;

Lm10: for O being set
for o being Element of O
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of G st g in H holds
(G ^ o) . g in H

proof end;

definition

let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func CosAc N -> Action of O,(Cosets N) means :Def16: :: GROUP_9:def 16
for o being Element of O holds it . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st
( g in A & h in B & h = (G ^ o) . g ) } if not O is empty
otherwise it = [:{},{(id (Cosets N))}:];
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def16 defines CosAc GROUP_9:def 16 :

definition

let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func G ./. N -> HGrWOpStr of O equals :: GROUP_9:def 17
HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);
correctness ;

end;

:: deftheorem defines ./. GROUP_9:def 17 :

registration

let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
cluster G ./. N -> non empty ;
correctness

proof end;

cluster G ./. N -> Group-like associative distributive ;
correctness

proof end;

end;

definition

let O be set ;
let G, H be GroupWithOperators of O;
let f be Function of G,H;
attr f is homomorphic means :Def18: :: GROUP_9:def 18
for o being Element of O
for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g);

end;

:: deftheorem Def18 defines homomorphic GROUP_9:def 18 :

registration

let O be set ;
let G, H be GroupWithOperators of O;
cluster non empty Relation-like the carrier of G -defined the carrier of H -valued Function-like total quasi_total multiplicative homomorphic Element of bool [: the carrier of G, the carrier of H:];
existence

proof end;

end;

definition

let O be set ;
let G, H be GroupWithOperators of O;
mode Homomorphism of G,H is multiplicative homomorphic Function of G,H;

end;

Lm11: for O being set
for G, H, I being GroupWithOperators of O
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 O be set ;
let G, H, I be GroupWithOperators of O;
let h be Homomorphism of G,H;
let h1 be Homomorphism of H,I;
:: original: *
redefine func h1 * h -> Homomorphism of G,I;
correctness by Lm11;

end;

definition

canceled;
canceled;
canceled;
let O be set ;
let G, H be GroupWithOperators of O;
pred G,H are_isomorphic means :Def22: :: GROUP_9:def 22
ex h being Homomorphism of G,H st h is bijective ;
reflexivity

proof end;

end;

:: deftheorem GROUP_9:def 19 :

:: deftheorem GROUP_9:def 20 :

:: deftheorem GROUP_9:def 21 :

:: deftheorem Def22 defines are_isomorphic GROUP_9:def 22 :

Lm12: for O being set
for G, H being GroupWithOperators of O st G,H are_isomorphic holds
H,G are_isomorphic

proof end;

definition

let O be set ;
let G, H be GroupWithOperators of O;
:: original: are_isomorphic
redefine pred G,H are_isomorphic ;
symmetry by Lm12;

end;

definition

let O be set ;
let G be GroupWithOperators of O;
let N be normal StableSubgroup of G;
func nat_hom N -> Homomorphism of G,(G ./. N) means :Def23: :: GROUP_9:def 23
for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds
it = nat_hom H;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines nat_hom GROUP_9:def 23 :

Lm13: for O being set
for G, H being GroupWithOperators of O
for g being Homomorphism of G,H holds g . (1_ G) = 1_ H

proof end;

Lm14: for O being set
for G, H being GroupWithOperators of O
for a being Element of G
for g being Homomorphism of G,H holds g . (a ") = (g . a) "

proof end;

Lm15: for O being set
for G being GroupWithOperators of O
for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g being Element of G st g in A holds
g " in A ) & ( for o being Element of O
for g being Element of G st g in A holds
(G ^ o) . g in A ) holds
ex H being strict StableSubgroup of G st the carrier of H = A

proof end;

definition

let O be set ;
let G, H be GroupWithOperators of O;
let g be Homomorphism of G,H;
func Ker g -> strict StableSubgroup of G means :Def24: :: GROUP_9:def 24
the carrier of it = { a where a is Element of G : g . a = 1_ H } ;
existence

proof end;

uniqueness by Lm5;

end;

:: deftheorem Def24 defines Ker GROUP_9:def 24 :

registration

let O be set ;
let G, H be GroupWithOperators of O;
let g be Homomorphism of G,H;
cluster Ker g -> strict normal ;
correctness

proof end;

end;

Lm16: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G holds multMagma(# the carrier of H, the multF of H #) is strict Subgroup of G

proof end;

Lm17: for O being set
for G, H being GroupWithOperators of O
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9

proof end;

definition

let O be set ;
let G, H be GroupWithOperators of O;
let g be Homomorphism of G,H;
func Image g -> strict StableSubgroup of H means :Def25: :: GROUP_9:def 25
the carrier of it = g .: the carrier of G;
existence

proof end;

uniqueness by Lm5;

end;

:: deftheorem Def25 defines Image GROUP_9:def 25 :

definition

let O be set ;
let G be GroupWithOperators of O;
let H be StableSubgroup of G;
func carr H -> Subset of G equals :: GROUP_9:def 26
the carrier of H;
coherence

proof end;

end;

:: deftheorem defines carr GROUP_9:def 26 :

definition

let O be set ;
let G be GroupWithOperators of O;
let H1, H2 be StableSubgroup of G;
func H1 * H2 -> Subset of G equals :: GROUP_9:def 27
(carr H1) * (carr H2);
coherence ;

end;

:: deftheorem defines * GROUP_9:def 27 :

Lm18: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G holds 1_ G in H

proof end;

Lm19: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g1, g2 being Element of G st g1 in H & g2 in H holds
g1 * g2 in H

proof end;

Lm20: for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for g being Element of G st g in H holds
g " in H

proof end;

definition

let O be set ;
let G be GroupWithOperators of O;
let H1, H2 be StableSubgroup of G;
func H1 /\ H2 -> strict StableSubgroup of G means :Def28: :: GROUP_9:def 28
the carrier of it = (carr H1) /\ (carr H2);
existence

proof end;

uniqueness by Lm5;
commutativity ;

end;

:: deftheorem Def28 defines /\ GROUP_9:def 28 :

Lm21: for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is StableSubgroup of H2

proof end;

definition

let O be set ;
let G be GroupWithOperators of O;
let A be Subset of G;
func the_stable_subgroup_of A -> strict StableSubgroup of G means :Def29: :: GROUP_9:def 29
( A c= the carrier of it & ( for H being strict StableSubgroup of G st A c= the carrier of H holds
it is StableSubgroup of H ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines the_stable_subgroup_of GROUP_9:def 29 :

definition

let O be set ;
let G be GroupWithOperators of O;
let H1, H2 be StableSubgroup of G;
func H1 "\/" H2 -> strict StableSubgroup of G equals :: GROUP_9:def 30
the_stable_subgroup_of ((carr H1) \/ (carr H2));
correctness ;

end;

:: deftheorem defines "\/" GROUP_9:def 30 :

begin

theorem Th1: :: GROUP_9:1

for O, x being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G st x in H1 holds
x in G

proof end;

theorem Th2: :: GROUP_9:2

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for h1 being Element of H1 holds h1 is Element of G

proof end;

theorem Th3: :: GROUP_9:3

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1, g2 being Element of G
for h1, h2 being Element of H1 st h1 = g1 & h2 = g2 holds
h1 * h2 = g1 * g2

proof end;

theorem Th4: :: GROUP_9:4

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds 1_ G = 1_ H1

proof end;

theorem :: GROUP_9:5

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds 1_ G in H1 by Lm18;

theorem Th6: :: GROUP_9:6

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G
for h1 being Element of H1 st h1 = g1 holds
h1 " = g1 "

proof end;

theorem :: GROUP_9:7

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1, g2 being Element of G st g1 in H1 & g2 in H1 holds
g1 * g2 in H1 by Lm19;

theorem :: GROUP_9:8

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G st g1 in H1 holds
g1 " in H1 by Lm20;

theorem :: GROUP_9:9

for O being set
for G being GroupWithOperators of O
for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds
g1 * g2 in A ) & ( for g1 being Element of G st g1 in A holds
g1 " in A ) & ( for o being Element of O
for g1 being Element of G st g1 in A holds
(G ^ o) . g1 in A ) holds
ex H being strict StableSubgroup of G st the carrier of H = A by Lm15;

theorem Th10: :: GROUP_9:10

for O being set
for G being GroupWithOperators of O holds G is StableSubgroup of G

proof end;

theorem Th11: :: GROUP_9:11

for O being set
for G1, G2, G3 being GroupWithOperators of O st G1 is StableSubgroup of G2 & G2 is StableSubgroup of G3 holds
G1 is StableSubgroup of G3

proof end;

theorem :: GROUP_9:12

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds
H1 is StableSubgroup of H2 by Lm21;

theorem Th13: :: GROUP_9:13

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st ( for g being Element of G st g in H1 holds
g in H2 ) holds
H1 is StableSubgroup of H2

proof end;

theorem :: GROUP_9:14

for O being set
for G being GroupWithOperators of O
for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
H1 = H2 by Lm5;

theorem Th15: :: GROUP_9:15

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds (1). G = (1). H1

proof end;

theorem Th16: :: GROUP_9:16

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds (1). G is StableSubgroup of H1

proof end;

theorem Th17: :: GROUP_9:17

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st (carr H1) * (carr H2) = (carr H2) * (carr H1) holds
ex H being strict StableSubgroup of G st the carrier of H = (carr H1) * (carr H2)

proof end;

theorem Th18: :: GROUP_9:18

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds
( ( for H being StableSubgroup of G st H = H1 /\ H2 holds
the carrier of H = the carrier of H1 /\ the carrier of H2 ) & ( for H being strict StableSubgroup of G st the carrier of H = the carrier of H1 /\ the carrier of H2 holds
H = H1 /\ H2 ) )

proof end;

theorem Th19: :: GROUP_9:19

for O being set
for G being GroupWithOperators of O
for H being strict StableSubgroup of G holds H /\ H = H

proof end;

theorem Th20: :: GROUP_9:20

for O being set
for G being GroupWithOperators of O
for H1, H2, H3 being StableSubgroup of G holds (H1 /\ H2) /\ H3 = H1 /\ (H2 /\ H3)

proof end;

Lm22: for O being set
for G being GroupWithOperators of O
for H2 being StableSubgroup of G
for H1 being strict StableSubgroup of G holds
( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 )

proof end;

theorem Th21: :: GROUP_9:21

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds
( ((1). G) /\ H1 = (1). G & H1 /\ ((1). G) = (1). G )

proof end;

theorem Th22: :: GROUP_9:22

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds union (Cosets N) = the carrier of G

proof end;

theorem Th23: :: GROUP_9:23

for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2)

proof end;

Lm23: for F1 being FinSequence
for y being Element of NAT st y in dom F1 holds
( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 )

proof end;

Lm24: for G, H being Group
for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I)

proof end;

theorem Th24: :: GROUP_9:24

for O being set
for G being GroupWithOperators of O
for A being Subset of G
for g1 being Element of G holds
( g1 in the_stable_subgroup_of A iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT ex C being Subset of G st
( C = the_stable_subset_generated_by (A, the action of G) & len F = len I & rng F c= C & Product (F |^ I) = g1 ) )

proof end;

Lm25: for O being set
for G being GroupWithOperators of O
for A being Subset of G st A is empty holds
the_stable_subgroup_of A = (1). G

proof end;

Lm26: for O being non empty set
for E being set
for o being Element of O
for A being Action of O,E holds Product (<*o*>,A) = A . o

proof end;

Lm27: for O being non empty set
for E being set
for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product ((F ^ <*o*>),A) = (Product (F,A)) * (Product (<*o*>,A))

proof end;

Lm28: for O being non empty set
for E being set
for o being Element of O
for F being FinSequence of O
for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

proof end;

Lm29: for O being non empty set
for E being set
for F1, F2 being FinSequence of O
for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A))

proof end;

Lm30: for O, E being set
for F being FinSequence of O
for Y being Subset of E
for A being Action of O,E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y

proof end;

Lm31: for O being set
for E being non empty set
for A being Action of O,E
for X being Subset of E
for a being Element of E st not X is empty holds
( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a )

proof end;

theorem Th25: :: GROUP_9:25

for O being set
for G being GroupWithOperators of O
for H being strict StableSubgroup of G holds the_stable_subgroup_of (carr H) = H

proof end;

theorem Th26: :: GROUP_9:26

for O being set
for G being GroupWithOperators of O
for A, B being Subset of G st A c= B holds
the_stable_subgroup_of A is StableSubgroup of the_stable_subgroup_of B

proof end;

scheme :: GROUP_9:sch 1
MeetSbgWOpEx{ F₁() -> set , F₂() -> GroupWithOperators of F₁(), P₁[ set ] } :

ex H being strict StableSubgroup of F₂() st the carrier of H = meet { A where A is Subset of F₂() : ex K being strict StableSubgroup of F₂() st
( A = the carrier of K & P₁[K] ) }

provided

A1: ex H being strict StableSubgroup of F₂() st P₁[H]

proof end;

theorem Th27: :: GROUP_9:27

for O being set
for G being GroupWithOperators of O
for A being Subset of G holds the carrier of (the_stable_subgroup_of A) = meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & A c= carr H ) }

proof end;

Lm32: for O being set
for G being GroupWithOperators of O
for B, A being Subset of G st B = the carrier of (gr A) holds
the_stable_subgroup_of A = the_stable_subgroup_of B

proof end;

theorem Th28: :: GROUP_9:28

for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 * N2 = N2 * N1

proof end;

theorem Th29: :: GROUP_9:29

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)

proof end;

theorem Th30: :: GROUP_9:30

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st H1 * H2 = H2 * H1 holds
the carrier of (H1 "\/" H2) = H1 * H2

proof end;

theorem Th31: :: GROUP_9:31

for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds the carrier of (N1 "\/" N2) = N1 * N2

proof end;

theorem Th32: :: GROUP_9:32

for O being set
for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 "\/" N2 is normal StableSubgroup of G

proof end;

theorem Th33: :: GROUP_9:33

for O being set
for G being GroupWithOperators of O
for H being strict StableSubgroup of G holds
( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

proof end;

theorem Th34: :: GROUP_9:34

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds
( ((Omega). G) "\/" H1 = (Omega). G & H1 "\/" ((Omega). G) = (Omega). G )

proof end;

Lm33: for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 is StableSubgroup of H1 "\/" H2

proof end;

theorem Th35: :: GROUP_9:35

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds
( H1 is StableSubgroup of H1 "\/" H2 & H2 is StableSubgroup of H1 "\/" H2 )

proof end;

theorem Th36: :: GROUP_9:36

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for H2 being strict StableSubgroup of G holds
( H1 is StableSubgroup of H2 iff H1 "\/" H2 = H2 )

proof end;

theorem Th37: :: GROUP_9:37

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for H3 being strict StableSubgroup of G st H1 is StableSubgroup of H3 & H2 is StableSubgroup of H3 holds
H1 "\/" H2 is StableSubgroup of H3

proof end;

theorem Th38: :: GROUP_9:38

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds
H1 "\/" H3 is StableSubgroup of H2 "\/" H3

proof end;

theorem Th39: :: GROUP_9:39

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for X, Y being StableSubgroup of H1
for X9, Y9 being StableSubgroup of G st X = X9 & Y = Y9 holds
X9 /\ Y9 = X /\ Y

proof end;

theorem Th40: :: GROUP_9:40

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for H1 being StableSubgroup of G st N is StableSubgroup of H1 holds
N is normal StableSubgroup of H1

proof end;

Lm34: for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 /\ H2 is StableSubgroup of H1

proof end;

theorem Th41: :: GROUP_9:41

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for H1 being StableSubgroup of G holds
( H1 /\ N is normal StableSubgroup of H1 & N /\ H1 is normal StableSubgroup of H1 )

proof end;

theorem Th42: :: GROUP_9:42

for O being set
for G being strict GroupWithOperators of O st G is trivial holds
(1). G = G

proof end;

Lm35: for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds
( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) )

proof end;

theorem Th43: :: GROUP_9:43

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds 1_ (G ./. N) = carr N

proof end;

theorem Th44: :: GROUP_9:44

for O being set
for G being GroupWithOperators of O
for M, N being strict normal StableSubgroup of G
for MN being normal StableSubgroup of N st MN = M & M is StableSubgroup of N holds
N ./. MN is normal StableSubgroup of G ./. M

proof end;

theorem :: GROUP_9:45

for O being set
for G, H being GroupWithOperators of O
for h being Homomorphism of G,H holds h . (1_ G) = 1_ H by Lm13;

theorem :: GROUP_9:46

for O being set
for G, H being GroupWithOperators of O
for g1 being Element of G
for h being Homomorphism of G,H holds h . (g1 ") = (h . g1) " by Lm14;

theorem Th47: :: GROUP_9:47

for O being set
for G, H being GroupWithOperators of O
for g1 being Element of G
for h being Homomorphism of G,H holds
( g1 in Ker h iff h . g1 = 1_ H )

proof end;

theorem Th48: :: GROUP_9:48

for O being set
for G being GroupWithOperators of O
for N being strict normal StableSubgroup of G holds Ker (nat_hom N) = N

proof end;

theorem Th49: :: GROUP_9:49

for O being set
for G, H being GroupWithOperators of O
for h being Homomorphism of G,H holds rng h = the carrier of (Image h)

proof end;

theorem Th50: :: GROUP_9:50

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds Image (nat_hom N) = G ./. N

proof end;

theorem Th51: :: GROUP_9:51

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

proof end;

theorem Th52: :: GROUP_9:52

for O being set
for G being GroupWithOperators of O
for H being strict GroupWithOperators of O
for h being Homomorphism 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 Th53: :: GROUP_9:53

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds nat_hom N is onto

proof end;

theorem Th54: :: GROUP_9:54

for O being set
for G being GroupWithOperators of O holds nat_hom ((1). G) is bijective

proof end;

theorem Th55: :: GROUP_9:55

for O being set
for G, H, I being GroupWithOperators of O st G,H are_isomorphic & H,I are_isomorphic holds
G,I are_isomorphic

proof end;

theorem Th56: :: GROUP_9:56

for O being set
for G being strict GroupWithOperators of O holds G,G ./. ((1). G) are_isomorphic

proof end;

theorem Th57: :: GROUP_9:57

for O being set
for G being strict GroupWithOperators of O holds G ./. ((Omega). G) is trivial

proof end;

theorem Th58: :: GROUP_9:58

for O being set
for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is trivial holds
H is trivial

proof end;

theorem Th59: :: GROUP_9:59

for O being set
for H, G being GroupWithOperators of O
for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic

proof end;

theorem Th60: :: GROUP_9:60

for O being set
for G being GroupWithOperators of O
for H, F1, F2 being strict StableSubgroup of G st F1 is normal StableSubgroup of F2 holds
H /\ F1 is normal StableSubgroup of H /\ F2

proof end;

begin

theorem :: GROUP_9:61

for O, E being set
for A being Action of O,E holds [#] E is_stable_under_the_action_of A by Lm1;

theorem :: GROUP_9:62

for O, E being set holds [:O,{(id E)}:] is Action of O,E by Lm2;

theorem :: GROUP_9:63

for O being non empty set
for E being set
for o being Element of O
for A being Action of O,E holds Product (<*o*>,A) = A . o by Lm26;

theorem :: GROUP_9:64

for O being non empty set
for E being set
for F1, F2 being FinSequence of O
for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) by Lm29;

theorem :: GROUP_9:65

for O, E being set
for A being Action of O,E
for F being FinSequence of O
for Y being Subset of E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y by Lm30;

theorem :: GROUP_9:66

for O being set
for E being non empty set
for A being Action of O,E
for X being Subset of E
for a being Element of E st not X is empty holds
( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a ) by Lm31;

theorem :: GROUP_9:67

for O being set
for G being strict Group ex H being strict GroupWithOperators of O st G = multMagma(# the carrier of H, the multF of H #)

proof end;

theorem :: GROUP_9:68

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G holds multMagma(# the carrier of H1, the multF of H1 #) is strict Subgroup of G by Lm16;

theorem :: GROUP_9:69

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G by Lm7;

theorem :: GROUP_9:70

for O being set
for o being Element of O
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for g1 being Element of G st g1 in H1 holds
(G ^ o) . g1 in H1 by Lm10;

theorem :: GROUP_9:71

for O being set
for G, H being GroupWithOperators of O
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9 by Lm17;

theorem :: GROUP_9:72

for O being set
for G being GroupWithOperators of O
for B being Subset of G st B is empty holds
the_stable_subgroup_of B = (1). G by Lm25;

theorem :: GROUP_9:73

for O being set
for G being GroupWithOperators of O
for B, C being Subset of G st B = the carrier of (gr C) holds
the_stable_subgroup_of C = the_stable_subgroup_of B by Lm32;

theorem :: GROUP_9:74

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G
for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds
( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) ) by Lm35;

theorem Th75: :: GROUP_9:75

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds
HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #)

proof end;

theorem Th76: :: GROUP_9:76

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st H1 ./. N1 is trivial holds
HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of N1, the multF of N1, the action of N1 #)

proof end;

theorem Th77: :: GROUP_9:77

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1 being normal StableSubgroup of H1 st the carrier of H1 = the carrier of N1 holds
H1 ./. N1 is trivial

proof end;

theorem Th78: :: GROUP_9:78

for O being set
for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for H9 being strict StableSubgroup of H
for f being Homomorphism of G,H st N = Ker f holds
ex G9 being strict StableSubgroup of G st
( the carrier of G9 = f " the carrier of H9 & ( H9 is normal implies ( N is normal StableSubgroup of G9 & G9 is normal ) ) )

proof end;

theorem Th79: :: GROUP_9:79

for O being set
for G, H being GroupWithOperators of O
for N being StableSubgroup of G
for G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f holds
ex H9 being strict StableSubgroup of H st
( the carrier of H9 = f .: the carrier of G9 & f " the carrier of H9 = the carrier of (G9 "\/" N) & ( f is onto & G9 is normal implies H9 is normal ) )

proof end;

theorem Th80: :: GROUP_9:80

for O being set
for G being strict GroupWithOperators of O
for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of G = (nat_hom N) " the carrier of H holds
H = (Omega). (G ./. N)

proof end;

theorem Th81: :: GROUP_9:81

for O being set
for G being strict GroupWithOperators of O
for N being strict normal StableSubgroup of G
for H being strict StableSubgroup of G ./. N st the carrier of N = (nat_hom N) " the carrier of H holds
H = (1). (G ./. N)

proof end;

theorem Th82: :: GROUP_9:82

for O being set
for G, H being strict GroupWithOperators of O st G,H are_isomorphic & G is simple holds
H is simple

proof end;

theorem Th83: :: GROUP_9:83

for O being set
for G being GroupWithOperators of O
for H being StableSubgroup of G
for FG being FinSequence of the carrier of G
for FH being FinSequence of the carrier of H
for I being FinSequence of INT st FG = FH & len FG = len I holds
Product (FG |^ I) = Product (FH |^ I)

proof end;

theorem Th84: :: GROUP_9:84

for O, E1, E2 being set
for A1 being Action of O,E1
for A2 being Action of O,E2
for F being FinSequence of O st E1 c= E2 & ( for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ) holds
Product (F,A1) = (Product (F,A2)) | E1

proof end;

theorem Th85: :: GROUP_9:85

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of H1
for N19, N29 being strict StableSubgroup of G st N1 = N19 & N2 = N29 holds
N19 * N29 = N1 * N2

proof end;

theorem Th86: :: GROUP_9:86

proof end;

theorem Th87: :: GROUP_9:87

for O being set
for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of G st N1 is normal StableSubgroup of H1 & N2 is normal StableSubgroup of H1 holds
N1 "\/" N2 is normal StableSubgroup of H1

proof end;

theorem Th88: :: GROUP_9:88

for O being set
for G, H, I being GroupWithOperators of O
for f being Homomorphism of G,H
for g being Homomorphism of H,I holds the carrier of (Ker (g * f)) = f " the carrier of (Ker g)

proof end;

theorem Th89: :: GROUP_9:89

for O being set
for G, H being GroupWithOperators of O
for G9 being StableSubgroup of G
for H9 being StableSubgroup of H
for f being Homomorphism of G,H st ( the carrier of H9 = f .: the carrier of G9 or the carrier of G9 = f " the carrier of H9 ) holds
f | the carrier of G9 is Homomorphism of G9,H9

proof end;

theorem Th90: :: GROUP_9:90

for O being set
for G, H being strict GroupWithOperators of O
for N, L, G9 being strict StableSubgroup of G
for f being Homomorphism of G,H st N = Ker f & L is strict normal StableSubgroup of G9 holds
( L "\/" (G9 /\ N) is normal StableSubgroup of G9 & L "\/" N is normal StableSubgroup of G9 "\/" N & ( for N1 being strict normal StableSubgroup of G9 "\/" N
for N2 being strict normal StableSubgroup of G9 st N1 = L "\/" N & N2 = L "\/" (G9 /\ N) holds
(G9 "\/" N) ./. N1,G9 ./. N2 are_isomorphic ) )

proof end;

begin

theorem Th91: :: GROUP_9:91

for O being set
for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G
for JH being normal StableSubgroup of H9 "\/" (H /\ K)
for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds
(H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic

proof end;

theorem Th92: :: GROUP_9:92

for O being set
for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
H9 "\/" (H /\ K9) is normal StableSubgroup of H9 "\/" (H /\ K)

proof end;

theorem Th93: :: GROUP_9:93

for O being set
for G being GroupWithOperators of O
for H, K, H9, K9 being strict StableSubgroup of G
for JH being normal StableSubgroup of H9 "\/" (H /\ K)
for JK being normal StableSubgroup of K9 "\/" (K /\ H) st JH = H9 "\/" (H /\ K9) & JK = K9 "\/" (K /\ H9) & H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K holds
(H9 "\/" (H /\ K)) ./. JH,(K9 "\/" (K /\ H)) ./. JK are_isomorphic

proof end;

begin

definition

let O be set ;
let G be GroupWithOperators of O;
let IT be FinSequence of the_stable_subgroups_of G;
attr IT is composition_series means :Def31: :: GROUP_9:def 31
( IT . 1 = (Omega). G & IT . (len IT) = (1). G & ( for i being Nat st i in dom IT & i + 1 in dom IT holds
for H1, H2 being StableSubgroup of G st H1 = IT . i & H2 = IT . (i + 1) holds
H2 is normal StableSubgroup of H1 ) );

end;

:: deftheorem Def31 defines composition_series GROUP_9:def 31 :

registration

let O be set ;
let G be GroupWithOperators of O;
cluster Relation-like NAT -defined the_stable_subgroups_of G -valued Function-like finite FinSequence-like FinSubsequence-like composition_series FinSequence of the_stable_subgroups_of G;
existence

proof end;

end;

definition

let O be set ;
let G be GroupWithOperators of O;
mode CompositionSeries of G is composition_series FinSequence of the_stable_subgroups_of G;

end;

definition

let O be set ;
let G be GroupWithOperators of O;
let s1, s2 be CompositionSeries of G;
pred s1 is_finer_than s2 means :Def32: :: GROUP_9:def 32
ex x being set st
( x c= dom s1 & s2 = s1 * (Sgm x) );
reflexivity

proof end;

end;

:: deftheorem Def32 defines is_finer_than GROUP_9:def 32 :

definition

let O be set ;
let G be GroupWithOperators of O;
let IT be CompositionSeries of G;
attr IT is strictly_decreasing means :Def33: :: GROUP_9:def 33
for i being Nat st i in dom IT & i + 1 in dom IT holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = IT . i & N = IT . (i + 1) holds
not H ./. N is trivial ;

end;

:: deftheorem Def33 defines strictly_decreasing GROUP_9:def 33 :

definition

let O be set ;
let G be GroupWithOperators of O;
let IT be CompositionSeries of G;
attr IT is jordan_holder means :Def34: :: GROUP_9:def 34
( IT is strictly_decreasing & ( for s being CompositionSeries of G holds
( not s <> IT or not s is strictly_decreasing or not s is_finer_than IT ) ) );

end;

:: deftheorem Def34 defines jordan_holder GROUP_9:def 34 :

definition

let O be set ;
let G1, G2 be GroupWithOperators of O;
let s1 be CompositionSeries of G1;
let s2 be CompositionSeries of G2;
pred s1 is_equivalent_with s2 means :Def35: :: GROUP_9:def 35
( len s1 = len s2 & ( for n being Nat st n + 1 = len s1 holds
ex p being Permutation of (Seg n) st
for H1 being StableSubgroup of G1
for H2 being StableSubgroup of G2
for N1 being normal StableSubgroup of H1
for N2 being normal StableSubgroup of H2
for i, j being Nat st 1 <= i & i <= n & j = p . i & H1 = s1 . i & H2 = s2 . j & N1 = s1 . (i + 1) & N2 = s2 . (j + 1) holds
H1 ./. N1,H2 ./. N2 are_isomorphic ) );

end;

:: deftheorem Def35 defines is_equivalent_with GROUP_9:def 35 :

definition

let O be set ;
let G be GroupWithOperators of O;
let s be CompositionSeries of G;
func the_series_of_quotients_of s -> FinSequence means :Def36: :: GROUP_9:def 36
( len s = (len it) + 1 & ( for i being Nat st i in dom it holds
for H being StableSubgroup of G
for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds
it . i = H ./. N ) ) if len s > 1
otherwise it = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def36 defines the_series_of_quotients_of GROUP_9:def 36 :

definition

let O be set ;
let f1, f2 be FinSequence;
let p be Permutation of (dom f1);
pred f1,f2 are_equivalent_under p,O means :Def37: :: GROUP_9:def 37
( len f1 = len f2 & ( for H1, H2 being GroupWithOperators of O
for i, j being Nat st i in dom f1 & j = (p ") . i & H1 = f1 . i & H2 = f2 . j holds
H1,H2 are_isomorphic ) );

end;

:: deftheorem Def37 defines are_equivalent_under GROUP_9:def 37 :

theorem Th94: :: GROUP_9:94

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for fs being FinSequence of the_stable_subgroups_of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & fs = Del (s1,i) holds
fs is composition_series

proof end;

theorem Th95: :: GROUP_9:95

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 holds
ex n being Nat st len s1 = (len s2) + n

proof end;

theorem Th96: :: GROUP_9:96

for O being set
for G being GroupWithOperators of O
for s2, s1 being CompositionSeries of G st len s2 = len s1 & s2 is_finer_than s1 holds
s1 = s2

proof end;

theorem Th97: :: GROUP_9:97

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st not s1 is empty & s2 is_finer_than s1 holds
not s2 is empty

proof end;

theorem Th98: :: GROUP_9:98

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s1 is jordan_holder & s2 is jordan_holder holds
s1 = s2

proof end;

Lm36: for P, R being Relation holds
( P = (rng P) | R iff P ~ = (R ~) | (dom (P ~)) )

proof end;

Lm37: for X being set
for P, R being Relation holds P * (R | X) = (X | P) * R

proof end;

Lm38: for n being Nat
for X being set
for f being PartFunc of REAL,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0} holds
Sgm (f .: X) = f * (Sgm X)

proof end;

Lm39: for y being set
for n, i being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds
ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n )

proof end;

theorem Th99: :: GROUP_9:99

for O being set
for G being GroupWithOperators of O
for s1, s19, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s19 = Del (s1,i) & s2 is jordan_holder & s1 is_finer_than s2 holds
s19 is_finer_than s2

proof end;

theorem Th100: :: GROUP_9:100

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & s2 <> s1 & s2 is strictly_decreasing & s2 is_finer_than s1 holds
ex i, j being Nat st
( i in dom s1 & i in dom s2 & i + 1 in dom s1 & i + 1 in dom s2 & j in dom s2 & i + 1 < j & s1 . i = s2 . i & s1 . (i + 1) <> s2 . (i + 1) & s1 . (i + 1) = s2 . j )

proof end;

theorem Th101: :: GROUP_9:101

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for s1 being CompositionSeries of G
for i, j being Nat st i in dom s1 & j in dom s1 & i <= j & H1 = s1 . i & H2 = s1 . j holds
H2 is StableSubgroup of H1

proof end;

theorem Th102: :: GROUP_9:102

for O being set
for G being GroupWithOperators of O
for y being set
for s1 being CompositionSeries of G st y in rng (the_series_of_quotients_of s1) holds
y is strict GroupWithOperators of O

proof end;

theorem Th103: :: GROUP_9:103

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for i being Nat st i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds
H is trivial ) holds
( i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) )

proof end;

theorem Th104: :: GROUP_9:104

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for i being Nat st i in dom s1 & i + 1 in dom s1 & s1 . i = s1 . (i + 1) & s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del ((the_series_of_quotients_of s1),i)

proof end;

theorem :: GROUP_9:105

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for f1 being FinSequence
for i being Nat st f1 = the_series_of_quotients_of s1 & i in dom f1 & ( for H being GroupWithOperators of O st H = f1 . i holds
H is trivial ) holds
( Del (s1,i) is CompositionSeries of G & ( for s2 being CompositionSeries of G st s2 = Del (s1,i) holds
the_series_of_quotients_of s2 = Del (f1,i) ) )

proof end;

theorem Th106: :: GROUP_9:106

for O being set
for f1, f2 being FinSequence
for i, j being Nat st i in dom f1 & ex p being Permutation of (dom f1) st
( f1,f2 are_equivalent_under p,O & j = (p ") . i ) holds
ex p9 being Permutation of (dom (Del (f1,i))) st Del (f1,i), Del (f2,j) are_equivalent_under p9,O

proof end;

theorem Th107: :: GROUP_9:107

for O being set
for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st s1 is empty & s2 is empty holds
s1 is_equivalent_with s2

proof end;

theorem Th108: :: GROUP_9:108

for O being set
for G1, G2 being GroupWithOperators of O
for s1 being CompositionSeries of G1
for s2 being CompositionSeries of G2 st not s1 is empty & not s2 is empty holds
( s1 is_equivalent_with s2 iff ex p being Permutation of (dom (the_series_of_quotients_of s1)) st the_series_of_quotients_of s1, the_series_of_quotients_of s2 are_equivalent_under p,O )

proof end;

theorem Th109: :: GROUP_9:109

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s2 is jordan_holder & len s1 > len s2 holds
ex i being Nat st
( i in dom (the_series_of_quotients_of s1) & ( for H being GroupWithOperators of O st H = (the_series_of_quotients_of s1) . i holds
H is trivial ) )

proof end;

Lm40: for k, m being Element of NAT holds
( k < m iff k <= m - 1 )

proof end;

Lm41: for a being Element of NAT
for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )

proof end;

Lm42: for a being Element of NAT
for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2

proof end;

Lm43: for a being Element of NAT
for fs1, fs2 being FinSequence holds
( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) )

proof end;

Lm44: for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1))

proof end;

theorem Th110: :: GROUP_9:110

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G st len s1 > 1 holds
( s1 is jordan_holder iff for i being Nat st i in dom (the_series_of_quotients_of s1) holds
(the_series_of_quotients_of s1) . i is strict simple GroupWithOperators of O )

proof end;

theorem Th111: :: GROUP_9:111

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G
for i being Nat st 1 <= i & i <= (len s1) - 1 holds
( s1 . i is strict StableSubgroup of G & s1 . (i + 1) is strict StableSubgroup of G )

proof end;

theorem Th112: :: GROUP_9:112

for O being set
for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for s1 being CompositionSeries of G
for i being Nat st 1 <= i & i <= (len s1) - 1 & H1 = s1 . i & H2 = s1 . (i + 1) holds
H2 is normal StableSubgroup of H1

proof end;

theorem Th113: :: GROUP_9:113

for O being set
for G being GroupWithOperators of O
for s1 being CompositionSeries of G holds s1 is_equivalent_with s1

proof end;

theorem Th114: :: GROUP_9:114

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st ( len s1 <= 1 or len s2 <= 1 ) & len s1 <= len s2 holds
s2 is_finer_than s1

proof end;

theorem Th115: :: GROUP_9:115

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is_equivalent_with s2 & s1 is jordan_holder holds
s2 is jordan_holder

proof end;

Lm45: for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G
for k, l being Nat st k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds
ex i, j being Nat st
( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 )

proof end;

Lm46: for O being set
for G being GroupWithOperators of O
for i1, j1, i2, j2 being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 holds
( j1 = j2 & i1 = i2 )

proof end;

Lm47: for O being set
for G being GroupWithOperators of O
for k being integer number
for i, j being Nat
for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds
( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) )

proof end;

begin

definition

let O be set ;
let G be GroupWithOperators of O;
let s1, s2 be CompositionSeries of G;
assume that
A1: len s1 > 1 and
A2: len s2 > 1 ;
func the_schreier_series_of (s1,s2) -> CompositionSeries of G means :Def38: :: GROUP_9:def 38
for k, i, j being Nat
for H1, H2, H3 being StableSubgroup of G holds
( ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 & H1 = s1 . (i + 1) & H2 = s1 . i & H3 = s2 . j implies it . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies it . k = (1). G ) & len it = (((len s1) - 1) * ((len s2) - 1)) + 1 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def38 defines the_schreier_series_of GROUP_9:def 38 :

theorem Th116: :: GROUP_9:116

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_finer_than s1

proof end;

theorem Th117: :: GROUP_9:117

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st len s1 > 1 & len s2 > 1 holds
the_schreier_series_of (s1,s2) is_equivalent_with the_schreier_series_of (s2,s1)

proof end;

theorem Th118: :: GROUP_9:118

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G ex s19, s29 being CompositionSeries of G st
( s19 is_finer_than s1 & s29 is_finer_than s2 & s19 is_equivalent_with s29 )

proof end;

begin

theorem :: GROUP_9:119

for O being set
for G being GroupWithOperators of O
for s1, s2 being CompositionSeries of G st s1 is jordan_holder & s2 is jordan_holder holds
s1 is_equivalent_with s2

proof end;

begin

theorem :: GROUP_9:120

for P, R being Relation holds
( P = (rng P) | R iff P ~ = (R ~) | (dom (P ~)) ) by Lm36;

theorem :: GROUP_9:121

for X being set
for P, R being Relation holds P * (R | X) = (X | P) * R by Lm37;

theorem :: GROUP_9:122

for n being Nat
for X being set
for f being PartFunc of REAL,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0} holds
Sgm (f .: X) = f * (Sgm X) by Lm38;

theorem :: GROUP_9:123

for y being set
for i, n being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds
ex x being set st
( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) by Lm39;

theorem :: GROUP_9:124

for D being non empty set
for f being FinSequence of D
for p being Element of D
for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1)) by Lm44;

theorem :: GROUP_9:125

for G, H being Group
for F1 being FinSequence of the carrier of G
for F2 being FinSequence of the carrier of H
for I being FinSequence of INT
for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds
F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds
f . (Product (F1 |^ I)) = Product (F2 |^ I) by Lm24;