:: The Sylow Theorems :: by Marco Riccardi :: :: Received August 13, 2007 :: Copyright (c) 2007-2012 Association of Mizar Users begin notation let S be non empty 1-sorted ; let E be set ; let A be Action of the carrier of S,E; let s be Element of S; synonym A ^ s for S . E; end; definition let S be non empty 1-sorted ; let E be set ; let A be Action of the carrier of S,E; let s be Element of S; :: original:^ redefine funcA ^ s -> Function of E,E; correctness coherence ^ is Function of E,E; proofend; end; definition let S be non empty unital multMagma ; let E be set ; let A be Action of the carrier of S,E; attrA is being_left_operation means :Def1: :: GROUP_10:def 1 ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ); end; :: deftheorem Def1 defines being_left_operation GROUP_10:def_1_:_ for S being non empty unital multMagma for E being set for A being Action of the carrier of S,E holds ( A is being_left_operation iff ( A ^ (1_ S) = id E & ( for s1, s2 being Element of S holds A ^ (s1 * s2) = (A ^ s1) * (A ^ s2) ) ) ); registration let S be non empty unital multMagma ; let E be set ; cluster Relation-like the carrier of S -defined Funcs (E,E) -valued non empty Function-like total quasi_total being_left_operation for Element of bool [: the carrier of S,(Funcs (E,E)):]; correctness existence ex b1 being Action of the carrier of S,E st b1 is being_left_operation ; proofend; end; :: ALG I.5.1 DEF 1 definition let S be non empty unital multMagma ; let E be set ; mode LeftOperation of S,E is being_left_operation Action of the carrier of S,E; end; scheme :: GROUP_10:sch 1 ExLeftOperation{ F1() -> set , F2() -> non empty Group-like multMagma , F3( Element of F2()) -> Function of F1(),F1() } : ex T being LeftOperation of F2(),F1() st for s being Element of F2() holds T . s = F3(s) provided A1: F3((1_ F2())) = id F1() and A2: for s1, s2 being Element of F2() holds F3((s1 * s2)) = F3(s1) * F3(s2) proofend; registration let E be non empty set ; let S be non empty Group-like multMagma ; let s be Element of S; let LO be LeftOperation of S,E; cluster ^ -> one-to-one for Function of E,E; coherence for b1 being Function of E,E st b1 = LO ^ s holds b1 is one-to-one proofend; end; notation let S be non empty multMagma ; let s be Element of S; synonym the_left_translation_of s for s * ; end; definition let S be non empty Group-like associative multMagma ; func the_left_operation_of S -> LeftOperation of S, the carrier of S means :Def2: :: GROUP_10:def 2 for s being Element of S holds it . s = the_left_translation_of s; existence ex b1 being LeftOperation of S, the carrier of S st for s being Element of S holds b1 . s = the_left_translation_of s proofend; uniqueness for b1, b2 being LeftOperation of S, the carrier of S st ( for s being Element of S holds b1 . s = the_left_translation_of s ) & ( for s being Element of S holds b2 . s = the_left_translation_of s ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines the_left_operation_of GROUP_10:def_2_:_ for S being non empty Group-like associative multMagma for b2 being LeftOperation of S, the carrier of S holds ( b2 = the_left_operation_of S iff for s being Element of S holds b2 . s = the_left_translation_of s ); definition let E, n be set ; func the_subsets_of_card (n,E) -> Subset-Family of E equals :: GROUP_10:def 3 { X where X is Subset of E : card X = n } ; correctness coherence { X where X is Subset of E : card X = n } is Subset-Family of E; proofend; end; :: deftheorem defines the_subsets_of_card GROUP_10:def_3_:_ for E, n being set holds the_subsets_of_card (n,E) = { X where X is Subset of E : card X = n } ; registration let E be finite set ; let n be set ; cluster the_subsets_of_card (n,E) -> finite ; correctness coherence the_subsets_of_card (n,E) is finite ; ; end; theorem Th1: :: GROUP_10:1 for n being Nat for E being non empty set st card n c= card E holds not the_subsets_of_card (n,E) is empty proofend; theorem Th2: :: GROUP_10:2 for E being non empty finite set for k being Element of NAT for x1, x2 being set st x1 <> x2 holds card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) proofend; definition let E be non empty set ; let n be Nat; let S be non empty Group-like multMagma ; let s be Element of S; let LO be LeftOperation of S,E; assume A1: card n c= card E ; func the_extension_of_left_translation_of (n,s,LO) -> Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) means :Def4: :: GROUP_10:def 4 for X being Element of the_subsets_of_card (n,E) holds it . X = (LO ^ s) .: X; existence ex b1 being Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) st for X being Element of the_subsets_of_card (n,E) holds b1 . X = (LO ^ s) .: X proofend; uniqueness for b1, b2 being Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) st ( for X being Element of the_subsets_of_card (n,E) holds b1 . X = (LO ^ s) .: X ) & ( for X being Element of the_subsets_of_card (n,E) holds b2 . X = (LO ^ s) .: X ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines the_extension_of_left_translation_of GROUP_10:def_4_:_ for E being non empty set for n being Nat for S being non empty Group-like multMagma for s being Element of S for LO being LeftOperation of S,E st card n c= card E holds for b6 being Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) holds ( b6 = the_extension_of_left_translation_of (n,s,LO) iff for X being Element of the_subsets_of_card (n,E) holds b6 . X = (LO ^ s) .: X ); definition let E be non empty set ; let n be Nat; let S be non empty Group-like multMagma ; let LO be LeftOperation of S,E; assume A1: card n c= card E ; func the_extension_of_left_operation_of (n,LO) -> LeftOperation of S,(the_subsets_of_card (n,E)) means :Def5: :: GROUP_10:def 5 for s being Element of S holds it . s = the_extension_of_left_translation_of (n,s,LO); existence ex b1 being LeftOperation of S,(the_subsets_of_card (n,E)) st for s being Element of S holds b1 . s = the_extension_of_left_translation_of (n,s,LO) proofend; uniqueness for b1, b2 being LeftOperation of S,(the_subsets_of_card (n,E)) st ( for s being Element of S holds b1 . s = the_extension_of_left_translation_of (n,s,LO) ) & ( for s being Element of S holds b2 . s = the_extension_of_left_translation_of (n,s,LO) ) holds b1 = b2 proofend; end; :: deftheorem Def5 defines the_extension_of_left_operation_of GROUP_10:def_5_:_ for E being non empty set for n being Nat for S being non empty Group-like multMagma for LO being LeftOperation of S,E st card n c= card E holds for b5 being LeftOperation of S,(the_subsets_of_card (n,E)) holds ( b5 = the_extension_of_left_operation_of (n,LO) iff for s being Element of S holds b5 . s = the_extension_of_left_translation_of (n,s,LO) ); definition let S be non empty multMagma ; let s be Element of S; let Z be non empty set ; func the_left_translation_of (s,Z) -> Function of [: the carrier of S,Z:],[: the carrier of S,Z:] means :Def6: :: GROUP_10:def 6 for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st ( z2 = it . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ); existence ex b1 being Function of [: the carrier of S,Z:],[: the carrier of S,Z:] st for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st ( z2 = b1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) proofend; uniqueness for b1, b2 being Function of [: the carrier of S,Z:],[: the carrier of S,Z:] st ( for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st ( z2 = b1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) & ( for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st ( z2 = b2 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines the_left_translation_of GROUP_10:def_6_:_ for S being non empty multMagma for s being Element of S for Z being non empty set for b4 being Function of [: the carrier of S,Z:],[: the carrier of S,Z:] holds ( b4 = the_left_translation_of (s,Z) iff for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st ( z2 = b4 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ); definition let S be non empty Group-like associative multMagma ; let Z be non empty set ; func the_left_operation_of (S,Z) -> LeftOperation of S,[: the carrier of S,Z:] means :Def7: :: GROUP_10:def 7 for s being Element of S holds it . s = the_left_translation_of (s,Z); existence ex b1 being LeftOperation of S,[: the carrier of S,Z:] st for s being Element of S holds b1 . s = the_left_translation_of (s,Z) proofend; uniqueness for b1, b2 being LeftOperation of S,[: the carrier of S,Z:] st ( for s being Element of S holds b1 . s = the_left_translation_of (s,Z) ) & ( for s being Element of S holds b2 . s = the_left_translation_of (s,Z) ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines the_left_operation_of GROUP_10:def_7_:_ for S being non empty Group-like associative multMagma for Z being non empty set for b3 being LeftOperation of S,[: the carrier of S,Z:] holds ( b3 = the_left_operation_of (S,Z) iff for s being Element of S holds b3 . s = the_left_translation_of (s,Z) ); definition let G be Group; let H, P be Subgroup of G; let h be Element of H; func the_left_translation_of (h,P) -> Function of (Left_Cosets P),(Left_Cosets P) means :Def8: :: GROUP_10:def 8 for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st ( P2 = it . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ); existence ex b1 being Function of (Left_Cosets P),(Left_Cosets P) st for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st ( P2 = b1 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) proofend; uniqueness for b1, b2 being Function of (Left_Cosets P),(Left_Cosets P) st ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st ( P2 = b1 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) & ( for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st ( P2 = b2 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines the_left_translation_of GROUP_10:def_8_:_ for G being Group for H, P being Subgroup of G for h being Element of H for b5 being Function of (Left_Cosets P),(Left_Cosets P) holds ( b5 = the_left_translation_of (h,P) iff for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st ( P2 = b5 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ); definition let G be Group; let H, P be Subgroup of G; func the_left_operation_of (H,P) -> LeftOperation of H,(Left_Cosets P) means :Def9: :: GROUP_10:def 9 for h being Element of H holds it . h = the_left_translation_of (h,P); existence ex b1 being LeftOperation of H,(Left_Cosets P) st for h being Element of H holds b1 . h = the_left_translation_of (h,P) proofend; uniqueness for b1, b2 being LeftOperation of H,(Left_Cosets P) st ( for h being Element of H holds b1 . h = the_left_translation_of (h,P) ) & ( for h being Element of H holds b2 . h = the_left_translation_of (h,P) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines the_left_operation_of GROUP_10:def_9_:_ for G being Group for H, P being Subgroup of G for b4 being LeftOperation of H,(Left_Cosets P) holds ( b4 = the_left_operation_of (H,P) iff for h being Element of H holds b4 . h = the_left_translation_of (h,P) ); begin :: stabilizer :: ALG I.5.2 Definition 3 definition let G be Group; let E be non empty set ; let T be LeftOperation of G,E; let A be Subset of E; func the_strict_stabilizer_of (A,T) -> strict Subgroup of G means :Def10: :: GROUP_10:def 10 the carrier of it = { g where g is Element of G : (T ^ g) .: A = A } ; existence ex b1 being strict Subgroup of G st the carrier of b1 = { g where g is Element of G : (T ^ g) .: A = A } proofend; uniqueness for b1, b2 being strict Subgroup of G st the carrier of b1 = { g where g is Element of G : (T ^ g) .: A = A } & the carrier of b2 = { g where g is Element of G : (T ^ g) .: A = A } holds b1 = b2 by GROUP_2:59; end; :: deftheorem Def10 defines the_strict_stabilizer_of GROUP_10:def_10_:_ for G being Group for E being non empty set for T being LeftOperation of G,E for A being Subset of E for b5 being strict Subgroup of G holds ( b5 = the_strict_stabilizer_of (A,T) iff the carrier of b5 = { g where g is Element of G : (T ^ g) .: A = A } ); definition let G be Group; let E be non empty set ; let T be LeftOperation of G,E; let x be Element of E; func the_strict_stabilizer_of (x,T) -> strict Subgroup of G equals :: GROUP_10:def 11 the_strict_stabilizer_of ({x},T); correctness coherence the_strict_stabilizer_of ({x},T) is strict Subgroup of G; ; end; :: deftheorem defines the_strict_stabilizer_of GROUP_10:def_11_:_ for G being Group for E being non empty set for T being LeftOperation of G,E for x being Element of E holds the_strict_stabilizer_of (x,T) = the_strict_stabilizer_of ({x},T); definition let S be non empty unital multMagma ; let E be set ; let T be LeftOperation of S,E; let x be Element of E; predx is_fixed_under T means :Def12: :: GROUP_10:def 12 for s being Element of S holds x = (T ^ s) . x; end; :: deftheorem Def12 defines is_fixed_under GROUP_10:def_12_:_ for S being non empty unital multMagma for E being set for T being LeftOperation of S,E for x being Element of E holds ( x is_fixed_under T iff for s being Element of S holds x = (T ^ s) . x ); definition let S be non empty unital multMagma ; let E be set ; let T be LeftOperation of S,E; func the_fixed_points_of T -> Subset of E equals :Def13: :: GROUP_10:def 13 { x where x is Element of E : x is_fixed_under T } if not E is empty otherwise {} E; correctness coherence ( ( not E is empty implies { x where x is Element of E : x is_fixed_under T } is Subset of E ) & ( E is empty implies {} E is Subset of E ) ); consistency for b1 being Subset of E holds verum; proofend; end; :: deftheorem Def13 defines the_fixed_points_of GROUP_10:def_13_:_ for S being non empty unital multMagma for E being set for T being LeftOperation of S,E holds ( ( not E is empty implies the_fixed_points_of T = { x where x is Element of E : x is_fixed_under T } ) & ( E is empty implies the_fixed_points_of T = {} E ) ); :: ALG I.5.4 Definition 5 definition let S be non empty unital multMagma ; let E be set ; let T be LeftOperation of S,E; let x, y be Element of E; predx,y are_conjugated_under T means :Def14: :: GROUP_10:def 14 ex s being Element of S st y = (T ^ s) . x; end; :: deftheorem Def14 defines are_conjugated_under GROUP_10:def_14_:_ for S being non empty unital multMagma for E being set for T being LeftOperation of S,E for x, y being Element of E holds ( x,y are_conjugated_under T iff ex s being Element of S st y = (T ^ s) . x ); theorem Th3: :: GROUP_10:3 for S being non empty unital multMagma for E being non empty set for x being Element of E for T being LeftOperation of S,E holds x,x are_conjugated_under T proofend; theorem Th4: :: GROUP_10:4 for G being Group for E being non empty set for x, y being Element of E for T being LeftOperation of G,E st x,y are_conjugated_under T holds y,x are_conjugated_under T proofend; theorem Th5: :: GROUP_10:5 for S being non empty unital multMagma for E being non empty set for x, y, z being Element of E for T being LeftOperation of S,E st x,y are_conjugated_under T & y,z are_conjugated_under T holds x,z are_conjugated_under T proofend; definition let S be non empty unital multMagma ; let E be non empty set ; let T be LeftOperation of S,E; let x be Element of E; func the_orbit_of (x,T) -> Subset of E equals :: GROUP_10:def 15 { y where y is Element of E : x,y are_conjugated_under T } ; correctness coherence { y where y is Element of E : x,y are_conjugated_under T } is Subset of E; proofend; end; :: deftheorem defines the_orbit_of GROUP_10:def_15_:_ for S being non empty unital multMagma for E being non empty set for T being LeftOperation of S,E for x being Element of E holds the_orbit_of (x,T) = { y where y is Element of E : x,y are_conjugated_under T } ; registration let S be non empty unital multMagma ; let E be non empty set ; let x be Element of E; let T be LeftOperation of S,E; cluster the_orbit_of (x,T) -> non empty ; coherence not the_orbit_of (x,T) is empty proofend; end; theorem Th6: :: GROUP_10:6 for G being Group for E being non empty set for x, y being Element of E for T being LeftOperation of G,E holds ( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) ) proofend; theorem Th7: :: GROUP_10:7 for S being non empty unital multMagma for E being non empty finite set for x being Element of E for T being LeftOperation of S,E st x is_fixed_under T holds the_orbit_of (x,T) = {x} proofend; :: the orbit-stabilizer theorem theorem Th8: :: GROUP_10:8 for G being Group for E being non empty set for a being Element of E for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T)) proofend; definition let G be Group; let E be non empty set ; let T be LeftOperation of G,E; func the_orbits_of T -> a_partition of E equals :: GROUP_10:def 16 { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ; correctness coherence { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } is a_partition of E; proofend; end; :: deftheorem defines the_orbits_of GROUP_10:def_16_:_ for G being Group for E being non empty set for T being LeftOperation of G,E holds the_orbits_of T = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ; begin :: ALG I.6.5 Definition 9 definition let p be Nat; let G be Group; attrG is p -group means :Def17: :: GROUP_10:def 17 ex r being Nat st card G = p |^ r; end; :: deftheorem Def17 defines -group GROUP_10:def_17_:_ for p being Nat for G being Group holds ( G is p -group iff ex r being Nat st card G = p |^ r ); Lm1: for n being non zero Nat holds card (INT.Group n) = n proofend; registration let p be non zero Nat; cluster INT.Group p -> p -group ; coherence INT.Group p is p -group proofend; end; registration let p be non zero Nat; cluster non empty finite strict unital Group-like associative commutative cyclic p -group for multMagma ; existence ex b1 being Group st ( b1 is p -group & b1 is finite & b1 is cyclic & b1 is commutative & b1 is strict ) proofend; end; :: like WEDDWITT:39 :: ALG I.6.5 PRO 11 theorem Th9: :: GROUP_10:9 for E being non empty finite set for G being finite Group for p being prime Nat for T being LeftOperation of G,E st G is p -group holds (card (the_fixed_points_of T)) mod p = (card E) mod p proofend; begin :: ALG I.6.6 Definition 10 definition let p be Nat; let G be Group; let P be Subgroup of G; predP is_Sylow_p-subgroup_of_prime p means :Def18: :: GROUP_10:def 18 ( P is p -group & not p divides index P ); end; :: deftheorem Def18 defines is_Sylow_p-subgroup_of_prime GROUP_10:def_18_:_ for p being Nat for G being Group for P being Subgroup of G holds ( P is_Sylow_p-subgroup_of_prime p iff ( P is p -group & not p divides index P ) ); Lm2: for n being Nat for p being prime Nat st n <> 0 holds ex m, r being Nat st ( n = (p |^ r) * m & not p divides m ) proofend; Lm3: for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y proofend; Lm4: for G being finite Group for E, T being non empty set for LO being LeftOperation of G,E for n being Nat st LO = the_left_operation_of (G,T) & n = card G & E = [: the carrier of G,T:] & card n c= card E holds the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum } proofend; Lm5: for n, m, r being Nat for p being prime Nat st n = (p |^ r) * m & not p divides m holds (n choose (p |^ r)) mod p <> 0 proofend; Lm6: for r, n, m1, m2 being Nat for p being prime Nat st (p |^ r) * n = m1 * m2 & not p divides n & not p divides m2 holds p |^ r divides m1 proofend; Lm7: for G being Group for A being non empty Subset of G for x being Element of G holds card A = card (A * x) proofend; :: ALG I.6.6 Theorem 2 :: The first Sylow theorem :: [WP: ] First_Sylow_Theorem theorem Th10: :: GROUP_10:10 for G being finite Group for p being prime Nat ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p proofend; Lm8: for n, r being Nat for p being prime Nat st n divides p |^ r & n > 1 holds p divides n proofend; :: ALG I.6.6 Corollary :: The Cauchy theorem theorem :: GROUP_10:11 for G being finite Group for p being prime Nat st p divides card G holds ex g being Element of G st ord g = p proofend; :: ALG I.6.6 Theorem 3 :: The second Sylow theorem :: [WP: ] Second_Sylow_Theorem theorem Th12: :: GROUP_10:12 for G being finite Group for p being prime Nat holds ( ( for H being Subgroup of G st H is p -group holds ex P being Subgroup of G st ( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) ) & ( for P1, P2 being Subgroup of G st P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p holds P1,P2 are_conjugated ) ) proofend; definition let G be Group; let p be Nat; func the_sylow_p-subgroups_of_prime (p,G) -> Subset of (Subgroups G) equals :: GROUP_10:def 19 { H where H is Element of Subgroups G : ex P being strict Subgroup of G st ( P = H & P is_Sylow_p-subgroup_of_prime p ) } ; correctness coherence { H where H is Element of Subgroups G : ex P being strict Subgroup of G st ( P = H & P is_Sylow_p-subgroup_of_prime p ) } is Subset of (Subgroups G); proofend; end; :: deftheorem defines the_sylow_p-subgroups_of_prime GROUP_10:def_19_:_ for G being Group for p being Nat holds the_sylow_p-subgroups_of_prime (p,G) = { H where H is Element of Subgroups G : ex P being strict Subgroup of G st ( P = H & P is_Sylow_p-subgroup_of_prime p ) } ; registration let G be finite Group; let p be prime Nat; cluster the_sylow_p-subgroups_of_prime (p,G) -> non empty finite ; correctness coherence ( not the_sylow_p-subgroups_of_prime (p,G) is empty & the_sylow_p-subgroups_of_prime (p,G) is finite ); proofend; end; definition let G be finite Group; let p be prime Nat; let H be Subgroup of G; let h be Element of H; func the_left_translation_of (h,p) -> Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) means :Def20: :: GROUP_10:def 20 for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P2 = it . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ); existence ex b1 being Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) st for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P2 = b1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) proofend; uniqueness for b1, b2 being Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) st ( for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P2 = b1 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) & ( for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P2 = b2 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) holds b1 = b2 proofend; end; :: deftheorem Def20 defines the_left_translation_of GROUP_10:def_20_:_ for G being finite Group for p being prime Nat for H being Subgroup of G for h being Element of H for b5 being Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) holds ( b5 = the_left_translation_of (h,p) iff for P1 being Element of the_sylow_p-subgroups_of_prime (p,G) ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P2 = b5 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ); definition let G be finite Group; let p be prime Nat; let H be Subgroup of G; func the_left_operation_of (H,p) -> LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) means :Def21: :: GROUP_10:def 21 for h being Element of H holds it . h = the_left_translation_of (h,p); existence ex b1 being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) st for h being Element of H holds b1 . h = the_left_translation_of (h,p) proofend; uniqueness for b1, b2 being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) st ( for h being Element of H holds b1 . h = the_left_translation_of (h,p) ) & ( for h being Element of H holds b2 . h = the_left_translation_of (h,p) ) holds b1 = b2 proofend; end; :: deftheorem Def21 defines the_left_operation_of GROUP_10:def_21_:_ for G being finite Group for p being prime Nat for H being Subgroup of G for b4 being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) holds ( b4 = the_left_operation_of (H,p) iff for h being Element of H holds b4 . h = the_left_translation_of (h,p) ); Lm9: for G, H being finite Group for p being prime Nat for I being Subgroup of G for P being Subgroup of H st I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G holds P is_Sylow_p-subgroup_of_prime p proofend; :: ALG I.6.6 Theorem 3 :: The third Sylow theorem :: [WP: ] Third_Sylow_Theorem theorem :: GROUP_10:13 for G being finite Group for p being prime Nat holds ( (card (the_sylow_p-subgroups_of_prime (p,G))) mod p = 1 & card (the_sylow_p-subgroups_of_prime (p,G)) divides card G ) proofend; begin theorem :: GROUP_10:14 for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y by Lm3; theorem :: GROUP_10:15 for n, m, r being Nat for p being prime Nat st n = (p |^ r) * m & not p divides m holds (n choose (p |^ r)) mod p <> 0 by Lm5; theorem :: GROUP_10:16 for n being non zero Nat holds card (INT.Group n) = n by Lm1; theorem :: GROUP_10:17 for G being Group for A being non empty Subset of G for g being Element of G holds card A = card (A * g) by Lm7;