:: by Marco Riccardi

::

:: Received April 20, 2007

:: Copyright (c) 2007-2017 Association of Mizar Users

:: ALG I.3.2 Definition 2

definition

let O, E be set ;

let A be Action of O,E;

let IT be set ;

end;
let A be Action of O,E;

let IT be set ;

pred IT is_stable_under_the_action_of A means :: 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;

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;

:: deftheorem defines is_stable_under_the_action_of GROUP_9:def 1 :

for O, E being set

for A being Action of O,E

for IT being set holds

( IT is_stable_under_the_action_of A iff 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 );

for O, E being set

for A being Action of O,E

for IT being set holds

( IT is_stable_under_the_action_of A iff 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 );

definition

let O, E be set ;

let A be Action of O,E;

let X be Subset of E;

ex b_{1} being Subset of E st

( X c= b_{1} & b_{1} 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

b_{1} c= Y ) )

for b_{1}, b_{2} being Subset of E st X c= b_{1} & b_{1} 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

b_{1} c= Y ) & X c= b_{2} & b_{2} 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

b_{2} c= Y ) holds

b_{1} = b_{2}

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

ex b

( X c= b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines the_stable_subset_generated_by GROUP_9:def 2 :

for O, E being set

for A being Action of O,E

for X, b_{5} being Subset of E holds

( b_{5} = the_stable_subset_generated_by (X,A) iff ( X c= b_{5} & b_{5} 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

b_{5} c= Y ) ) );

for O, E being set

for A being Action of O,E

for X, b

( b

b

definition

let O, E be set ;

let A be Action of O,E;

let F be FinSequence of O;

( ( len F = 0 implies ex b_{1} being Function of E,E st b_{1} = id E ) & ( not len F = 0 implies ex b_{1} being Function of E,E ex PF being FinSequence of Funcs (E,E) st

( b_{1} = 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 ) ) ) ) )

for b_{1}, b_{2} being Function of E,E holds

( ( len F = 0 & b_{1} = id E & b_{2} = id E implies b_{1} = b_{2} ) & ( not len F = 0 & ex PF being FinSequence of Funcs (E,E) st

( b_{1} = 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 ) ) ) & ex PF being FinSequence of Funcs (E,E) st

( b_{2} = 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 ) ) ) implies b_{1} = b_{2} ) )

for b_{1} being Function of E,E holds verum
;

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

