let G be Group; :: thesis: for phi being Automorphism of G st G is finite holds
for p being prime Nat
for P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p holds
Image (phi | P) is_Sylow_p-subgroup_of_prime p
let phi be Automorphism of G; :: thesis: ( G is finite implies for p being prime Nat
for P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p holds
Image (phi | P) is_Sylow_p-subgroup_of_prime p )
assume A0: G is finite ; :: thesis: for p being prime Nat
for P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p holds
Image (phi | P) is_Sylow_p-subgroup_of_prime p
let p be prime Nat; :: thesis: for P being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p holds
Image (phi | P) is_Sylow_p-subgroup_of_prime p
let P be strict Subgroup of G; :: thesis: ( P is_Sylow_p-subgroup_of_prime p implies Image (phi | P) is_Sylow_p-subgroup_of_prime p )
assume A1: P is_Sylow_p-subgroup_of_prime p ; :: thesis: Image (phi | P) is_Sylow_p-subgroup_of_prime p
then A2: P is p -group by GROUP_10:def 18;
set Q = phi .: P;
consider r being Nat such that
A3: card P = p |^ r by A2, GROUP_10:def 17;
card (phi .: P) = p |^ r by A3, Th19, GROUP_6:75;
then A4: phi .: P is p -group by GROUP_10:def 17;
A5: phi .: P = Image (phi | P) by GRSOLV_1:def 3;
not p divides index P by A1, GROUP_10:def 18;
then not p divides index (phi .: P) by A0, Th19, Th20;
hence Image (phi | P) is_Sylow_p-subgroup_of_prime p by A4, A5, GROUP_10:def 18; :: thesis: verum