:: GROUP_10 semantic presentation 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; proof A . s in Funcs (E,E) ; hence ^ is Function of E,E by FUNCT_2:66; ::_thesis: verum end; 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 ; proof reconsider IT = [: the carrier of S,{(id E)}:] as Action of the carrier of S,E by GROUP_9:62; take IT ; ::_thesis: IT is being_left_operation A1: now__::_thesis:_for_s_being_Element_of_S_holds_IT_._s_=_id_E let s be Element of S; ::_thesis: IT . s = id E IT c= [: the carrier of S,{(id E)}:] ; then reconsider IT9 = IT as Relation of the carrier of S,{(id E)} ; now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S_holds_ ex_y_being_set_st_[x,y]_in_[:_the_carrier_of_S,{(id_E)}:] let x be set ; ::_thesis: ( x in the carrier of S implies ex y being set st [x,y] in [: the carrier of S,{(id E)}:] ) assume A2: x in the carrier of S ; ::_thesis: ex y being set st [x,y] in [: the carrier of S,{(id E)}:] consider y being set such that A3: y = id E ; take y = y; ::_thesis: [x,y] in [: the carrier of S,{(id E)}:] y in {(id E)} by A3, TARSKI:def_1; hence [x,y] in [: the carrier of S,{(id E)}:] by A2, ZFMISC_1:def_2; ::_thesis: verum end; then dom IT = the carrier of S by RELSET_1:9; then A4: IT . s in rng IT by FUNCT_1:3; rng IT9 c= {(id E)} ; hence IT . s = id E by A4, TARSKI:def_1; ::_thesis: verum end; hence IT ^ (1_ S) = id E ; :: according to GROUP_10:def_1 ::_thesis: for s1, s2 being Element of S holds IT ^ (s1 * s2) = (IT ^ s1) * (IT ^ s2) let s1, s2 be Element of S; ::_thesis: IT ^ (s1 * s2) = (IT ^ s1) * (IT ^ s2) ( IT ^ s1 = id E & IT ^ s2 = id E ) by A1; then (IT ^ s1) * (IT ^ s2) = id E by PARTFUN1:6; hence IT ^ (s1 * s2) = (IT ^ s1) * (IT ^ s2) by A1; ::_thesis: verum end; end; 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) proof set T = { [s,F3(s)] where s is Element of F2() : verum } ; A3: now__::_thesis:_for_x_being_set_st_x_in__{__[s,F3(s)]_where_s_is_Element_of_F2()_:_verum__}__holds_ x_in_[:_the_carrier_of_F2(),(Funcs_(F1(),F1())):] let x be set ; ::_thesis: ( x in { [s,F3(s)] where s is Element of F2() : verum } implies x in [: the carrier of F2(),(Funcs (F1(),F1())):] ) assume x in { [s,F3(s)] where s is Element of F2() : verum } ; ::_thesis: x in [: the carrier of F2(),(Funcs (F1(),F1())):] then consider s being Element of F2() such that A4: x = [s,F3(s)] ; F3(s) in Funcs (F1(),F1()) by FUNCT_2:9; hence x in [: the carrier of F2(),(Funcs (F1(),F1())):] by A4, ZFMISC_1:def_2; ::_thesis: verum end; now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[s,F3(s)]_where_s_is_Element_of_F2()_:_verum__}__&_[x,y2]_in__{__[s,F3(s)]_where_s_is_Element_of_F2()_:_verum__}__holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [s,F3(s)] where s is Element of F2() : verum } & [x,y2] in { [s,F3(s)] where s is Element of F2() : verum } implies y1 = y2 ) assume [x,y1] in { [s,F3(s)] where s is Element of F2() : verum } ; ::_thesis: ( [x,y2] in { [s,F3(s)] where s is Element of F2() : verum } implies y1 = y2 ) then consider s1 being Element of F2() such that A5: [x,y1] = [s1,F3(s1)] ; A6: x = s1 by A5, XTUPLE_0:1; assume [x,y2] in { [s,F3(s)] where s is Element of F2() : verum } ; ::_thesis: y1 = y2 then consider s2 being Element of F2() such that A7: [x,y2] = [s2,F3(s2)] ; x = s2 by A7, XTUPLE_0:1; hence y1 = y2 by A5, A7, A6, XTUPLE_0:1; ::_thesis: verum end; then reconsider T = { [s,F3(s)] where s is Element of F2() : verum } as Function-like Relation of the carrier of F2(),(Funcs (F1(),F1())) by A3, FUNCT_1:def_1, TARSKI:def_3; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_carrier_of_F2()_implies_ex_y_being_set_st_[x,y]_in_T_)_&_(_ex_y_being_set_st_[x,y]_in_T_implies_x_in_the_carrier_of_F2()_)_) let x be set ; ::_thesis: ( ( x in the carrier of F2() implies ex y being set st [x,y] in T ) & ( ex y being set st [x,y] in T implies x in the carrier of F2() ) ) hereby ::_thesis: ( ex y being set st [x,y] in T implies x in the carrier of F2() ) assume x in the carrier of F2() ; ::_thesis: ex y being set st [x,y] in T then reconsider s = x as Element of F2() ; reconsider y = F3(s) as set ; take y = y; ::_thesis: [x,y] in T thus [x,y] in T ; ::_thesis: verum end; given y being set such that A8: [x,y] in T ; ::_thesis: x in the carrier of F2() consider s being Element of F2() such that A9: [x,y] = [s,F3(s)] by A8; x = s by A9, XTUPLE_0:1; hence x in the carrier of F2() ; ::_thesis: verum end; then the carrier of F2() = dom T by XTUPLE_0:def_12; then reconsider T = T as Action of the carrier of F2(),F1() by FUNCT_2:def_1; A10: now__::_thesis:_for_s1,_s2_being_Element_of_F2()_holds_T_^_(s1_*_s2)_=_(T_^_s1)_*_(T_^_s2) let s1, s2 be Element of F2(); ::_thesis: T ^ (s1 * s2) = (T ^ s1) * (T ^ s2) s1 in the carrier of F2() ; then s1 in dom T by FUNCT_2:def_1; then [s1,(T . s1)] in T by FUNCT_1:1; then consider s19 being Element of F2() such that A11: [s1,(T . s1)] = [s19,F3(s19)] ; A12: ( s1 = s19 & F3(s19) = T . s1 ) by A11, XTUPLE_0:1; s2 in the carrier of F2() ; then s2 in dom T by FUNCT_2:def_1; then [s2,(T . s2)] in T by FUNCT_1:1; then consider s29 being Element of F2() such that A13: [s2,(T . s2)] = [s29,F3(s29)] ; s1 * s2 in the carrier of F2() ; then s1 * s2 in dom T by FUNCT_2:def_1; then [(s1 * s2),(T . (s1 * s2))] in T by FUNCT_1:1; then consider s129 being Element of F2() such that A14: [(s1 * s2),(T . (s1 * s2))] = [s129,F3(s129)] ; A15: ( s2 = s29 & F3(s29) = T . s2 ) by A13, XTUPLE_0:1; thus T ^ (s1 * s2) = F3(s129) by A14, XTUPLE_0:1 .= F3((s1 * s2)) by A14, XTUPLE_0:1 .= (T ^ s1) * (T ^ s2) by A2, A12, A15 ; ::_thesis: verum end; A16: dom T = the carrier of F2() by FUNCT_2:def_1; then [(1_ F2()),(T . (1_ F2()))] in T by FUNCT_1:1; then consider s9 being Element of F2() such that A17: [(1_ F2()),(T . (1_ F2()))] = [s9,F3(s9)] ; ( 1_ F2() = s9 & T . (1_ F2()) = F3(s9) ) by A17, XTUPLE_0:1; then reconsider T = T as LeftOperation of F2(),F1() by A1, A10, Def1; take T ; ::_thesis: for s being Element of F2() holds T . s = F3(s) thus for s being Element of F2() holds T . s = F3(s) ::_thesis: verum proof let s be Element of F2(); ::_thesis: T . s = F3(s) [s,(T . s)] in T by A16, FUNCT_1:1; then consider s9 being Element of F2() such that A18: [s,(T . s)] = [s9,F3(s9)] ; s = s9 by A18, XTUPLE_0:1; hence T . s = F3(s) by A18, XTUPLE_0:1; ::_thesis: verum end; end; 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 proof consider e being Element of S such that A1: for h being Element of S holds ( h * e = h & e * h = h & ex g being Element of S st ( h * g = e & g * h = e ) ) by GROUP_1:def_2; consider s9 being Element of S such that s * s9 = e and A2: s9 * s = e by A1; LO ^ s9 in Funcs (E,E) by FUNCT_2:9; then A3: ex f being Function st ( LO ^ s9 = f & dom f = E & rng f c= E ) by FUNCT_2:def_2; LO ^ s in Funcs (E,E) by FUNCT_2:9; then A4: ex f being Function st ( LO ^ s = f & dom f = E & rng f c= E ) by FUNCT_2:def_2; id E = LO ^ (1_ S) by Def1 .= LO ^ (s9 * s) by A1, A2, GROUP_1:4 .= (LO ^ s9) * (LO ^ s) by Def1 ; hence for b1 being Function of E,E st b1 = LO ^ s holds b1 is one-to-one by A4, A3, FUNCT_1:25; ::_thesis: verum end; 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 proof deffunc H1( Element of S) -> Element of bool [: the carrier of S, the carrier of S:] = the_left_translation_of $1; set E = the carrier of S; A1: for s1, s2 being Element of S holds H1(s1 * s2) = H1(s1) * H1(s2) proof let s1, s2 be Element of S; ::_thesis: H1(s1 * s2) = H1(s1) * H1(s2) set f12 = the_left_translation_of (s1 * s2); set f1 = the_left_translation_of s1; set f2 = the_left_translation_of s2; the_left_translation_of s1 in Funcs ( the carrier of S, the carrier of S) by FUNCT_2:9; then A2: ex f being Function st ( the_left_translation_of s1 = f & dom f = the carrier of S & rng f c= the carrier of S ) by FUNCT_2:def_2; the_left_translation_of s2 in Funcs ( the carrier of S, the carrier of S) by FUNCT_2:9; then A3: ex f being Function st ( the_left_translation_of s2 = f & dom f = the carrier of S & rng f c= the carrier of S ) by FUNCT_2:def_2; the_left_translation_of (s1 * s2) in Funcs ( the carrier of S, the carrier of S) by FUNCT_2:9; then A4: ex f being Function st ( the_left_translation_of (s1 * s2) = f & dom f = the carrier of S & rng f c= the carrier of S ) by FUNCT_2:def_2; A5: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(the_left_translation_of_(s1_*_s2))_implies_(_x_in_dom_(the_left_translation_of_s2)_&_(the_left_translation_of_s2)_._x_in_dom_(the_left_translation_of_s1)_)_)_&_(_x_in_dom_(the_left_translation_of_s2)_&_(the_left_translation_of_s2)_._x_in_dom_(the_left_translation_of_s1)_implies_x_in_dom_(the_left_translation_of_(s1_*_s2))_)_) let x be set ; ::_thesis: ( ( x in dom (the_left_translation_of (s1 * s2)) implies ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) ) ) & ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) implies x in dom (the_left_translation_of (s1 * s2)) ) ) hereby ::_thesis: ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) implies x in dom (the_left_translation_of (s1 * s2)) ) assume A6: x in dom (the_left_translation_of (s1 * s2)) ; ::_thesis: ( x in dom (the_left_translation_of s2) & (the_left_translation_of s2) . x in dom (the_left_translation_of s1) ) hence x in dom (the_left_translation_of s2) by A3; ::_thesis: (the_left_translation_of s2) . x in dom (the_left_translation_of s1) (the_left_translation_of s2) . x in rng (the_left_translation_of s2) by A3, A6, FUNCT_1:3; hence (the_left_translation_of s2) . x in dom (the_left_translation_of s1) by A2; ::_thesis: verum end; assume that A7: x in dom (the_left_translation_of s2) and (the_left_translation_of s2) . x in dom (the_left_translation_of s1) ; ::_thesis: x in dom (the_left_translation_of (s1 * s2)) thus x in dom (the_left_translation_of (s1 * s2)) by A4, A7; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_(the_left_translation_of_(s1_*_s2))_holds_ (the_left_translation_of_(s1_*_s2))_._x_=_(the_left_translation_of_s1)_._((the_left_translation_of_s2)_._x) let x be set ; ::_thesis: ( x in dom (the_left_translation_of (s1 * s2)) implies (the_left_translation_of (s1 * s2)) . x = (the_left_translation_of s1) . ((the_left_translation_of s2) . x) ) assume A8: x in dom (the_left_translation_of (s1 * s2)) ; ::_thesis: (the_left_translation_of (s1 * s2)) . x = (the_left_translation_of s1) . ((the_left_translation_of s2) . x) then reconsider s19 = x as Element of S ; (the_left_translation_of s2) . x in rng (the_left_translation_of s2) by A3, A8, FUNCT_1:3; then reconsider s199 = (the_left_translation_of s2) . x as Element of S ; thus (the_left_translation_of (s1 * s2)) . x = (s1 * s2) * s19 by TOPGRP_1:def_1 .= s1 * (s2 * s19) by GROUP_1:def_3 .= s1 * s199 by TOPGRP_1:def_1 .= (the_left_translation_of s1) . ((the_left_translation_of s2) . x) by TOPGRP_1:def_1 ; ::_thesis: verum end; hence H1(s1 * s2) = H1(s1) * H1(s2) by A5, FUNCT_1:10; ::_thesis: verum end; A9: H1( 1_ S) = id the carrier of S proof set f = the_left_translation_of (1_ S); A10: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S_holds_ (the_left_translation_of_(1__S))_._x_=_x let x be set ; ::_thesis: ( x in the carrier of S implies (the_left_translation_of (1_ S)) . x = x ) assume x in the carrier of S ; ::_thesis: (the_left_translation_of (1_ S)) . x = x then reconsider s1 = x as Element of S ; (the_left_translation_of (1_ S)) . s1 = (1_ S) * s1 by TOPGRP_1:def_1; hence (the_left_translation_of (1_ S)) . x = x by GROUP_1:def_4; ::_thesis: verum end; the_left_translation_of (1_ S) in Funcs ( the carrier of S, the carrier of S) by FUNCT_2:9; then ex f9 being Function st ( the_left_translation_of (1_ S) = f9 & dom f9 = the carrier of S & rng f9 c= the carrier of S ) by FUNCT_2:def_2; hence H1( 1_ S) = id the carrier of S by A10, FUNCT_1:17; ::_thesis: verum end; ex T being LeftOperation of S, the carrier of S st for s being Element of S holds T . s = H1(s) from GROUP_10:sch_1(A9, A1); hence 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 ; ::_thesis: verum end; 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 proof let T1, T2 be LeftOperation of S, the carrier of S; ::_thesis: ( ( for s being Element of S holds T1 . s = the_left_translation_of s ) & ( for s being Element of S holds T2 . s = the_left_translation_of s ) implies T1 = T2 ) assume that A11: for s being Element of S holds T1 . s = the_left_translation_of s and A12: for s being Element of S holds T2 . s = the_left_translation_of s ; ::_thesis: T1 = T2 let x be Element of S; :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ thus T1 . x = the_left_translation_of x by A11 .= T2 . x by A12 ; ::_thesis: verum end; 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; proof set SF = { X where X is Subset of E : card X = n } ; now__::_thesis:_for_x_being_set_st_x_in__{__X_where_X_is_Subset_of_E_:_card_X_=_n__}__holds_ x_in_bool_E let x be set ; ::_thesis: ( x in { X where X is Subset of E : card X = n } implies x in bool E ) assume x in { X where X is Subset of E : card X = n } ; ::_thesis: x in bool E then ex X being Subset of E st ( X = x & card X = n ) ; hence x in bool E ; ::_thesis: verum end; hence { X where X is Subset of E : card X = n } is Subset-Family of E by TARSKI:def_3; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: for E being non empty set st card n c= card E holds not the_subsets_of_card (n,E) is empty let E be non empty set ; ::_thesis: ( card n c= card E implies not the_subsets_of_card (n,E) is empty ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; assume card n c= card E ; ::_thesis: not the_subsets_of_card (n,E) is empty then consider f being Function such that A1: f is one-to-one and A2: dom f = n and A3: rng f c= E by CARD_1:10; set X = f .: n; A4: rng f = f .: n by A2, RELAT_1:113; then n,f .: n are_equipotent by A1, A2, WELLORD2:def_4; then card (f .: n) = n9 by CARD_1:def_2; then f .: n in { X9 where X9 is Subset of E : card X9 = n } by A3, A4; hence not the_subsets_of_card (n,E) is empty ; ::_thesis: verum end; 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)) proof let E be non empty finite set ; ::_thesis: 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)) let k be Element of NAT ; ::_thesis: for x1, x2 being set st x1 <> x2 holds card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) let x1, x2 be set ; ::_thesis: ( x1 <> x2 implies card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) ) set f = { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } ; now__::_thesis:_for_x_being_set_st_x_in__{__[fX,X]_where_fX_is_Function_of_E,{x1,x2},_X_is_Subset_of_E_:_(_card_(fX_"_{x1})_=_k_&_fX_"_{x1}_=_X_)__}__holds_ ex_y,_z_being_set_st_x_=_[y,z] let x be set ; ::_thesis: ( x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } implies ex y, z being set st x = [y,z] ) assume x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } ; ::_thesis: ex y, z being set st x = [y,z] then consider y being Function of E,{x1,x2}, z being Subset of E such that A1: x = [y,z] and card (y " {x1}) = k and y " {x1} = z ; reconsider y = y, z = z as set ; take y = y; ::_thesis: ex z being set st x = [y,z] take z = z; ::_thesis: x = [y,z] thus x = [y,z] by A1; ::_thesis: verum end; then reconsider f = { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } as Relation-like set by RELAT_1:def_1; now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in_f_&_[x,y2]_in_f_holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in f & [x,y2] in f implies y1 = y2 ) assume [x,y1] in f ; ::_thesis: ( [x,y2] in f implies y1 = y2 ) then consider fX1 being Function of E,{x1,x2}, X1 being Subset of E such that A2: [x,y1] = [fX1,X1] and card (fX1 " {x1}) = k and A3: fX1 " {x1} = X1 ; A4: x = fX1 by A2, XTUPLE_0:1; assume [x,y2] in f ; ::_thesis: y1 = y2 then consider fX2 being Function of E,{x1,x2}, X2 being Subset of E such that A5: [x,y2] = [fX2,X2] and card (fX2 " {x1}) = k and A6: fX2 " {x1} = X2 ; x = fX2 by A5, XTUPLE_0:1; hence y1 = y2 by A2, A3, A5, A6, A4, XTUPLE_0:1; ::_thesis: verum end; then reconsider f = f as Function by FUNCT_1:def_1; assume A7: x1 <> x2 ; ::_thesis: card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) now__::_thesis:_for_y1,_y2_being_set_st_y1_in_dom_f_&_y2_in_dom_f_&_f_._y1_=_f_._y2_holds_ y1_=_y2 let y1, y2 be set ; ::_thesis: ( y1 in dom f & y2 in dom f & f . y1 = f . y2 implies y1 = y2 ) assume that A8: y1 in dom f and A9: y2 in dom f ; ::_thesis: ( f . y1 = f . y2 implies y1 = y2 ) assume A10: f . y1 = f . y2 ; ::_thesis: y1 = y2 [y2,(f . y2)] in f by A9, FUNCT_1:1; then consider fX2 being Function of E,{x1,x2}, X2 being Subset of E such that A11: [y2,(f . y2)] = [fX2,X2] and card (fX2 " {x1}) = k and A12: fX2 " {x1} = X2 ; A13: y2 = fX2 by A11, XTUPLE_0:1; [y1,(f . y1)] in f by A8, FUNCT_1:1; then consider fX1 being Function of E,{x1,x2}, X1 being Subset of E such that A14: [y1,(f . y1)] = [fX1,X1] and card (fX1 " {x1}) = k and A15: fX1 " {x1} = X1 ; dom fX1 = E by FUNCT_2:def_1; then A16: dom fX1 = dom fX2 by FUNCT_2:def_1; f . y1 = X1 by A14, XTUPLE_0:1; then A17: fX1 " {x1} = fX2 " {x1} by A10, A15, A11, A12, XTUPLE_0:1; A18: for z being set st z in dom fX1 holds fX1 . z = fX2 . z proof assume ex z being set st ( z in dom fX1 & fX1 . z <> fX2 . z ) ; ::_thesis: contradiction then consider z being set such that A19: z in dom fX1 and A20: fX1 . z <> fX2 . z ; A21: fX1 . z in {x1,x2} by A19, FUNCT_2:5; fX2 . z in {x1,x2} by A19, FUNCT_2:5; then A22: ( fX2 . z = x1 or fX2 . z = x2 ) by TARSKI:def_2; percases ( ( fX1 . z = x1 & fX2 . z = x2 ) or ( fX1 . z = x2 & fX2 . z = x1 ) ) by A20, A21, A22, TARSKI:def_2; supposeA23: ( fX1 . z = x1 & fX2 . z = x2 ) ; ::_thesis: contradiction then A24: fX1 . z in {x1} by TARSKI:def_1; [z,(fX1 . z)] in fX1 by A19, FUNCT_1:1; then z in fX2 " {x1} by A17, A24, RELAT_1:def_14; then consider z9 being set such that A25: [z,z9] in fX2 and A26: z9 in {x1} by RELAT_1:def_14; z9 = fX2 . z by A25, FUNCT_1:1; hence contradiction by A7, A23, A26, TARSKI:def_1; ::_thesis: verum end; supposeA27: ( fX1 . z = x2 & fX2 . z = x1 ) ; ::_thesis: contradiction then A28: fX2 . z in {x1} by TARSKI:def_1; [z,(fX2 . z)] in fX2 by A16, A19, FUNCT_1:1; then z in fX1 " {x1} by A17, A28, RELAT_1:def_14; then consider z9 being set such that A29: [z,z9] in fX1 and A30: z9 in {x1} by RELAT_1:def_14; z9 = fX1 . z by A29, FUNCT_1:1; hence contradiction by A7, A27, A30, TARSKI:def_1; ::_thesis: verum end; end; end; y1 = fX1 by A14, XTUPLE_0:1; hence y1 = y2 by A13, A16, A18, FUNCT_1:2; ::_thesis: verum end; then A31: f is one-to-one by FUNCT_1:def_4; for y being set holds ( y in the_subsets_of_card (k,E) iff ex x being set st [x,y] in f ) proof let y be set ; ::_thesis: ( y in the_subsets_of_card (k,E) iff ex x being set st [x,y] in f ) hereby ::_thesis: ( ex x being set st [x,y] in f implies y in the_subsets_of_card (k,E) ) assume y in the_subsets_of_card (k,E) ; ::_thesis: ex x being set st [x,y] in f then consider X being Subset of E such that A32: ( y = X & card X = k ) ; defpred S1[ set , set ] means ( ( $1 in X & $2 = x1 ) or ( not $1 in X & $2 = x2 ) ); A33: for z1 being Element of E ex z2 being Element of {x1,x2} st S1[z1,z2] proof let z1 be Element of E; ::_thesis: ex z2 being Element of {x1,x2} st S1[z1,z2] percases ( z1 in X or not z1 in X ) ; supposeA34: z1 in X ; ::_thesis: ex z2 being Element of {x1,x2} st S1[z1,z2] reconsider z2 = x1 as Element of {x1,x2} by TARSKI:def_2; take z2 ; ::_thesis: S1[z1,z2] thus S1[z1,z2] by A34; ::_thesis: verum end; supposeA35: not z1 in X ; ::_thesis: ex z2 being Element of {x1,x2} st S1[z1,z2] reconsider z2 = x2 as Element of {x1,x2} by TARSKI:def_2; take z2 ; ::_thesis: S1[z1,z2] thus S1[z1,z2] by A35; ::_thesis: verum end; end; end; ex f being Function of E,{x1,x2} st for z being Element of E holds S1[z,f . z] from FUNCT_2:sch_3(A33); then consider f9 being Function of E,{x1,x2} such that A36: for z being Element of E holds S1[z,f9 . z] ; reconsider x = f9 as set ; take x = x; ::_thesis: [x,y] in f now__::_thesis:_for_z_being_set_holds_ (_(_z_in_X_implies_z_in_f9_"_{x1}_)_&_(_z_in_f9_"_{x1}_implies_z_in_X_)_) let z be set ; ::_thesis: ( ( z in X implies z in f9 " {x1} ) & ( z in f9 " {x1} implies z in X ) ) hereby ::_thesis: ( z in f9 " {x1} implies z in X ) assume A37: z in X ; ::_thesis: z in f9 " {x1} then reconsider z9 = z as Element of E ; set z99 = f9 . z9; z in E by A37; then z in dom f9 by FUNCT_2:def_1; then A38: [z,(f9 . z)] in f9 by FUNCT_1:1; f9 . z9 = x1 by A36, A37; then f9 . z9 in {x1} by TARSKI:def_1; hence z in f9 " {x1} by A38, RELAT_1:def_14; ::_thesis: verum end; assume z in f9 " {x1} ; ::_thesis: z in X then consider z9 being set such that A39: [z,z9] in f9 and A40: z9 in {x1} by RELAT_1:def_14; z in dom f9 by A39, XTUPLE_0:def_12; then reconsider z99 = z as Element of E ; z9 = x1 by A40, TARSKI:def_1; then f9 . z99 = x1 by A39, FUNCT_1:1; hence z in X by A7, A36; ::_thesis: verum end; then X = f9 " {x1} by TARSKI:1; hence [x,y] in f by A32; ::_thesis: verum end; given x being set such that A41: [x,y] in f ; ::_thesis: y in the_subsets_of_card (k,E) consider fX being Function of E,{x1,x2}, X being Subset of E such that A42: [x,y] = [fX,X] and A43: ( card (fX " {x1}) = k & fX " {x1} = X ) by A41; y = X by A42, XTUPLE_0:1; hence y in the_subsets_of_card (k,E) by A43; ::_thesis: verum end; then A44: rng f = the_subsets_of_card (k,E) by XTUPLE_0:def_13; for x being set holds ( x in Choose (E,k,x1,x2) iff ex y being set st [x,y] in f ) proof let x be set ; ::_thesis: ( x in Choose (E,k,x1,x2) iff ex y being set st [x,y] in f ) thus ( x in Choose (E,k,x1,x2) implies ex y being set st [x,y] in f ) ::_thesis: ( ex y being set st [x,y] in f implies x in Choose (E,k,x1,x2) ) proof assume x in Choose (E,k,x1,x2) ; ::_thesis: ex y being set st [x,y] in f then consider fX being Function of E,{x1,x2} such that A45: ( fX = x & card (fX " {x1}) = k ) by CARD_FIN:def_1; set y = fX " {x1}; take fX " {x1} ; ::_thesis: [x,(fX " {x1})] in f thus [x,(fX " {x1})] in f by A45; ::_thesis: verum end; thus ( ex y being set st [x,y] in f implies x in Choose (E,k,x1,x2) ) ::_thesis: verum proof given y being set such that A46: [x,y] in f ; ::_thesis: x in Choose (E,k,x1,x2) consider fX being Function of E,{x1,x2}, X being Subset of E such that A47: [x,y] = [fX,X] and A48: card (fX " {x1}) = k and fX " {x1} = X by A46; x = fX by A47, XTUPLE_0:1; hence x in Choose (E,k,x1,x2) by A48, CARD_FIN:def_1; ::_thesis: verum end; end; then dom f = Choose (E,k,x1,x2) by XTUPLE_0:def_12; then Choose (E,k,x1,x2), the_subsets_of_card (k,E) are_equipotent by A31, A44, WELLORD2:def_4; hence card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) by CARD_1:5; ::_thesis: verum end; 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 proof set EE = the_subsets_of_card (n,E); set f = { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } ; A2: now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[X,((LO_^_s)_.:_X)]_where_X_is_Element_of_the_subsets_of_card_(n,E)_:_verum__}__&_[x,y2]_in__{__[X,((LO_^_s)_.:_X)]_where_X_is_Element_of_the_subsets_of_card_(n,E)_:_verum__}__holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } & [x,y2] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } implies y1 = y2 ) assume [x,y1] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } ; ::_thesis: ( [x,y2] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } implies y1 = y2 ) then consider X1 being Element of the_subsets_of_card (n,E) such that A3: [x,y1] = [X1,((LO ^ s) .: X1)] ; A4: x = X1 by A3, XTUPLE_0:1; assume [x,y2] in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } ; ::_thesis: y1 = y2 then consider X2 being Element of the_subsets_of_card (n,E) such that A5: [x,y2] = [X2,((LO ^ s) .: X2)] ; x = X2 by A5, XTUPLE_0:1; hence y1 = y2 by A3, A5, A4, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in__{__[X,((LO_^_s)_.:_X)]_where_X_is_Element_of_the_subsets_of_card_(n,E)_:_verum__}__holds_ ex_y,_z_being_set_st_x_=_[y,z] let x be set ; ::_thesis: ( x in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } implies ex y, z being set st x = [y,z] ) assume x in { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } ; ::_thesis: ex y, z being set st x = [y,z] then consider X being Element of the_subsets_of_card (n,E) such that A6: x = [X,((LO ^ s) .: X)] ; reconsider y = X, z = (LO ^ s) .: X as set ; take y = y; ::_thesis: ex z being set st x = [y,z] take z = z; ::_thesis: x = [y,z] thus x = [y,z] by A6; ::_thesis: verum end; then reconsider f = { [X,((LO ^ s) .: X)] where X is Element of the_subsets_of_card (n,E) : verum } as Function by A2, FUNCT_1:def_1, RELAT_1:def_1; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_subsets_of_card_(n,E)_implies_ex_y_being_set_st_[x,y]_in_f_)_&_(_ex_y_being_set_st_[x,y]_in_f_implies_x_in_the_subsets_of_card_(n,E)_)_) let x be set ; ::_thesis: ( ( x in the_subsets_of_card (n,E) implies ex y being set st [x,y] in f ) & ( ex y being set st [x,y] in f implies x in the_subsets_of_card (n,E) ) ) hereby ::_thesis: ( ex y being set st [x,y] in f implies x in the_subsets_of_card (n,E) ) assume x in the_subsets_of_card (n,E) ; ::_thesis: ex y being set st [x,y] in f then reconsider X = x as Element of the_subsets_of_card (n,E) ; reconsider y = (LO ^ s) .: X as set ; take y = y; ::_thesis: [x,y] in f thus [x,y] in f ; ::_thesis: verum end; given y being set such that A7: [x,y] in f ; ::_thesis: x in the_subsets_of_card (n,E) consider X being Element of the_subsets_of_card (n,E) such that A8: [x,y] = [X,((LO ^ s) .: X)] by A7; A9: x = X by A8, XTUPLE_0:1; not the_subsets_of_card (n,E) is empty by A1, Th1; hence x in the_subsets_of_card (n,E) by A9; ::_thesis: verum end; then A10: dom f = the_subsets_of_card (n,E) by XTUPLE_0:def_12; now__::_thesis:_for_Y_being_set_st_Y_in_rng_f_holds_ Y_in_the_subsets_of_card_(n,E) let Y be set ; ::_thesis: ( Y in rng f implies Y in the_subsets_of_card (n,E) ) assume Y in rng f ; ::_thesis: Y in the_subsets_of_card (n,E) then consider X1 being set such that A11: [X1,Y] in f by XTUPLE_0:def_13; consider X2 being Element of the_subsets_of_card (n,E) such that A12: [X1,Y] = [X2,((LO ^ s) .: X2)] by A11; set fe = (LO ^ s) | X2; A13: (LO ^ s) | X2 is one-to-one by FUNCT_1:52; not the_subsets_of_card (n,E) is empty by A1, Th1; then A14: X2 in the_subsets_of_card (n,E) ; then A15: ex X being Subset of E st ( X = X2 & card X = n ) ; LO ^ s in Funcs (E,E) by FUNCT_2:9; then ex f being Function st ( LO ^ s = f & dom f = E & rng f c= E ) by FUNCT_2:def_2; then A16: dom ((LO ^ s) | X2) = X2 by A14, RELAT_1:62; A17: Y = (LO ^ s) .: X2 by A12, XTUPLE_0:1; then rng ((LO ^ s) | X2) = Y by RELAT_1:115; then X2,Y are_equipotent by A13, A16, WELLORD2:def_4; then card Y = n by A15, CARD_1:5; hence Y in the_subsets_of_card (n,E) by A17; ::_thesis: verum end; then rng f c= the_subsets_of_card (n,E) by TARSKI:def_3; then reconsider f = f as Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) by A10, FUNCT_2:2; take f ; ::_thesis: for X being Element of the_subsets_of_card (n,E) holds f . X = (LO ^ s) .: X thus for X being Element of the_subsets_of_card (n,E) holds f . X = (LO ^ s) .: X ::_thesis: verum proof let X be Element of the_subsets_of_card (n,E); ::_thesis: f . X = (LO ^ s) .: X not the_subsets_of_card (n,E) is empty by A1, Th1; then [X,(f . X)] in f by A10, FUNCT_1:1; then consider X9 being Element of the_subsets_of_card (n,E) such that A18: [X,(f . X)] = [X9,((LO ^ s) .: X9)] ; X = X9 by A18, XTUPLE_0:1; hence f . X = (LO ^ s) .: X by A18, XTUPLE_0:1; ::_thesis: verum end; end; 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 proof set EE = the_subsets_of_card (n,E); let IT1, IT2 be Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)); ::_thesis: ( ( for X being Element of the_subsets_of_card (n,E) holds IT1 . X = (LO ^ s) .: X ) & ( for X being Element of the_subsets_of_card (n,E) holds IT2 . X = (LO ^ s) .: X ) implies IT1 = IT2 ) assume that A19: for X being Element of the_subsets_of_card (n,E) holds IT1 . X = (LO ^ s) .: X and A20: for X being Element of the_subsets_of_card (n,E) holds IT2 . X = (LO ^ s) .: X ; ::_thesis: IT1 = IT2 let x be Element of the_subsets_of_card (n,E); :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ thus IT1 . x = (LO ^ s) .: x by A19 .= IT2 . x by A20 ; ::_thesis: verum end; 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) proof deffunc H1( Element of S) -> Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) = the_extension_of_left_translation_of (n,$1,LO); set EE = the_subsets_of_card (n,E); A2: for s1, s2 being Element of S holds H1(s1 * s2) = H1(s1) * H1(s2) proof let s1, s2 be Element of S; ::_thesis: H1(s1 * s2) = H1(s1) * H1(s2) set f12 = the_extension_of_left_translation_of (n,(s1 * s2),LO); set f1 = the_extension_of_left_translation_of (n,s1,LO); set f2 = the_extension_of_left_translation_of (n,s2,LO); the_extension_of_left_translation_of (n,s1,LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9; then A3: ex f being Function st ( the_extension_of_left_translation_of (n,s1,LO) = f & dom f = the_subsets_of_card (n,E) & rng f c= the_subsets_of_card (n,E) ) by FUNCT_2:def_2; the_extension_of_left_translation_of (n,s2,LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9; then A4: ex f being Function st ( the_extension_of_left_translation_of (n,s2,LO) = f & dom f = the_subsets_of_card (n,E) & rng f c= the_subsets_of_card (n,E) ) by FUNCT_2:def_2; the_extension_of_left_translation_of (n,(s1 * s2),LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9; then A5: ex f being Function st ( the_extension_of_left_translation_of (n,(s1 * s2),LO) = f & dom f = the_subsets_of_card (n,E) & rng f c= the_subsets_of_card (n,E) ) by FUNCT_2:def_2; A6: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(the_extension_of_left_translation_of_(n,(s1_*_s2),LO))_implies_(_x_in_dom_(the_extension_of_left_translation_of_(n,s2,LO))_&_(the_extension_of_left_translation_of_(n,s2,LO))_._x_in_dom_(the_extension_of_left_translation_of_(n,s1,LO))_)_)_&_(_x_in_dom_(the_extension_of_left_translation_of_(n,s2,LO))_&_(the_extension_of_left_translation_of_(n,s2,LO))_._x_in_dom_(the_extension_of_left_translation_of_(n,s1,LO))_implies_x_in_dom_(the_extension_of_left_translation_of_(n,(s1_*_s2),LO))_)_) let x be set ; ::_thesis: ( ( x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) implies ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) ) ) & ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) implies x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ) ) hereby ::_thesis: ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) implies x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ) assume A7: x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ; ::_thesis: ( x in dom (the_extension_of_left_translation_of (n,s2,LO)) & (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) ) hence x in dom (the_extension_of_left_translation_of (n,s2,LO)) by A4; ::_thesis: (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) (the_extension_of_left_translation_of (n,s2,LO)) . x in rng (the_extension_of_left_translation_of (n,s2,LO)) by A4, A7, FUNCT_1:3; hence (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) by A3; ::_thesis: verum end; assume that A8: x in dom (the_extension_of_left_translation_of (n,s2,LO)) and (the_extension_of_left_translation_of (n,s2,LO)) . x in dom (the_extension_of_left_translation_of (n,s1,LO)) ; ::_thesis: x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) thus x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) by A5, A8; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_(the_extension_of_left_translation_of_(n,(s1_*_s2),LO))_holds_ (the_extension_of_left_translation_of_(n,(s1_*_s2),LO))_._x_=_(the_extension_of_left_translation_of_(n,s1,LO))_._((the_extension_of_left_translation_of_(n,s2,LO))_._x) let x be set ; ::_thesis: ( x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) implies (the_extension_of_left_translation_of (n,(s1 * s2),LO)) . x = (the_extension_of_left_translation_of (n,s1,LO)) . ((the_extension_of_left_translation_of (n,s2,LO)) . x) ) assume A9: x in dom (the_extension_of_left_translation_of (n,(s1 * s2),LO)) ; ::_thesis: (the_extension_of_left_translation_of (n,(s1 * s2),LO)) . x = (the_extension_of_left_translation_of (n,s1,LO)) . ((the_extension_of_left_translation_of (n,s2,LO)) . x) then reconsider X1 = x as Element of the_subsets_of_card (n,E) ; (the_extension_of_left_translation_of (n,s2,LO)) . x in rng (the_extension_of_left_translation_of (n,s2,LO)) by A4, A9, FUNCT_1:3; then reconsider X2 = (the_extension_of_left_translation_of (n,s2,LO)) . x as Element of the_subsets_of_card (n,E) ; thus (the_extension_of_left_translation_of (n,(s1 * s2),LO)) . x = (LO ^ (s1 * s2)) .: X1 by A1, Def4 .= ((LO ^ s1) * (LO ^ s2)) .: X1 by Def1 .= (LO ^ s1) .: ((LO ^ s2) .: X1) by RELAT_1:126 .= (LO ^ s1) .: X2 by A1, Def4 .= (the_extension_of_left_translation_of (n,s1,LO)) . ((the_extension_of_left_translation_of (n,s2,LO)) . x) by A1, Def4 ; ::_thesis: verum end; hence H1(s1 * s2) = H1(s1) * H1(s2) by A6, FUNCT_1:10; ::_thesis: verum end; A10: H1( 1_ S) = id (the_subsets_of_card (n,E)) proof set f = the_extension_of_left_translation_of (n,(1_ S),LO); A11: now__::_thesis:_for_x_being_set_st_x_in_the_subsets_of_card_(n,E)_holds_ (the_extension_of_left_translation_of_(n,(1__S),LO))_._x_=_x let x be set ; ::_thesis: ( x in the_subsets_of_card (n,E) implies (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = x ) assume x in the_subsets_of_card (n,E) ; ::_thesis: (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = x then reconsider X = x as Element of the_subsets_of_card (n,E) ; not the_subsets_of_card (n,E) is empty by A1, Th1; then X in the_subsets_of_card (n,E) ; then consider X9 being Subset of E such that A12: X9 = X and card X9 = n ; (the_extension_of_left_translation_of (n,(1_ S),LO)) . X = (LO ^ (1_ S)) .: X by A1, Def4; then (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = (id E) .: X9 by A12, Def1 .= X9 by FUNCT_1:92 ; hence (the_extension_of_left_translation_of (n,(1_ S),LO)) . x = x by A12; ::_thesis: verum end; the_extension_of_left_translation_of (n,(1_ S),LO) in Funcs ((the_subsets_of_card (n,E)),(the_subsets_of_card (n,E))) by FUNCT_2:9; then ex f9 being Function st ( the_extension_of_left_translation_of (n,(1_ S),LO) = f9 & dom f9 = the_subsets_of_card (n,E) & rng f9 c= the_subsets_of_card (n,E) ) by FUNCT_2:def_2; hence H1( 1_ S) = id (the_subsets_of_card (n,E)) by A11, FUNCT_1:17; ::_thesis: verum end; ex T being LeftOperation of S,(the_subsets_of_card (n,E)) st for s being Element of S holds T . s = H1(s) from GROUP_10:sch_1(A10, A2); hence 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) ; ::_thesis: verum end; 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 proof let T1, T2 be LeftOperation of S,(the_subsets_of_card (n,E)); ::_thesis: ( ( for s being Element of S holds T1 . s = the_extension_of_left_translation_of (n,s,LO) ) & ( for s being Element of S holds T2 . s = the_extension_of_left_translation_of (n,s,LO) ) implies T1 = T2 ) assume that A13: for s being Element of S holds T1 . s = the_extension_of_left_translation_of (n,s,LO) and A14: for s being Element of S holds T2 . s = the_extension_of_left_translation_of (n,s,LO) ; ::_thesis: T1 = T2 let x be Element of S; :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ thus T1 . x = the_extension_of_left_translation_of (n,x,LO) by A13 .= T2 . x by A14 ; ::_thesis: verum end; 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] ) proof set E = [: the carrier of S,Z:]; set f = { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ; A1: now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[z1,z2]_where_z1,_z2_is_Element_of_[:_the_carrier_of_S,Z:]_:_ex_s1,_s2_being_Element_of_S_ex_z_being_Element_of_Z_st_ (_s2_=_s_*_s1_&_z1_=_[s1,z]_&_z2_=_[s2,z]_)__}__&_[x,y2]_in__{__[z1,z2]_where_z1,_z2_is_Element_of_[:_the_carrier_of_S,Z:]_:_ex_s1,_s2_being_Element_of_S_ex_z_being_Element_of_Z_st_ (_s2_=_s_*_s1_&_z1_=_[s1,z]_&_z2_=_[s2,z]_)__}__holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } & [x,y2] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } implies y1 = y2 ) assume [x,y1] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ; ::_thesis: ( [x,y2] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } implies y1 = y2 ) then consider z19, z29 being Element of [: the carrier of S,Z:] such that A2: [x,y1] = [z19,z29] and A3: ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z19 = [s1,z] & z29 = [s2,z] ) ; consider s19, s29 being Element of S, z9 being Element of Z such that A4: s29 = s * s19 and A5: z19 = [s19,z9] and A6: z29 = [s29,z9] by A3; assume [x,y2] in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ; ::_thesis: y1 = y2 then consider z199, z299 being Element of [: the carrier of S,Z:] such that A7: [x,y2] = [z199,z299] and A8: ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z199 = [s1,z] & z299 = [s2,z] ) ; consider s199, s299 being Element of S, z99 being Element of Z such that A9: s299 = s * s199 and A10: z199 = [s199,z99] and A11: z299 = [s299,z99] by A8; x = z199 by A7, XTUPLE_0:1; then [s19,z9] = [s199,z99] by A2, A5, A10, XTUPLE_0:1; then ( s19 = s199 & z9 = z99 ) by XTUPLE_0:1; hence y1 = y2 by A2, A4, A5, A6, A7, A9, A10, A11, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in__{__[z1,z2]_where_z1,_z2_is_Element_of_[:_the_carrier_of_S,Z:]_:_ex_s1,_s2_being_Element_of_S_ex_z_being_Element_of_Z_st_ (_s2_=_s_*_s1_&_z1_=_[s1,z]_&_z2_=_[s2,z]_)__}__holds_ ex_y,_z_being_set_st_x_=_[y,z] let x be set ; ::_thesis: ( x in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } implies ex y, z being set st x = [y,z] ) assume x in { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } ; ::_thesis: ex y, z being set st x = [y,z] then consider z1, z2 being Element of [: the carrier of S,Z:] such that A12: x = [z1,z2] and ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ; reconsider y = z1, z = z2 as set ; take y = y; ::_thesis: ex z being set st x = [y,z] take z = z; ::_thesis: x = [y,z] thus x = [y,z] by A12; ::_thesis: verum end; then reconsider f = { [z1,z2] where z1, z2 is Element of [: the carrier of S,Z:] : ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) } as Function by A1, FUNCT_1:def_1, RELAT_1:def_1; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_[:_the_carrier_of_S,Z:]_implies_ex_y_being_set_st_[x,y]_in_f_)_&_(_ex_y_being_set_st_[x,y]_in_f_implies_x_in_[:_the_carrier_of_S,Z:]_)_) let x be set ; ::_thesis: ( ( x in [: the carrier of S,Z:] implies ex y being set st [x,y] in f ) & ( ex y being set st [x,y] in f implies x in [: the carrier of S,Z:] ) ) hereby ::_thesis: ( ex y being set st [x,y] in f implies x in [: the carrier of S,Z:] ) assume x in [: the carrier of S,Z:] ; ::_thesis: ex y being set st [x,y] in f then consider s1, z being set such that A13: s1 in the carrier of S and A14: z in Z and A15: x = [s1,z] by ZFMISC_1:def_2; reconsider z = z as Element of Z by A14; reconsider s1 = s1 as Element of S by A13; set s2 = s * s1; reconsider y = [(s * s1),z] as set ; take y = y; ::_thesis: [x,y] in f x = [s1,z] by A15; hence [x,y] in f ; ::_thesis: verum end; given y being set such that A16: [x,y] in f ; ::_thesis: x in [: the carrier of S,Z:] consider z1, z2 being Element of [: the carrier of S,Z:] such that A17: [x,y] = [z1,z2] and ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) by A16; x = z1 by A17, XTUPLE_0:1; hence x in [: the carrier of S,Z:] ; ::_thesis: verum end; then A18: dom f = [: the carrier of S,Z:] by XTUPLE_0:def_12; now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_[:_the_carrier_of_S,Z:] let y be set ; ::_thesis: ( y in rng f implies y in [: the carrier of S,Z:] ) assume y in rng f ; ::_thesis: y in [: the carrier of S,Z:] then consider x being set such that A19: [x,y] in f by XTUPLE_0:def_13; consider z1, z2 being Element of [: the carrier of S,Z:] such that A20: [x,y] = [z1,z2] and ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) by A19; y = z2 by A20, XTUPLE_0:1; hence y in [: the carrier of S,Z:] ; ::_thesis: verum end; then rng f c= [: the carrier of S,Z:] by TARSKI:def_3; then reconsider f = f as Function of [: the carrier of S,Z:],[: the carrier of S,Z:] by A18, FUNCT_2:2; take f ; ::_thesis: 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 = f . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) thus 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 = f . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ::_thesis: verum proof let z1 be Element of [: the carrier of S,Z:]; ::_thesis: 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 = f . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) set z2 = f . z1; [z1,(f . z1)] in f by A18, FUNCT_1:1; then consider z19, z29 being Element of [: the carrier of S,Z:] such that A21: [z1,(f . z1)] = [z19,z29] and A22: ex s1, s2 being Element of S ex z being Element of Z st ( s2 = s * s1 & z19 = [s1,z] & z29 = [s2,z] ) ; consider s1, s2 being Element of S, z being Element of Z such that A23: ( s2 = s * s1 & z19 = [s1,z] & z29 = [s2,z] ) by A22; take f . z1 ; ::_thesis: ex s1, s2 being Element of S ex z being Element of Z st ( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] ) take s1 ; ::_thesis: ex s2 being Element of S ex z being Element of Z st ( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] ) take s2 ; ::_thesis: ex z being Element of Z st ( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] ) take z ; ::_thesis: ( f . z1 = f . z1 & s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] ) thus f . z1 = f . z1 ; ::_thesis: ( s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] ) thus ( s2 = s * s1 & z1 = [s1,z] & f . z1 = [s2,z] ) by A21, A23, XTUPLE_0:1; ::_thesis: verum end; end; 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 proof let IT1, IT2 be Function of [: the carrier of S,Z:],[: the carrier of S,Z:]; ::_thesis: ( ( 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 = IT1 . 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 = IT2 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ) implies IT1 = IT2 ) assume that A24: 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 = IT1 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) and A25: 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 = IT2 . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) ; ::_thesis: IT1 = IT2 let x be Element of [: the carrier of S,Z:]; :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ consider z12 being Element of [: the carrier of S,Z:], s11, s12 being Element of S, z9 being Element of Z such that A26: ( z12 = IT1 . x & s12 = s * s11 ) and A27: x = [s11,z9] and A28: z12 = [s12,z9] by A24; consider z22 being Element of [: the carrier of S,Z:], s21, s22 being Element of S, z99 being Element of Z such that A29: ( z22 = IT2 . x & s22 = s * s21 ) and A30: x = [s21,z99] and A31: z22 = [s22,z99] by A25; s11 = s21 by A27, A30, XTUPLE_0:1; hence IT1 . x = IT2 . x by A26, A27, A28, A29, A30, A31, XTUPLE_0:1; ::_thesis: verum end; 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) proof deffunc H1( Element of S) -> Function of [: the carrier of S,Z:],[: the carrier of S,Z:] = the_left_translation_of ($1,Z); set E = [: the carrier of S,Z:]; A1: for s1, s2 being Element of S holds H1(s1 * s2) = H1(s1) * H1(s2) proof let s1, s2 be Element of S; ::_thesis: H1(s1 * s2) = H1(s1) * H1(s2) set f12 = the_left_translation_of ((s1 * s2),Z); set f1 = the_left_translation_of (s1,Z); set f2 = the_left_translation_of (s2,Z); the_left_translation_of (s1,Z) in Funcs ([: the carrier of S,Z:],[: the carrier of S,Z:]) by FUNCT_2:9; then A2: ex f being Function st ( the_left_translation_of (s1,Z) = f & dom f = [: the carrier of S,Z:] & rng f c= [: the carrier of S,Z:] ) by FUNCT_2:def_2; the_left_translation_of (s2,Z) in Funcs ([: the carrier of S,Z:],[: the carrier of S,Z:]) by FUNCT_2:9; then A3: ex f being Function st ( the_left_translation_of (s2,Z) = f & dom f = [: the carrier of S,Z:] & rng f c= [: the carrier of S,Z:] ) by FUNCT_2:def_2; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_left_translation_of_((s1_*_s2),Z))_holds_ (the_left_translation_of_((s1_*_s2),Z))_._x_=_(the_left_translation_of_(s1,Z))_._((the_left_translation_of_(s2,Z))_._x) let x be set ; ::_thesis: ( x in dom (the_left_translation_of ((s1 * s2),Z)) implies (the_left_translation_of ((s1 * s2),Z)) . x = (the_left_translation_of (s1,Z)) . ((the_left_translation_of (s2,Z)) . x) ) assume A5: x in dom (the_left_translation_of ((s1 * s2),Z)) ; ::_thesis: (the_left_translation_of ((s1 * s2),Z)) . x = (the_left_translation_of (s1,Z)) . ((the_left_translation_of (s2,Z)) . x) then reconsider z19 = x as Element of [: the carrier of S,Z:] ; reconsider z1999 = x as Element of [: the carrier of S,Z:] by A5; consider z29 being Element of [: the carrier of S,Z:], s19, s29 being Element of S, z9 being Element of Z such that A6: z29 = (the_left_translation_of (s2,Z)) . z19 and A7: s29 = s2 * s19 and A8: z19 = [s19,z9] and A9: z29 = [s29,z9] by Def6; (the_left_translation_of (s2,Z)) . x in rng (the_left_translation_of (s2,Z)) by A3, A5, FUNCT_1:3; then reconsider z199 = (the_left_translation_of (s2,Z)) . x as Element of [: the carrier of S,Z:] ; consider z299 being Element of [: the carrier of S,Z:], s199, s299 being Element of S, z99 being Element of Z such that A10: z299 = (the_left_translation_of (s1,Z)) . z199 and A11: s299 = s1 * s199 and A12: z199 = [s199,z99] and A13: z299 = [s299,z99] by Def6; A14: z99 = z9 by A6, A9, A12, XTUPLE_0:1; consider z2999 being Element of [: the carrier of S,Z:], s1999, s2999 being Element of S, z999 being Element of Z such that A15: z2999 = (the_left_translation_of ((s1 * s2),Z)) . z1999 and A16: s2999 = (s1 * s2) * s1999 and A17: z1999 = [s1999,z999] and A18: z2999 = [s2999,z999] by Def6; s2999 = (s1 * s2) * s19 by A8, A16, A17, XTUPLE_0:1 .= s1 * (s2 * s19) by GROUP_1:def_3 .= s299 by A6, A7, A9, A11, A12, XTUPLE_0:1 ; hence (the_left_translation_of ((s1 * s2),Z)) . x = (the_left_translation_of (s1,Z)) . ((the_left_translation_of (s2,Z)) . x) by A8, A10, A13, A15, A17, A18, A14, XTUPLE_0:1; ::_thesis: verum end; the_left_translation_of ((s1 * s2),Z) in Funcs ([: the carrier of S,Z:],[: the carrier of S,Z:]) by FUNCT_2:9; then A19: ex f being Function st ( the_left_translation_of ((s1 * s2),Z) = f & dom f = [: the carrier of S,Z:] & rng f c= [: the carrier of S,Z:] ) by FUNCT_2:def_2; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(the_left_translation_of_((s1_*_s2),Z))_implies_(_x_in_dom_(the_left_translation_of_(s2,Z))_&_(the_left_translation_of_(s2,Z))_._x_in_dom_(the_left_translation_of_(s1,Z))_)_)_&_(_x_in_dom_(the_left_translation_of_(s2,Z))_&_(the_left_translation_of_(s2,Z))_._x_in_dom_(the_left_translation_of_(s1,Z))_implies_x_in_dom_(the_left_translation_of_((s1_*_s2),Z))_)_) let x be set ; ::_thesis: ( ( x in dom (the_left_translation_of ((s1 * s2),Z)) implies ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) ) ) & ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) implies x in dom (the_left_translation_of ((s1 * s2),Z)) ) ) hereby ::_thesis: ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) implies x in dom (the_left_translation_of ((s1 * s2),Z)) ) assume A20: x in dom (the_left_translation_of ((s1 * s2),Z)) ; ::_thesis: ( x in dom (the_left_translation_of (s2,Z)) & (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) ) hence x in dom (the_left_translation_of (s2,Z)) by A3; ::_thesis: (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) (the_left_translation_of (s2,Z)) . x in rng (the_left_translation_of (s2,Z)) by A3, A20, FUNCT_1:3; hence (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) by A2; ::_thesis: verum end; assume that A21: x in dom (the_left_translation_of (s2,Z)) and (the_left_translation_of (s2,Z)) . x in dom (the_left_translation_of (s1,Z)) ; ::_thesis: x in dom (the_left_translation_of ((s1 * s2),Z)) thus x in dom (the_left_translation_of ((s1 * s2),Z)) by A19, A21; ::_thesis: verum end; hence H1(s1 * s2) = H1(s1) * H1(s2) by A4, FUNCT_1:10; ::_thesis: verum end; A22: H1( 1_ S) = id [: the carrier of S,Z:] proof set f = the_left_translation_of ((1_ S),Z); A23: now__::_thesis:_for_x_being_set_st_x_in_[:_the_carrier_of_S,Z:]_holds_ (the_left_translation_of_((1__S),Z))_._x_=_x let x be set ; ::_thesis: ( x in [: the carrier of S,Z:] implies (the_left_translation_of ((1_ S),Z)) . x = x ) assume x in [: the carrier of S,Z:] ; ::_thesis: (the_left_translation_of ((1_ S),Z)) . x = x then reconsider z1 = x as 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 = (the_left_translation_of ((1_ S),Z)) . z1 & s2 = (1_ S) * s1 & z1 = [s1,z] & z2 = [s2,z] ) by Def6; hence (the_left_translation_of ((1_ S),Z)) . x = x by GROUP_1:def_4; ::_thesis: verum end; the_left_translation_of ((1_ S),Z) in Funcs ([: the carrier of S,Z:],[: the carrier of S,Z:]) by FUNCT_2:9; then ex f9 being Function st ( the_left_translation_of ((1_ S),Z) = f9 & dom f9 = [: the carrier of S,Z:] & rng f9 c= [: the carrier of S,Z:] ) by FUNCT_2:def_2; hence H1( 1_ S) = id [: the carrier of S,Z:] by A23, FUNCT_1:17; ::_thesis: verum end; ex T being LeftOperation of S,[: the carrier of S,Z:] st for s being Element of S holds T . s = H1(s) from GROUP_10:sch_1(A22, A1); hence 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) ; ::_thesis: verum end; 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 proof let T1, T2 be LeftOperation of S,[: the carrier of S,Z:]; ::_thesis: ( ( for s being Element of S holds T1 . s = the_left_translation_of (s,Z) ) & ( for s being Element of S holds T2 . s = the_left_translation_of (s,Z) ) implies T1 = T2 ) assume that A24: for s being Element of S holds T1 . s = the_left_translation_of (s,Z) and A25: for s being Element of S holds T2 . s = the_left_translation_of (s,Z) ; ::_thesis: T1 = T2 let x be Element of S; :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ thus T1 . x = the_left_translation_of (x,Z) by A24 .= T2 . x by A25 ; ::_thesis: verum end; 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 ) proof set f = { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ; A1: now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[P1,P2]_where_P1,_P2_is_Element_of_Left_Cosets_P_:_ex_A1,_A2_being_Subset_of_G_ex_g_being_Element_of_G_st_ (_A2_=_g_*_A1_&_A1_=_P1_&_A2_=_P2_&_g_=_h_)__}__&_[x,y2]_in__{__[P1,P2]_where_P1,_P2_is_Element_of_Left_Cosets_P_:_ex_A1,_A2_being_Subset_of_G_ex_g_being_Element_of_G_st_ (_A2_=_g_*_A1_&_A1_=_P1_&_A2_=_P2_&_g_=_h_)__}__holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } & [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies y1 = y2 ) assume [x,y1] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ; ::_thesis: ( [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies y1 = y2 ) then consider P19, P29 being Element of Left_Cosets P such that A2: [x,y1] = [P19,P29] and A3: ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P19 & A2 = P29 & g = h ) ; A4: x = P19 by A2, XTUPLE_0:1; assume [x,y2] in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ; ::_thesis: y1 = y2 then consider P199, P299 being Element of Left_Cosets P such that A5: [x,y2] = [P199,P299] and A6: ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P199 & A2 = P299 & g = h ) ; x = P199 by A5, XTUPLE_0:1; hence y1 = y2 by A2, A3, A5, A6, A4, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in__{__[P1,P2]_where_P1,_P2_is_Element_of_Left_Cosets_P_:_ex_A1,_A2_being_Subset_of_G_ex_g_being_Element_of_G_st_ (_A2_=_g_*_A1_&_A1_=_P1_&_A2_=_P2_&_g_=_h_)__}__holds_ ex_y,_z_being_set_st_x_=_[y,z] let x be set ; ::_thesis: ( x in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } implies ex y, z being set st x = [y,z] ) assume x in { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } ; ::_thesis: ex y, z being set st x = [y,z] then consider P1, P2 being Element of Left_Cosets P such that A7: x = [P1,P2] and ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ; reconsider y = P1, z = P2 as set ; take y = y; ::_thesis: ex z being set st x = [y,z] take z = z; ::_thesis: x = [y,z] thus x = [y,z] by A7; ::_thesis: verum end; then reconsider f = { [P1,P2] where P1, P2 is Element of Left_Cosets P : ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) } as Function by A1, FUNCT_1:def_1, RELAT_1:def_1; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Left_Cosets_P_implies_ex_y_being_set_st_[x,y]_in_f_)_&_(_ex_y_being_set_st_[x,y]_in_f_implies_x_in_Left_Cosets_P_)_) let x be set ; ::_thesis: ( ( x in Left_Cosets P implies ex y being set st [x,y] in f ) & ( ex y being set st [x,y] in f implies x in Left_Cosets P ) ) hereby ::_thesis: ( ex y being set st [x,y] in f implies x in Left_Cosets P ) reconsider g = h as Element of G by GROUP_2:42; assume x in Left_Cosets P ; ::_thesis: ex y being set st [x,y] in f then consider a being Element of G such that A8: x = a * P by GROUP_2:def_15; reconsider P1 = x as Element of Left_Cosets P by A8, GROUP_2:def_15; reconsider y = g * (a * P) as set ; take y = y; ::_thesis: [x,y] in f g * (a * P) = (g * a) * P by GROUP_2:105; then reconsider P2 = y as Element of Left_Cosets P by GROUP_2:def_15; ex A1, A2 being Subset of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 ) by A8; hence [x,y] in f ; ::_thesis: verum end; given y being set such that A9: [x,y] in f ; ::_thesis: x in Left_Cosets P consider P1, P2 being Element of Left_Cosets P such that A10: [x,y] = [P1,P2] and ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) by A9; A11: not Left_Cosets P is empty by GROUP_2:135; x = P1 by A10, XTUPLE_0:1; hence x in Left_Cosets P by A11; ::_thesis: verum end; then A12: dom f = Left_Cosets P by XTUPLE_0:def_12; now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_Left_Cosets_P let y be set ; ::_thesis: ( y in rng f implies y in Left_Cosets P ) A13: not Left_Cosets P is empty by GROUP_2:135; assume y in rng f ; ::_thesis: y in Left_Cosets P then consider x being set such that A14: ( x in dom f & y = f . x ) by FUNCT_1:def_3; [x,y] in f by A14, FUNCT_1:1; then consider P1, P2 being Element of Left_Cosets P such that A15: [x,y] = [P1,P2] and ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P1 & A2 = P2 & h = g ) ; y = P2 by A15, XTUPLE_0:1; hence y in Left_Cosets P by A13; ::_thesis: verum end; then rng f c= Left_Cosets P by TARSKI:def_3; then reconsider f = f as Function of (Left_Cosets P),(Left_Cosets P) by A12, FUNCT_2:2; take f ; ::_thesis: 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 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) thus 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 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ::_thesis: verum proof let P1 be Element of Left_Cosets P; ::_thesis: ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st ( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) set P2 = f . P1; not Left_Cosets P is empty by GROUP_2:135; then [P1,(f . P1)] in f by A12, FUNCT_1:1; then consider P19, P29 being Element of Left_Cosets P such that A16: [P1,(f . P1)] = [P19,P29] and A17: ex A1, A2 being Subset of G ex g being Element of G st ( A2 = g * A1 & A1 = P19 & A2 = P29 & h = g ) ; reconsider P2 = f . P1 as Element of Left_Cosets P by A16, XTUPLE_0:1; consider A1, A2 being Subset of G, g being Element of G such that A18: ( A2 = g * A1 & A1 = P19 ) and A2 = P29 and A19: h = g by A17; take P2 ; ::_thesis: ex A1, A2 being Subset of G ex g being Element of G st ( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) take A1 ; ::_thesis: ex A2 being Subset of G ex g being Element of G st ( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) take A2 ; ::_thesis: ex g being Element of G st ( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) take g ; ::_thesis: ( P2 = f . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) thus P2 = f . P1 ; ::_thesis: ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) thus ( A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) by A16, A17, A18, A19, XTUPLE_0:1; ::_thesis: verum end; end; 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 proof let IT1, IT2 be Function of (Left_Cosets P),(Left_Cosets P); ::_thesis: ( ( 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 = IT1 . 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 = IT2 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) implies IT1 = IT2 ) assume A20: ( ( 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 = IT1 . 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 = IT2 . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) ) ) ; ::_thesis: IT1 = IT2 let x be Element of Left_Cosets P; :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ ( ex P12 being Element of Left_Cosets P ex A11, A12 being Subset of G ex g1 being Element of G st ( P12 = IT1 . x & A12 = g1 * A11 & A11 = x & A12 = P12 & g1 = h ) & ex P22 being Element of Left_Cosets P ex A21, A22 being Subset of G ex g2 being Element of G st ( P22 = IT2 . x & A22 = g2 * A21 & A21 = x & A22 = P22 & g2 = h ) ) by A20; hence ^ = ^ ; ::_thesis: verum end; 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) proof deffunc H1( Element of H) -> Function of (Left_Cosets P),(Left_Cosets P) = the_left_translation_of ($1,P); A1: for h1, h2 being Element of H holds H1(h1 * h2) = H1(h1) * H1(h2) proof let h1, h2 be Element of H; ::_thesis: H1(h1 * h2) = H1(h1) * H1(h2) set f12 = the_left_translation_of ((h1 * h2),P); set f1 = the_left_translation_of (h1,P); set f2 = the_left_translation_of (h2,P); the_left_translation_of (h1,P) in Funcs ((Left_Cosets P),(Left_Cosets P)) by FUNCT_2:9; then A2: ex f being Function st ( the_left_translation_of (h1,P) = f & dom f = Left_Cosets P & rng f c= Left_Cosets P ) by FUNCT_2:def_2; the_left_translation_of (h2,P) in Funcs ((Left_Cosets P),(Left_Cosets P)) by FUNCT_2:9; then A3: ex f being Function st ( the_left_translation_of (h2,P) = f & dom f = Left_Cosets P & rng f c= Left_Cosets P ) by FUNCT_2:def_2; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_left_translation_of_((h1_*_h2),P))_holds_ (the_left_translation_of_((h1_*_h2),P))_._x_=_(the_left_translation_of_(h1,P))_._((the_left_translation_of_(h2,P))_._x) let x be set ; ::_thesis: ( x in dom (the_left_translation_of ((h1 * h2),P)) implies (the_left_translation_of ((h1 * h2),P)) . x = (the_left_translation_of (h1,P)) . ((the_left_translation_of (h2,P)) . x) ) assume A5: x in dom (the_left_translation_of ((h1 * h2),P)) ; ::_thesis: (the_left_translation_of ((h1 * h2),P)) . x = (the_left_translation_of (h1,P)) . ((the_left_translation_of (h2,P)) . x) then reconsider P19 = x as Element of Left_Cosets P ; (the_left_translation_of (h2,P)) . x in rng (the_left_translation_of (h2,P)) by A3, A5, FUNCT_1:3; then reconsider P199 = (the_left_translation_of (h2,P)) . x as Element of Left_Cosets P ; consider P299 being Element of Left_Cosets P, A199, A299 being Subset of G, g99 being Element of G such that A6: ( P299 = (the_left_translation_of (h1,P)) . P199 & A299 = g99 * A199 & A199 = P199 & A299 = P299 ) and A7: g99 = h1 by Def8; reconsider P1999 = x as Element of Left_Cosets P by A5; consider P29 being Element of Left_Cosets P, A19, A29 being Subset of G, g9 being Element of G such that A8: ( P29 = (the_left_translation_of (h2,P)) . P19 & A29 = g9 * A19 & A19 = P19 & A29 = P29 ) and A9: g9 = h2 by Def8; consider P2999 being Element of Left_Cosets P, A1999, A2999 being Subset of G, g999 being Element of G such that A10: ( P2999 = (the_left_translation_of ((h1 * h2),P)) . P1999 & A2999 = g999 * A1999 & A1999 = P1999 & A2999 = P2999 ) and A11: g999 = h1 * h2 by Def8; g999 = g99 * g9 by A9, A7, A11, GROUP_2:43; hence (the_left_translation_of ((h1 * h2),P)) . x = (the_left_translation_of (h1,P)) . ((the_left_translation_of (h2,P)) . x) by A8, A6, A10, GROUP_2:32; ::_thesis: verum end; the_left_translation_of ((h1 * h2),P) in Funcs ((Left_Cosets P),(Left_Cosets P)) by FUNCT_2:9; then A12: ex f being Function st ( the_left_translation_of ((h1 * h2),P) = f & dom f = Left_Cosets P & rng f c= Left_Cosets P ) by FUNCT_2:def_2; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(the_left_translation_of_((h1_*_h2),P))_implies_(_x_in_dom_(the_left_translation_of_(h2,P))_&_(the_left_translation_of_(h2,P))_._x_in_dom_(the_left_translation_of_(h1,P))_)_)_&_(_x_in_dom_(the_left_translation_of_(h2,P))_&_(the_left_translation_of_(h2,P))_._x_in_dom_(the_left_translation_of_(h1,P))_implies_x_in_dom_(the_left_translation_of_((h1_*_h2),P))_)_) let x be set ; ::_thesis: ( ( x in dom (the_left_translation_of ((h1 * h2),P)) implies ( x in dom (the_left_translation_of (h2,P)) & (the_left_translation_of (h2,P)) . x in dom (the_left_translation_of (h1,P)) ) ) & ( x in dom (the_left_translation_of (h2,P)) & (the_left_translation_of (h2,P)) . x in dom (the_left_translation_of (h1,P)) implies x in dom (the_left_translation_of ((h1 * h2),P)) ) ) hereby ::_thesis: ( x in dom (the_left_translation_of (h2,P)) & (the_left_translation_of (h2,P)) . x in dom (the_left_translation_of (h1,P)) implies x in dom (the_left_translation_of ((h1 * h2),P)) ) assume A13: x in dom (the_left_translation_of ((h1 * h2),P)) ; ::_thesis: ( x in dom (the_left_translation_of (h2,P)) & (the_left_translation_of (h2,P)) . x in dom (the_left_translation_of (h1,P)) ) hence x in dom (the_left_translation_of (h2,P)) by A3; ::_thesis: (the_left_translation_of (h2,P)) . x in dom (the_left_translation_of (h1,P)) (the_left_translation_of (h2,P)) . x in rng (the_left_translation_of (h2,P)) by A3, A13, FUNCT_1:3; hence (the_left_translation_of (h2,P)) . x in dom (the_left_translation_of (h1,P)) by A2; ::_thesis: verum end; assume that A14: x in dom (the_left_translation_of (h2,P)) and (the_left_translation_of (h2,P)) . x in dom (the_left_translation_of (h1,P)) ; ::_thesis: x in dom (the_left_translation_of ((h1 * h2),P)) thus x in dom (the_left_translation_of ((h1 * h2),P)) by A12, A14; ::_thesis: verum end; hence H1(h1 * h2) = H1(h1) * H1(h2) by A4, FUNCT_1:10; ::_thesis: verum end; A15: H1( 1_ H) = id (Left_Cosets P) proof set f = the_left_translation_of ((1_ H),P); A16: now__::_thesis:_for_x_being_set_st_x_in_Left_Cosets_P_holds_ (the_left_translation_of_((1__H),P))_._x_=_x let x be set ; ::_thesis: ( x in Left_Cosets P implies (the_left_translation_of ((1_ H),P)) . x = x ) assume x in Left_Cosets P ; ::_thesis: (the_left_translation_of ((1_ H),P)) . x = x then reconsider P1 = x as 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 = (the_left_translation_of ((1_ H),P)) . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = 1_ H ) & 1_ H = 1_ G ) by Def8, GROUP_2:44; hence (the_left_translation_of ((1_ H),P)) . x = x by GROUP_2:37; ::_thesis: verum end; the_left_translation_of ((1_ H),P) in Funcs ((Left_Cosets P),(Left_Cosets P)) by FUNCT_2:9; then ex f9 being Function st ( the_left_translation_of ((1_ H),P) = f9 & dom f9 = Left_Cosets P & rng f9 c= Left_Cosets P ) by FUNCT_2:def_2; hence H1( 1_ H) = id (Left_Cosets P) by A16, FUNCT_1:17; ::_thesis: verum end; ex T being LeftOperation of H,(Left_Cosets P) st for h being Element of H holds T . h = H1(h) from GROUP_10:sch_1(A15, A1); hence 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) ; ::_thesis: verum end; 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 proof let T1, T2 be LeftOperation of H,(Left_Cosets P); ::_thesis: ( ( for h being Element of H holds T1 . h = the_left_translation_of (h,P) ) & ( for h being Element of H holds T2 . h = the_left_translation_of (h,P) ) implies T1 = T2 ) assume that A17: for h being Element of H holds T1 . h = the_left_translation_of (h,P) and A18: for h being Element of H holds T2 . h = the_left_translation_of (h,P) ; ::_thesis: T1 = T2 let x be Element of H; :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ thus T1 . x = the_left_translation_of (x,P) by A17 .= T2 . x by A18 ; ::_thesis: verum end; 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 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 } proof set X = { g where g is Element of G : (T ^ g) .: A = A } ; now__::_thesis:_for_x_being_set_st_x_in__{__g_where_g_is_Element_of_G_:_(T_^_g)_.:_A_=_A__}__holds_ x_in_the_carrier_of_G let x be set ; ::_thesis: ( x in { g where g is Element of G : (T ^ g) .: A = A } implies x in the carrier of G ) assume x in { g where g is Element of G : (T ^ g) .: A = A } ; ::_thesis: x in the carrier of G then ex g being Element of G st ( x = g & (T ^ g) .: A = A ) ; hence x in the carrier of G ; ::_thesis: verum end; then reconsider X = { g where g is Element of G : (T ^ g) .: A = A } as Subset of G by TARSKI:def_3; A1: for g1, g2 being Element of G st g1 in X & g2 in X holds g1 * g2 in X proof let g1, g2 be Element of G; ::_thesis: ( g1 in X & g2 in X implies g1 * g2 in X ) assume g1 in X ; ::_thesis: ( not g2 in X or g1 * g2 in X ) then A2: ex g being Element of G st ( g = g1 & (T ^ g) .: A = A ) ; assume g2 in X ; ::_thesis: g1 * g2 in X then A3: ex g being Element of G st ( g = g2 & (T ^ g) .: A = A ) ; (T ^ (g1 * g2)) .: A = ((T ^ g1) * (T ^ g2)) .: A by Def1 .= A by A2, A3, RELAT_1:126 ; hence g1 * g2 in X ; ::_thesis: verum end; A4: (id E) .: A = A by FUNCT_1:92; A5: for g being Element of G st g in X holds g " in X proof let g be Element of G; ::_thesis: ( g in X implies g " in X ) assume g in X ; ::_thesis: g " in X then ex g9 being Element of G st ( g9 = g & (T ^ g9) .: A = A ) ; then (T ^ (g ")) .: A = ((T ^ (g ")) * (T ^ g)) .: A by RELAT_1:126 .= (T ^ ((g ") * g)) .: A by Def1 .= (T ^ (1_ G)) .: A by GROUP_1:def_5 .= A by A4, Def1 ; hence g " in X ; ::_thesis: verum end; (T ^ (1_ G)) .: A = A by A4, Def1; then 1_ G in X ; hence ex b1 being strict Subgroup of G st the carrier of b1 = { g where g is Element of G : (T ^ g) .: A = A } by A1, A5, GROUP_2:52; ::_thesis: verum end; 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; proof ( not E is empty implies { x where x is Element of E : x is_fixed_under T } is Subset of E ) proof set Y = { x where x is Element of E : x is_fixed_under T } ; defpred S1[ set ] means for x being Element of E st x = $1 holds x is_fixed_under T; consider X being Subset of E such that A1: for x being set holds ( x in X iff ( x in E & S1[x] ) ) from SUBSET_1:sch_1(); assume A2: not E is empty ; ::_thesis: { x where x is Element of E : x is_fixed_under T } is Subset of E now__::_thesis:_for_y_being_set_holds_ (_(_y_in_X_implies_y_in__{__x_where_x_is_Element_of_E_:_x_is_fixed_under_T__}__)_&_(_y_in__{__x_where_x_is_Element_of_E_:_x_is_fixed_under_T__}__implies_y_in_X_)_) let y be set ; ::_thesis: ( ( y in X implies y in { x where x is Element of E : x is_fixed_under T } ) & ( y in { x where x is Element of E : x is_fixed_under T } implies y in X ) ) hereby ::_thesis: ( y in { x where x is Element of E : x is_fixed_under T } implies y in X ) assume A3: y in X ; ::_thesis: y in { x where x is Element of E : x is_fixed_under T } then reconsider y9 = y as Element of E ; y9 is_fixed_under T by A1, A3; hence y in { x where x is Element of E : x is_fixed_under T } ; ::_thesis: verum end; assume y in { x where x is Element of E : x is_fixed_under T } ; ::_thesis: y in X then A4: ex y9 being Element of E st ( y = y9 & y9 is_fixed_under T ) ; then S1[y] ; hence y in X by A2, A1, A4; ::_thesis: verum end; hence { x where x is Element of E : x is_fixed_under T } is Subset of E by TARSKI:1; ::_thesis: verum end; hence ( ( 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 ) & ( for b1 being Subset of E holds verum ) ) ; ::_thesis: verum end; 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 ) ); 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 proof let S be non empty unital multMagma ; ::_thesis: 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 let E be non empty set ; ::_thesis: for x being Element of E for T being LeftOperation of S,E holds x,x are_conjugated_under T let x be Element of E; ::_thesis: for T being LeftOperation of S,E holds x,x are_conjugated_under T let T be LeftOperation of S,E; ::_thesis: x,x are_conjugated_under T x = (id E) . x by FUNCT_1:18 .= (T ^ (1_ S)) . x by Def1 ; hence x,x are_conjugated_under T by Def14; ::_thesis: verum end; 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 proof let G be Group; ::_thesis: 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 let E be non empty set ; ::_thesis: 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 let x, y be Element of E; ::_thesis: for T being LeftOperation of G,E st x,y are_conjugated_under T holds y,x are_conjugated_under T let T be LeftOperation of G,E; ::_thesis: ( x,y are_conjugated_under T implies y,x are_conjugated_under T ) assume x,y are_conjugated_under T ; ::_thesis: y,x are_conjugated_under T then consider g being Element of G such that A1: y = (T ^ g) . x by Def14; x in E ; then x in dom (T ^ g) by FUNCT_2:def_1; then (T ^ (g ")) . y = ((T ^ (g ")) * (T ^ g)) . x by A1, FUNCT_1:13 .= (T ^ ((g ") * g)) . x by Def1 .= (T ^ (1_ G)) . x by GROUP_1:def_5 .= (id E) . x by Def1 .= x by FUNCT_1:18 ; hence y,x are_conjugated_under T by Def14; ::_thesis: verum end; 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 proof let S be non empty unital multMagma ; ::_thesis: 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 let E be non empty set ; ::_thesis: 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 let x, y, z be Element of E; ::_thesis: 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 let T be LeftOperation of S,E; ::_thesis: ( x,y are_conjugated_under T & y,z are_conjugated_under T implies x,z are_conjugated_under T ) assume x,y are_conjugated_under T ; ::_thesis: ( not y,z are_conjugated_under T or x,z are_conjugated_under T ) then consider s1 being Element of S such that A1: y = (T ^ s1) . x by Def14; assume y,z are_conjugated_under T ; ::_thesis: x,z are_conjugated_under T then consider s2 being Element of S such that A2: z = (T ^ s2) . y by Def14; x in E ; then x in dom (T ^ s1) by FUNCT_2:def_1; then z = ((T ^ s2) * (T ^ s1)) . x by A1, A2, FUNCT_1:13 .= (T ^ (s2 * s1)) . x by Def1 ; hence x,z are_conjugated_under T by Def14; ::_thesis: verum end; 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; proof defpred S1[ set ] means for y being Element of E st y = $1 holds x,y are_conjugated_under T; set Y = { y where y is Element of E : x,y are_conjugated_under T } ; consider X being Subset of E such that A1: for y being Element of E holds ( y in X iff S1[y] ) from SUBSET_1:sch_3(); now__::_thesis:_for_y_being_set_holds_ (_(_y_in_X_implies_y_in__{__y_where_y_is_Element_of_E_:_x,y_are_conjugated_under_T__}__)_&_(_y_in__{__y_where_y_is_Element_of_E_:_x,y_are_conjugated_under_T__}__implies_y_in_X_)_) let y be set ; ::_thesis: ( ( y in X implies y in { y where y is Element of E : x,y are_conjugated_under T } ) & ( y in { y where y is Element of E : x,y are_conjugated_under T } implies y in X ) ) hereby ::_thesis: ( y in { y where y is Element of E : x,y are_conjugated_under T } implies y in X ) assume A2: y in X ; ::_thesis: y in { y where y is Element of E : x,y are_conjugated_under T } then reconsider y9 = y as Element of E ; x,y9 are_conjugated_under T by A1, A2; hence y in { y where y is Element of E : x,y are_conjugated_under T } ; ::_thesis: verum end; assume y in { y where y is Element of E : x,y are_conjugated_under T } ; ::_thesis: y in X then A3: ex y9 being Element of E st ( y9 = y & x,y9 are_conjugated_under T ) ; then S1[y] ; hence y in X by A1, A3; ::_thesis: verum end; hence { y where y is Element of E : x,y are_conjugated_under T } is Subset of E by TARSKI:1; ::_thesis: verum end; 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 proof x,x are_conjugated_under T by Th3; then x in { y where y is Element of E : x,y are_conjugated_under T } ; hence not the_orbit_of (x,T) is empty ; ::_thesis: verum end; 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) ) proof let G be Group; ::_thesis: 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) ) let E be non empty set ; ::_thesis: 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) ) let x, y be Element of E; ::_thesis: 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) ) let T be LeftOperation of G,E; ::_thesis: ( the_orbit_of (x,T) misses the_orbit_of (y,T) or the_orbit_of (x,T) = the_orbit_of (y,T) ) assume not the_orbit_of (x,T) misses the_orbit_of (y,T) ; ::_thesis: the_orbit_of (x,T) = the_orbit_of (y,T) then (the_orbit_of (x,T)) /\ (the_orbit_of (y,T)) <> {} by XBOOLE_0:def_7; then consider z1 being set such that A1: z1 in (the_orbit_of (x,T)) /\ (the_orbit_of (y,T)) by XBOOLE_0:def_1; z1 in the_orbit_of (y,T) by A1, XBOOLE_0:def_4; then consider z199 being Element of E such that A2: z1 = z199 and A3: y,z199 are_conjugated_under T ; z1 in the_orbit_of (x,T) by A1, XBOOLE_0:def_4; then consider z19 being Element of E such that A4: z1 = z19 and A5: x,z19 are_conjugated_under T ; now__::_thesis:_for_z2_being_set_holds_ (_(_z2_in_the_orbit_of_(x,T)_implies_z2_in_the_orbit_of_(y,T)_)_&_(_z2_in_the_orbit_of_(y,T)_implies_z2_in_the_orbit_of_(x,T)_)_) let z2 be set ; ::_thesis: ( ( z2 in the_orbit_of (x,T) implies z2 in the_orbit_of (y,T) ) & ( z2 in the_orbit_of (y,T) implies z2 in the_orbit_of (x,T) ) ) hereby ::_thesis: ( z2 in the_orbit_of (y,T) implies z2 in the_orbit_of (x,T) ) assume z2 in the_orbit_of (x,T) ; ::_thesis: z2 in the_orbit_of (y,T) then consider z29 being Element of E such that A6: z2 = z29 and A7: x,z29 are_conjugated_under T ; z29,x are_conjugated_under T by A7, Th4; then z29,z199 are_conjugated_under T by A4, A5, A2, Th5; then z199,z29 are_conjugated_under T by Th4; then y,z29 are_conjugated_under T by A3, Th5; hence z2 in the_orbit_of (y,T) by A6; ::_thesis: verum end; assume z2 in the_orbit_of (y,T) ; ::_thesis: z2 in the_orbit_of (x,T) then consider z29 being Element of E such that A8: z2 = z29 and A9: y,z29 are_conjugated_under T ; z29,y are_conjugated_under T by A9, Th4; then z29,z19 are_conjugated_under T by A4, A2, A3, Th5; then z19,z29 are_conjugated_under T by Th4; then x,z29 are_conjugated_under T by A5, Th5; hence z2 in the_orbit_of (x,T) by A8; ::_thesis: verum end; hence the_orbit_of (x,T) = the_orbit_of (y,T) by TARSKI:1; ::_thesis: verum end; 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} proof let S be non empty unital multMagma ; ::_thesis: 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} let E be non empty finite set ; ::_thesis: 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} let x be Element of E; ::_thesis: for T being LeftOperation of S,E st x is_fixed_under T holds the_orbit_of (x,T) = {x} let T be LeftOperation of S,E; ::_thesis: ( x is_fixed_under T implies the_orbit_of (x,T) = {x} ) set X = the_orbit_of (x,T); assume A1: x is_fixed_under T ; ::_thesis: the_orbit_of (x,T) = {x} now__::_thesis:_not_the_orbit_of_(x,T)_<>_{x} assume the_orbit_of (x,T) <> {x} ; ::_thesis: contradiction then A2: not for x9 being set holds ( x9 in the_orbit_of (x,T) iff x9 = x ) by TARSKI:def_1; ex x9 being set st x9 in the_orbit_of (x,T) by XBOOLE_0:def_1; then consider x99 being set such that A3: x99 <> x and A4: x99 in the_orbit_of (x,T) by A2; consider y9 being Element of E such that A5: x99 = y9 and A6: x,y9 are_conjugated_under T by A4; ex s being Element of S st y9 = (T ^ s) . x by A6, Def14; hence contradiction by A1, A3, A5, Def12; ::_thesis: verum end; hence the_orbit_of (x,T) = {x} ; ::_thesis: verum end; 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)) proof let G be Group; ::_thesis: 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)) let E be non empty set ; ::_thesis: 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)) let a be Element of E; ::_thesis: for T being LeftOperation of G,E holds card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T)) let T be LeftOperation of G,E; ::_thesis: card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T)) set H = the_strict_stabilizer_of (a,T); set f = { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ; reconsider A9 = {a} as Subset of E ; A1: now__::_thesis:_for_x_being_set_st_x_in__{__[b,A]_where_b_is_Element_of_E,_A_is_Subset_of_G_:_ex_g_being_Element_of_G_st_ (_b_=_(T_^_g)_._a_&_A_=_g_*_(the_strict_stabilizer_of_(a,T))_)__}__holds_ ex_b,_A_being_set_st_x_=_[b,A] let x be set ; ::_thesis: ( x in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } implies ex b, A being set st x = [b,A] ) assume x in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ; ::_thesis: ex b, A being set st x = [b,A] then consider b being Element of E, A being Subset of G such that A2: [b,A] = x and ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) ; reconsider b = b, A = A as set ; take b = b; ::_thesis: ex A being set st x = [b,A] take A = A; ::_thesis: x = [b,A] thus x = [b,A] by A2; ::_thesis: verum end; now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[b,A]_where_b_is_Element_of_E,_A_is_Subset_of_G_:_ex_g_being_Element_of_G_st_ (_b_=_(T_^_g)_._a_&_A_=_g_*_(the_strict_stabilizer_of_(a,T))_)__}__&_[x,y2]_in__{__[b,A]_where_b_is_Element_of_E,_A_is_Subset_of_G_:_ex_g_being_Element_of_G_st_ (_b_=_(T_^_g)_._a_&_A_=_g_*_(the_strict_stabilizer_of_(a,T))_)__}__holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } & [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } implies y1 = y2 ) assume [x,y1] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ; ::_thesis: ( [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } implies y1 = y2 ) then consider b1 being Element of E, A1 being Subset of G such that A3: [b1,A1] = [x,y1] and A4: ex g being Element of G st ( b1 = (T ^ g) . a & A1 = g * (the_strict_stabilizer_of (a,T)) ) ; assume [x,y2] in { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } ; ::_thesis: y1 = y2 then consider b2 being Element of E, A2 being Subset of G such that A5: [b2,A2] = [x,y2] and A6: ex g being Element of G st ( b2 = (T ^ g) . a & A2 = g * (the_strict_stabilizer_of (a,T)) ) ; A7: y2 = A2 by A5, XTUPLE_0:1; consider g1 being Element of G such that A8: b1 = (T ^ g1) . a and A9: A1 = g1 * (the_strict_stabilizer_of (a,T)) by A4; consider g2 being Element of G such that A10: b2 = (T ^ g2) . a and A11: A2 = g2 * (the_strict_stabilizer_of (a,T)) by A6; x = b2 by A5, XTUPLE_0:1; then ( dom (T ^ g1) = E & (T ^ g1) . a = (T ^ g2) . a ) by A3, A8, A10, FUNCT_2:def_1, XTUPLE_0:1; then ( dom (T ^ g2) = E & Im ((T ^ g1),a) = {((T ^ g2) . a)} ) by FUNCT_1:59, FUNCT_2:def_1; then A12: Im ((T ^ g1),a) = Im ((T ^ g2),a) by FUNCT_1:59; set g = (g2 ") * g1; reconsider g = (g2 ") * g1 as Element of G ; A13: the carrier of (the_strict_stabilizer_of (A9,T)) = { g9 where g9 is Element of G : (T ^ g9) .: A9 = A9 } by Def10; (T ^ g) .: A9 = ((T ^ (g2 ")) * (T ^ g1)) .: A9 by Def1 .= (T ^ (g2 ")) .: ((T ^ g1) .: A9) by RELAT_1:126 .= ((T ^ (g2 ")) * (T ^ g2)) .: A9 by A12, RELAT_1:126 .= (T ^ ((g2 ") * g2)) .: A9 by Def1 .= (T ^ (1_ G)) .: A9 by GROUP_1:def_5 .= (id E) .: A9 by Def1 .= A9 by FUNCT_1:92 ; then g in { g9 where g9 is Element of G : (T ^ g9) .: A9 = A9 } ; then A14: g in the_strict_stabilizer_of (A9,T) by A13, STRUCT_0:def_5; y1 = A1 by A3, XTUPLE_0:1; hence y1 = y2 by A7, A9, A11, A14, GROUP_2:114; ::_thesis: verum end; then reconsider f = { [b,A] where b is Element of E, A is Subset of G : ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) } as Function by A1, FUNCT_1:def_1, RELAT_1:def_1; for y being set holds ( y in Left_Cosets (the_strict_stabilizer_of (a,T)) iff ex x being set st [x,y] in f ) proof let y be set ; ::_thesis: ( y in Left_Cosets (the_strict_stabilizer_of (a,T)) iff ex x being set st [x,y] in f ) hereby ::_thesis: ( ex x being set st [x,y] in f implies y in Left_Cosets (the_strict_stabilizer_of (a,T)) ) assume A15: y in Left_Cosets (the_strict_stabilizer_of (a,T)) ; ::_thesis: ex x being set st [x,y] in f then reconsider A = y as Subset of G ; consider g being Element of G such that A16: A = g * (the_strict_stabilizer_of (a,T)) by A15, GROUP_2:def_15; reconsider x = (T ^ g) . a as set ; take x = x; ::_thesis: [x,y] in f thus [x,y] in f by A16; ::_thesis: verum end; given x being set such that A17: [x,y] in f ; ::_thesis: y in Left_Cosets (the_strict_stabilizer_of (a,T)) consider b being Element of E, A being Subset of G such that A18: [b,A] = [x,y] and A19: ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) by A17; A = y by A18, XTUPLE_0:1; hence y in Left_Cosets (the_strict_stabilizer_of (a,T)) by A19, GROUP_2:def_15; ::_thesis: verum end; then A20: rng f = Left_Cosets (the_strict_stabilizer_of (a,T)) by XTUPLE_0:def_13; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_f_&_x2_in_dom_f_&_f_._x1_=_f_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) A21: the carrier of (the_strict_stabilizer_of (A9,T)) = { g9 where g9 is Element of G : (T ^ g9) .: A9 = A9 } by Def10; assume x1 in dom f ; ::_thesis: ( x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) then [x1,(f . x1)] in f by FUNCT_1:1; then consider b1 being Element of E, A1 being Subset of G such that A22: [b1,A1] = [x1,(f . x1)] and A23: ex g being Element of G st ( b1 = (T ^ g) . a & A1 = g * (the_strict_stabilizer_of (a,T)) ) ; assume x2 in dom f ; ::_thesis: ( f . x1 = f . x2 implies x1 = x2 ) then [x2,(f . x2)] in f by FUNCT_1:1; then consider b2 being Element of E, A2 being Subset of G such that A24: [b2,A2] = [x2,(f . x2)] and A25: ex g being Element of G st ( b2 = (T ^ g) . a & A2 = g * (the_strict_stabilizer_of (a,T)) ) ; consider g2 being Element of G such that A26: b2 = (T ^ g2) . a and A27: A2 = g2 * (the_strict_stabilizer_of (a,T)) by A25; assume A28: f . x1 = f . x2 ; ::_thesis: x1 = x2 consider g1 being Element of G such that A29: b1 = (T ^ g1) . a and A30: A1 = g1 * (the_strict_stabilizer_of (a,T)) by A23; set g = (g2 ") * g1; f . x2 = A2 by A24, XTUPLE_0:1; then g1 * (the_strict_stabilizer_of (a,T)) = g2 * (the_strict_stabilizer_of (a,T)) by A22, A30, A27, A28, XTUPLE_0:1; then (g2 ") * g1 in the_strict_stabilizer_of (a,T) by GROUP_2:114; then (g2 ") * g1 in the carrier of (the_strict_stabilizer_of (A9,T)) by STRUCT_0:def_5; then A31: ex g9 being Element of G st ( (g2 ") * g1 = g9 & (T ^ g9) .: A9 = A9 ) by A21; (T ^ g1) .: A9 = (id E) .: ((T ^ g1) .: A9) by FUNCT_1:92 .= (T ^ (1_ G)) .: ((T ^ g1) .: A9) by Def1 .= (T ^ (g2 * (g2 "))) .: ((T ^ g1) .: A9) by GROUP_1:def_5 .= ((T ^ (g2 * (g2 "))) * (T ^ g1)) .: A9 by RELAT_1:126 .= (T ^ ((g2 * (g2 ")) * g1)) .: A9 by Def1 .= (T ^ (g2 * ((g2 ") * g1))) .: A9 by GROUP_1:def_3 .= ((T ^ g2) * (T ^ ((g2 ") * g1))) .: A9 by Def1 .= (T ^ g2) .: A9 by A31, RELAT_1:126 ; then ( dom (T ^ g2) = E & Im ((T ^ g1),a) = Im ((T ^ g2),a) ) by FUNCT_2:def_1; then ( dom (T ^ g1) = E & Im ((T ^ g1),a) = {((T ^ g2) . a)} ) by FUNCT_1:59, FUNCT_2:def_1; then A32: {((T ^ g1) . a)} = {((T ^ g2) . a)} by FUNCT_1:59; A33: x2 = b2 by A24, XTUPLE_0:1; x1 = b1 by A22, XTUPLE_0:1; hence x1 = x2 by A33, A29, A26, A32, ZFMISC_1:18; ::_thesis: verum end; then A34: f is one-to-one by FUNCT_1:def_4; for x being set holds ( x in the_orbit_of (a,T) iff ex y being set st [x,y] in f ) proof let x be set ; ::_thesis: ( x in the_orbit_of (a,T) iff ex y being set st [x,y] in f ) hereby ::_thesis: ( ex y being set st [x,y] in f implies x in the_orbit_of (a,T) ) assume x in the_orbit_of (a,T) ; ::_thesis: ex y being set st [x,y] in f then consider b being Element of E such that A35: b = x and A36: a,b are_conjugated_under T ; consider g being Element of G such that A37: b = (T ^ g) . a by A36, Def14; reconsider y = g * (the_strict_stabilizer_of (a,T)) as set ; take y = y; ::_thesis: [x,y] in f thus [x,y] in f by A35, A37; ::_thesis: verum end; given y being set such that A38: [x,y] in f ; ::_thesis: x in the_orbit_of (a,T) consider b being Element of E, A being Subset of G such that A39: ( [b,A] = [x,y] & ex g being Element of G st ( b = (T ^ g) . a & A = g * (the_strict_stabilizer_of (a,T)) ) ) by A38; ( b = x & a,b are_conjugated_under T ) by A39, Def14, XTUPLE_0:1; hence x in the_orbit_of (a,T) ; ::_thesis: verum end; then dom f = the_orbit_of (a,T) by XTUPLE_0:def_12; then the_orbit_of (a,T), Left_Cosets (the_strict_stabilizer_of (a,T)) are_equipotent by A34, A20, WELLORD2:def_4; hence card (the_orbit_of (a,T)) = Index (the_strict_stabilizer_of (a,T)) by CARD_1:5; ::_thesis: verum end; 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; proof set P = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ; now__::_thesis:_for_x_being_set_st_x_in__{__X_where_X_is_Subset_of_E_:_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)__}__holds_ x_in_bool_E let x be set ; ::_thesis: ( x in { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } implies x in bool E ) assume x in { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ; ::_thesis: x in bool E then ex X being Subset of E st ( x = X & ex x being Element of E st X = the_orbit_of (x,T) ) ; hence x in bool E ; ::_thesis: verum end; then reconsider P = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } as Subset-Family of E by TARSKI:def_3; for x being set holds ( x in E iff ex Y being set st ( x in Y & Y in P ) ) proof let x be set ; ::_thesis: ( x in E iff ex Y being set st ( x in Y & Y in P ) ) hereby ::_thesis: ( ex Y being set st ( x in Y & Y in P ) implies x in E ) assume x in E ; ::_thesis: ex Y being set st ( x in Y & Y in P ) then reconsider x9 = x as Element of E ; reconsider Y = the_orbit_of (x9,T) as set ; take Y = Y; ::_thesis: ( x in Y & Y in P ) x9,x9 are_conjugated_under T by Th3; hence x in Y ; ::_thesis: Y in P thus Y in P ; ::_thesis: verum end; given Y being set such that A1: ( x in Y & Y in P ) ; ::_thesis: x in E thus x in E by A1; ::_thesis: verum end; then A2: union P = E by TARSKI:def_4; for A being Subset of E st A in P holds ( A <> {} & ( for B being Subset of E holds ( not B in P or A = B or A misses B ) ) ) proof let A be Subset of E; ::_thesis: ( A in P implies ( A <> {} & ( for B being Subset of E holds ( not B in P or A = B or A misses B ) ) ) ) assume A in P ; ::_thesis: ( A <> {} & ( for B being Subset of E holds ( not B in P or A = B or A misses B ) ) ) then A3: ex X being Subset of E st ( A = X & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ; hence A <> {} ; ::_thesis: for B being Subset of E holds ( not B in P or A = B or A misses B ) let B be Subset of E; ::_thesis: ( not B in P or A = B or A misses B ) assume B in P ; ::_thesis: ( A = B or A misses B ) then ex X being Subset of E st ( B = X & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ; hence ( A = B or A misses B ) by A3, Th6; ::_thesis: verum end; hence { 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 by A2, EQREL_1:def_4; ::_thesis: verum end; 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 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 proof let n be non zero Nat; ::_thesis: card (INT.Group n) = n multMagma(# (Segm n),(addint n) #) = INT.Group n by GR_CY_1:def_5; hence card (INT.Group n) = n by CARD_1:def_2; ::_thesis: verum end; registration let p be non zero Nat; cluster INT.Group p -> p -group ; coherence INT.Group p is p -group proof take 1 ; :: according to GROUP_10:def_17 ::_thesis: card (INT.Group p) = p |^ 1 thus card (INT.Group p) = p by Lm1 .= p |^ 1 by NEWTON:5 ; ::_thesis: verum end; 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 ) proof take INT.Group p ; ::_thesis: ( INT.Group p is p -group & INT.Group p is finite & INT.Group p is cyclic & INT.Group p is commutative & INT.Group p is strict ) thus ( INT.Group p is p -group & INT.Group p is finite & INT.Group p is cyclic & INT.Group p is commutative & INT.Group p is strict ) ; ::_thesis: verum end; end; 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 proof let E be non empty finite set ; ::_thesis: 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 let G be finite Group; ::_thesis: 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 let p be prime Nat; ::_thesis: 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 let T be LeftOperation of G,E; ::_thesis: ( G is p -group implies (card (the_fixed_points_of T)) mod p = (card E) mod p ) set O1 = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; set O2 = { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; set O = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; defpred S1[ set , set ] means ex x being Element of E ex X being Subset of E st ( $1 = x & $2 = X & X = the_orbit_of (x,T) & x is_fixed_under T ); reconsider p9 = p as Element of NAT by ORDINAL1:def_12; A1: for x being set st x in the_fixed_points_of T holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in the_fixed_points_of T implies ex y being set st S1[x,y] ) assume A2: x in the_fixed_points_of T ; ::_thesis: ex y being set st S1[x,y] then reconsider x9 = x as Element of E ; reconsider y = the_orbit_of (x9,T) as set ; take y ; ::_thesis: S1[x,y] now__::_thesis:_ex_x_being_Element_of_E_ex_X_being_set_st_ (_x9_=_x_&_y_=_X_&_X_=_the_orbit_of_(x,T)_&_x_is_fixed_under_T_) set X = y; set x = x9; take x = x9; ::_thesis: ex X being set st ( x9 = x & y = X & X = the_orbit_of (x,T) & x is_fixed_under T ) take X = y; ::_thesis: ( x9 = x & y = X & X = the_orbit_of (x,T) & x is_fixed_under T ) thus ( x9 = x & y = X & X = the_orbit_of (x,T) ) ; ::_thesis: x is_fixed_under T the_fixed_points_of T = { x99 where x99 is Element of E : x99 is_fixed_under T } by Def13; then ex e being Element of E st ( x = e & e is_fixed_under T ) by A2; hence x is_fixed_under T ; ::_thesis: verum end; hence S1[x,y] ; ::_thesis: verum end; consider FX being Function such that A3: ( dom FX = the_fixed_points_of T & ( for x being set st x in the_fixed_points_of T holds S1[x,FX . x] ) ) from CLASSES1:sch_1(A1); now__::_thesis:_for_y_being_set_holds_ (_(_y_in__{__X_where_X_is_Subset_of_E_:_(_card_X_=_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}__implies_ex_x_being_set_st_[x,y]_in_FX_)_&_(_ex_x_being_set_st_[x,y]_in_FX_implies_y_in__{__X_where_X_is_Subset_of_E_:_(_card_X_=_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}__)_) let y be set ; ::_thesis: ( ( y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } implies ex x being set st [x,y] in FX ) & ( ex x being set st [x,y] in FX implies y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ) ) hereby ::_thesis: ( ex x being set st [x,y] in FX implies y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ) assume y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; ::_thesis: ex x being set st [x,y] in FX then consider X being Subset of E such that A4: y = X and A5: card X = 1 and A6: ex x being Element of E st X = the_orbit_of (x,T) ; consider x9 being Element of E such that A7: X = the_orbit_of (x9,T) by A6; reconsider x = x9 as set ; card X = card {x} by A5, CARD_1:30; then consider x99 being set such that A8: X = {x99} by CARD_1:29; take x = x; ::_thesis: [x,y] in FX now__::_thesis:_for_g_being_Element_of_G_holds_not_x9_<>_(T_^_g)_._x9 x9,x9 are_conjugated_under T by Th3; then A9: x9 in { y99 where y99 is Element of E : x9,y99 are_conjugated_under T } ; given g being Element of G such that A10: x9 <> (T ^ g) . x9 ; ::_thesis: contradiction set y9 = (T ^ g) . x9; x9,(T ^ g) . x9 are_conjugated_under T by Def14; then (T ^ g) . x9 in { y99 where y99 is Element of E : x9,y99 are_conjugated_under T } ; then (T ^ g) . x9 = x99 by A7, A8, TARSKI:def_1; hence contradiction by A7, A8, A10, A9, TARSKI:def_1; ::_thesis: verum end; then x9 is_fixed_under T by Def12; then x in { x999 where x999 is Element of E : x999 is_fixed_under T } ; then A11: x in the_fixed_points_of T by Def13; then ex x99 being Element of E ex X9 being Subset of E st ( x99 = x & X9 = FX . x & X9 = the_orbit_of (x99,T) & x99 is_fixed_under T ) by A3; hence [x,y] in FX by A3, A4, A7, A11, FUNCT_1:1; ::_thesis: verum end; given x being set such that A12: [x,y] in FX ; ::_thesis: y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ( x in dom FX & y = FX . x ) by A12, FUNCT_1:1; then consider x9 being Element of E, X9 being Subset of E such that x9 = x and A13: X9 = y and A14: X9 = the_orbit_of (x9,T) and A15: x9 is_fixed_under T by A3; X9 = {x9} by A14, A15, Th7; then card X9 = 1 by CARD_1:30; hence y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A13, A14; ::_thesis: verum end; then A16: rng FX = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by XTUPLE_0:def_13; now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_FX_&_x2_in_dom_FX_&_FX_._x1_=_FX_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_thesis: ( x1 in dom FX & x2 in dom FX & FX . x1 = FX . x2 implies x1 = x2 ) assume x1 in dom FX ; ::_thesis: ( x2 in dom FX & FX . x1 = FX . x2 implies x1 = x2 ) then consider x19 being Element of E, X1 being Subset of E such that A17: x19 = x1 and A18: ( X1 = FX . x1 & X1 = the_orbit_of (x19,T) & x19 is_fixed_under T ) by A3; assume x2 in dom FX ; ::_thesis: ( FX . x1 = FX . x2 implies x1 = x2 ) then consider x29 being Element of E, X2 being Subset of E such that A19: x29 = x2 and A20: ( X2 = FX . x2 & X2 = the_orbit_of (x29,T) ) and A21: x29 is_fixed_under T by A3; assume FX . x1 = FX . x2 ; ::_thesis: x1 = x2 then {x19} = the_orbit_of (x29,T) by A18, A20, Th7 .= {x29} by A21, Th7 ; hence x1 = x2 by A17, A19, ZFMISC_1:3; ::_thesis: verum end; then FX is one-to-one by FUNCT_1:def_4; then A22: the_fixed_points_of T, { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } are_equipotent by A3, A16, WELLORD2:def_4; A23: now__::_thesis:_for_y_being_set_holds_ (_(_y_in_the_orbits_of_T_implies_y_in__{__X_where_X_is_Subset_of_E_:_(_card_X_=_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}__\/__{__X_where_X_is_Subset_of_E_:_(_card_X_>_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}__)_&_(_y_in__{__X_where_X_is_Subset_of_E_:_(_card_X_=_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}__\/__{__X_where_X_is_Subset_of_E_:_(_card_X_>_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}__implies_y_in_the_orbits_of_T_)_) let y be set ; ::_thesis: ( ( y in the_orbits_of T implies y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ) & ( y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } implies b1 in the_orbits_of T ) ) hereby ::_thesis: ( y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } implies b1 in the_orbits_of T ) assume y in the_orbits_of T ; ::_thesis: y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } then consider X being Subset of E such that A24: y = X and A25: ex x being Element of E st X = the_orbit_of (x,T) ; not X is empty by A25; then 0 + 1 < (card X) + 1 by XREAL_1:6; then A26: 1 <= card X by NAT_1:13; percases ( 1 = card X or 1 < card X ) by A26, XXREAL_0:1; suppose 1 = card X ; ::_thesis: y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } then y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A24, A25; hence y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by XBOOLE_0:def_3; ::_thesis: verum end; suppose 1 < card X ; ::_thesis: y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } then y in { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A24, A25; hence y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by XBOOLE_0:def_3; ::_thesis: verum end; end; end; assume A27: y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; ::_thesis: b1 in the_orbits_of T percases ( y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } or y in { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ) by A27, XBOOLE_0:def_3; suppose y in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; ::_thesis: b1 in the_orbits_of T then ex X being Subset of E st ( y = X & card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ; hence y in the_orbits_of T ; ::_thesis: verum end; suppose y in { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; ::_thesis: b1 in the_orbits_of T then ex X being Subset of E st ( y = X & card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ; hence y in the_orbits_of T ; ::_thesis: verum end; end; end; then A28: { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } = the_orbits_of T by TARSKI:1; then { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } is finite by FINSET_1:1, XBOOLE_1:7; then consider f1 being FinSequence such that A29: rng f1 = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } and A30: f1 is one-to-one by FINSEQ_4:58; { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } is finite by A28, FINSET_1:1, XBOOLE_1:7; then consider f2 being FinSequence such that A31: rng f2 = { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } and A32: f2 is one-to-one by FINSEQ_4:58; set f = f1 ^ f2; reconsider O = { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } \/ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } as a_partition of E by A23, TARSKI:1; A33: rng (f1 ^ f2) = O by A29, A31, FINSEQ_1:31; now__::_thesis:_for_x_being_set_holds_not_x_in__{__X_where_X_is_Subset_of_E_:_(_card_X_=_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}__/\__{__X_where_X_is_Subset_of_E_:_(_card_X_>_1_&_ex_x_being_Element_of_E_st_X_=_the_orbit_of_(x,T)_)__}_ given x being set such that A34: x in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } /\ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } ; ::_thesis: contradiction x in { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A34, XBOOLE_0:def_4; then A35: ex X being Subset of E st ( x = X & card X > 1 & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ; x in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A34, XBOOLE_0:def_4; then ex X being Subset of E st ( x = X & card X = 1 & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ; hence contradiction by A35; ::_thesis: verum end; then { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } /\ { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } = {} by XBOOLE_0:def_1; then rng f1 misses rng f2 by A29, A31, XBOOLE_0:def_7; then A36: f1 ^ f2 is one-to-one by A30, A32, FINSEQ_3:91; reconsider f = f1 ^ f2 as FinSequence of O by A33, FINSEQ_1:def_4; deffunc H1( set ) -> set = card (f1 . $1); consider p1 being FinSequence such that A37: ( len p1 = len f1 & ( for i being Nat st i in dom p1 holds p1 . i = H1(i) ) ) from FINSEQ_1:sch_2(); for x being set st x in rng p1 holds x in NAT proof let x be set ; ::_thesis: ( x in rng p1 implies x in NAT ) assume x in rng p1 ; ::_thesis: x in NAT then consider i being Nat such that A38: i in dom p1 and A39: p1 . i = x by FINSEQ_2:10; i in dom f1 by A37, A38, FINSEQ_3:29; then f1 . i in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A29, FUNCT_1:3; then A40: ex X being Subset of E st ( f1 . i = X & card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ; x = card (f1 . i) by A37, A38, A39; hence x in NAT by A40; ::_thesis: verum end; then rng p1 c= NAT by TARSKI:def_3; then reconsider c1 = p1 as FinSequence of NAT by FINSEQ_1:def_4; deffunc H2( set ) -> set = card (f2 . $1); consider p2 being FinSequence such that A41: ( len p2 = len f2 & ( for i being Nat st i in dom p2 holds p2 . i = H2(i) ) ) from FINSEQ_1:sch_2(); for x being set st x in rng p2 holds x in NAT proof let x be set ; ::_thesis: ( x in rng p2 implies x in NAT ) assume x in rng p2 ; ::_thesis: x in NAT then consider i being Nat such that A42: i in dom p2 and A43: p2 . i = x by FINSEQ_2:10; i in dom f2 by A41, A42, FINSEQ_3:29; then f2 . i in { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A31, FUNCT_1:3; then A44: ex X being Subset of E st ( f2 . i = X & card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ; x = card (f2 . i) by A41, A42, A43; hence x in NAT by A44; ::_thesis: verum end; then rng p2 c= NAT by TARSKI:def_3; then reconsider c2 = p2 as FinSequence of NAT by FINSEQ_1:def_4; set c = c1 ^ c2; reconsider c = c1 ^ c2 as FinSequence of NAT ; A45: for i being Element of NAT st i in dom c holds c . i = card (f . i) proof let i be Element of NAT ; ::_thesis: ( i in dom c implies c . i = card (f . i) ) assume A46: i in dom c ; ::_thesis: c . i = card (f . i) now__::_thesis:_c_._i_=_card_(f_._i) percases ( i in dom c1 or ex j being Nat st ( j in dom c2 & i = (len c1) + j ) ) by A46, FINSEQ_1:25; supposeA47: i in dom c1 ; ::_thesis: c . i = card (f . i) then A48: i in dom f1 by A37, FINSEQ_3:29; c . i = c1 . i by A47, FINSEQ_1:def_7 .= card (f1 . i) by A37, A47 .= card (f . i) by A48, FINSEQ_1:def_7 ; hence c . i = card (f . i) ; ::_thesis: verum end; suppose ex j being Nat st ( j in dom c2 & i = (len c1) + j ) ; ::_thesis: c . i = card (f . i) then consider j being Nat such that A49: j in dom c2 and A50: i = (len c1) + j ; A51: j in dom f2 by A41, A49, FINSEQ_3:29; c . i = c2 . j by A49, A50, FINSEQ_1:def_7 .= card (f2 . j) by A41, A49 .= card (f . i) by A37, A50, A51, FINSEQ_1:def_7 ; hence c . i = card (f . i) ; ::_thesis: verum end; end; end; hence c . i = card (f . i) ; ::_thesis: verum end; assume A52: G is p -group ; ::_thesis: (card (the_fixed_points_of T)) mod p = (card E) mod p for i being Element of NAT st i in dom c2 holds p9 divides c2 /. i proof let i be Element of NAT ; ::_thesis: ( i in dom c2 implies p9 divides c2 /. i ) set i9 = c2 /. i; consider r being Nat such that A53: card G = p |^ r by A52, Def17; reconsider r9 = r as Element of NAT by ORDINAL1:def_12; assume A54: i in dom c2 ; ::_thesis: p9 divides c2 /. i then i in dom f2 by A41, FINSEQ_3:29; then f2 . i in { X where X is Subset of E : ( card X > 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A31, FUNCT_1:3; then consider X being Subset of E such that A55: f2 . i = X and A56: card X > 1 and A57: ex x being Element of E st X = the_orbit_of (x,T) ; consider x being Element of E such that A58: X = the_orbit_of (x,T) by A57; set H = the_strict_stabilizer_of (x,T); c2 . i = card (f2 . i) by A41, A54; then c2 /. i = card (f2 . i) by A54, PARTFUN1:def_6; then c2 /. i = Index (the_strict_stabilizer_of (x,T)) by A55, A58, Th8; then c2 /. i = index (the_strict_stabilizer_of (x,T)) by GROUP_2:def_18; then A59: card G = (card (the_strict_stabilizer_of (x,T))) * (c2 /. i) by GROUP_2:147; then A60: c2 /. i divides p9 |^ r9 by A53, NAT_D:def_3; A61: card (the_orbit_of (x,T)) = Index (the_strict_stabilizer_of (x,T)) by Th8; A62: now__::_thesis:_not_card_(the_strict_stabilizer_of_(x,T))_=_card_G assume card (the_strict_stabilizer_of (x,T)) = card G ; ::_thesis: contradiction then card G = (card G) * (index (the_strict_stabilizer_of (x,T))) by GROUP_2:147; then 1 = ((card G) * (index (the_strict_stabilizer_of (x,T)))) / (card G) by XCMPLX_1:60; then 1 = ((card G) / (card G)) * (index (the_strict_stabilizer_of (x,T))) by XCMPLX_1:74; then 1 * (index (the_strict_stabilizer_of (x,T))) = 1 by XCMPLX_1:60; hence contradiction by A56, A58, A61, GROUP_2:def_18; ::_thesis: verum end; percases ( c2 /. i = 1 or ex k being Element of NAT st c2 /. i = p * k ) by A60, PEPIN:32; suppose c2 /. i = 1 ; ::_thesis: p9 divides c2 /. i hence p9 divides c2 /. i by A59, A62; ::_thesis: verum end; suppose ex k being Element of NAT st c2 /. i = p * k ; ::_thesis: p9 divides c2 /. i hence p9 divides c2 /. i by NAT_D:def_3; ::_thesis: verum end; end; end; then p divides Sum c2 by WEDDWITT:5; then ex t being Nat st Sum c2 = p * t by NAT_D:def_3; then A63: (Sum c2) mod p = 0 by NAT_D:13; len c = (len f1) + (len f2) by A37, A41, FINSEQ_1:22; then len c = len f by FINSEQ_1:22; then card E = Sum c by A36, A33, A45, WEDDWITT:6 .= (Sum c1) + (Sum c2) by RVSUM_1:75 ; then A64: (card E) mod p = ((Sum c1) + ((Sum c2) mod p)) mod p by NAT_D:23 .= (Sum c1) mod p by A63 ; A65: for i being Element of NAT st i in dom c1 holds c1 . i = 1 proof let i be Element of NAT ; ::_thesis: ( i in dom c1 implies c1 . i = 1 ) assume A66: i in dom c1 ; ::_thesis: c1 . i = 1 then i in dom f1 by A37, FINSEQ_3:29; then f1 . i in { X where X is Subset of E : ( card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) } by A29, FUNCT_1:3; then ex X being Subset of E st ( f1 . i = X & card X = 1 & ex x being Element of E st X = the_orbit_of (x,T) ) ; hence c1 . i = 1 by A37, A66; ::_thesis: verum end; for x being set st x in rng c1 holds x in {1} proof let x be set ; ::_thesis: ( x in rng c1 implies x in {1} ) assume x in rng c1 ; ::_thesis: x in {1} then ex i being Nat st ( i in dom c1 & x = c1 . i ) by FINSEQ_2:10; then x = 1 by A65; hence x in {1} by TARSKI:def_1; ::_thesis: verum end; then A67: rng c1 c= {1} by TARSKI:def_3; A68: Sum c1 = len c1 proof percases ( len c1 = 0 or len c1 <> 0 ) ; suppose len c1 = 0 ; ::_thesis: Sum c1 = len c1 then c1 = {} ; hence Sum c1 = len c1 by RVSUM_1:72; ::_thesis: verum end; supposeA69: len c1 <> 0 ; ::_thesis: Sum c1 = len c1 for x being set st x in {1} holds x in rng c1 proof let x be set ; ::_thesis: ( x in {1} implies x in rng c1 ) assume A70: x in {1} ; ::_thesis: x in rng c1 A71: Seg (len c1) = dom c1 by FINSEQ_1:def_3; then c1 . (len c1) = 1 by A65, A69, FINSEQ_1:3; then c1 . (len c1) = x by A70, TARSKI:def_1; hence x in rng c1 by A69, A71, FINSEQ_1:3, FUNCT_1:3; ::_thesis: verum end; then {1} c= rng c1 by TARSKI:def_3; then rng c1 = {1} by A67, XBOOLE_0:def_10; then c1 = (dom c1) --> 1 by FUNCOP_1:9; then c1 = (Seg (len c1)) --> 1 by FINSEQ_1:def_3; then c1 = (len c1) |-> 1 by FINSEQ_2:def_2; then Sum c1 = (len c1) * 1 by RVSUM_1:80; hence Sum c1 = len c1 ; ::_thesis: verum end; end; end; len c1 = card (rng f1) by A30, A37, FINSEQ_4:62; hence (card (the_fixed_points_of T)) mod p = (card E) mod p by A29, A68, A22, A64, CARD_1:5; ::_thesis: verum end; begin 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 ) proof let n be Nat; ::_thesis: for p being prime Nat st n <> 0 holds ex m, r being Nat st ( n = (p |^ r) * m & not p divides m ) let p be prime Nat; ::_thesis: ( n <> 0 implies ex m, r being Nat st ( n = (p |^ r) * m & not p divides m ) ) set r = p |-count n; A1: p <> 1 by NAT_4:12; assume A2: n <> 0 ; ::_thesis: ex m, r being Nat st ( n = (p |^ r) * m & not p divides m ) then p |^ (p |-count n) divides n by A1, NAT_3:def_7; then consider m being Nat such that A3: n = (p |^ (p |-count n)) * m by NAT_D:def_3; take m ; ::_thesis: ex r being Nat st ( n = (p |^ r) * m & not p divides m ) take p |-count n ; ::_thesis: ( n = (p |^ (p |-count n)) * m & not p divides m ) thus n = (p |^ (p |-count n)) * m by A3; ::_thesis: not p divides m A4: not p |^ ((p |-count n) + 1) divides n by A2, A1, NAT_3:def_7; thus not p divides m ::_thesis: verum proof assume p divides m ; ::_thesis: contradiction then consider t being Nat such that A5: m = p * t by NAT_D:def_3; n = ((p |^ (p |-count n)) * p) * t by A3, A5 .= (p |^ ((p |-count n) + 1)) * t by NEWTON:6 ; hence contradiction by A4, NAT_D:def_3; ::_thesis: verum end; end; Lm3: for X, Y being non empty set holds card { [:X,{y}:] where y is Element of Y : verum } = card Y proof let X, Y be non empty set ; ::_thesis: card { [:X,{y}:] where y is Element of Y : verum } = card Y set Z = { [:X,{y}:] where y is Element of Y : verum } ; deffunc H1( set ) -> set = [:X,{$1}:]; ex f being Function st ( dom f = Y & ( for x being set st x in Y holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); then consider f being Function such that A1: dom f = Y and A2: for x being set st x in Y holds f . x = H1(x) ; for y being set holds ( y in { [:X,{y}:] where y is Element of Y : verum } iff ex x being set st ( x in dom f & y = f . x ) ) proof let y be set ; ::_thesis: ( y in { [:X,{y}:] where y is Element of Y : verum } iff ex x being set st ( x in dom f & y = f . x ) ) hereby ::_thesis: ( ex x being set st ( x in dom f & y = f . x ) implies y in { [:X,{y}:] where y is Element of Y : verum } ) assume y in { [:X,{y}:] where y is Element of Y : verum } ; ::_thesis: ex x being set st ( x in dom f & y = f . x ) then consider y9 being Element of Y such that A3: y = [:X,{y9}:] ; reconsider x = y9 as set ; take x = x; ::_thesis: ( x in dom f & y = f . x ) thus x in dom f by A1; ::_thesis: y = f . x thus y = f . x by A2, A3; ::_thesis: verum end; given x being set such that A4: x in dom f and A5: y = f . x ; ::_thesis: y in { [:X,{y}:] where y is Element of Y : verum } f . x = [:X,{x}:] by A1, A2, A4; hence y in { [:X,{y}:] where y is Element of Y : verum } by A1, A4, A5; ::_thesis: verum end; then A6: rng f = { [:X,{y}:] where y is Element of Y : verum } by FUNCT_1:def_3; for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume ( x1 in dom f & x2 in dom f ) ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 ) then A7: ( f . x1 = H1(x1) & f . x2 = H1(x2) ) by A1, A2; assume f . x1 = f . x2 ; ::_thesis: x1 = x2 then {x1} = {x2} by A7, ZFMISC_1:110; hence x1 = x2 by ZFMISC_1:3; ::_thesis: verum end; then f is one-to-one by FUNCT_1:def_4; then { [:X,{y}:] where y is Element of Y : verum } ,Y are_equipotent by A1, A6, WELLORD2:def_4; hence card { [:X,{y}:] where y is Element of Y : verum } = card Y by CARD_1:5; ::_thesis: verum end; 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 } proof let G be finite Group; ::_thesis: 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 } let E, T be non empty set ; ::_thesis: 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 } let LO be LeftOperation of G,E; ::_thesis: 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 } let n be Nat; ::_thesis: ( LO = the_left_operation_of (G,T) & n = card G & E = [: the carrier of G,T:] & card n c= card E implies the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum } ) assume A1: LO = the_left_operation_of (G,T) ; ::_thesis: ( not n = card G or not E = [: the carrier of G,T:] or not card n c= card E or the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum } ) set EE = the_subsets_of_card (n,E); set LO9 = the_extension_of_left_operation_of (n,LO); assume A2: n = card G ; ::_thesis: ( not E = [: the carrier of G,T:] or not card n c= card E or the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum } ) assume A3: E = [: the carrier of G,T:] ; ::_thesis: ( not card n c= card E or the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum } ) assume A4: card n c= card E ; ::_thesis: the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum } now__::_thesis:_for_z_being_set_holds_ (_(_z_in_the_fixed_points_of_(the_extension_of_left_operation_of_(n,LO))_implies_z_in__{__[:_the_carrier_of_G,{t9}:]_where_t9_is_Element_of_T_:_verum__}__)_&_(_z_in__{__[:_the_carrier_of_G,{t}:]_where_t_is_Element_of_T_:_verum__}__implies_z_in_the_fixed_points_of_(the_extension_of_left_operation_of_(n,LO))_)_) let z be set ; ::_thesis: ( ( z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) implies z in { [: the carrier of G,{t9}:] where t9 is Element of T : verum } ) & ( z in { [: the carrier of G,{t}:] where t is Element of T : verum } implies z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) ) ) hereby ::_thesis: ( z in { [: the carrier of G,{t}:] where t is Element of T : verum } implies z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) ) assume z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) ; ::_thesis: z in { [: the carrier of G,{t9}:] where t9 is Element of T : verum } then z in { x where x is Element of the_subsets_of_card (n,E) : x is_fixed_under the_extension_of_left_operation_of (n,LO) } by Def13; then consider e being Element of the_subsets_of_card (n,E) such that A5: z = e and A6: e is_fixed_under the_extension_of_left_operation_of (n,LO) ; not the_subsets_of_card (n,E) is empty by A4, Th1; then z in the_subsets_of_card (n,E) by A5; then consider X being Subset of E such that A7: z = X and A8: card X = n ; A9: for g being Element of G holds e = (the_left_translation_of (g,T)) .: e proof let g be Element of G; ::_thesis: e = (the_left_translation_of (g,T)) .: e (the_extension_of_left_operation_of (n,LO)) . g = the_extension_of_left_translation_of (n,g,LO) by A4, Def5; then A10: ((the_extension_of_left_operation_of (n,LO)) ^ g) . e = (LO ^ g) .: e by A4, Def4; e = ((the_extension_of_left_operation_of (n,LO)) ^ g) . e by A6, Def12; hence e = (the_left_translation_of (g,T)) .: e by A1, A10, Def7; ::_thesis: verum end; ex t being Element of T st [: the carrier of G,{t}:] c= z proof not X is empty by A2, A8; then consider x1 being set such that A11: x1 in X by XBOOLE_0:def_1; consider g1, t being set such that A12: g1 in the carrier of G and A13: t in T and A14: x1 = [g1,t] by A3, A11, ZFMISC_1:def_2; reconsider t = t as Element of T by A13; reconsider g1 = g1 as Element of G by A12; take t ; ::_thesis: [: the carrier of G,{t}:] c= z now__::_thesis:_for_x2_being_set_st_x2_in_[:_the_carrier_of_G,{t}:]_holds_ x2_in_z reconsider z19 = x1 as Element of [: the carrier of G,T:] by A3, A11; let x2 be set ; ::_thesis: ( x2 in [: the carrier of G,{t}:] implies x2 in z ) assume x2 in [: the carrier of G,{t}:] ; ::_thesis: x2 in z then consider g2, t9 being set such that A15: g2 in the carrier of G and A16: ( t9 in {t} & x2 = [g2,t9] ) by ZFMISC_1:def_2; reconsider g2 = g2 as Element of G by A15; set g = g2 * (g1 "); consider z29 being Element of [: the carrier of G,T:], g19, g29 being Element of G, t99 being Element of T such that A17: z29 = (the_left_translation_of ((g2 * (g1 ")),T)) . z19 and A18: g29 = (g2 * (g1 ")) * g19 and A19: z19 = [g19,t99] and A20: z29 = [g29,t99] by Def6; A21: t = t99 by A14, A19, XTUPLE_0:1; dom (the_left_translation_of ((g2 * (g1 ")),T)) = E by A3, FUNCT_2:def_1; then A22: (the_left_translation_of ((g2 * (g1 ")),T)) . x1 in (the_left_translation_of ((g2 * (g1 ")),T)) .: e by A5, A7, A11, FUNCT_1:def_6; g29 = (g2 * (g1 ")) * g1 by A14, A18, A19, XTUPLE_0:1 .= g2 * ((g1 ") * g1) by GROUP_1:def_3 .= g2 * (1_ G) by GROUP_1:def_5 .= g2 by GROUP_1:def_4 ; then z29 = x2 by A16, A20, A21, TARSKI:def_1; hence x2 in z by A5, A9, A17, A22; ::_thesis: verum end; hence [: the carrier of G,{t}:] c= z by TARSKI:def_3; ::_thesis: verum end; then consider t being Element of T such that A23: [: the carrier of G,{t}:] c= z ; n,X are_equipotent by A8, CARD_1:def_2; then consider f being Function such that f is one-to-one and A24: dom f = n and A25: rng f = X by WELLORD2:def_4; dom f in omega by A24, ORDINAL1:def_12; then reconsider X = X as finite set by A25, FINSET_1:def_1; card [: the carrier of G,{t}:] = n by A2, CARD_1:69; then [: the carrier of G,{t}:] = X by A7, A8, A23, CARD_FIN:1; hence z in { [: the carrier of G,{t9}:] where t9 is Element of T : verum } by A7; ::_thesis: verum end; assume z in { [: the carrier of G,{t}:] where t is Element of T : verum } ; ::_thesis: z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) then consider t being Element of T such that A26: z = [: the carrier of G,{t}:] ; A27: now__::_thesis:_for_z9_being_set_st_z9_in_z_holds_ z9_in_[:_the_carrier_of_G,T:] let z9 be set ; ::_thesis: ( z9 in z implies z9 in [: the carrier of G,T:] ) assume z9 in z ; ::_thesis: z9 in [: the carrier of G,T:] then ex x, y being set st ( x in the carrier of G & y in {t} & z9 = [x,y] ) by A26, ZFMISC_1:def_2; hence z9 in [: the carrier of G,T:] by ZFMISC_1:def_2; ::_thesis: verum end; then reconsider X = z as Subset of E by A3, TARSKI:def_3; card X = card the carrier of G by A26, CARD_1:69; then z in the_subsets_of_card (n,E) by A2; then reconsider e = z as Element of the_subsets_of_card (n,E) ; A28: z c= [: the carrier of G,T:] by A27, TARSKI:def_3; A29: for g being Element of G holds e = (LO ^ g) .: e proof let g be Element of G; ::_thesis: e = (LO ^ g) .: e A30: LO ^ g = the_left_translation_of (g,T) by A1, Def7; now__::_thesis:_for_e2_being_set_holds_ (_(_e2_in_e_implies_ex_e1_being_set_st_ (_e1_in_dom_(LO_^_g)_&_e1_in_e_&_e2_=_(LO_^_g)_._e1_)_)_&_(_ex_e1_being_set_st_ (_e1_in_dom_(LO_^_g)_&_e1_in_e_&_e2_=_(LO_^_g)_._e1_)_implies_e2_in_e_)_) let e2 be set ; ::_thesis: ( ( e2 in e implies ex e1 being set st ( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) ) & ( ex e1 being set st ( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) implies e2 in e ) ) hereby ::_thesis: ( ex e1 being set st ( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) implies e2 in e ) assume e2 in e ; ::_thesis: ex e1 being set st ( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) then consider g2, t2 being set such that A31: g2 in the carrier of G and A32: t2 in {t} and A33: e2 = [g2,t2] by A26, ZFMISC_1:def_2; reconsider g2 = g2 as Element of G by A31; reconsider e1 = [((g ") * g2),t2] as set ; take e1 = e1; ::_thesis: ( e1 in dom (LO ^ g) & e1 in e & e2 = (LO ^ g) . e1 ) A34: z c= dom (LO ^ g) by A3, A28, FUNCT_2:def_1; e1 in e by A26, A32, ZFMISC_1:def_2; hence ( e1 in dom (LO ^ g) & e1 in e ) by A34; ::_thesis: e2 = (LO ^ g) . e1 then reconsider z1 = e1 as Element of [: the carrier of G,T:] by A3; consider z2 being Element of [: the carrier of G,T:], g19, g29 being Element of G, t9 being Element of T such that A35: z2 = (LO ^ g) . z1 and A36: g29 = g * g19 and A37: z1 = [g19,t9] and A38: z2 = [g29,t9] by A30, Def6; g29 = g * ((g ") * g2) by A36, A37, XTUPLE_0:1 .= (g * (g ")) * g2 by GROUP_1:def_3 .= (1_ G) * g2 by GROUP_1:def_5 .= g2 by GROUP_1:def_4 ; hence e2 = (LO ^ g) . e1 by A33, A35, A37, A38, XTUPLE_0:1; ::_thesis: verum end; given e1 being set such that A39: e1 in dom (LO ^ g) and A40: e1 in e and A41: e2 = (LO ^ g) . e1 ; ::_thesis: e2 in e reconsider z1 = e1 as Element of [: the carrier of G,T:] by A3, A39; consider z2 being Element of [: the carrier of G,T:], g19, g29 being Element of G, t9 being Element of T such that A42: z2 = (LO ^ g) . z1 and g29 = g * g19 and A43: z1 = [g19,t9] and A44: z2 = [g29,t9] by A30, Def6; A45: t9 in {t9} by TARSKI:def_1; consider g1, t1 being set such that g1 in the carrier of G and A46: t1 in {t} and A47: e1 = [g1,t1] by A26, A40, ZFMISC_1:def_2; t1 = t by A46, TARSKI:def_1; then t9 = t by A47, A43, XTUPLE_0:1; hence e2 in e by A26, A41, A42, A44, A45, ZFMISC_1:def_2; ::_thesis: verum end; hence e = (LO ^ g) .: e by FUNCT_1:def_6; ::_thesis: verum end; for g being Element of G holds e = ((the_extension_of_left_operation_of (n,LO)) ^ g) . e proof let g be Element of G; ::_thesis: e = ((the_extension_of_left_operation_of (n,LO)) ^ g) . e (the_extension_of_left_operation_of (n,LO)) . g = the_extension_of_left_translation_of (n,g,LO) by A4, Def5; then ((the_extension_of_left_operation_of (n,LO)) ^ g) . e = (LO ^ g) .: e by A4, Def4; then consider Y being Element of the_subsets_of_card (n,E) such that A48: [Y,((LO ^ g) .: Y)] = [e,(((the_extension_of_left_operation_of (n,LO)) ^ g) . e)] ; ( Y = e & (LO ^ g) .: Y = ((the_extension_of_left_operation_of (n,LO)) ^ g) . e ) by A48, XTUPLE_0:1; hence e = ((the_extension_of_left_operation_of (n,LO)) ^ g) . e by A29; ::_thesis: verum end; then e is_fixed_under the_extension_of_left_operation_of (n,LO) by Def12; then A49: z in { x where x is Element of the_subsets_of_card (n,E) : x is_fixed_under the_extension_of_left_operation_of (n,LO) } ; not the_subsets_of_card (n,E) is empty by A4, Th1; hence z in the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) by A49, Def13; ::_thesis: verum end; hence the_fixed_points_of (the_extension_of_left_operation_of (n,LO)) = { [: the carrier of G,{t}:] where t is Element of T : verum } by TARSKI:1; ::_thesis: verum end; 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 proof reconsider x1 = 1, x2 = 0 as set ; let n, m, r be Nat; ::_thesis: for p being prime Nat st n = (p |^ r) * m & not p divides m holds (n choose (p |^ r)) mod p <> 0 let p be prime Nat; ::_thesis: ( n = (p |^ r) * m & not p divides m implies (n choose (p |^ r)) mod p <> 0 ) assume A1: n = (p |^ r) * m ; ::_thesis: ( p divides m or (n choose (p |^ r)) mod p <> 0 ) reconsider n9 = n as real number ; reconsider k2 = m as Element of NAT by ORDINAL1:def_12; reconsider p9 = p as prime Element of NAT by ORDINAL1:def_12; reconsider k1 = p9 |^ r as non zero Element of NAT by ORDINAL1:def_12; set S = INT.Group k1; set CS = the carrier of (INT.Group k1); set T = Segm k2; A2: card (Segm k2) = m by CARD_1:def_2; assume A3: not p divides m ; ::_thesis: (n choose (p |^ r)) mod p <> 0 then A4: k2 <> 0 by NAT_D:6; then reconsider T = Segm k2 as non empty finite set ; set X = [: the carrier of (INT.Group k1),T:]; reconsider X9 = [: the carrier of (INT.Group k1),T:] as non empty finite set ; set E = the_subsets_of_card (k1,X9); multMagma(# (Segm k1),(addint k1) #) = INT.Group k1 by GR_CY_1:def_5; then card the carrier of (INT.Group k1) = p |^ r by CARD_1:def_2; then A5: card [: the carrier of (INT.Group k1),T:] = n by A1, A2, CARD_2:46; now__::_thesis:_not_p_|^_r_>_n assume p |^ r > n ; ::_thesis: contradiction then (p |^ r) * m > n * m by A4, XREAL_1:68; then n9 / n9 > (n9 * m) / n9 by A1, XREAL_1:74; then 1 > (n9 * m) / n9 by A5, XCMPLX_1:60; then 1 > (n9 / n9) * m by XCMPLX_1:74; then 1 > 1 * m by A5, XCMPLX_1:60; then m < 0 + 1 ; hence contradiction by A4, NAT_1:13; ::_thesis: verum end; then A6: card k1 c= card (card [: the carrier of (INT.Group k1),T:]) by A5, NAT_1:40; then reconsider E9 = the_subsets_of_card (k1,X9) as non empty finite set by Th1; card (Choose ([: the carrier of (INT.Group k1),T:],k1,x1,x2)) = card E9 by Th2; then A7: card E9 = n choose k1 by A5, CARD_FIN:16; set LO = the_left_operation_of ((INT.Group k1),T); set LO9 = the_extension_of_left_operation_of (k1,(the_left_operation_of ((INT.Group k1),T))); A8: now__::_thesis:_not_m_mod_p9_=_0 assume m mod p9 = 0 ; ::_thesis: contradiction then m = (p * (m div p)) + 0 by NAT_D:2; hence contradiction by A3, NAT_D:def_3; ::_thesis: verum end; A9: card (INT.Group k1) = k1 by Lm1; then card (the_fixed_points_of (the_extension_of_left_operation_of (k1,(the_left_operation_of ((INT.Group k1),T))))) = card { [: the carrier of (INT.Group k1),{t}:] where t is Element of T : verum } by A6, Lm4 .= card k2 by Lm3 ; then A10: card (the_fixed_points_of (the_extension_of_left_operation_of (k1,(the_left_operation_of ((INT.Group k1),T))))) = m by CARD_1:def_2; INT.Group k1 is p -group by A9, Def17; hence (n choose (p |^ r)) mod p <> 0 by A7, A10, A8, Th9; ::_thesis: verum end; 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 proof defpred S1[ Nat] means for n, m1, m2 being Nat for p being prime Nat st (p |^ $1) * n = m1 * m2 & not p divides n & not p divides m2 holds p |^ $1 divides m1; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] for n, m1, m2 being Nat for p being prime Nat st (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 holds p |^ (k + 1) divides m1 proof let n, m1, m2 be Nat; ::_thesis: for p being prime Nat st (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 holds p |^ (k + 1) divides m1 let p be prime Nat; ::_thesis: ( (p |^ (k + 1)) * n = m1 * m2 & not p divides n & not p divides m2 implies p |^ (k + 1) divides m1 ) assume A3: (p |^ (k + 1)) * n = m1 * m2 ; ::_thesis: ( p divides n or p divides m2 or p |^ (k + 1) divides m1 ) reconsider p9 = p as prime Element of NAT by ORDINAL1:def_12; assume A4: not p divides n ; ::_thesis: ( p divides m2 or p |^ (k + 1) divides m1 ) assume A5: not p divides m2 ; ::_thesis: p |^ (k + 1) divides m1 A6: (p |^ (k + 1)) * n = ((p |^ k) * p) * n by NEWTON:6 .= ((p |^ k) * n) * p ; then p divides m1 * m2 by A3, NAT_D:def_3; then p divides m1 by A5, NEWTON:80; then consider m19 being Nat such that A7: m1 = p * m19 by NAT_D:def_3; ((p |^ k) * n) * p9 = (m19 * m2) * p9 by A3, A6, A7; then p |^ k divides m19 by A2, A4, A5, XCMPLX_1:5; then consider m199 being Nat such that A8: m19 = (p |^ k) * m199 by NAT_D:def_3; m1 = ((p |^ k) * p) * m199 by A7, A8 .= (p |^ (k + 1)) * m199 by NEWTON:6 ; hence p |^ (k + 1) divides m1 by NAT_D:def_3; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A9: S1[ 0 ] proof let n, m1, m2 be Nat; ::_thesis: for p being prime Nat st (p |^ 0) * n = m1 * m2 & not p divides n & not p divides m2 holds p |^ 0 divides m1 let p be prime Nat; ::_thesis: ( (p |^ 0) * n = m1 * m2 & not p divides n & not p divides m2 implies p |^ 0 divides m1 ) assume that (p |^ 0) * n = m1 * m2 and not p divides n and not p divides m2 ; ::_thesis: p |^ 0 divides m1 p |^ 0 = 1 by NEWTON:4; hence p |^ 0 divides m1 by NAT_D:6; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A9, A1); hence 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 ; ::_thesis: verum end; 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) proof let G be Group; ::_thesis: for A being non empty Subset of G for x being Element of G holds card A = card (A * x) let A be non empty Subset of G; ::_thesis: for x being Element of G holds card A = card (A * x) let x be Element of G; ::_thesis: card A = card (A * x) set B = A * x; ( not A is empty & not A * x is empty ) proof set a = the Element of A; the Element of A * x in A * x by GROUP_2:28; hence ( not A is empty & not A * x is empty ) ; ::_thesis: verum end; then reconsider B = A * x as non empty Subset of G ; deffunc H1( Element of G) -> Element of the carrier of G = $1 * x; consider f being Function of A, the carrier of G such that A1: for a being Element of A holds f . a = H1(a) from FUNCT_2:sch_4(); A2: B c= rng f proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in B or s in rng f ) assume s in B ; ::_thesis: s in rng f then consider a being Element of G such that A3: ( s = a * x & a in A ) by GROUP_2:28; ex x being set st ( x in dom f & s = f . x ) proof take a ; ::_thesis: ( a in dom f & s = f . a ) thus ( a in dom f & s = f . a ) by A1, A3, FUNCT_2:def_1; ::_thesis: verum end; hence s in rng f by FUNCT_1:def_3; ::_thesis: verum end; A4: dom f = A by FUNCT_2:def_1; A5: rng f c= B proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng f or s in B ) assume s in rng f ; ::_thesis: s in B then consider a being set such that A6: a in A and A7: s = f . a by A4, FUNCT_1:def_3; reconsider a = a as Element of A by A6; s = H1(a) by A1, A7; hence s in B by GROUP_2:28; ::_thesis: verum end; then reconsider f = f as Function of A,B by A4, FUNCT_2:2; A8: for a, b being Element of A st f . a = f . b holds a = b proof let a, b be Element of A; ::_thesis: ( f . a = f . b implies a = b ) assume f . a = f . b ; ::_thesis: a = b then H1(a) = f . b by A1; then a * x = b * x by A1; hence a = b by GROUP_1:6; ::_thesis: verum end; A,B are_equipotent proof take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = A & rng f = B ) thus ( f is one-to-one & dom f = A & rng f = B ) by A5, A2, A8, FUNCT_2:def_1, GROUP_6:1, XBOOLE_0:def_10; ::_thesis: verum end; hence card A = card (A * x) by CARD_1:5; ::_thesis: verum end; 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 proof reconsider x1 = 1, x2 = 0 as set ; let G be finite Group; ::_thesis: for p being prime Nat ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p let p be prime Nat; ::_thesis: ex P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p reconsider p9 = p as prime Element of NAT by ORDINAL1:def_12; set n = card G; set LO = the_left_operation_of G; consider m, r being Nat such that A1: card G = (p |^ r) * m and A2: not p divides m by Lm2; reconsider k1 = p9 |^ r as Element of NAT by ORDINAL1:def_12; set SF = the_subsets_of_card (k1, the carrier of G); card (the_subsets_of_card (k1, the carrier of G)) = card (Choose ( the carrier of G,k1,x1,x2)) by Th2; then A3: card (the_subsets_of_card (k1, the carrier of G)) = (card G) choose k1 by CARD_FIN:16; then (card (the_subsets_of_card (k1, the carrier of G))) mod p <> 0 by A1, A2, Lm5; then reconsider E = the_subsets_of_card (k1, the carrier of G) as non empty finite set by CARD_1:27, NAT_D:26; set LO9 = the_extension_of_left_operation_of (k1,(the_left_operation_of G)); reconsider T = the_extension_of_left_operation_of (k1,(the_left_operation_of G)) as LeftOperation of G,E ; ex X being Element of E st (card (the_orbit_of (X,T))) mod p <> 0 proof consider f being FinSequence such that A4: rng f = the_orbits_of T and A5: f is one-to-one by FINSEQ_4:58; reconsider f = f as FinSequence of the_orbits_of T by A4, FINSEQ_1:def_4; deffunc H1( set ) -> set = card (f . $1); consider pf being FinSequence such that A6: ( len pf = len f & ( for i being Nat st i in dom pf holds pf . i = H1(i) ) ) from FINSEQ_1:sch_2(); for x being set st x in rng pf holds x in NAT proof let x be set ; ::_thesis: ( x in rng pf implies x in NAT ) assume x in rng pf ; ::_thesis: x in NAT then consider i being Nat such that A7: i in dom pf and A8: pf . i = x by FINSEQ_2:10; i in dom f by A6, A7, FINSEQ_3:29; then f . i in the_orbits_of T by A4, FUNCT_1:3; then consider X being Subset of E such that A9: f . i = X and ex x9 being Element of E st X = the_orbit_of (x9,T) ; x = card X by A6, A7, A8, A9; hence x in NAT ; ::_thesis: verum end; then rng pf c= NAT by TARSKI:def_3; then reconsider c = pf as FinSequence of NAT by FINSEQ_1:def_4; deffunc H2( set ) -> set = (c . $1) / p; consider c9 being FinSequence such that A10: ( len c9 = len c & ( for i being Nat st i in dom c9 holds c9 . i = H2(i) ) ) from FINSEQ_1:sch_2(); assume A11: for X being Element of E holds (card (the_orbit_of (X,T))) mod p = 0 ; ::_thesis: contradiction for x being set st x in rng c9 holds x in NAT proof reconsider p99 = p9 as real number ; let x be set ; ::_thesis: ( x in rng c9 implies x in NAT ) assume x in rng c9 ; ::_thesis: x in NAT then consider i being Nat such that A12: i in dom c9 and A13: c9 . i = x by FINSEQ_2:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; i in dom f by A6, A10, A12, FINSEQ_3:29; then f . i in the_orbits_of T by A4, FUNCT_1:3; then consider X being Subset of E such that A14: f . i = X and A15: ex x9 being Element of E st X = the_orbit_of (x9,T) ; dom pf = dom c9 by A10, FINSEQ_3:29; then c . i = card X by A6, A12, A14; then A16: (c . i) mod p = 0 by A11, A15; set q = (c . i) div p9; c . i = (p9 * ((c . i) div p9)) + ((c . i) mod p9) by NAT_D:2 .= p9 * ((c . i) div p9) by A16 ; then consider q being Nat such that A17: c . i = p * q ; x = (p99 * q) / p99 by A10, A12, A13, A17 .= (p99 / p99) * q by XCMPLX_1:74 .= 1 * q by XCMPLX_1:60 ; hence x in NAT ; ::_thesis: verum end; then rng c9 c= NAT by TARSKI:def_3; then reconsider c9 = c9 as FinSequence of NAT by FINSEQ_1:def_4; A18: dom c = Seg (len c9) by A10, FINSEQ_1:def_3 .= dom c9 by FINSEQ_1:def_3 .= dom (p9 * c9) by VALUED_1:def_5 ; for k being Nat st k in dom c holds c . k = (p9 * c9) . k proof reconsider p99 = p9 as real number ; let k be Nat; ::_thesis: ( k in dom c implies c . k = (p9 * c9) . k ) assume A19: k in dom c ; ::_thesis: c . k = (p9 * c9) . k then k in dom c9 by A10, FINSEQ_3:29; then p * (c9 . k) = p * ((c . k) / p9) by A10 .= (p99 * (c . k)) / p99 by XCMPLX_1:74 .= (p99 / p99) * (c . k) by XCMPLX_1:74 .= 1 * (c . k) by XCMPLX_1:60 ; hence c . k = (p9 * c9) . k by A18, A19, VALUED_1:def_5; ::_thesis: verum end; then A20: c = p9 * c9 by A18, FINSEQ_1:13; for i being Element of NAT st i in dom pf holds pf . i = H1(i) by A6; then card E = Sum c by A4, A5, A6, WEDDWITT:6; then (card E) mod p = (p9 * (Sum c9)) mod p9 by A20, RVSUM_1:87 .= 0 by NAT_D:13 ; hence contradiction by A1, A2, A3, Lm5; ::_thesis: verum end; then consider X being Element of E such that A21: (card (the_orbit_of (X,T))) mod p <> 0 ; set HX = the_strict_stabilizer_of (X,T); card (the_orbit_of (X,T)) = Index (the_strict_stabilizer_of (X,T)) by Th8; then A22: (index (the_strict_stabilizer_of (X,T))) mod p <> 0 by A21, GROUP_2:def_18; A23: now__::_thesis:_not_p_divides_index_(the_strict_stabilizer_of_(X,T)) assume p divides index (the_strict_stabilizer_of (X,T)) ; ::_thesis: contradiction then ex t being Nat st index (the_strict_stabilizer_of (X,T)) = p * t by NAT_D:def_3; hence contradiction by A22, NAT_D:13; ::_thesis: verum end; take the_strict_stabilizer_of (X,T) ; ::_thesis: the_strict_stabilizer_of (X,T) is_Sylow_p-subgroup_of_prime p X in { X9 where X9 is Subset of the carrier of G : card X9 = k1 } ; then A24: ex X9 being Subset of the carrier of G st ( X9 = X & card X9 = k1 ) ; reconsider H = the_strict_stabilizer_of (X,T) as finite Group ; A25: the carrier of (the_strict_stabilizer_of (X,T)) = { g where g is Element of G : (T ^ g) .: {X} = {X} } by Def10; reconsider X = X as non empty Subset of G by A24; set x = the Element of X; reconsider x = the Element of X as Element of G ; k1 divides card G by A1, NAT_D:def_3; then k1 <= card G by NAT_D:7; then card k1 <= card the carrier of G by CARD_1:def_2; then A26: card k1 c= card the carrier of G by NAT_1:39; now__::_thesis:_for_z_being_set_st_z_in_the_carrier_of_H_holds_ z_in_X_*_(x_") reconsider X1 = X as Element of E ; let z be set ; ::_thesis: ( z in the carrier of H implies z in X * (x ") ) assume z in the carrier of H ; ::_thesis: z in X * (x ") then consider g being Element of G such that A27: z = g and A28: (T ^ g) .: {X} = {X} by A25; dom (T ^ g) = E by FUNCT_2:def_1; then Im ((T ^ g),X) = {((T ^ g) . X)} by FUNCT_1:59; then A29: (T ^ g) . X = X by A28, ZFMISC_1:3; set h = g * x; T . g = the_extension_of_left_translation_of (k1,g,(the_left_operation_of G)) by A26, Def5; then A30: (T ^ g) . X1 = ((the_left_operation_of G) ^ g) .: X1 by A26, Def4; reconsider LO = the_left_operation_of G as LeftOperation of G, the carrier of G ; A31: LO ^ g = the_left_translation_of g by Def2; ex x9 being set st ( x9 in dom (LO ^ g) & x9 in X & g * x = (LO ^ g) . x9 ) proof reconsider x9 = x as set ; take x9 ; ::_thesis: ( x9 in dom (LO ^ g) & x9 in X & g * x = (LO ^ g) . x9 ) dom (LO ^ g) = the carrier of G by FUNCT_2:def_1; hence ( x9 in dom (LO ^ g) & x9 in X ) ; ::_thesis: g * x = (LO ^ g) . x9 thus g * x = (LO ^ g) . x9 by A31, TOPGRP_1:def_1; ::_thesis: verum end; then A32: g * x in (LO ^ g) .: X by FUNCT_1:def_6; (g * x) * (x ") = g * (x * (x ")) by GROUP_1:def_3 .= g * (1_ G) by GROUP_1:def_5 .= z by A27, GROUP_1:def_4 ; hence z in X * (x ") by A29, A30, A32, GROUP_2:28; ::_thesis: verum end; then the carrier of H c= X * (x ") by TARSKI:def_3; then card the carrier of H <= card (X * (x ")) by NAT_1:43; then A33: card H <= p |^ r by A24, Lm7; (p |^ r) * m = (card (the_strict_stabilizer_of (X,T))) * (index (the_strict_stabilizer_of (X,T))) by A1, GROUP_2:147; then p |^ r divides card H by A2, A23, Lm6; then A34: p |^ r <= card H by NAT_D:7; then card H = p |^ r by A33, XXREAL_0:1; then A35: H is p -group by Def17; index (the_strict_stabilizer_of (X,T)) = ((index (the_strict_stabilizer_of (X,T))) * (card (the_strict_stabilizer_of (X,T)))) * (1 / (card (the_strict_stabilizer_of (X,T)))) by XCMPLX_1:107 .= ((p |^ r) * m) * (1 / (card (the_strict_stabilizer_of (X,T)))) by A1, GROUP_2:147 .= ((p9 |^ r) * m) * (1 / (p9 |^ r)) by A34, A33, XXREAL_0:1 .= m * ((p9 |^ r) * (1 / (p9 |^ r))) .= m * ((p9 |^ r) / (p9 |^ r)) by XCMPLX_1:99 .= m by XCMPLX_1:88 ; hence the_strict_stabilizer_of (X,T) is_Sylow_p-subgroup_of_prime p by A2, A35, Def18; ::_thesis: verum end; Lm8: for n, r being Nat for p being prime Nat st n divides p |^ r & n > 1 holds p divides n proof let n, r be Nat; ::_thesis: for p being prime Nat st n divides p |^ r & n > 1 holds p divides n let p be prime Nat; ::_thesis: ( n divides p |^ r & n > 1 implies p divides n ) assume A1: n divides p |^ r ; ::_thesis: ( not n > 1 or p divides n ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; assume A2: n > 1 ; ::_thesis: p divides n percases ( n9 = 1 or ex k being Element of NAT st n9 = p * k ) by A1, PEPIN:32; suppose n9 = 1 ; ::_thesis: p divides n hence p divides n by A2; ::_thesis: verum end; suppose ex k being Element of NAT st n9 = p * k ; ::_thesis: p divides n hence p divides n by NAT_D:def_3; ::_thesis: verum end; end; end; 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 proof let G be finite Group; ::_thesis: for p being prime Nat st p divides card G holds ex g being Element of G st ord g = p let p be prime Nat; ::_thesis: ( p divides card G implies ex g being Element of G st ord g = p ) reconsider p9 = p as prime Element of NAT by ORDINAL1:def_12; A1: 1 < p9 by NAT_4:12; consider P being strict Subgroup of G such that A2: P is_Sylow_p-subgroup_of_prime p by Th10; P is p -group by A2, Def18; then consider H being finite Group such that A3: P = H and A4: H is p -group ; consider r being Nat such that A5: card H = p |^ r by A4, Def17; assume A6: p divides card G ; ::_thesis: ex g being Element of G st ord g = p now__::_thesis:_not_r_=_0 assume r = 0 ; ::_thesis: contradiction then card H = 1 by A5, NEWTON:4; then card G = 1 * (index P) by A3, GROUP_2:147; hence contradiction by A6, A2, Def18; ::_thesis: verum end; then 0 + 1 < r + 1 by XREAL_1:6; then 1 <= r by NAT_1:13; then 1 - 1 <= r - 1 by XREAL_1:9; then reconsider r9 = r - 1 as Element of NAT by INT_1:3; 0 + 1 < (p9 |^ r9) + 1 by XREAL_1:6; then 1 <= p |^ r9 by NAT_1:13; then A7: 1 * p <= (p |^ r9) * p by XREAL_1:64; set H9 = (Omega). H; A8: card H = (card ((Omega). H)) * 1 ; p |^ r = p |^ (r9 + 1) .= (p |^ r9) * p by NEWTON:6 ; then card ((Omega). H) > 1 by A5, A7, A1, XXREAL_0:2; then consider g being Element of ((Omega). H) such that A9: g <> 1_ ((Omega). H) by GR_CY_1:11; reconsider H99 = gr {g} as strict Group ; A10: H99 is cyclic Group by GR_CY_2:4; reconsider H99 = H99 as finite strict Group ; set n = card H99; A11: now__::_thesis:_not_card_H99_=_1 assume card H99 = 1 ; ::_thesis: contradiction then ord g = 1 by GR_CY_1:7; hence contradiction by A9, GROUP_1:43; ::_thesis: verum end; card H99 >= 1 by GROUP_1:45; then card H99 > 1 by A11, XXREAL_0:1; then p divides card H99 by A5, A8, Lm8, GROUP_2:148; then consider H999 being strict Subgroup of H99 such that A12: card H999 = p9 and for G2 being strict Subgroup of H99 st card G2 = p9 holds G2 = H999 by A10, GR_CY_2:22; consider h9 being Element of H999 such that A13: ord h9 = p by A12, GROUP_8:1; H99 is Subgroup of G by A3, GROUP_2:56; then reconsider H999 = H999 as strict Subgroup of G by GROUP_2:56; reconsider h9 = h9 as Element of H999 ; reconsider h = h9 as Element of G by GROUP_2:42; take h ; ::_thesis: ord h = p thus ord h = p by A13, GROUP_8:5; ::_thesis: verum end; 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 ) ) proof let G be finite Group; ::_thesis: 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 ) ) let p be prime Nat; ::_thesis: ( ( 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 ) ) reconsider p9 = p as prime Element of NAT by ORDINAL1:def_12; A1: for H, P being Subgroup of G st H is p -group & P is_Sylow_p-subgroup_of_prime p holds ex g being Element of G st carr H c= carr (P |^ g) proof let H, P be Subgroup of G; ::_thesis: ( H is p -group & P is_Sylow_p-subgroup_of_prime p implies ex g being Element of G st carr H c= carr (P |^ g) ) set H9 = H; set E = Left_Cosets P; set T = the_left_operation_of (H,P); reconsider E = Left_Cosets P as non empty finite set by GROUP_2:135; reconsider T = the_left_operation_of (H,P) as LeftOperation of H,E ; assume H is p -group ; ::_thesis: ( not P is_Sylow_p-subgroup_of_prime p or ex g being Element of G st carr H c= carr (P |^ g) ) then A2: (card (the_fixed_points_of T)) mod p = (card E) mod p by Th9; assume P is_Sylow_p-subgroup_of_prime p ; ::_thesis: ex g being Element of G st carr H c= carr (P |^ g) then A3: not p divides index P by Def18; now__::_thesis:_not_(card_E)_mod_p_=_0 assume (card E) mod p = 0 ; ::_thesis: contradiction then ( ex t being Nat st ( card E = (p * t) + 0 & 0 < p ) or ( 0 = 0 & p = 0 ) ) by NAT_D:def_2; then p9 divides card E by NAT_D:def_3; hence contradiction by A3, GROUP_2:def_18; ::_thesis: verum end; then card (the_fixed_points_of T) <> 0 by A2, NAT_D:26; then consider x being set such that A4: x in the_fixed_points_of T by CARD_1:27, XBOOLE_0:def_1; x in { x9 where x9 is Element of E : x9 is_fixed_under T } by A4, Def13; then consider x9 being Element of E such that x = x9 and A5: x9 is_fixed_under T ; x9 in Left_Cosets P ; then consider g9 being Element of G such that A6: x9 = g9 * P by GROUP_2:def_15; set g = g9 " ; take g9 " ; ::_thesis: carr H c= carr (P |^ (g9 ")) now__::_thesis:_for_y_being_set_st_y_in_carr_H_holds_ y_in_(g9_*_P)_*_(g9_") reconsider P1 = x9 as Element of Left_Cosets P ; let y be set ; ::_thesis: ( y in carr H implies y in (g9 * P) * (g9 ") ) assume y in carr H ; ::_thesis: y in (g9 * P) * (g9 ") then reconsider h = y as Element of H ; reconsider h9 = h as Element of H ; consider P2 being Element of Left_Cosets P, A1, A2 being Subset of G, g99 being Element of G such that A7: ( P2 = (the_left_translation_of (h9,P)) . P1 & A2 = g99 * A1 & A1 = P1 & A2 = P2 ) and A8: g99 = h9 by Def8; (the_left_operation_of (H,P)) . h9 = the_left_translation_of (h9,P) by Def9; then A9: (g9 * P) * (g9 ") = (g99 * (g9 * P)) * (g9 ") by A5, A6, A7, Def12 .= g99 * ((g9 * P) * (g9 ")) by GROUP_2:33 ; g99 in (g9 * P) * (g9 ") proof 1_ G in P by GROUP_2:46; then A10: 1_ G in carr P by STRUCT_0:def_5; g9 = g9 * (1_ G) by GROUP_1:def_4; then ( g9 * (g9 ") = 1_ G & g9 in g9 * P ) by A10, GROUP_1:def_5, GROUP_2:27; then A11: ( g99 = g99 * (1_ G) & 1_ G in (g9 * P) * (g9 ") ) by GROUP_1:def_4, GROUP_2:28; assume not g99 in (g9 * P) * (g9 ") ; ::_thesis: contradiction hence contradiction by A9, A11, GROUP_2:27; ::_thesis: verum end; hence y in (g9 * P) * (g9 ") by A8; ::_thesis: verum end; then carr H c= (((g9 ") ") * P) * (g9 ") by TARSKI:def_3; hence carr H c= carr (P |^ (g9 ")) by GROUP_3:59; ::_thesis: verum end; thus 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 ) ::_thesis: 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 proof let H be Subgroup of G; ::_thesis: ( H is p -group implies ex P being Subgroup of G st ( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) ) consider P9 being strict Subgroup of G such that A12: P9 is_Sylow_p-subgroup_of_prime p by Th10; assume H is p -group ; ::_thesis: ex P being Subgroup of G st ( P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P ) then consider g being Element of G such that A13: carr H c= carr (P9 |^ g) by A1, A12; set P = P9 |^ g; take P9 |^ g ; ::_thesis: ( P9 |^ g is_Sylow_p-subgroup_of_prime p & H is Subgroup of P9 |^ g ) set H2 = P9 |^ g; reconsider H2 = P9 |^ g as finite Group ; A14: card P9 = card (P9 |^ g) by GROUP_3:66; P9 is p -group by A12, Def18; then consider H1 being finite Group such that A15: P9 = H1 and A16: H1 is p -group ; ex r being Nat st card H1 = p |^ r by A16, Def17; then A17: H2 is p -group by A15, A14, Def17; A18: not p divides index P9 by A12, Def18; (card (P9 |^ g)) * (index (P9 |^ g)) = card G by GROUP_2:147 .= (card (P9 |^ g)) * (index P9) by A14, GROUP_2:147 ; then not p divides index (P9 |^ g) by A18, XCMPLX_1:5; hence P9 |^ g is_Sylow_p-subgroup_of_prime p by A17, Def18; ::_thesis: H is Subgroup of P9 |^ g thus H is Subgroup of P9 |^ g by A13, GROUP_2:57; ::_thesis: verum end; let P1, P2 be Subgroup of G; ::_thesis: ( P1 is_Sylow_p-subgroup_of_prime p & P2 is_Sylow_p-subgroup_of_prime p implies P1,P2 are_conjugated ) assume A19: P1 is_Sylow_p-subgroup_of_prime p ; ::_thesis: ( not P2 is_Sylow_p-subgroup_of_prime p or P1,P2 are_conjugated ) then A20: P1 is p -group by Def18; then consider H1 being finite Group such that A21: P1 = H1 and A22: H1 is p -group ; A23: not p divides index P1 by A19, Def18; consider r1 being Nat such that A24: card H1 = p |^ r1 by A22, Def17; assume A25: P2 is_Sylow_p-subgroup_of_prime p ; ::_thesis: P1,P2 are_conjugated then A26: not p divides index P2 by Def18; P2 is p -group by A25, Def18; then consider H2 being finite Group such that A27: P2 = H2 and A28: H2 is p -group ; consider r2 being Nat such that A29: card H2 = p |^ r2 by A28, Def17; A30: card G = (card P2) * (index P2) by GROUP_2:147; then A31: (p |^ r1) * (index P1) = (p |^ r2) * (index P2) by A21, A24, A27, A29, GROUP_2:147; now__::_thesis:_not_r1_<>_r2 assume A32: r1 <> r2 ; ::_thesis: contradiction percases ( r1 > r2 or r1 < r2 ) by A32, XXREAL_0:1; supposeA33: r1 > r2 ; ::_thesis: contradiction set r = r1 -' r2; A34: r1 - r2 > r2 - r2 by A33, XREAL_1:9; then A35: r1 -' r2 = r1 - r2 by XREAL_0:def_2; then consider k being Nat such that A36: r1 -' r2 = k + 1 by A34, NAT_1:6; r1 = r2 + (r1 -' r2) by A35; then p9 |^ r1 = (p9 |^ r2) * (p9 |^ (r1 -' r2)) by NEWTON:8; then (p9 |^ r2) * ((p9 |^ (r1 -' r2)) * (index P1)) = (p9 |^ r2) * (index P2) by A31; then (p9 |^ (r1 -' r2)) * (index P1) = index P2 by XCMPLX_1:5; then ((p |^ k) * p) * (index P1) = index P2 by A36, NEWTON:6; then p * ((p |^ k) * (index P1)) = index P2 ; hence contradiction by A26, NAT_D:def_3; ::_thesis: verum end; supposeA37: r1 < r2 ; ::_thesis: contradiction set r = r2 -' r1; A38: r2 - r1 > r1 - r1 by A37, XREAL_1:9; then A39: r2 -' r1 = r2 - r1 by XREAL_0:def_2; then consider k being Nat such that A40: r2 -' r1 = k + 1 by A38, NAT_1:6; r2 = r1 + (r2 -' r1) by A39; then p9 |^ r2 = (p9 |^ r1) * (p9 |^ (r2 -' r1)) by NEWTON:8; then (p9 |^ r1) * ((p9 |^ (r2 -' r1)) * (index P2)) = (p9 |^ r1) * (index P1) by A21, A24, A27, A29, A30, GROUP_2:147; then (p9 |^ (r2 -' r1)) * (index P2) = index P1 by XCMPLX_1:5; then ((p |^ k) * p) * (index P2) = index P1 by A40, NEWTON:6; then p * ((p |^ k) * (index P2)) = index P1 ; hence contradiction by A23, NAT_D:def_3; ::_thesis: verum end; end; end; then A41: card (carr P1) = card (carr P2) by A21, A24, A27, A29; consider g being Element of G such that A42: carr P1 c= carr (P2 |^ g) by A1, A20, A25; card (carr P2) = card P2 .= card (P2 |^ g) by GROUP_3:66 .= card (carr (P2 |^ g)) ; then multMagma(# the carrier of P1, the multF of P1 #) = multMagma(# the carrier of (P2 |^ g), the multF of (P2 |^ g) #) by A42, A41, CARD_FIN:1, GROUP_2:59; hence P1,P2 are_conjugated by GROUP_3:def_11; ::_thesis: verum end; 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); proof set X = { 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 ) } ; now__::_thesis:_for_x_being_set_st_x_in__{__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_)__}__holds_ x_in_Subgroups_G let x be set ; ::_thesis: ( x in { 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 ) } implies x in Subgroups G ) assume x in { 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 ) } ; ::_thesis: x in Subgroups G then ex H being Element of Subgroups G st ( x = H & ex P being strict Subgroup of G st ( P = H & P is_Sylow_p-subgroup_of_prime p ) ) ; hence x in Subgroups G ; ::_thesis: verum end; hence { 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) by TARSKI:def_3; ::_thesis: verum end; 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 ); proof consider P being strict Subgroup of G such that A1: P is_Sylow_p-subgroup_of_prime p by Th10; reconsider H9 = (Omega). P as Element of Subgroups G by GROUP_3:def_1; H9 in the_sylow_p-subgroups_of_prime (p,G) by A1; hence ( not the_sylow_p-subgroups_of_prime (p,G) is empty & the_sylow_p-subgroups_of_prime (p,G) is finite ) by FINSET_1:1, GROUP_3:15; ::_thesis: verum end; 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 ) proof set E = the_sylow_p-subgroups_of_prime (p,G); set f = { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ; A1: now__::_thesis:_for_x,_y1,_y2_being_set_st_[x,y1]_in__{__[P1,P2]_where_P1,_P2_is_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_ (_P1_=_H1_&_P2_=_H2_&_h_"_=_g_&_H2_=_H1_|^_g_)__}__&_[x,y2]_in__{__[P1,P2]_where_P1,_P2_is_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_ (_P1_=_H1_&_P2_=_H2_&_h_"_=_g_&_H2_=_H1_|^_g_)__}__holds_ y1_=_y2 let x, y1, y2 be set ; ::_thesis: ( [x,y1] in { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } & [x,y2] in { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies y1 = y2 ) assume [x,y1] in { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ; ::_thesis: ( [x,y2] in { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies y1 = y2 ) then consider P19, P29 being Element of the_sylow_p-subgroups_of_prime (p,G) such that A2: [x,y1] = [P19,P29] and A3: ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P19 = H1 & P29 = H2 & h " = g & H2 = H1 |^ g ) ; A4: x = P19 by A2, XTUPLE_0:1; assume [x,y2] in { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ; ::_thesis: y1 = y2 then consider P199, P299 being Element of the_sylow_p-subgroups_of_prime (p,G) such that A5: [x,y2] = [P199,P299] and A6: ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P199 = H1 & P299 = H2 & h " = g & H2 = H1 |^ g ) ; x = P199 by A5, XTUPLE_0:1; hence y1 = y2 by A2, A3, A5, A6, A4, XTUPLE_0:1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in__{__[P1,P2]_where_P1,_P2_is_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_ (_P1_=_H1_&_P2_=_H2_&_h_"_=_g_&_H2_=_H1_|^_g_)__}__holds_ ex_y,_z_being_set_st_x_=_[y,z] let x be set ; ::_thesis: ( x in { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } implies ex y, z being set st x = [y,z] ) assume x in { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } ; ::_thesis: ex y, z being set st x = [y,z] then consider P1, P2 being Element of the_sylow_p-subgroups_of_prime (p,G) such that A7: x = [P1,P2] and ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ; reconsider y = P1, z = P2 as set ; take y = y; ::_thesis: ex z being set st x = [y,z] take z = z; ::_thesis: x = [y,z] thus x = [y,z] by A7; ::_thesis: verum end; then reconsider f = { [P1,P2] where P1, P2 is 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 ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) } as Function by A1, FUNCT_1:def_1, RELAT_1:def_1; now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_the_sylow_p-subgroups_of_prime_(p,G) let y be set ; ::_thesis: ( y in rng f implies y in the_sylow_p-subgroups_of_prime (p,G) ) assume y in rng f ; ::_thesis: y in the_sylow_p-subgroups_of_prime (p,G) then consider x being set such that A8: [x,y] in f by XTUPLE_0:def_13; consider P1, P2 being Element of the_sylow_p-subgroups_of_prime (p,G) such that A9: [x,y] = [P1,P2] and ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) by A8; y = P2 by A9, XTUPLE_0:1; hence y in the_sylow_p-subgroups_of_prime (p,G) ; ::_thesis: verum end; then A10: rng f c= the_sylow_p-subgroups_of_prime (p,G) by TARSKI:def_3; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_sylow_p-subgroups_of_prime_(p,G)_implies_ex_y_being_set_st_[x,y]_in_f_)_&_(_ex_y_being_set_st_[x,y]_in_f_implies_x_in_the_sylow_p-subgroups_of_prime_(p,G)_)_) let x be set ; ::_thesis: ( ( x in the_sylow_p-subgroups_of_prime (p,G) implies ex y being set st [x,y] in f ) & ( ex y being set st [x,y] in f implies x in the_sylow_p-subgroups_of_prime (p,G) ) ) hereby ::_thesis: ( ex y being set st [x,y] in f implies x in the_sylow_p-subgroups_of_prime (p,G) ) reconsider g = h " as Element of G by GROUP_2:42; assume x in the_sylow_p-subgroups_of_prime (p,G) ; ::_thesis: ex y being set st [x,y] in f then reconsider P1 = x as Element of the_sylow_p-subgroups_of_prime (p,G) ; P1 in the_sylow_p-subgroups_of_prime (p,G) ; then consider H1 being Element of Subgroups G such that A11: P1 = H1 and A12: ex P being strict Subgroup of G st ( P = H1 & P is_Sylow_p-subgroup_of_prime p ) ; reconsider H1 = H1 as strict Subgroup of G by A12; H1 is p -group by A12, Def18; then consider H9 being finite Group such that A13: ( H1 = H9 & H9 is p -group ) ; set H2 = H1 |^ g; reconsider H2 = H1 |^ g as strict Subgroup of G ; reconsider H99 = H2 as finite Group ; ( ex r being Nat st card H9 = p |^ r & card H9 = card H99 ) by A13, Def17, GROUP_3:66; then A14: H99 is p -group by Def17; reconsider H29 = H2 as Element of Subgroups G by GROUP_3:def_1; A15: card H1 = card H2 by GROUP_3:66; A16: (card H1) * (index H1) = card G by GROUP_2:147 .= (card H1) * (index H2) by A15, GROUP_2:147 ; not p divides index H1 by A12, Def18; then not p divides index H2 by A16, XCMPLX_1:5; then H2 is_Sylow_p-subgroup_of_prime p by A14, Def18; then H29 in the_sylow_p-subgroups_of_prime (p,G) ; then reconsider P2 = H2 as Element of the_sylow_p-subgroups_of_prime (p,G) ; reconsider y = P2 as set ; take y = y; ::_thesis: [x,y] in f thus [x,y] in f by A11; ::_thesis: verum end; given y being set such that A17: [x,y] in f ; ::_thesis: x in the_sylow_p-subgroups_of_prime (p,G) consider P1, P2 being Element of the_sylow_p-subgroups_of_prime (p,G) such that A18: [x,y] = [P1,P2] and ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) by A17; x = P1 by A18, XTUPLE_0:1; hence x in the_sylow_p-subgroups_of_prime (p,G) ; ::_thesis: verum end; then A19: dom f = the_sylow_p-subgroups_of_prime (p,G) by XTUPLE_0:def_12; then reconsider f = f as Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) by A10, FUNCT_2:2; take f ; ::_thesis: 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 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) thus 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 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ::_thesis: verum proof let P1 be Element of the_sylow_p-subgroups_of_prime (p,G); ::_thesis: 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 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) set P2 = f . P1; [P1,(f . P1)] in f by A19, FUNCT_1:1; then consider P19, P29 being Element of the_sylow_p-subgroups_of_prime (p,G) such that A20: [P1,(f . P1)] = [P19,P29] and A21: ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P19 = H1 & P29 = H2 & h " = g & H2 = H1 |^ g ) ; reconsider P2 = f . P1 as Element of the_sylow_p-subgroups_of_prime (p,G) ; consider H1, H2 being strict Subgroup of G, g being Element of G such that A22: ( P19 = H1 & P29 = H2 & h " = g ) and H2 = H1 |^ g by A21; take P2 ; ::_thesis: ex H1, H2 being strict Subgroup of G ex g being Element of G st ( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) take H1 ; ::_thesis: ex H2 being strict Subgroup of G ex g being Element of G st ( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) take H2 ; ::_thesis: ex g being Element of G st ( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) take g ; ::_thesis: ( P2 = f . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) thus P2 = f . P1 ; ::_thesis: ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) thus ( P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) by A20, A21, A22, XTUPLE_0:1; ::_thesis: verum end; end; 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 proof let IT1, IT2 be Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)); ::_thesis: ( ( 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 = IT1 . 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 = IT2 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) implies IT1 = IT2 ) assume A23: ( ( 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 = IT1 . 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 = IT2 . P1 & P1 = H1 & P2 = H2 & h " = g & H2 = H1 |^ g ) ) ) ; ::_thesis: IT1 = IT2 let x be Element of the_sylow_p-subgroups_of_prime (p,G); :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ ( ex P12 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H11, H12 being strict Subgroup of G ex g1 being Element of G st ( P12 = IT1 . x & x = H11 & P12 = H12 & h " = g1 & H12 = H11 |^ g1 ) & ex P22 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H21, H22 being strict Subgroup of G ex g2 being Element of G st ( P22 = IT2 . x & x = H21 & P22 = H22 & h " = g2 & H22 = H21 |^ g2 ) ) by A23; hence IT1 . x = IT2 . x ; ::_thesis: verum end; 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) proof deffunc H1( Element of H) -> Function of (the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G)) = the_left_translation_of ($1,p); set E = the_sylow_p-subgroups_of_prime (p,G); A1: for h1, h2 being Element of H holds H1(h1 * h2) = H1(h1) * H1(h2) proof let h1, h2 be Element of H; ::_thesis: H1(h1 * h2) = H1(h1) * H1(h2) set f12 = the_left_translation_of ((h1 * h2),p); set f1 = the_left_translation_of (h1,p); set f2 = the_left_translation_of (h2,p); the_left_translation_of (h1,p) in Funcs ((the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G))) by FUNCT_2:9; then A2: ex f being Function st ( the_left_translation_of (h1,p) = f & dom f = the_sylow_p-subgroups_of_prime (p,G) & rng f c= the_sylow_p-subgroups_of_prime (p,G) ) by FUNCT_2:def_2; the_left_translation_of (h2,p) in Funcs ((the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G))) by FUNCT_2:9; then A3: ex f being Function st ( the_left_translation_of (h2,p) = f & dom f = the_sylow_p-subgroups_of_prime (p,G) & rng f c= the_sylow_p-subgroups_of_prime (p,G) ) by FUNCT_2:def_2; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_(the_left_translation_of_((h1_*_h2),p))_holds_ (the_left_translation_of_((h1_*_h2),p))_._x_=_(the_left_translation_of_(h1,p))_._((the_left_translation_of_(h2,p))_._x) let x be set ; ::_thesis: ( x in dom (the_left_translation_of ((h1 * h2),p)) implies (the_left_translation_of ((h1 * h2),p)) . x = (the_left_translation_of (h1,p)) . ((the_left_translation_of (h2,p)) . x) ) assume A5: x in dom (the_left_translation_of ((h1 * h2),p)) ; ::_thesis: (the_left_translation_of ((h1 * h2),p)) . x = (the_left_translation_of (h1,p)) . ((the_left_translation_of (h2,p)) . x) then reconsider P19 = x as Element of the_sylow_p-subgroups_of_prime (p,G) ; reconsider P1999 = x as Element of the_sylow_p-subgroups_of_prime (p,G) by A5; consider P29 being Element of the_sylow_p-subgroups_of_prime (p,G), H19, H29 being strict Subgroup of G, g2 being Element of G such that A6: ( P29 = (the_left_translation_of (h2,p)) . P19 & P19 = H19 & P29 = H29 ) and A7: h2 " = g2 and A8: H29 = H19 |^ g2 by Def20; (the_left_translation_of (h2,p)) . x in rng (the_left_translation_of (h2,p)) by A3, A5, FUNCT_1:3; then reconsider P199 = (the_left_translation_of (h2,p)) . x as Element of the_sylow_p-subgroups_of_prime (p,G) ; consider P299 being Element of the_sylow_p-subgroups_of_prime (p,G), H199, H299 being strict Subgroup of G, g1 being Element of G such that A9: P299 = (the_left_translation_of (h1,p)) . P199 and A10: ( P199 = H199 & P299 = H299 ) and A11: h1 " = g1 and A12: H299 = H199 |^ g1 by Def20; consider P2999 being Element of the_sylow_p-subgroups_of_prime (p,G), H1999, H2999 being strict Subgroup of G, g3 being Element of G such that A13: P2999 = (the_left_translation_of ((h1 * h2),p)) . P1999 and A14: P1999 = H1999 and A15: P2999 = H2999 and A16: (h1 * h2) " = g3 and A17: H2999 = H1999 |^ g3 by Def20; g3 = (h2 ") * (h1 ") by A16, GROUP_1:17; then P2999 = H1999 |^ (g2 * g1) by A7, A11, A15, A17, GROUP_2:43 .= P299 by A6, A8, A10, A12, A14, GROUP_3:60 ; hence (the_left_translation_of ((h1 * h2),p)) . x = (the_left_translation_of (h1,p)) . ((the_left_translation_of (h2,p)) . x) by A9, A13; ::_thesis: verum end; the_left_translation_of ((h1 * h2),p) in Funcs ((the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G))) by FUNCT_2:9; then A18: ex f being Function st ( the_left_translation_of ((h1 * h2),p) = f & dom f = the_sylow_p-subgroups_of_prime (p,G) & rng f c= the_sylow_p-subgroups_of_prime (p,G) ) by FUNCT_2:def_2; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_dom_(the_left_translation_of_((h1_*_h2),p))_implies_(_x_in_dom_(the_left_translation_of_(h2,p))_&_(the_left_translation_of_(h2,p))_._x_in_dom_(the_left_translation_of_(h1,p))_)_)_&_(_x_in_dom_(the_left_translation_of_(h2,p))_&_(the_left_translation_of_(h2,p))_._x_in_dom_(the_left_translation_of_(h1,p))_implies_x_in_dom_(the_left_translation_of_((h1_*_h2),p))_)_) let x be set ; ::_thesis: ( ( x in dom (the_left_translation_of ((h1 * h2),p)) implies ( x in dom (the_left_translation_of (h2,p)) & (the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p)) ) ) & ( x in dom (the_left_translation_of (h2,p)) & (the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p)) implies x in dom (the_left_translation_of ((h1 * h2),p)) ) ) hereby ::_thesis: ( x in dom (the_left_translation_of (h2,p)) & (the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p)) implies x in dom (the_left_translation_of ((h1 * h2),p)) ) assume A19: x in dom (the_left_translation_of ((h1 * h2),p)) ; ::_thesis: ( x in dom (the_left_translation_of (h2,p)) & (the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p)) ) hence x in dom (the_left_translation_of (h2,p)) by A3; ::_thesis: (the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p)) (the_left_translation_of (h2,p)) . x in rng (the_left_translation_of (h2,p)) by A3, A19, FUNCT_1:3; hence (the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p)) by A2; ::_thesis: verum end; assume that A20: x in dom (the_left_translation_of (h2,p)) and (the_left_translation_of (h2,p)) . x in dom (the_left_translation_of (h1,p)) ; ::_thesis: x in dom (the_left_translation_of ((h1 * h2),p)) thus x in dom (the_left_translation_of ((h1 * h2),p)) by A18, A20; ::_thesis: verum end; hence H1(h1 * h2) = H1(h1) * H1(h2) by A4, FUNCT_1:10; ::_thesis: verum end; A21: H1( 1_ H) = id (the_sylow_p-subgroups_of_prime (p,G)) proof set f = the_left_translation_of ((1_ H),p); A22: now__::_thesis:_for_x_being_set_st_x_in_the_sylow_p-subgroups_of_prime_(p,G)_holds_ (the_left_translation_of_((1__H),p))_._x_=_x let x be set ; ::_thesis: ( x in the_sylow_p-subgroups_of_prime (p,G) implies (the_left_translation_of ((1_ H),p)) . x = x ) assume x in the_sylow_p-subgroups_of_prime (p,G) ; ::_thesis: (the_left_translation_of ((1_ H),p)) . x = x then reconsider P1 = x as Element of the_sylow_p-subgroups_of_prime (p,G) ; consider P2 being Element of the_sylow_p-subgroups_of_prime (p,G), H1, H2 being strict Subgroup of G, g being Element of G such that A23: ( P2 = (the_left_translation_of ((1_ H),p)) . P1 & P1 = H1 & P2 = H2 ) and A24: (1_ H) " = g and A25: H2 = H1 |^ g by Def20; (1_ H) " = 1_ H by GROUP_1:8; then g = 1_ G by A24, GROUP_2:44; hence (the_left_translation_of ((1_ H),p)) . x = x by A23, A25, GROUP_3:61; ::_thesis: verum end; the_left_translation_of ((1_ H),p) in Funcs ((the_sylow_p-subgroups_of_prime (p,G)),(the_sylow_p-subgroups_of_prime (p,G))) by FUNCT_2:9; then ex f9 being Function st ( the_left_translation_of ((1_ H),p) = f9 & dom f9 = the_sylow_p-subgroups_of_prime (p,G) & rng f9 c= the_sylow_p-subgroups_of_prime (p,G) ) by FUNCT_2:def_2; hence H1( 1_ H) = id (the_sylow_p-subgroups_of_prime (p,G)) by A22, FUNCT_1:17; ::_thesis: verum end; ex T being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) st for h being Element of H holds T . h = H1(h) from GROUP_10:sch_1(A21, A1); hence 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) ; ::_thesis: verum end; 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 proof let T1, T2 be LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)); ::_thesis: ( ( for h being Element of H holds T1 . h = the_left_translation_of (h,p) ) & ( for h being Element of H holds T2 . h = the_left_translation_of (h,p) ) implies T1 = T2 ) assume that A26: for h being Element of H holds T1 . h = the_left_translation_of (h,p) and A27: for h being Element of H holds T2 . h = the_left_translation_of (h,p) ; ::_thesis: T1 = T2 let x be Element of H; :: according to FUNCT_2:def_8 ::_thesis: ^ = ^ thus T1 . x = the_left_translation_of (x,p) by A26 .= T2 . x by A27 ; ::_thesis: verum end; 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 proof let G, H be finite Group; ::_thesis: 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 let p be prime Nat; ::_thesis: 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 let I be Subgroup of G; ::_thesis: 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 let P be Subgroup of H; ::_thesis: ( I = P & I is_Sylow_p-subgroup_of_prime p & H is Subgroup of G implies P is_Sylow_p-subgroup_of_prime p ) assume A1: I = P ; ::_thesis: ( not I is_Sylow_p-subgroup_of_prime p or not H is Subgroup of G or P is_Sylow_p-subgroup_of_prime p ) assume A2: I is_Sylow_p-subgroup_of_prime p ; ::_thesis: ( not H is Subgroup of G or P is_Sylow_p-subgroup_of_prime p ) then A3: I is p -group by Def18; assume H is Subgroup of G ; ::_thesis: P is_Sylow_p-subgroup_of_prime p then reconsider H9 = H as Subgroup of G ; A4: index I = (index P) * (index H9) by A1, GROUP_2:149; not p divides index I by A2, Def18; then not p divides index P by A4, NAT_D:9; hence P is_Sylow_p-subgroup_of_prime p by A1, A3, Def18; ::_thesis: verum end; 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 ) proof let G be finite Group; ::_thesis: 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 ) let p be prime Nat; ::_thesis: ( (card (the_sylow_p-subgroups_of_prime (p,G))) mod p = 1 & card (the_sylow_p-subgroups_of_prime (p,G)) divides card G ) set E = the_sylow_p-subgroups_of_prime (p,G); A1: p > 1 by NAT_4:12; consider P being strict Subgroup of G such that A2: P is_Sylow_p-subgroup_of_prime p by Th10; set P9 = (Omega). P; reconsider P9 = (Omega). P as strict Subgroup of G ; reconsider H9 = P9 as Element of Subgroups G by GROUP_3:def_1; reconsider P9 = P9 as finite strict Subgroup of G ; H9 = P9 ; then P9 in the_sylow_p-subgroups_of_prime (p,G) by A2; then reconsider P9 = P9 as Element of the_sylow_p-subgroups_of_prime (p,G) ; set T = the_left_operation_of (P,p); A3: P is p -group by A2, Def18; set G9 = (Omega). G; set T9 = the_left_operation_of (((Omega). G),p); set K = the_strict_stabilizer_of (P9,(the_left_operation_of (((Omega). G),p))); A4: now__::_thesis:_for_y_being_set_holds_ (_(_y_in_the_orbit_of_(P9,(the_left_operation_of_(((Omega)._G),p)))_implies_y_in_the_sylow_p-subgroups_of_prime_(p,G)_)_&_(_y_in_the_sylow_p-subgroups_of_prime_(p,G)_implies_y_in_the_orbit_of_(P9,(the_left_operation_of_(((Omega)._G),p)))_)_) reconsider P1 = P9 as Element of the_sylow_p-subgroups_of_prime (p,G) ; reconsider P99 = P9 as strict Subgroup of G ; let y be set ; ::_thesis: ( ( y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) implies y in the_sylow_p-subgroups_of_prime (p,G) ) & ( y in the_sylow_p-subgroups_of_prime (p,G) implies y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) ) ) thus ( y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) implies y in the_sylow_p-subgroups_of_prime (p,G) ) ; ::_thesis: ( y in the_sylow_p-subgroups_of_prime (p,G) implies y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) ) assume y in the_sylow_p-subgroups_of_prime (p,G) ; ::_thesis: y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) then consider Q being Element of Subgroups G such that A5: y = Q and A6: ex P being strict Subgroup of G st ( P = Q & P is_Sylow_p-subgroup_of_prime p ) ; consider Q9 being strict Subgroup of G such that A7: Q9 = Q and A8: Q9 is_Sylow_p-subgroup_of_prime p by A6; P99,Q9 are_conjugated by A2, A8, Th12; then consider g being Element of G such that A9: Q9 = P99 |^ g by GROUP_3:def_11; Q9 in the_sylow_p-subgroups_of_prime (p,G) by A7, A8; then reconsider Q99 = Q9 as Element of the_sylow_p-subgroups_of_prime (p,G) ; reconsider g9 = g " as Element of ((Omega). G) ; A10: g9 " = (g ") " by GROUP_2:48 .= g ; ex P2 being Element of the_sylow_p-subgroups_of_prime (p,G) ex H1, H2 being strict Subgroup of G ex g999 being Element of G st ( P2 = (the_left_translation_of (g9,p)) . P1 & P1 = H1 & P2 = H2 & g9 " = g999 & H2 = H1 |^ g999 ) by Def20; then Q9 = ((the_left_operation_of (((Omega). G),p)) ^ g9) . P9 by A9, A10, Def21; then P9,Q99 are_conjugated_under the_left_operation_of (((Omega). G),p) by Def14; hence y in the_orbit_of (P9,(the_left_operation_of (((Omega). G),p))) by A5, A7; ::_thesis: verum end; reconsider P = P as finite Subgroup of G ; reconsider T = the_left_operation_of (P,p) as LeftOperation of P,(the_sylow_p-subgroups_of_prime (p,G)) ; for x being set holds ( x in the_fixed_points_of T iff x = P9 ) proof let x be set ; ::_thesis: ( x in the_fixed_points_of T iff x = P9 ) for h being Element of P holds P9 = (T ^ h) . P9 proof reconsider P1 = P9 as Element of the_sylow_p-subgroups_of_prime (p,G) ; let h be Element of P; ::_thesis: P9 = (T ^ h) . P9 consider P2 being Element of the_sylow_p-subgroups_of_prime (p,G), H1, H2 being strict Subgroup of G, g being Element of G such that A11: P2 = (the_left_translation_of (h,p)) . P1 and A12: P1 = H1 and A13: P2 = H2 and A14: h " = g and A15: H2 = H1 |^ g by Def20; A16: g in H1 by A12, A14, STRUCT_0:def_5; now__::_thesis:_for_y_being_set_st_y_in_carr_H1_holds_ y_in_((g_")_*_H1)_*_g let y be set ; ::_thesis: ( y in carr H1 implies y in ((g ") * H1) * g ) assume A17: y in carr H1 ; ::_thesis: y in ((g ") * H1) * g then reconsider h9 = y as Element of G ; A18: h9 in H1 by A17, STRUCT_0:def_5; ex h being Element of G st ( y = h * g & h in (g ") * H1 ) proof set h99 = h9 * (g "); take h9 * (g ") ; ::_thesis: ( y = (h9 * (g ")) * g & h9 * (g ") in (g ") * H1 ) thus (h9 * (g ")) * g = h9 * ((g ") * g) by GROUP_1:def_3 .= h9 * (1_ G) by GROUP_1:def_5 .= y by GROUP_1:def_4 ; ::_thesis: h9 * (g ") in (g ") * H1 g " in H1 by A16, GROUP_2:51; then A19: h9 * (g ") in H1 by A18, GROUP_2:50; ex h being Element of G st ( h9 * (g ") = (g ") * h & h in H1 ) proof set h999 = g * (h9 * (g ")); take g * (h9 * (g ")) ; ::_thesis: ( h9 * (g ") = (g ") * (g * (h9 * (g "))) & g * (h9 * (g ")) in H1 ) thus (g ") * (g * (h9 * (g "))) = ((g ") * g) * (h9 * (g ")) by GROUP_1:def_3 .= (1_ G) * (h9 * (g ")) by GROUP_1:def_5 .= h9 * (g ") by GROUP_1:def_4 ; ::_thesis: g * (h9 * (g ")) in H1 thus g * (h9 * (g ")) in H1 by A16, A19, GROUP_2:50; ::_thesis: verum end; hence h9 * (g ") in (g ") * H1 by GROUP_2:103; ::_thesis: verum end; hence y in ((g ") * H1) * g by GROUP_2:28; ::_thesis: verum end; then carr H1 c= ((g ") * H1) * g by TARSKI:def_3; then A20: carr H1 c= carr (H1 |^ g) by GROUP_3:59; A21: card (carr H1) = card H1 .= card (H1 |^ g) by GROUP_3:66 .= card (carr (H1 |^ g)) ; (T ^ h) . P9 = P2 by A11, Def21; hence P9 = (T ^ h) . P9 by A12, A13, A15, A20, A21, CARD_FIN:1, GROUP_2:59; ::_thesis: verum end; then A22: P9 is_fixed_under T by Def12; hereby ::_thesis: ( x = P9 implies x in the_fixed_points_of T ) assume x in the_fixed_points_of T ; ::_thesis: x = P9 then x in { x9 where x9 is Element of the_sylow_p-subgroups_of_prime (p,G) : x9 is_fixed_under T } by Def13; then consider Q being Element of the_sylow_p-subgroups_of_prime (p,G) such that A23: x = Q and A24: Q is_fixed_under T ; Q in { H99 where H99 is Element of Subgroups G : ex P being strict Subgroup of G st ( P = H99 & P is_Sylow_p-subgroup_of_prime p ) } ; then consider H99 being Element of Subgroups G such that A25: Q = H99 and A26: ex P being strict Subgroup of G st ( P = H99 & P is_Sylow_p-subgroup_of_prime p ) ; consider Q9 being strict Subgroup of G such that A27: Q9 = H99 and A28: Q9 is_Sylow_p-subgroup_of_prime p by A26; set N = Normalizer Q9; now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_P_holds_ y_in_the_carrier_of_(Normalizer_Q9) let y be set ; ::_thesis: ( y in the carrier of P implies y in the carrier of (Normalizer Q9) ) assume A29: y in the carrier of P ; ::_thesis: y in the carrier of (Normalizer Q9) ex h being Element of G st ( y = h & Q9 |^ h = Q9 ) proof set h = y; the carrier of P c= the carrier of G by GROUP_2:def_5; then reconsider h = y as Element of G by A29; reconsider h9 = h as Element of P by A29; take h ; ::_thesis: ( y = h & Q9 |^ h = Q9 ) thus y = h ; ::_thesis: Q9 |^ h = Q9 dom (T ^ h9) = the_sylow_p-subgroups_of_prime (p,G) by FUNCT_2:def_1; then Q9 in dom (T ^ h9) by A27, A28; then reconsider Q1 = Q9 as Element of the_sylow_p-subgroups_of_prime (p,G) ; A30: ex Q2 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 ( Q2 = (the_left_translation_of (h9,p)) . Q1 & Q1 = H1 & Q2 = H2 & h9 " = g & H2 = H1 |^ g ) by Def20; ( Q9 = (T ^ h9) . Q9 & T . h9 = the_left_translation_of (h9,p) ) by A24, A25, A27, Def12, Def21; then Q9 |^ (h ") = Q9 by A30, GROUP_2:48; then ( (h ") * h = 1_ G & Q9 |^ ((h ") * h) = Q9 |^ h ) by GROUP_1:def_5, GROUP_3:60; hence Q9 |^ h = Q9 by GROUP_3:61; ::_thesis: verum end; then y in Normalizer Q9 by GROUP_3:134; hence y in the carrier of (Normalizer Q9) by STRUCT_0:def_5; ::_thesis: verum end; then A31: the carrier of P c= the carrier of (Normalizer Q9) by TARSKI:def_3; A32: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_Q9_holds_ y_in_the_carrier_of_(Normalizer_Q9) let y be set ; ::_thesis: ( y in the carrier of Q9 implies y in the carrier of (Normalizer Q9) ) assume A33: y in the carrier of Q9 ; ::_thesis: y in the carrier of (Normalizer Q9) ex h being Element of G st ( y = h & Q9 |^ h = Q9 ) proof set h = y; the carrier of Q9 c= the carrier of G by GROUP_2:def_5; then reconsider h = y as Element of G by A33; take h ; ::_thesis: ( y = h & Q9 |^ h = Q9 ) thus y = h ; ::_thesis: Q9 |^ h = Q9 for g being Element of G holds ( g in Q9 iff g in Q9 |^ h ) proof let g be Element of G; ::_thesis: ( g in Q9 iff g in Q9 |^ h ) hereby ::_thesis: ( g in Q9 |^ h implies g in Q9 ) assume A34: g in Q9 ; ::_thesis: g in Q9 |^ h ex g9 being Element of G st ( g = g9 |^ h & g9 in Q9 ) proof set g9 = (h * g) * (h "); take (h * g) * (h ") ; ::_thesis: ( g = ((h * g) * (h ")) |^ h & (h * g) * (h ") in Q9 ) thus ((h * g) * (h ")) |^ h = ((h ") * ((h * g) * (h "))) * h by GROUP_3:def_2 .= ((h ") * (h * (g * (h ")))) * h by GROUP_1:def_3 .= (((h ") * h) * (g * (h "))) * h by GROUP_1:def_3 .= ((1_ G) * (g * (h "))) * h by GROUP_1:def_5 .= (g * (h ")) * h by GROUP_1:def_4 .= g * ((h ") * h) by GROUP_1:def_3 .= g * (1_ G) by GROUP_1:def_5 .= g by GROUP_1:def_4 ; ::_thesis: (h * g) * (h ") in Q9 h in Q9 by A33, STRUCT_0:def_5; then ( h " in Q9 & h * g in Q9 ) by A34, GROUP_2:50, GROUP_2:51; hence (h * g) * (h ") in Q9 by GROUP_2:50; ::_thesis: verum end; hence g in Q9 |^ h by GROUP_3:58; ::_thesis: verum end; assume g in Q9 |^ h ; ::_thesis: g in Q9 then consider g9 being Element of G such that A35: g = g9 |^ h and A36: g9 in Q9 by GROUP_3:58; A37: h in Q9 by A33, STRUCT_0:def_5; then h " in Q9 by GROUP_2:51; then (h ") * g9 in Q9 by A36, GROUP_2:50; then ((h ") * g9) * h in Q9 by A37, GROUP_2:50; hence g in Q9 by A35, GROUP_3:def_2; ::_thesis: verum end; hence Q9 |^ h = Q9 by GROUP_2:def_6; ::_thesis: verum end; then y in Normalizer Q9 by GROUP_3:134; hence y in the carrier of (Normalizer Q9) by STRUCT_0:def_5; ::_thesis: verum end; then A38: the carrier of Q9 c= the carrier of (Normalizer Q9) by TARSKI:def_3; reconsider N = Normalizer Q9 as finite Group ; reconsider Q99 = Q9 as strict Subgroup of N by A38, GROUP_2:57; A39: Q99 is_Sylow_p-subgroup_of_prime p by A28, Lm9; reconsider P99 = P9 as strict Subgroup of N by A31, GROUP_2:57; P99 is_Sylow_p-subgroup_of_prime p by A2, Lm9; then P99,Q99 are_conjugated by A39, Th12; then consider n being Element of N such that A40: P99 = Q99 |^ n by GROUP_3:def_11; the carrier of (Q99 |^ n) c= the carrier of N by GROUP_2:def_5; then A41: the multF of G || the carrier of (Q99 |^ n) = ( the multF of G || the carrier of N) || the carrier of (Q99 |^ n) by RELAT_1:74, ZFMISC_1:96 .= the multF of N || the carrier of (Q99 |^ n) by GROUP_2:def_5 ; n in Normalizer Q9 by STRUCT_0:def_5; then consider n9 being Element of G such that A42: n = n9 and A43: Q9 |^ n9 = Q9 by GROUP_3:134; A44: now__::_thesis:_for_y_being_set_holds_ (_(_y_in_the_carrier_of_(Q9_|^_n9)_implies_y_in_the_carrier_of_(Q99_|^_n)_)_&_(_y_in_the_carrier_of_(Q99_|^_n)_implies_y_in_the_carrier_of_(Q9_|^_n9)_)_) let y be set ; ::_thesis: ( ( y in the carrier of (Q9 |^ n9) implies y in the carrier of (Q99 |^ n) ) & ( y in the carrier of (Q99 |^ n) implies y in the carrier of (Q9 |^ n9) ) ) hereby ::_thesis: ( y in the carrier of (Q99 |^ n) implies y in the carrier of (Q9 |^ n9) ) assume y in the carrier of (Q9 |^ n9) ; ::_thesis: y in the carrier of (Q99 |^ n) then y in (carr Q9) |^ n9 by GROUP_3:def_6; then consider q9 being Element of G such that A45: y = q9 |^ n9 and A46: q9 in carr Q9 by GROUP_3:41; reconsider q99 = q9 as Element of N by A32, A46; n9 " = n " by A42, GROUP_2:48; then (n9 ") * q9 = (n ") * q99 by GROUP_2:43; then A47: ((n9 ") * q9) * n9 = ((n ") * q99) * n by A42, GROUP_2:43; q9 |^ n9 = ((n9 ") * q9) * n9 by GROUP_3:def_2 .= q99 |^ n by A47, GROUP_3:def_2 ; then y in (carr Q99) |^ n by A45, A46, GROUP_3:41; hence y in the carrier of (Q99 |^ n) by GROUP_3:def_6; ::_thesis: verum end; assume y in the carrier of (Q99 |^ n) ; ::_thesis: y in the carrier of (Q9 |^ n9) then y in (carr Q99) |^ n by GROUP_3:def_6; then consider q99 being Element of N such that A48: y = q99 |^ n and A49: q99 in carr Q99 by GROUP_3:41; the carrier of Q99 c= the carrier of G by GROUP_2:def_5; then reconsider q9 = q99 as Element of G by A49; n9 " = n " by A42, GROUP_2:48; then (n9 ") * q9 = (n ") * q99 by GROUP_2:43; then A50: ((n9 ") * q9) * n9 = ((n ") * q99) * n by A42, GROUP_2:43; q9 |^ n9 = ((n9 ") * q9) * n9 by GROUP_3:def_2 .= q99 |^ n by A50, GROUP_3:def_2 ; then y in (carr Q9) |^ n9 by A48, A49, GROUP_3:41; hence y in the carrier of (Q9 |^ n9) by GROUP_3:def_6; ::_thesis: verum end; then the carrier of (Q9 |^ n9) = the carrier of (Q99 |^ n) by TARSKI:1; then the multF of (Q9 |^ n9) = the multF of G || the carrier of (Q99 |^ n) by GROUP_2:def_5 .= the multF of (Q99 |^ n) by A41, GROUP_2:def_5 ; hence x = P9 by A23, A25, A27, A40, A43, A44, TARSKI:1; ::_thesis: verum end; assume x = P9 ; ::_thesis: x in the_fixed_points_of T then x in { x9 where x9 is Element of the_sylow_p-subgroups_of_prime (p,G) : x9 is_fixed_under T } by A22; hence x in the_fixed_points_of T by Def13; ::_thesis: verum end; then A51: the_fixed_points_of T = {P9} by TARSKI:def_1; (card (the_sylow_p-subgroups_of_prime (p,G))) mod p = (card (the_fixed_points_of T)) mod p by A3, Th9 .= 1 mod p by A51, CARD_1:30 ; hence (card (the_sylow_p-subgroups_of_prime (p,G))) mod p = 1 by A1, NAT_D:14; ::_thesis: card (the_sylow_p-subgroups_of_prime (p,G)) divides card G A52: card (the_orbit_of (P9,(the_left_operation_of (((Omega). G),p)))) = Index (the_strict_stabilizer_of (P9,(the_left_operation_of (((Omega). G),p)))) by Th8; reconsider K = the_strict_stabilizer_of (P9,(the_left_operation_of (((Omega). G),p))) as Subgroup of (Omega). G ; card G = (card ((Omega). G)) * 1 ; then A53: card G = (card K) * (index K) by GROUP_2:147; ex B being finite set st ( B = Left_Cosets K & index K = card B ) by GROUP_2:146; then card (the_sylow_p-subgroups_of_prime (p,G)) = index K by A52, A4, TARSKI:1; hence card (the_sylow_p-subgroups_of_prime (p,G)) divides card G by A53, NAT_D:def_3; ::_thesis: verum end; 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;