( ( len F = 0 implies ex b

( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) )

proof end;

uniqueness for b

( ( len F = 0 & b

( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) & ex PF being FinSequence of Funcs (E,E) st

( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) implies b

proof end;

consistency for b

:: deftheorem Def3 defines Product GROUP_9:def 3 :

for O, E being set

for A being Action of O,E

for F being FinSequence of O

for b_{5} being Function of E,E holds

( ( len F = 0 implies ( b_{5} = Product (F,A) iff b_{5} = id E ) ) & ( not len F = 0 implies ( b_{5} = Product (F,A) iff ex PF being FinSequence of Funcs (E,E) st

( b_{5} = 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 ) ) ) ) ) );

for O, E being set

for A being Action of O,E

for F being FinSequence of O

for b

( ( len F = 0 implies ( b

( b

ex f, g being Function of E,E st

( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ) ) ) );

:: ALG I.3.4 Definition 6

definition

let O be set ;

let G be Group;

let IT be Action of O, the carrier of G;

end;
let G be Group;

let IT be Action of O, the carrier of G;

attr IT is distributive means :: GROUP_9:def 4

for o being Element of O st o in O holds

IT . o is Homomorphism of G,G;

for o being Element of O st o in O holds

IT . o is Homomorphism of G,G;

:: deftheorem defines distributive GROUP_9:def 4 :

for O being set

for G being Group

for IT being Action of O, the carrier of G holds

( IT is distributive iff for o being Element of O st o in O holds

IT . o is Homomorphism of G,G );

for O being set

for G being Group

for IT being Action of O, the carrier of G holds

( IT is distributive iff for o being Element of O st o in O holds

IT . o is Homomorphism of G,G );

definition

let O be set ;

attr c_{2} is strict ;

struct HGrWOpStr over O -> multMagma ;

aggr HGrWOpStr(# carrier, multF, action #) -> HGrWOpStr over O;

sel action c_{2} -> Action of O, the carrier of c_{2};

end;
attr c

struct HGrWOpStr over O -> multMagma ;

aggr HGrWOpStr(# carrier, multF, action #) -> HGrWOpStr over O;

sel action c

registration
end;

:: deftheorem Def5 defines distributive GROUP_9:def 5 :

for O being set

for IT being non empty HGrWOpStr over O holds

( IT is distributive iff 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 );

for O being set

for IT being non empty HGrWOpStr over O holds

( IT is distributive iff 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 );

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

proof end;

Lm2: for O being set

for G being strict Group ex H being non empty HGrWOpStr over 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 ;

existence

ex b_{1} being non empty HGrWOpStr over O st

( b_{1} is strict & b_{1} is distributive & b_{1} is Group-like & b_{1} is associative )

end;
existence

ex b

( b

proof end;

:: ALG I.4.2 Definition 2

definition

let O be set ;

mode GroupWithOperators of O is non empty Group-like associative distributive HGrWOpStr over O;

end;
mode GroupWithOperators of O is non empty Group-like associative distributive HGrWOpStr over O;

definition

let O be set ;

let G be GroupWithOperators of O;

let o be Element of O;

coherence

( ( o in O implies the action of G . o is Homomorphism of G,G ) & ( not o in O implies id the carrier of G is Homomorphism of G,G ) );

consistency

for b_{1} being Homomorphism of G,G holds verum;

end;
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 the action of G . o if o in O

otherwise id the carrier of G;

coherence

( ( o in O implies the action of G . o is Homomorphism of G,G ) & ( not o in O implies id the carrier of G is Homomorphism of G,G ) );

consistency

for b

proof end;

:: deftheorem Def6 defines ^ GROUP_9:def 6 :

for O being set

for G being GroupWithOperators of O

for o being Element of O holds

( ( o in O implies G ^ o = the action of G . o ) & ( not o in O implies G ^ o = id the carrier of G ) );

for O being set

for G being GroupWithOperators of O

for o being Element of O holds

( ( o in O implies G ^ o = the action of G . o ) & ( not o in O implies G ^ o = id the carrier of G ) );

definition

let O be set ;

let G be GroupWithOperators of O;

existence

ex b_{1} being non empty Group-like associative distributive HGrWOpStr over O st

( b_{1} is Subgroup of G & ( for o being Element of O holds b_{1} ^ o = (G ^ o) | the carrier of b_{1} ) );

end;
let G be GroupWithOperators of O;

mode StableSubgroup of G -> non empty Group-like associative distributive HGrWOpStr over 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 ( it is Subgroup of G & ( for o being Element of O holds it ^ o = (G ^ o) | the carrier of it ) );

existence

ex b

( b

proof end;

:: deftheorem Def7 defines StableSubgroup GROUP_9:def 7 :

for O being set

for G being GroupWithOperators of O

for b_{3} being non empty Group-like associative distributive HGrWOpStr over O holds

( b_{3} is StableSubgroup of G iff ( b_{3} is Subgroup of G & ( for o being Element of O holds b_{3} ^ o = (G ^ o) | the carrier of b_{3} ) ) );

for O being set

for G being GroupWithOperators of O

for b

( b

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

correctness

existence

ex b_{1} being StableSubgroup of G st b_{1} is strict ;

end;
let G be GroupWithOperators of O;

correctness

existence

ex b

proof end;

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

ex b_{1} being strict StableSubgroup of G st the carrier of b_{1} = {(1_ G)}

for b_{1}, b_{2} being strict StableSubgroup of G st the carrier of b_{1} = {(1_ G)} & the carrier of b_{2} = {(1_ G)} holds

b_{1} = b_{2}
by Lm4;

end;
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 the carrier of it = {(1_ G)};

ex b

proof end;

uniqueness for b

b

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

for O being set

for G being GroupWithOperators of O

for b_{3} being strict StableSubgroup of G holds

( b_{3} = (1). G iff the carrier of b_{3} = {(1_ G)} );

for O being set

for G being GroupWithOperators of O

for b

( b

definition

let O be set ;

let G be GroupWithOperators of O;

coherence

HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is strict StableSubgroup of G;

by Lm3;

end;
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 HGrWOpStr(# the carrier of G, the multF of G, the action of G #);

coherence

HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is strict StableSubgroup of G;

by Lm3;

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

for O being set

for G being GroupWithOperators of O holds (Omega). G = HGrWOpStr(# the carrier of G, the multF of G, the action of G #);

for O being set

for G being GroupWithOperators of O holds (Omega). G = HGrWOpStr(# the carrier of G, the multF of G, the action of G #);

:: deftheorem Def10 defines normal GROUP_9:def 10 :

for O being set

for G being GroupWithOperators of O

for IT being StableSubgroup of G holds

( IT is normal iff for H being strict Subgroup of G st H = multMagma(# the carrier of IT, the multF of IT #) holds

H is normal );

for O being set

for G being GroupWithOperators of O

for IT being StableSubgroup of G holds

( IT is normal iff for H being strict Subgroup of G st H = multMagma(# the carrier of IT, the multF of IT #) holds

H is normal );

registration

let O be set ;

let G be GroupWithOperators of O;

existence

ex b_{1} being StableSubgroup of G st

( b_{1} is strict & b_{1} is normal )

end;
let G be GroupWithOperators of O;

existence

ex b

( b

proof end;

registration

let O be set ;

let G be GroupWithOperators of O;

let H be StableSubgroup of G;

existence

ex b_{1} being StableSubgroup of H st b_{1} is normal

end;
let G be GroupWithOperators of O;

let H be StableSubgroup of G;

existence

ex b

proof end;

registration

let O be set ;

let G be GroupWithOperators of O;

correctness

coherence

(1). G is normal ;

coherence

(Omega). G is normal ;

end;
let G be GroupWithOperators of O;

correctness

coherence

(1). G is normal ;

proof end;

correctness coherence

(Omega). G is normal ;

proof end;

definition

let O be set ;

let G be GroupWithOperators of O;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is strict StableSubgroup of G )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is strict StableSubgroup of G ) ) & ( for x being object holds

( x in b_{2} iff x is strict StableSubgroup of G ) ) holds

b_{1} = b_{2}

end;
let G be GroupWithOperators of O;

func the_stable_subgroups_of G -> set means :Def11: :: GROUP_9:def 11

for x being object holds

( x in it iff x is strict StableSubgroup of G );

existence for x being object holds

( x in it iff x is strict StableSubgroup of G );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def11 defines the_stable_subgroups_of GROUP_9:def 11 :

for O being set

for G being GroupWithOperators of O

for b_{3} being set holds

( b_{3} = the_stable_subgroups_of G iff for x being object holds

( x in b_{3} iff x is strict StableSubgroup of G ) );

for O being set

for G being GroupWithOperators of O

for b

( b

( x in b

registration

let O be set ;

let G be GroupWithOperators of O;

correctness

coherence

not the_stable_subgroups_of G is empty ;

end;
let G be GroupWithOperators of O;

correctness

coherence

not the_stable_subgroups_of G is empty ;

proof end;

:: deftheorem defines simple GROUP_9:def 12 :

for IT being Group holds

( IT is simple iff ( not IT is trivial & ( for H being strict normal Subgroup of IT holds

( not H <> (Omega). IT or not H <> (1). IT ) ) ) );

for IT being Group holds

( IT is simple iff ( not IT is trivial & ( for H being strict normal Subgroup of IT holds

( not H <> (Omega). IT or not H <> (1). IT ) ) ) );

Lm5: Group_of_Perm 2 is simple

proof end;

:: ALG I.4.4 Definition 7

:: deftheorem Def13 defines simple GROUP_9:def 13 :

for O being set

for IT being GroupWithOperators of O holds

( IT is simple iff ( not IT is trivial & ( for H being strict normal StableSubgroup of IT holds

( not H <> (Omega). IT or not H <> (1). IT ) ) ) );

for O being set

for IT being GroupWithOperators of O holds

( IT is simple iff ( not IT is trivial & ( for H being strict normal StableSubgroup of IT holds

( not H <> (Omega). IT or not H <> (1). IT ) ) ) );

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

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

existence

ex b_{1} being GroupWithOperators of O st

( b_{1} is strict & b_{1} is simple )

end;
existence

ex b

( b

proof end;

definition

let O be set ;

let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

ex b_{1} being set st

for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{1} = Cosets H

for b_{1}, b_{2} being set st ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{1} = Cosets H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{2} = Cosets H ) holds

b_{1} = b_{2}

end;
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 for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

it = Cosets H;

ex b

for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def14 defines Cosets GROUP_9:def 14 :

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for b_{4} being set holds

( b_{4} = Cosets N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{4} = Cosets H );

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for b

( b

b

definition

let O be set ;

let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

ex b_{1} being BinOp of (Cosets N) st

for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{1} = CosOp H

for b_{1}, b_{2} being BinOp of (Cosets N) st ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{1} = CosOp H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{2} = CosOp H ) holds

b_{1} = b_{2}

end;
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 for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

it = CosOp H;

ex b

for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def15 defines CosOp GROUP_9:def 15 :

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

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

( b_{4} = CosOp N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{4} = CosOp H );

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for b

( b

b

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

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

( ( not O is empty implies ex b_{1} being Action of O,(Cosets N) st

for o being Element of O holds b_{1} . 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 ) } ) & ( O is empty implies ex b_{1} being Action of O,(Cosets N) st b_{1} = [:{},{(id (Cosets N))}:] ) )

for b_{1}, b_{2} being Action of O,(Cosets N) holds

( ( not O is empty & ( for o being Element of O holds b_{1} . 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 ) } ) & ( for o being Element of O holds b_{2} . 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 ) } ) implies b_{1} = b_{2} ) & ( O is empty & b_{1} = [:{},{(id (Cosets N))}:] & b_{2} = [:{},{(id (Cosets N))}:] implies b_{1} = b_{2} ) )

consistency

for b_{1} being Action of O,(Cosets N) holds verum;

;

end;
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 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))}:];

( ( not O is empty implies ex b

for o being Element of O holds b

( g in A & h in B & h = (G ^ o) . g ) } ) & ( O is empty implies ex b

proof end;

uniqueness for b

( ( not O is empty & ( for o being Element of O holds b

( g in A & h in B & h = (G ^ o) . g ) } ) & ( for o being Element of O holds b

( g in A & h in B & h = (G ^ o) . g ) } ) implies b

proof end;

correctness consistency

for b

;

:: deftheorem Def16 defines CosAc GROUP_9:def 16 :

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for b_{4} being Action of O,(Cosets N) holds

( ( not O is empty implies ( b_{4} = CosAc N iff for o being Element of O holds b_{4} . 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 ) } ) ) & ( O is empty implies ( b_{4} = CosAc N iff b_{4} = [:{},{(id (Cosets N))}:] ) ) );

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for b

( ( not O is empty implies ( b

( g in A & h in B & h = (G ^ o) . g ) } ) ) & ( O is empty implies ( b

definition

let O be set ;

let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

coherence

HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #) is HGrWOpStr over O;

;

end;
let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

func G ./. N -> HGrWOpStr over O equals :: GROUP_9:def 17

HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);

correctness HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);

coherence

HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #) is HGrWOpStr over O;

;

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

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G holds G ./. N = HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G holds G ./. N = HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #);

registration

let O be set ;

let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

correctness

coherence

not G ./. N is empty ;

coherence

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

end;
let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

correctness

coherence

not G ./. N is empty ;

proof end;

correctness coherence

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

proof end;

:: ALG I.4.2 Definition 3

:: deftheorem Def18 defines homomorphic GROUP_9:def 18 :

for O being set

for G, H being GroupWithOperators of O

for f being Function of G,H holds

( f is homomorphic iff for o being Element of O

for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g) );

for O being set

for G, H being GroupWithOperators of O

for f being Function of G,H holds

( f is homomorphic iff for o being Element of O

for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g) );

registration

let O be set ;

let G, H be GroupWithOperators of O;

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

( b_{1} is multiplicative & b_{1} is homomorphic )

end;
let G, H be GroupWithOperators of O;

cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty total quasi_total multiplicative homomorphic for Element of bool [: the carrier of G, the carrier of H:];

existence ex b

( b

proof 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;
let G, H be GroupWithOperators of O;

mode Homomorphism of G,H is multiplicative homomorphic Function of G,H;

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

coherence

h * h1 is Homomorphism of G,I;

by Lm10;

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

coherence

h * h1 is Homomorphism of G,I;

by Lm10;

definition

let O be set ;

let G, H be GroupWithOperators of O;

reflexivity

for G being GroupWithOperators of O ex h being Homomorphism of G,G st h is bijective

end;
let G, H be GroupWithOperators of O;

reflexivity

for G being GroupWithOperators of O ex h being Homomorphism of G,G st h is bijective

proof end;

:: deftheorem defines are_isomorphic GROUP_9:def 19 :

for O being set

for G, H being GroupWithOperators of O holds

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

for O being set

for G, H being GroupWithOperators of O holds

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

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

for G, H being GroupWithOperators of O st (O,b_{1},b_{2}) holds

(O,b_{2},b_{1})
by Lm11;

end;
let G, H be GroupWithOperators of O;

:: original: are_isomorphic

redefine pred G,H are_isomorphic ;

symmetry

for G, H being GroupWithOperators of O st (O,b

(O,b

definition

let O be set ;

let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

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

for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{1} = nat_hom H

for b_{1}, b_{2} being Homomorphism of G,(G ./. N) st ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{1} = nat_hom H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{2} = nat_hom H ) holds

b_{1} = b_{2}

end;
let G be GroupWithOperators of O;

let N be normal StableSubgroup of G;

func nat_hom N -> Homomorphism of G,(G ./. N) means :Def20: :: GROUP_9:def 20

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 for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

it = nat_hom H;

ex b

for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def20 defines nat_hom GROUP_9:def 20 :

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for b_{4} being Homomorphism of G,(G ./. N) holds

( b_{4} = nat_hom N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds

b_{4} = nat_hom H );

for O being set

for G being GroupWithOperators of O

for N being normal StableSubgroup of G

for b

( b

b

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

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

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

ex b_{1} being strict StableSubgroup 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 StableSubgroup 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 Lm4;

end;
let G, H be GroupWithOperators of O;

let g be Homomorphism of G,H;

func Ker g -> strict StableSubgroup of G means :Def21: :: GROUP_9:def 21

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 Def21 defines Ker GROUP_9:def 21 :

for O being set

for G, H being GroupWithOperators of O

for g being Homomorphism of G,H

for b_{5} being strict StableSubgroup of G holds

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

for O being set

for G, H being GroupWithOperators of O

for g being Homomorphism of G,H

for b

( b

registration

let O be set ;

let G, H be GroupWithOperators of O;

let g be Homomorphism of G,H;

correctness

coherence

Ker g is normal ;

end;
let G, H be GroupWithOperators of O;

let g be Homomorphism of G,H;

correctness

coherence

Ker g is normal ;

proof end;

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

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

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

for b_{1}, b_{2} being strict StableSubgroup 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 Lm4;

end;
let G, H be GroupWithOperators of O;

let g be Homomorphism of G,H;

func Image g -> strict StableSubgroup of H means :Def22: :: GROUP_9:def 22

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 Def22 defines Image GROUP_9:def 22 :

for O being set

for G, H being GroupWithOperators of O

for g being Homomorphism of G,H

for b_{5} being strict StableSubgroup of H holds

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

for O being set

for G, H being GroupWithOperators of O

for g being Homomorphism of G,H

for b

( b

definition

let O be set ;

let G be GroupWithOperators of O;

let H be StableSubgroup of G;

coherence

the carrier of H is Subset of G

end;
let G be GroupWithOperators of O;

let H be StableSubgroup of G;

coherence

the carrier of H is Subset of G

proof end;

:: deftheorem defines carr GROUP_9:def 23 :

for O being set

for G being GroupWithOperators of O

for H being StableSubgroup of G holds carr H = the carrier of H;

for O being set

for G being GroupWithOperators of O

for H being StableSubgroup of G holds carr H = the carrier of H;

definition

let O be set ;

let G be GroupWithOperators of O;

let H1, H2 be StableSubgroup of G;

coherence

(carr H1) * (carr H2) is Subset of G ;

end;
let G be GroupWithOperators of O;

let H1, H2 be StableSubgroup of G;

coherence

(carr H1) * (carr H2) is Subset of G ;

:: deftheorem defines * GROUP_9:def 24 :

for O being set

for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G holds H1 * H2 = (carr H1) * (carr H2);

for O being set

for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G holds H1 * H2 = (carr H1) * (carr H2);

Lm17: for O being set

for G being GroupWithOperators of O

for H being StableSubgroup of G holds 1_ G in H

proof end;

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

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

ex b_{1} being strict StableSubgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2)

for b_{1}, b_{2} being strict StableSubgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2) & the carrier of b_{2} = (carr H1) /\ (carr H2) holds

b_{1} = b_{2}
by Lm4;

commutativity

for b_{1} being strict StableSubgroup of G

for H1, H2 being StableSubgroup of G st the carrier of b_{1} = (carr H1) /\ (carr H2) holds

the carrier of b_{1} = (carr H2) /\ (carr H1)
;

end;
let G be GroupWithOperators of O;

let H1, H2 be StableSubgroup of G;

func H1 /\ H2 -> strict StableSubgroup of G means :Def25: :: GROUP_9:def 25

the carrier of it = (carr H1) /\ (carr H2);

existence the carrier of it = (carr H1) /\ (carr H2);

ex b

proof end;

uniqueness for b

b

commutativity

for b

for H1, H2 being StableSubgroup of G st the carrier of b

the carrier of b

:: deftheorem Def25 defines /\ GROUP_9:def 25 :

for O being set

for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G

for b_{5} being strict StableSubgroup of G holds

( b_{5} = H1 /\ H2 iff the carrier of b_{5} = (carr H1) /\ (carr H2) );

for O being set

for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G

for b

( b

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

:: like GROUP_4:def 5

definition

let O be set ;

let G be GroupWithOperators of O;

let A be Subset of G;

ex b_{1} being strict StableSubgroup of G st

( A c= the carrier of b_{1} & ( for H being strict StableSubgroup of G st A c= the carrier of H holds

b_{1} is StableSubgroup of H ) )

for b_{1}, b_{2} being strict StableSubgroup of G st A c= the carrier of b_{1} & ( for H being strict StableSubgroup of G st A c= the carrier of H holds

b_{1} is StableSubgroup of H ) & A c= the carrier of b_{2} & ( for H being strict StableSubgroup of G st A c= the carrier of H holds

b_{2} is StableSubgroup of H ) holds

b_{1} = b_{2}

end;
let G be GroupWithOperators of O;

let A be Subset of G;

func the_stable_subgroup_of A -> strict StableSubgroup of G means :Def26: :: GROUP_9:def 26

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

ex b

( A c= the carrier of b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def26 defines the_stable_subgroup_of GROUP_9:def 26 :

for O being set

for G being GroupWithOperators of O

for A being Subset of G

for b_{4} being strict StableSubgroup of G holds

( b_{4} = the_stable_subgroup_of A iff ( A c= the carrier of b_{4} & ( for H being strict StableSubgroup of G st A c= the carrier of H holds

b_{4} is StableSubgroup of H ) ) );

for O being set

for G being GroupWithOperators of O

for A being Subset of G

for b

( b

b

definition

let O be set ;

let G be GroupWithOperators of O;

let H1, H2 be StableSubgroup of G;

coherence

the_stable_subgroup_of ((carr H1) \/ (carr H2)) is strict StableSubgroup of G;

;

end;
let G be GroupWithOperators of O;

let H1, H2 be StableSubgroup of G;

func H1 "\/" H2 -> strict StableSubgroup of G equals :: GROUP_9:def 27

the_stable_subgroup_of ((carr H1) \/ (carr H2));

correctness the_stable_subgroup_of ((carr H1) \/ (carr H2));

coherence

the_stable_subgroup_of ((carr H1) \/ (carr H2)) is strict StableSubgroup of G;

;

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

for O being set

for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of ((carr H1) \/ (carr H2));

for O being set

for G being GroupWithOperators of O

for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of ((carr H1) \/ (carr H2));

:: GROUP_2:49

theorem Th1: :: GROUP_9:1

for O being set

for G being GroupWithOperators of O

for H1 being StableSubgroup of G

for x being object st x in H1 holds

x in G

for G being GroupWithOperators of O

for H1 being StableSubgroup of G

for x being object st x in H1 holds

x in G

proof end;

:: GROUP_2:51

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

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;

:: GROUP_2:52

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

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;

:: GROUP_2:53

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

for G being GroupWithOperators of O

for H1 being StableSubgroup of G holds 1_ G = 1_ H1

proof end;

:: GROUP_2:55

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

for G being GroupWithOperators of O

for H1 being StableSubgroup of G holds 1_ G in H1 by Lm17;

:: GROUP_2:57

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 "

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;

:: GROUP_2:59

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

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

:: GROUP_2:60

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

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

:: GROUP_2:61

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

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

:: GROUP_2:63

:: GROUP_2:65

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

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;

:: GROUP_2:66

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

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

:: GROUP_2:67

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

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;

:: GROUP_2:68

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

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

:: GROUP_2:75

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_2:77

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_2:93

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)

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;

:: GROUP_2:97

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

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;

:: GROUP_2:100

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

for G being GroupWithOperators of O

for H being strict StableSubgroup of G holds H /\ H = H

proof end;

:: GROUP_2:102

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)

for G being GroupWithOperators of O

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

proof end;

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

:: GROUP_2:103

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 )

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;

:: GROUP_2:167

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_3:149

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)

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;

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

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

:: GROUP_4:37

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

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;

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

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

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

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 ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A))

proof end;

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

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

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

:: GROUP_4:40

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_4:41

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

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_{1}() -> set , F_{2}() -> GroupWithOperators of F_{1}(), P_{1}[ set ] } :

