:: The {J}ordan-H\"older Theorem :: by Marco Riccardi :: :: Received April 20, 2007 :: Copyright (c) 2007-2012 Association of Mizar Users begin :: ALG I.3.2 Definition 2 definition let O, E be set ; let A be Action of O,E; let IT be set ; predIT is_stable_under_the_action_of A means :Def1: :: GROUP_9:def 1 for o being Element of O for f being Function of E,E st o in O & f = A . o holds f .: IT c= IT; end; :: deftheorem Def1 defines is_stable_under_the_action_of GROUP_9:def_1_:_ 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 ); Lm1: for O, E being set for A being Action of O,E holds [#] E is_stable_under_the_action_of A proofend; definition let O, E be set ; let A be Action of O,E; let X be Subset of E; func the_stable_subset_generated_by (X,A) -> Subset of E means :Def2: :: GROUP_9:def 2 ( X c= it & it is_stable_under_the_action_of A & ( for Y being Subset of E st Y is_stable_under_the_action_of A & X c= Y holds it c= Y ) ); existence ex b1 being Subset of E st ( X c= b1 & b1 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 b1 c= Y ) ) proofend; uniqueness for b1, b2 being Subset of E st X c= b1 & b1 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 b1 c= Y ) & X c= b2 & b2 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 b2 c= Y ) holds b1 = b2 proofend; 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, b5 being Subset of E holds ( b5 = the_stable_subset_generated_by (X,A) iff ( X c= b5 & b5 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 b5 c= Y ) ) ); definition let O, E be set ; let A be Action of O,E; let F be FinSequence of O; func Product (F,A) -> Function of E,E means :Def3: :: GROUP_9:def 3 it = id E if len F = 0 otherwise ex PF being FinSequence of Funcs (E,E) st ( it = PF . (len F) & len PF = len F & PF . 1 = A . (F . 1) & ( for n being Nat st n <> 0 & n < len F holds ex f, g being Function of E,E st ( f = PF . n & g = A . (F . (n + 1)) & PF . (n + 1) = f * g ) ) ); existence ( ( len F = 0 implies ex b1 being Function of E,E st b1 = id E ) & ( not len F = 0 implies ex b1 being Function of E,E ex PF being FinSequence of Funcs (E,E) st ( b1 = 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 ) ) ) ) ) proofend; uniqueness for b1, b2 being Function of E,E holds ( ( len F = 0 & b1 = id E & b2 = id E implies b1 = b2 ) & ( not len F = 0 & ex PF being FinSequence of Funcs (E,E) st ( b1 = 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 ( b2 = 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 b1 = b2 ) ) proofend; consistency for b1 being Function of E,E holds verum ; end; :: 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 b5 being Function of E,E holds ( ( len F = 0 implies ( b5 = Product (F,A) iff b5 = id E ) ) & ( not len F = 0 implies ( b5 = Product (F,A) iff ex PF being FinSequence of Funcs (E,E) st ( b5 = 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 ) ) ) ) ) ); :: 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; attrIT is distributive means :Def4: :: GROUP_9:def 4 for o being Element of O st o in O holds IT . o is Homomorphism of G,G; end; :: deftheorem Def4 defines distributive GROUP_9:def_4_:_ 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 ; attrc2 is strict ; struct HGrWOpStr over O -> multMagma ; aggrHGrWOpStr(# carrier, multF, action #) -> HGrWOpStr over O; sel action c2 -> Action of O, the carrier of c2; end; registration let O be set ; cluster non empty for HGrWOpStr over O; existence not for b1 being HGrWOpStr over O holds b1 is empty proofend; end; definition let O be set ; let IT be non empty HGrWOpStr over O; attrIT is distributive means :Def5: :: GROUP_9:def 5 for G being Group for a being Action of O, the carrier of G st a = the action of IT & multMagma(# the carrier of G, the multF of G #) = multMagma(# the carrier of IT, the multF of IT #) holds a is distributive ; end; :: deftheorem Def5 defines distributive GROUP_9:def_5_:_ 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 ); Lm2: for O, E being set holds [:O,{(id E)}:] is Action of O,E proofend; Lm3: 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 #) ) proofend; registration let O be set ; cluster non empty Group-like associative strict distributive for HGrWOpStr over O; existence ex b1 being non empty HGrWOpStr over O st ( b1 is strict & b1 is distributive & b1 is Group-like & b1 is associative ) proofend; 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; definition let O be set ; let G be GroupWithOperators of O; let o be Element of O; funcG ^ 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 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 b1 being Homomorphism of G,G holds verum; proofend; 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 ) ); definition let O be set ; 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 existence ex b1 being non empty Group-like associative distributive HGrWOpStr over O st ( b1 is Subgroup of G & ( for o being Element of O holds b1 ^ o = (G ^ o) | the carrier of b1 ) ); proofend; end; :: deftheorem Def7 defines StableSubgroup GROUP_9:def_7_:_ for O being set for G being GroupWithOperators of O for b3 being non empty Group-like associative distributive HGrWOpStr over O holds ( b3 is StableSubgroup of G iff ( b3 is Subgroup of G & ( for o being Element of O holds b3 ^ o = (G ^ o) | the carrier of b3 ) ) ); Lm4: for O being set for G being GroupWithOperators of O holds HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is StableSubgroup of G proofend; registration let O be set ; let G be GroupWithOperators of O; cluster non empty unital Group-like associative strict distributive for StableSubgroup of G; correctness existence ex b1 being StableSubgroup of G st b1 is strict ; proofend; end; Lm5: for O being set for G being GroupWithOperators of O for H1, H2 being strict StableSubgroup of G st the carrier of H1 = the carrier of H2 holds H1 = H2 proofend; definition let O be set ; let G be GroupWithOperators of O; func (1). G -> strict StableSubgroup of G means :Def8: :: GROUP_9:def 8 the carrier of it = {(1_ G)}; existence ex b1 being strict StableSubgroup of G st the carrier of b1 = {(1_ G)} proofend; uniqueness for b1, b2 being strict StableSubgroup of G st the carrier of b1 = {(1_ G)} & the carrier of b2 = {(1_ G)} holds b1 = b2 by Lm5; end; :: deftheorem Def8 defines (1). GROUP_9:def_8_:_ for O being set for G being GroupWithOperators of O for b3 being strict StableSubgroup of G holds ( b3 = (1). G iff the carrier of b3 = {(1_ G)} ); definition let O be set ; let G be GroupWithOperators of O; func (Omega). G -> strict StableSubgroup of G equals :: GROUP_9:def 9 HGrWOpStr(# the carrier of G, the multF of G, the action of G #); correctness coherence HGrWOpStr(# the carrier of G, the multF of G, the action of G #) is strict StableSubgroup of G; by Lm4; end; :: 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 #); definition let O be set ; let G be GroupWithOperators of O; let IT be StableSubgroup of G; attrIT is normal means :Def10: :: GROUP_9:def 10 for H being strict Subgroup of G st H = multMagma(# the carrier of IT, the multF of IT #) holds H is normal ; end; :: deftheorem Def10 defines normal GROUP_9:def_10_:_ 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; cluster non empty unital Group-like associative strict distributive normal for StableSubgroup of G; existence ex b1 being StableSubgroup of G st ( b1 is strict & b1 is normal ) proofend; end; registration let O be set ; let G be GroupWithOperators of O; let H be StableSubgroup of G; cluster non empty unital Group-like associative distributive normal for StableSubgroup of H; existence ex b1 being StableSubgroup of H st b1 is normal proofend; end; registration let O be set ; let G be GroupWithOperators of O; cluster (1). G -> strict normal ; correctness coherence (1). G is normal ; proofend; cluster (Omega). G -> strict normal ; correctness coherence (Omega). G is normal ; proofend; end; definition let O be set ; let G be GroupWithOperators of O; func the_stable_subgroups_of G -> set means :Def11: :: GROUP_9:def 11 for x being set holds ( x in it iff x is strict StableSubgroup of G ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict StableSubgroup of G ) proofend; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict StableSubgroup of G ) ) & ( for x being set holds ( x in b2 iff x is strict StableSubgroup of G ) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines the_stable_subgroups_of GROUP_9:def_11_:_ for O being set for G being GroupWithOperators of O for b3 being set holds ( b3 = the_stable_subgroups_of G iff for x being set holds ( x in b3 iff x is strict StableSubgroup of G ) ); registration let O be set ; let G be GroupWithOperators of O; cluster the_stable_subgroups_of G -> non empty ; correctness coherence not the_stable_subgroups_of G is empty ; proofend; end; definition let IT be Group; attrIT is simple means :Def12: :: GROUP_9:def 12 ( not IT is trivial & ( for H being strict normal Subgroup of IT holds ( not H <> (Omega). IT or not H <> (1). IT ) ) ); end; :: deftheorem Def12 defines simple GROUP_9:def_12_:_ 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 ) ) ) ); Lm6: Group_of_Perm 2 is simple proofend; registration cluster non empty strict unital Group-like associative simple for multMagma ; existence ex b1 being Group st ( b1 is strict & b1 is simple ) by Lm6; end; :: ALG I.4.4 Definition 7 definition let O be set ; let IT be GroupWithOperators of O; attrIT is simple means :Def13: :: GROUP_9:def 13 ( not IT is trivial & ( for H being strict normal StableSubgroup of IT holds ( not H <> (Omega). IT or not H <> (1). IT ) ) ); end; :: deftheorem Def13 defines simple GROUP_9:def_13_:_ 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 ) ) ) ); Lm7: for O being set for G being GroupWithOperators of O for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G proofend; Lm8: for G1, G2 being Group for A1 being Subset of G1 for A2 being Subset of G2 for H1 being strict Subgroup of G1 for H2 being strict Subgroup of G2 st multMagma(# the carrier of G1, the multF of G1 #) = multMagma(# the carrier of G2, the multF of G2 #) & A1 = A2 & H1 = H2 holds ( A1 * H1 = A2 * H2 & H1 * A1 = H2 * A2 ) proofend; registration let O be set ; cluster non empty unital Group-like associative strict distributive simple for HGrWOpStr over O; existence ex b1 being GroupWithOperators of O st ( b1 is strict & b1 is simple ) proofend; end; definition let O be set ; let G be GroupWithOperators of O; let N be normal StableSubgroup of G; func Cosets N -> set means :Def14: :: GROUP_9:def 14 for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds it = Cosets H; existence ex b1 being set st for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b1 = Cosets H proofend; uniqueness for b1, b2 being set st ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b1 = Cosets H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b2 = Cosets H ) holds b1 = b2 proofend; 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 b4 being set holds ( b4 = Cosets N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b4 = Cosets H ); definition let O be set ; let G be GroupWithOperators of O; let N be normal StableSubgroup of G; func CosOp N -> BinOp of (Cosets N) means :Def15: :: GROUP_9:def 15 for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds it = CosOp H; existence ex b1 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 b1 = CosOp H proofend; uniqueness for b1, b2 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 b1 = CosOp H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b2 = CosOp H ) holds b1 = b2 proofend; 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 b4 being BinOp of (Cosets N) holds ( b4 = CosOp N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b4 = CosOp H ); Lm9: for G being Group for N being normal Subgroup of G for A being Element of Cosets N for g being Element of G holds ( g in A iff A = g * N ) proofend; Lm10: for O being set for o being Element of O for G being GroupWithOperators of O for H being StableSubgroup of G for g being Element of G st g in H holds (G ^ o) . g in H proofend; definition let O be set ; let G be GroupWithOperators of O; let N be normal StableSubgroup of G; func CosAc N -> Action of O,(Cosets N) means :Def16: :: GROUP_9:def 16 for o being Element of O holds it . o = { [A,B] where A, B is Element of Cosets N : ex g, h being Element of G st ( g in A & h in B & h = (G ^ o) . g ) } if not O is empty otherwise it = [:{},{(id (Cosets N))}:]; existence ( ( not O is empty implies ex b1 being Action of O,(Cosets N) st for o being Element of O holds b1 . 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 b1 being Action of O,(Cosets N) st b1 = [:{},{(id (Cosets N))}:] ) ) proofend; uniqueness for b1, b2 being Action of O,(Cosets N) holds ( ( not O is empty & ( for o being Element of O holds b1 . 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 b2 . 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 b1 = b2 ) & ( O is empty & b1 = [:{},{(id (Cosets N))}:] & b2 = [:{},{(id (Cosets N))}:] implies b1 = b2 ) ) proofend; correctness consistency for b1 being Action of O,(Cosets N) holds verum; ; end; :: 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 b4 being Action of O,(Cosets N) holds ( ( not O is empty implies ( b4 = CosAc N iff for o being Element of O holds b4 . 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 ( b4 = CosAc N iff b4 = [:{},{(id (Cosets N))}:] ) ) ); definition let O be set ; let G be GroupWithOperators of O; let N be normal StableSubgroup of G; funcG ./. N -> HGrWOpStr over O equals :: GROUP_9:def 17 HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #); correctness coherence HGrWOpStr(# (Cosets N),(CosOp N),(CosAc N) #) is HGrWOpStr over O; ; end; :: 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) #); registration let O be set ; let G be GroupWithOperators of O; let N be normal StableSubgroup of G; clusterG ./. N -> non empty ; correctness coherence not G ./. N is empty ; proofend; clusterG ./. N -> Group-like associative distributive ; correctness coherence ( G ./. N is distributive & G ./. N is Group-like & G ./. N is associative ); proofend; end; :: ALG I.4.2 Definition 3 definition let O be set ; let G, H be GroupWithOperators of O; let f be Function of G,H; attrf is homomorphic means :Def18: :: GROUP_9:def 18 for o being Element of O for g being Element of G holds f . ((G ^ o) . g) = (H ^ o) . (f . g); end; :: deftheorem Def18 defines homomorphic GROUP_9:def_18_:_ 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; 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 b1 being Function of G,H st ( b1 is multiplicative & b1 is homomorphic ) proofend; end; definition let O be set ; let G, H be GroupWithOperators of O; mode Homomorphism of G,H is multiplicative homomorphic Function of G,H; end; Lm11: for O being set for G, H, I being GroupWithOperators of O for h being Homomorphism of G,H for h1 being Homomorphism of H,I holds h1 * h is Homomorphism of G,I proofend; 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 funch1 * h -> Homomorphism of G,I; correctness coherence h * h1 is Homomorphism of G,I; by Lm11; end; definition let O be set ; let G, H be GroupWithOperators of O; predG,H are_isomorphic means :Def19: :: GROUP_9:def 19 ex h being Homomorphism of G,H st h is bijective ; reflexivity for G being GroupWithOperators of O ex h being Homomorphism of G,G st h is bijective proofend; end; :: deftheorem Def19 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 ); Lm12: for O being set for G, H being GroupWithOperators of O st G,H are_isomorphic holds H,G are_isomorphic proofend; definition let O be set ; let G, H be GroupWithOperators of O; :: original:are_isomorphic redefine predG,H are_isomorphic ; symmetry for G, H being GroupWithOperators of O st (O,b1,b2) holds (O,b2,b1) by Lm12; end; definition let O be set ; let G be GroupWithOperators of O; let N be normal StableSubgroup of G; func nat_hom N -> Homomorphism of G,(G ./. N) means :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 ex b1 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 b1 = nat_hom H proofend; uniqueness for b1, b2 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 b1 = nat_hom H ) & ( for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b2 = nat_hom H ) holds b1 = b2 proofend; 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 b4 being Homomorphism of G,(G ./. N) holds ( b4 = nat_hom N iff for H being strict normal Subgroup of G st H = multMagma(# the carrier of N, the multF of N #) holds b4 = nat_hom H ); Lm13: for O being set for G, H being GroupWithOperators of O for g being Homomorphism of G,H holds g . (1_ G) = 1_ H proofend; Lm14: for O being set for G, H being GroupWithOperators of O for a being Element of G for g being Homomorphism of G,H holds g . (a ") = (g . a) " proofend; Lm15: for O being set for G being GroupWithOperators of O for A being Subset of G st A <> {} & ( for g1, g2 being Element of G st g1 in A & g2 in A holds g1 * g2 in A ) & ( for g being Element of G st g in A holds g " in A ) & ( for o being Element of O for g being Element of G st g in A holds (G ^ o) . g in A ) holds ex H being strict StableSubgroup of G st the carrier of H = A proofend; definition let O be set ; let G, H be GroupWithOperators of O; let g be Homomorphism of G,H; func Ker g -> strict StableSubgroup of G means :Def21: :: GROUP_9:def 21 the carrier of it = { a where a is Element of G : g . a = 1_ H } ; existence ex b1 being strict StableSubgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H } proofend; uniqueness for b1, b2 being strict StableSubgroup of G st the carrier of b1 = { a where a is Element of G : g . a = 1_ H } & the carrier of b2 = { a where a is Element of G : g . a = 1_ H } holds b1 = b2 by Lm5; end; :: 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 b5 being strict StableSubgroup of G holds ( b5 = Ker g iff the carrier of b5 = { a where a is Element of G : g . a = 1_ H } ); registration let O be set ; let G, H be GroupWithOperators of O; let g be Homomorphism of G,H; cluster Ker g -> strict normal ; correctness coherence Ker g is normal ; proofend; end; Lm16: for O being set for G being GroupWithOperators of O for H being StableSubgroup of G holds multMagma(# the carrier of H, the multF of H #) is strict Subgroup of G proofend; Lm17: for O being set for G, H being GroupWithOperators of O for G9 being strict StableSubgroup of G for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9 proofend; definition let O be set ; let G, H be GroupWithOperators of O; let g be Homomorphism of G,H; func Image g -> strict StableSubgroup of H means :Def22: :: GROUP_9:def 22 the carrier of it = g .: the carrier of G; existence ex b1 being strict StableSubgroup of H st the carrier of b1 = g .: the carrier of G proofend; uniqueness for b1, b2 being strict StableSubgroup of H st the carrier of b1 = g .: the carrier of G & the carrier of b2 = g .: the carrier of G holds b1 = b2 by Lm5; end; :: 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 b5 being strict StableSubgroup of H holds ( b5 = Image g iff the carrier of b5 = g .: the carrier of G ); definition let O be set ; let G be GroupWithOperators of O; let H be StableSubgroup of G; func carr H -> Subset of G equals :: GROUP_9:def 23 the carrier of H; coherence the carrier of H is Subset of G proofend; 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; definition let O be set ; let G be GroupWithOperators of O; let H1, H2 be StableSubgroup of G; funcH1 * H2 -> Subset of G equals :: GROUP_9:def 24 (carr H1) * (carr H2); coherence (carr H1) * (carr H2) is Subset of G ; end; :: 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); Lm18: for O being set for G being GroupWithOperators of O for H being StableSubgroup of G holds 1_ G in H proofend; Lm19: for O being set for G being GroupWithOperators of O for H being StableSubgroup of G for g1, g2 being Element of G st g1 in H & g2 in H holds g1 * g2 in H proofend; Lm20: for O being set for G being GroupWithOperators of O for H being StableSubgroup of G for g being Element of G st g in H holds g " in H proofend; definition let O be set ; let G be GroupWithOperators of O; let H1, H2 be StableSubgroup of G; funcH1 /\ H2 -> strict StableSubgroup of G means :Def25: :: GROUP_9:def 25 the carrier of it = (carr H1) /\ (carr H2); existence ex b1 being strict StableSubgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) proofend; uniqueness for b1, b2 being strict StableSubgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) & the carrier of b2 = (carr H1) /\ (carr H2) holds b1 = b2 by Lm5; commutativity for b1 being strict StableSubgroup of G for H1, H2 being StableSubgroup of G st the carrier of b1 = (carr H1) /\ (carr H2) holds the carrier of b1 = (carr H2) /\ (carr H1) ; end; :: 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 b5 being strict StableSubgroup of G holds ( b5 = H1 /\ H2 iff the carrier of b5 = (carr H1) /\ (carr H2) ); Lm21: for O being set for G being GroupWithOperators of O for H1, H2 being StableSubgroup of G st the carrier of H1 c= the carrier of H2 holds H1 is StableSubgroup of H2 proofend; :: like GROUP_4:def 5 definition let O be set ; let G be GroupWithOperators of O; let A be Subset of G; func the_stable_subgroup_of A -> strict StableSubgroup of G means :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 ex b1 being strict StableSubgroup of G st ( A c= the carrier of b1 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds b1 is StableSubgroup of H ) ) proofend; uniqueness for b1, b2 being strict StableSubgroup of G st A c= the carrier of b1 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds b1 is StableSubgroup of H ) & A c= the carrier of b2 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds b2 is StableSubgroup of H ) holds b1 = b2 proofend; 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 b4 being strict StableSubgroup of G holds ( b4 = the_stable_subgroup_of A iff ( A c= the carrier of b4 & ( for H being strict StableSubgroup of G st A c= the carrier of H holds b4 is StableSubgroup of H ) ) ); definition let O be set ; let G be GroupWithOperators of O; let H1, H2 be StableSubgroup of G; funcH1 "\/" H2 -> strict StableSubgroup of G equals :: GROUP_9:def 27 the_stable_subgroup_of ((carr H1) \/ (carr H2)); correctness coherence the_stable_subgroup_of ((carr H1) \/ (carr H2)) is strict StableSubgroup of G; ; end; :: 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)); begin :: GROUP_2:49 theorem Th1: :: GROUP_9:1 for O, x being set for G being GroupWithOperators of O for H1 being StableSubgroup of G st x in H1 holds x in G proofend; :: 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 proofend; :: 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 proofend; :: 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 proofend; :: 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 Lm18; :: 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 " proofend; :: 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 Lm19; :: 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 Lm20; :: 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 Lm15; :: GROUP_2:63 theorem Th10: :: GROUP_9:10 for O being set for G being GroupWithOperators of O holds G is StableSubgroup of G proofend; :: 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 proofend; :: 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 Lm21; :: 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 proofend; :: 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 Lm5; :: 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 proofend; :: 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 proofend; :: 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) proofend; :: 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 ) ) proofend; :: 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 proofend; :: 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) proofend; Lm22: for O being set for G being GroupWithOperators of O for H2 being StableSubgroup of G for H1 being strict StableSubgroup of G holds ( H1 is StableSubgroup of H2 iff H1 /\ H2 = H1 ) proofend; :: 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 ) proofend; :: 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 proofend; :: 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) proofend; Lm23: for F1 being FinSequence for y being Element of NAT st y in dom F1 holds ( ((len F1) - y) + 1 is Element of NAT & ((len F1) - y) + 1 >= 1 & ((len F1) - y) + 1 <= len F1 ) proofend; Lm24: for G, H being Group for F1 being FinSequence of the carrier of G for F2 being FinSequence of the carrier of H for I being FinSequence of INT for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds f . (Product (F1 |^ I)) = Product (F2 |^ I) proofend; :: 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 ) ) proofend; Lm25: for O being set for G being GroupWithOperators of O for A being Subset of G st A is empty holds the_stable_subgroup_of A = (1). G proofend; Lm26: for O being non empty set for E being set for o being Element of O for A being Action of O,E holds Product (<*o*>,A) = A . o proofend; Lm27: for O being non empty set for E being set for o being Element of O for F being FinSequence of O for A being Action of O,E holds Product ((F ^ <*o*>),A) = (Product (F,A)) * (Product (<*o*>,A)) proofend; Lm28: for O being non empty set for E being set for o being Element of O for F being FinSequence of O for A being Action of O,E holds Product ((<*o*> ^ F),A) = (Product (<*o*>,A)) * (Product (F,A)) proofend; Lm29: for O being non empty set for E being set for F1, F2 being FinSequence of O for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) proofend; Lm30: for O, E being set for F being FinSequence of O for Y being Subset of E for A being Action of O,E st Y is_stable_under_the_action_of A holds (Product (F,A)) .: Y c= Y proofend; Lm31: for O being set for E being non empty set for A being Action of O,E for X being Subset of E for a being Element of E st not X is empty holds ( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a ) proofend; :: 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 proofend; :: 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 proofend; scheme :: GROUP_9:sch 1 MeetSbgWOpEx{ F1() -> set , F2() -> GroupWithOperators of F1(), P1[ set ] } : ex H being strict StableSubgroup of F2() st the carrier of H = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st ( A = the carrier of K & P1[K] ) } provided A1: ex H being strict StableSubgroup of F2() st P1[H] proofend; :: 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 ) } proofend; Lm32: for O being set for G being GroupWithOperators of O for B, A being Subset of G st B = the carrier of (gr A) holds the_stable_subgroup_of A = the_stable_subgroup_of B proofend; :: 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 proofend; :: 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) proofend; :: 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 proofend; :: 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 proofend; :: 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 proofend; :: 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 ) proofend; :: 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 ) proofend; Lm33: for O being set for G being GroupWithOperators of O for H1, H2 being StableSubgroup of G holds H1 is StableSubgroup of H1 "\/" H2 proofend; :: 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 ) proofend; :: 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 ) proofend; :: 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 proofend; :: 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 proofend; :: 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 proofend; :: 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 proofend; Lm34: for O being set for G being GroupWithOperators of O for H1, H2 being StableSubgroup of G holds H1 /\ H2 is StableSubgroup of H1 proofend; :: 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 ) proofend; :: GROUP_6:13 theorem Th42: :: GROUP_9:42 for O being set for G being strict GroupWithOperators of O st G is trivial holds (1). G = G proofend; Lm35: for O being set for G being GroupWithOperators of O for N being normal StableSubgroup of G for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds ( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) ) proofend; :: 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 proofend; :: 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 proofend; :: 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 Lm13; :: 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 Lm14; :: 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 ) proofend; :: 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 proofend; :: 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) proofend; :: 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 proofend; :: 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 ) proofend; :: 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 proofend; :: 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 proofend; :: GROUP_6:75 theorem Th54: :: GROUP_9:54 for O being set for G being GroupWithOperators of O holds nat_hom ((1). G) is bijective proofend; :: 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 proofend; :: GROUP_6:82 theorem Th56: :: GROUP_9:56 for O being set for G being strict GroupWithOperators of O holds G,G ./. ((1). G) are_isomorphic proofend; :: GROUP_6:83 theorem Th57: :: GROUP_9:57 for O being set for G being strict GroupWithOperators of O holds G ./. ((Omega). G) is trivial proofend; :: 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 proofend; :: GROUP_6:90 theorem Th59: :: GROUP_9:59 for O being set for H, G being GroupWithOperators of O for h being Homomorphism of G,H holds G ./. (Ker h), Image h are_isomorphic proofend; :: 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 proofend; begin theorem :: GROUP_9:61 for O, E being set for A being Action of O,E holds [#] E is_stable_under_the_action_of A by Lm1; theorem :: GROUP_9:62 for O, E being set holds [:O,{(id E)}:] is Action of O,E by Lm2; theorem :: GROUP_9:63 for O being non empty set for E being set for o being Element of O for A being Action of O,E holds Product (<*o*>,A) = A . o by Lm26; theorem :: GROUP_9:64 for O being non empty set for E being set for F1, F2 being FinSequence of O for A being Action of O,E holds Product ((F1 ^ F2),A) = (Product (F1,A)) * (Product (F2,A)) by Lm29; theorem :: GROUP_9:65 for O, E being set for A being Action of O,E for F being FinSequence of O for Y being Subset of E st Y is_stable_under_the_action_of A holds (Product (F,A)) .: Y c= Y by Lm30; theorem :: GROUP_9:66 for O being set for E being non empty set for A being Action of O,E for X being Subset of E for a being Element of E st not X is empty holds ( a in the_stable_subset_generated_by (X,A) iff ex F being FinSequence of O ex x being Element of X st (Product (F,A)) . x = a ) by Lm31; theorem :: GROUP_9:67 for O being set for G being strict Group ex H being strict GroupWithOperators of O st G = multMagma(# the carrier of H, the multF of H #) proofend; theorem :: GROUP_9:68 for O being set for G being GroupWithOperators of O for H1 being StableSubgroup of G holds multMagma(# the carrier of H1, the multF of H1 #) is strict Subgroup of G by Lm16; theorem :: GROUP_9:69 for O being set for G being GroupWithOperators of O for N being normal StableSubgroup of G holds multMagma(# the carrier of N, the multF of N #) is strict normal Subgroup of G by Lm7; theorem :: GROUP_9:70 for O being set for o being Element of O for G being GroupWithOperators of O for H1 being StableSubgroup of G for g1 being Element of G st g1 in H1 holds (G ^ o) . g1 in H1 by Lm10; theorem :: GROUP_9:71 for O being set for G, H being GroupWithOperators of O for G9 being strict StableSubgroup of G for f being Homomorphism of G,H ex H9 being strict StableSubgroup of H st the carrier of H9 = f .: the carrier of G9 by Lm17; theorem :: GROUP_9:72 for O being set for G being GroupWithOperators of O for B being Subset of G st B is empty holds the_stable_subgroup_of B = (1). G by Lm25; theorem :: GROUP_9:73 for O being set for G being GroupWithOperators of O for B, C being Subset of G st B = the carrier of (gr C) holds the_stable_subgroup_of C = the_stable_subgroup_of B by Lm32; theorem :: GROUP_9:74 for O being set for G being GroupWithOperators of O for N being normal StableSubgroup of G for N9 being normal Subgroup of G st N9 = multMagma(# the carrier of N, the multF of N #) holds ( G ./. N9 = multMagma(# the carrier of (G ./. N), the multF of (G ./. N) #) & 1_ (G ./. N9) = 1_ (G ./. N) ) by Lm35; theorem Th75: :: GROUP_9:75 for O being set for G being GroupWithOperators of O for H1, H2 being StableSubgroup of G st the carrier of H1 = the carrier of H2 holds HGrWOpStr(# the carrier of H1, the multF of H1, the action of H1 #) = HGrWOpStr(# the carrier of H2, the multF of H2, the action of H2 #) proofend; 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 #) proofend; 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 proofend; :: 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 ) ) ) proofend; :: 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 ) ) proofend; 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) proofend; 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) proofend; 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 proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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) proofend; 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 proofend; :: 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 ) ) proofend; begin theorem Th91: :: GROUP_9:91 for O being set for G being GroupWithOperators of O for H, K, H9, K9 being strict StableSubgroup of G for JH being normal StableSubgroup of H9 "\/" (H /\ K) for HK being normal StableSubgroup of H /\ K st H9 is normal StableSubgroup of H & K9 is normal StableSubgroup of K & JH = H9 "\/" (H /\ K9) & HK = (H9 /\ K) "\/" (K9 /\ H) holds (H9 "\/" (H /\ K)) ./. JH,(H /\ K) ./. HK are_isomorphic proofend; 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) proofend; :: [WP: ] Zassenhaus_Lemma 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 proofend; begin :: ALG I.4.7 Definition 9 definition let O be set ; let G be GroupWithOperators of O; let IT be FinSequence of the_stable_subgroups_of G; attrIT is composition_series means :Def28: :: GROUP_9:def 28 ( IT . 1 = (Omega). G & IT . (len IT) = (1). G & ( for i being Nat st i in dom IT & i + 1 in dom IT holds for H1, H2 being StableSubgroup of G st H1 = IT . i & H2 = IT . (i + 1) holds H2 is normal StableSubgroup of H1 ) ); end; :: deftheorem 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 ) ) ); registration let O be set ; let G be GroupWithOperators of O; cluster Relation-like NAT -defined the_stable_subgroups_of G -valued Function-like finite FinSequence-like FinSubsequence-like composition_series for FinSequence of the_stable_subgroups_of G; existence ex b1 being FinSequence of the_stable_subgroups_of G st b1 is composition_series proofend; 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; :: ALG I.4.7 Definition 9 definition let O be set ; let G be GroupWithOperators of O; let s1, s2 be CompositionSeries of G; preds1 is_finer_than s2 means :Def29: :: GROUP_9:def 29 ex x being set st ( x c= dom s1 & s2 = s1 * (Sgm x) ); reflexivity for s1 being CompositionSeries of G ex x being set st ( x c= dom s1 & s1 = s1 * (Sgm x) ) proofend; end; :: deftheorem Def29 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) ) ); definition let O be set ; let G be GroupWithOperators of O; let IT be CompositionSeries of G; attrIT is strictly_decreasing means :Def30: :: 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 ; end; :: deftheorem Def30 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 ); :: ALG I.4.7 Definition 10 definition let O be set ; let G be GroupWithOperators of O; let IT be CompositionSeries of G; attrIT is jordan_holder means :Def31: :: 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 ) ) ); end; :: deftheorem Def31 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 ) ) ) ); :: 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; preds1 is_equivalent_with s2 means :Def32: :: 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 ) ); end; :: deftheorem Def32 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 ) ) ); :: ALG I.4.7 Definition 9 definition let O be set ; let G be GroupWithOperators of O; let s be CompositionSeries of G; func the_series_of_quotients_of s -> FinSequence means :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 > 1 implies ex b1 being FinSequence st ( len s = (len b1) + 1 & ( for i being Nat st i in dom b1 holds for H being StableSubgroup of G for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds b1 . i = H ./. N ) ) ) & ( not len s > 1 implies ex b1 being FinSequence st b1 = {} ) ) proofend; uniqueness for b1, b2 being FinSequence holds ( ( len s > 1 & len s = (len b1) + 1 & ( for i being Nat st i in dom b1 holds for H being StableSubgroup of G for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds b1 . i = H ./. N ) & len s = (len b2) + 1 & ( for i being Nat st i in dom b2 holds for H being StableSubgroup of G for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds b2 . i = H ./. N ) implies b1 = b2 ) & ( not len s > 1 & b1 = {} & b2 = {} implies b1 = b2 ) ) proofend; consistency for b1 being FinSequence holds verum ; end; :: 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 b4 being FinSequence holds ( ( len s > 1 implies ( b4 = the_series_of_quotients_of s iff ( len s = (len b4) + 1 & ( for i being Nat st i in dom b4 holds for H being StableSubgroup of G for N being normal StableSubgroup of H st H = s . i & N = s . (i + 1) holds b4 . i = H ./. N ) ) ) ) & ( not len s > 1 implies ( b4 = the_series_of_quotients_of s iff b4 = {} ) ) ); definition let O be set ; let f1, f2 be FinSequence; let p be Permutation of (dom f1); predf1,f2 are_equivalent_under p,O means :Def34: :: 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 ) ); end; :: deftheorem Def34 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 ) ) ); 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 proofend; 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 proofend; theorem Th96: :: GROUP_9:96 for O being set for G being GroupWithOperators of O for s2, s1 being CompositionSeries of G st len s2 = len s1 & s2 is_finer_than s1 holds s1 = s2 proofend; 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 proofend; theorem Th98: :: GROUP_9:98 for O being set for G being GroupWithOperators of O for s1, s2 being CompositionSeries of G st s1 is_finer_than s2 & s1 is jordan_holder & s2 is jordan_holder holds s1 = s2 proofend; Lm36: for P, R being Relation holds ( P = (rng P) |` R iff P ~ = (R ~) | (dom (P ~)) ) proofend; Lm37: for X being set for P, R being Relation holds P * (R | X) = (X |` P) * R proofend; Lm38: for n being Nat for X being set for f being PartFunc of REAL,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0} holds Sgm (f .: X) = f * (Sgm X) proofend; Lm39: for y being set for n, i being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds ex x being set st ( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) proofend; 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 proofend; 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 ) proofend; 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 proofend; 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 proofend; 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) ) proofend; 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) proofend; 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) ) ) proofend; 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 proofend; theorem Th107: :: GROUP_9:107 for O being set for G1, G2 being GroupWithOperators of O for s1 being CompositionSeries of G1 for s2 being CompositionSeries of G2 st s1 is empty & s2 is empty holds s1 is_equivalent_with s2 proofend; 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 ) proofend; 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 ) ) proofend; Lm40: for k, m being Element of NAT holds ( k < m iff k <= m - 1 ) proofend; Lm41: for a being Element of NAT for fs being FinSequence st a in dom fs holds ex fs1, fs2 being FinSequence st ( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) proofend; Lm42: for a being Element of NAT for fs, fs1, fs2 being FinSequence for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds Del (fs,a) = fs1 ^ fs2 proofend; Lm43: for a being Element of NAT for fs1, fs2 being FinSequence holds ( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) ) proofend; Lm44: for D being non empty set for f being FinSequence of D for p being Element of D for n being Nat st n in dom f holds f = Del ((Ins (f,n,p)),(n + 1)) proofend; :: 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; Lm45: for O being set for G being GroupWithOperators of O for s1, s2 being CompositionSeries of G for k, l being Nat st k in Seg l & len s1 > 1 & len s2 > 1 & l = (((len s1) - 1) * ((len s2) - 1)) + 1 & not k = (((len s1) - 1) * ((len s2) - 1)) + 1 holds ex i, j being Nat st ( k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 ) proofend; Lm46: for O being set for G being GroupWithOperators of O for i1, j1, i2, j2 being Nat for s1, s2 being CompositionSeries of G st len s2 > 1 & ((i1 - 1) * ((len s2) - 1)) + j1 = ((i2 - 1) * ((len s2) - 1)) + j2 & 1 <= i1 & 1 <= j1 & j1 <= (len s2) - 1 & 1 <= i2 & 1 <= j2 & j2 <= (len s2) - 1 holds ( j1 = j2 & i1 = i2 ) proofend; Lm47: for O being set for G being GroupWithOperators of O for k being integer number for i, j being Nat for s1, s2 being CompositionSeries of G st len s2 > 1 & k = ((i - 1) * ((len s2) - 1)) + j & 1 <= i & i <= (len s1) - 1 & 1 <= j & j <= (len s2) - 1 holds ( 1 <= k & k <= ((len s1) - 1) * ((len s2) - 1) ) proofend; begin definition let O be set ; let G be GroupWithOperators of O; let s1, s2 be CompositionSeries of G; assume that A1: len s1 > 1 and A2: len s2 > 1 ; func the_schreier_series_of (s1,s2) -> CompositionSeries of G means :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 ex b1 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 b1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b1 . k = (1). G ) & len b1 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) proofend; uniqueness for b1, b2 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 b1 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b1 . k = (1). G ) & len b1 = (((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 b2 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b2 . k = (1). G ) & len b2 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ) holds b1 = b2 proofend; 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 b5 being CompositionSeries of G holds ( b5 = 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 b5 . k = H1 "\/" (H2 /\ H3) ) & ( k = (((len s1) - 1) * ((len s2) - 1)) + 1 implies b5 . k = (1). G ) & len b5 = (((len s1) - 1) * ((len s2) - 1)) + 1 ) ); 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 proofend; 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) proofend; :: ALG I.4.7 Theorem 5 :: [WP: ] Schreier_Refinement_Theorem 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 ) proofend; begin :: ALG I.4.7 Theorem 6 :: [WP: ] Jordan-H\"older_Theorem 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 proofend; begin theorem :: GROUP_9:120 for P, R being Relation holds ( P = (rng P) |` R iff P ~ = (R ~) | (dom (P ~)) ) by Lm36; theorem :: GROUP_9:121 for X being set for P, R being Relation holds P * (R | X) = (X |` P) * R by Lm37; theorem :: GROUP_9:122 for n being Nat for X being set for f being PartFunc of REAL,REAL st X c= Seg n & X c= dom f & f | X is increasing & f .: X c= NAT \ {0} holds Sgm (f .: X) = f * (Sgm X) by Lm38; theorem :: GROUP_9:123 for y being set for i, n being Nat st y c= Seg (n + 1) & i in Seg (n + 1) & not i in y holds ex x being set st ( Sgm x = ((Sgm ((Seg (n + 1)) \ {i})) ") * (Sgm y) & x c= Seg n ) by Lm39; theorem :: GROUP_9:124 for D being non empty set for f being FinSequence of D for p being Element of D for n being Nat st n in dom f holds f = Del ((Ins (f,n,p)),(n + 1)) by Lm44; theorem :: GROUP_9:125 for G, H being Group for F1 being FinSequence of the carrier of G for F2 being FinSequence of the carrier of H for I being FinSequence of INT for f being Homomorphism of G,H st ( for k being Nat st k in dom F1 holds F2 . k = f . (F1 . k) ) & len F1 = len I & len F2 = len I holds f . (Product (F1 |^ I)) = Product (F2 |^ I) by Lm24;