0 by A2,NAT_D:26;
then consider x be object 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 be Element of E such that
x=x9 and
A5: x9 is_fixed_under T;
x9 in Left_Cosets P;
then consider g9 be Element of G such that
A6: x9 = g9 * P by GROUP_2:def 15;
set g=g9";
take g;
now
reconsider P1=x9 as Element of Left_Cosets P;
let y be object;
assume y in carr H;
then reconsider h=y as Element of H9;
reconsider h9=h as Element of H;
consider P2 be Element of Left_Cosets P, A1,A2 be Subset of G, g99 be
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
.= 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;
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";
hence contradiction by A9,A11,GROUP_2:27;
end;
hence y in g9 * P * g9" by A8;
end;
then carr H c= g" * P * g;
hence thesis by GROUP_3:59;
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
proof
let H be Subgroup of G;
consider P9 be strict Subgroup of G such that
A12: P9 is_Sylow_p-subgroup_of_prime p by Th10;
assume H is p-group;
then consider g be Element of G such that
A13: carr H c= carr(P9 |^ g) by A1,A12;
set P = P9 |^ g;
take P;
set H2 = P;
reconsider H2 as finite Group;
A14: card P9 = card P by GROUP_3:66;
P9 is p-group by A12;
then consider H1 be finite Group such that
A15: P9 = H1 and
A16: H1 is p-group;
ex r be Nat st card H1 = p |^ r by A16;
then
A17: H2 is p-group by A15,A14;
A18: not p divides index P9 by A12;
card P * index P = card G by GROUP_2:147
.= card P * index P9 by A14,GROUP_2:147;
then not p divides index P by A18,XCMPLX_1:5;
hence P is_Sylow_p-subgroup_of_prime p by A17;
thus thesis by A13,GROUP_2:57;
end;
let P1,P2 be Subgroup of G;
assume
A19: P1 is_Sylow_p-subgroup_of_prime p;
then
A20: P1 is p-group;
then consider H1 be finite Group such that
A21: P1 = H1 and
A22: H1 is p-group;
A23: not p divides index P1 by A19;
consider r1 be Nat such that
A24: card H1 = p |^ r1 by A22;
assume
A25: P2 is_Sylow_p-subgroup_of_prime p;
then
A26: not p divides index P2;
P2 is p-group by A25;
then consider H2 be finite Group such that
A27: P2 = H2 and
A28: H2 is p-group;
consider r2 be Nat such that
A29: card H2 = p |^ r2 by A28;
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
assume
A32: r1<>r2;
per cases by A32,XXREAL_0:1;
suppose
A33: r1 > r2;
set r = r1 -' r2;
A34: r1 - r2 > r2 - r2 by A33,XREAL_1:9;
then
A35: r = r1 - r2 by XREAL_0:def 2;
then consider k be Nat such that
A36: r = k + 1 by A34,NAT_1:6;
r1 = r2 + r by A35;
then p9 |^ r1 = p9 |^r2 * p9 |^ r by NEWTON:8;
then p9 |^ r2 * (p9 |^ r * index P1) = p9 |^ r2 * index P2 by A31;
then p9 |^ r * 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;
end;
suppose
A37: r1