MeetSbgWOpEx{ F

ex H being strict StableSubgroup of F_{2}() st the carrier of H = meet { A where A is Subset of F_{2}() : ex K being strict StableSubgroup of F_{2}() st

( A = the carrier of K & P_{1}[K] ) }

provided
( A = the carrier of K & P

proof end;

:: GROUP_4:43

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

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;

Lm31: for O being set

for G being GroupWithOperators of O

for A, B being Subset of G st B = the carrier of (gr A) holds

the_stable_subgroup_of A = the_stable_subgroup_of B

proof end;

:: GROUP_4:64

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_4:68

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)

for G being GroupWithOperators of O

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

proof end;

:: GROUP_4:69

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

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;

:: GROUP_4:71

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

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;

:: GROUP_4:72

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

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;

:: GROUP_4:76

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 )

for G being GroupWithOperators of O

for H being strict StableSubgroup of G holds

( ((1). G) "\/" H = H & H "\/" ((1). G) = H )

proof end;

:: GROUP_4:77

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 )

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;

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

:: GROUP_4:78

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 )

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;

:: GROUP_4:79

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 )

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;

:: GROUP_4:81

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

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;

:: GROUP_4:82

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

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;

:: GROUP_6:3

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

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;

:: GROUP_6:9

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

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;

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

