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