:: GROUP_6:10

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 )

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;

:: GROUP_6:13

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

:: GROUP_6:29

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_6:35

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

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;

:: GROUP_6:40

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

for G, H being GroupWithOperators of O

for h being Homomorphism of G,H holds h . (1_ G) = 1_ H by Lm12;

:: GROUP_6:41

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

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

:: GROUP_6:50

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 )

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;

:: GROUP_6:52

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_6:53

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)

for G, H being GroupWithOperators of O

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

proof end;

:: GROUP_6:57

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

for G being GroupWithOperators of O

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

proof end;

:: GROUP_6:67

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 )

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;

:: GROUP_6:68

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

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;

:: GROUP_6:69

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

for G being GroupWithOperators of O

for N being normal StableSubgroup of G holds nat_hom N is onto

proof end;

:: GROUP_6:75

:: GROUP_6:78

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

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

G,I are_isomorphic

proof end;

:: GROUP_6:82

:: GROUP_6:83

:: GROUP_6:87

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

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

H is trivial

proof end;

:: GROUP_6:90

theorem Th59: :: GROUP_9:59

for O being set

for G, H being GroupWithOperators of O

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

for G, H being GroupWithOperators of O

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

proof end;

:: GRSOLV_1:1

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

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;

theorem :: GROUP_9:61

theorem :: GROUP_9:63

theorem :: GROUP_9:64

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

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

theorem :: GROUP_9:66

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

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

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

theorem :: GROUP_9:69

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

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

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

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

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

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

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

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

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

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

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

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

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

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;

:: ALG I.4.6 Proposition 7(a)

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

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;

:: ALG I.4.6 Proposition 7(b)

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

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)

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)

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

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)

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

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

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

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

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

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)

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

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;

:: ALG I.4.6 Corollary 2

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

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;

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

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)

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

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;

:: ALG I.4.7 Definition 9

definition
end;

:: deftheorem Def28 defines composition_series GROUP_9:def 28 :

for O being set

for G being GroupWithOperators of O

for IT being FinSequence of the_stable_subgroups_of G holds

( IT is composition_series iff ( 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 ) ) );

for O being set

for G being GroupWithOperators of O

for IT being FinSequence of the_stable_subgroups_of G holds

( IT is composition_series iff ( 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 ) ) );

registration

let O be set ;

let G be GroupWithOperators of O;

ex b_{1} being FinSequence of the_stable_subgroups_of G st b_{1} is composition_series

end;
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 for FinSequence of the_stable_subgroups_of G;

existence ex b

proof 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;
let G be GroupWithOperators of O;

mode CompositionSeries of G is composition_series FinSequence of the_stable_subgroups_of G;

:: ALG I.4.7 Definition 9

definition

let O be set ;

let G be GroupWithOperators of O;

let s1, s2 be CompositionSeries of G;

for s1 being CompositionSeries of G ex x being set st

( x c= dom s1 & s1 = s1 * (Sgm x) )

end;
let G be GroupWithOperators of O;

let s1, s2 be CompositionSeries of G;

pred s1 is_finer_than s2 means :: GROUP_9:def 29

ex x being set st

( x c= dom s1 & s2 = s1 * (Sgm x) );

reflexivity ex x being set st

( x c= dom s1 & s2 = s1 * (Sgm x) );

for s1 being CompositionSeries of G ex x being set st

( x c= dom s1 & s1 = s1 * (Sgm x) )

proof end;

:: deftheorem defines is_finer_than GROUP_9:def 29 :

for O being set

for G being GroupWithOperators of O

for s1, s2 being CompositionSeries of G holds

( s1 is_finer_than s2 iff ex x being set st

( x c= dom s1 & s2 = s1 * (Sgm x) ) );

for O being set

for G being GroupWithOperators of O

for s1, s2 being CompositionSeries of G holds

( s1 is_finer_than s2 iff ex x being set st

( x c= dom s1 & s2 = s1 * (Sgm x) ) );

definition

let O be set ;

let G be GroupWithOperators of O;

let IT be CompositionSeries of G;

end;
let G be GroupWithOperators of O;

let IT be CompositionSeries of G;

attr IT is strictly_decreasing means :: GROUP_9:def 30

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 ;

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 ;

:: deftheorem defines strictly_decreasing GROUP_9:def 30 :

for O being set

for G being GroupWithOperators of O

for IT being CompositionSeries of G holds

( IT is strictly_decreasing iff 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 );

for O being set

for G being GroupWithOperators of O

for IT being CompositionSeries of G holds

( IT is strictly_decreasing iff 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 );

:: ALG I.4.7 Definition 10

definition

let O be set ;

let G be GroupWithOperators of O;

let IT be CompositionSeries of G;

end;
let G be GroupWithOperators of O;

let IT be CompositionSeries of G;

attr IT is jordan_holder means :: GROUP_9:def 31

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

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

:: deftheorem defines jordan_holder GROUP_9:def 31 :

for O being set

for G being GroupWithOperators of O

for IT being CompositionSeries of G holds

( IT is jordan_holder iff ( 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 ) ) ) );

for O being set

for G being GroupWithOperators of O

for IT being CompositionSeries of G holds

( IT is jordan_holder iff ( 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 ) ) ) );

:: ALG I.4.7 Definition 9

definition

let O be set ;

let G1, G2 be GroupWithOperators of O;

let s1 be CompositionSeries of G1;

let s2 be CompositionSeries of G2;

end;
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 :: GROUP_9:def 32

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

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

:: deftheorem defines is_equivalent_with GROUP_9:def 32 :

for O being set

for G1, G2 being GroupWithOperators of O

for s1 being CompositionSeries of G1

for s2 being CompositionSeries of G2 holds

( s1 is_equivalent_with s2 iff ( 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 ) ) );

for O being set

for G1, G2 being GroupWithOperators of O

for s1 being CompositionSeries of G1

for s2 being CompositionSeries of G2 holds

( s1 is_equivalent_with s2 iff ( 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 ) ) );

:: ALG I.4.7 Definition 9

definition

let O be set ;

let G be GroupWithOperators of O;

let s be CompositionSeries of G;

( ( len s > 1 implies ex b_{1} being FinSequence st

( len s = (len b_{1}) + 1 & ( for i being Nat st i in dom b_{1} holds

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b_{1} . i = H ./. N ) ) ) & ( not len s > 1 implies ex b_{1} being FinSequence st b_{1} = {} ) )

for b_{1}, b_{2} being FinSequence holds

( ( len s > 1 & len s = (len b_{1}) + 1 & ( for i being Nat st i in dom b_{1} holds

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b_{1} . i = H ./. N ) & len s = (len b_{2}) + 1 & ( for i being Nat st i in dom b_{2} holds

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b_{2} . i = H ./. N ) implies b_{1} = b_{2} ) & ( not len s > 1 & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

for b_{1} being FinSequence holds verum
;

end;
let G be GroupWithOperators of O;

let s be CompositionSeries of G;

func the_series_of_quotients_of s -> FinSequence means :Def33: :: GROUP_9:def 33

( 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 ( 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 = {} ;

( ( len s > 1 implies ex b

( len s = (len b

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b

proof end;

uniqueness for b

( ( len s > 1 & len s = (len b

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b

proof end;

consistency for b

:: deftheorem Def33 defines the_series_of_quotients_of GROUP_9:def 33 :

for O being set

for G being GroupWithOperators of O

for s being CompositionSeries of G

for b_{4} being FinSequence holds

( ( len s > 1 implies ( b_{4} = the_series_of_quotients_of s iff ( len s = (len b_{4}) + 1 & ( for i being Nat st i in dom b_{4} holds

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b_{4} . i = H ./. N ) ) ) ) & ( not len s > 1 implies ( b_{4} = the_series_of_quotients_of s iff b_{4} = {} ) ) );

for O being set

for G being GroupWithOperators of O

for s being CompositionSeries of G

for b

( ( len s > 1 implies ( b

for H being StableSubgroup of G

for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds

b

definition

let O be set ;

let f1, f2 be FinSequence;

let p be Permutation of (dom f1);

end;
let f1, f2 be FinSequence;

let p be Permutation of (dom f1);

pred f1,f2 are_equivalent_under p,O means :: GROUP_9:def 34

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

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

:: deftheorem defines are_equivalent_under GROUP_9:def 34 :

for O being set

for f1, f2 being FinSequence

for p being Permutation of (dom f1) holds

( f1,f2 are_equivalent_under p,O iff ( 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 ) ) );

for O being set

for f1, f2 being FinSequence

for p being Permutation of (dom f1) holds

( f1,f2 are_equivalent_under p,O iff ( 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 ) ) );

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

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

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 s1, s2 being CompositionSeries of G st len s2 = len s1 & s2 is_finer_than s1 holds

s1 = s2

for G being GroupWithOperators of O

for s1, s2 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 ;

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 ;

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

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 ;

Lm35: for P, R being Relation holds

( P = (rng P) |` R iff P ~ = (R ~) | (dom (P ~)) )

proof end;

Lm36: for X being set

for P, R being Relation holds P * (R | X) = (X |` P) * R

proof end;

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

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

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

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 )

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

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

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

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)

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

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

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

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 ;

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 )

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

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;

Lm39: for k, m being Element of NAT holds

( k < m iff k <= m - 1 )

proof end;

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

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

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

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

:: ALG I.4.7 Proposition 9

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 )

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 )

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

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

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

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

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;

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

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

Lm46: for O being set

for G being GroupWithOperators of O

for k being Integer

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;

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 ;

ex b_{1} being CompositionSeries of G st

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 b_{1} . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b_{1} . k = (1). G ) & len b_{1} = (((len s1) - 1) * ((len s2) - 1)) + 1 )

for b_{1}, b_{2} being CompositionSeries of G st ( 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 b_{1} . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b_{1} . k = (1). G ) & len b_{1} = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) & ( 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 b_{2} . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b_{2} . k = (1). G ) & len b_{2} = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) holds

b_{1} = b_{2}

end;
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 :Def35: :: GROUP_9:def 35

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

ex b

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 b

proof end;

uniqueness for b

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 b

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 b

b

proof end;

:: deftheorem Def35 defines the_schreier_series_of GROUP_9:def 35 :

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

for b_{5} being CompositionSeries of G holds

( b_{5} = the_schreier_series_of (s1,s2) iff 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 b_{5} . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b_{5} . k = (1). G ) & len b_{5} = (((len s1) - 1) * ((len s2) - 1)) + 1 ) );

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

for b

( b

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 b

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

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)

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 )

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;

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

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;

theorem :: GROUP_9:120

theorem :: GROUP_9:121

theorem :: GROUP_9:122

theorem :: GROUP_9:123

theorem :: GROUP_9:124

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

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