[STATEMENT]
lemma ex_conj_sylow_group:
  assumes H:"H \<in> subgroups_of_size (p ^ b)"
  assumes Psize:"P \<in> subgroups_of_size (p ^ a)"
  obtains g where "g \<in> carrier G" "H \<subseteq> g <# (P #> inv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
H \<in> subgroups_of_size (p ^ b)
[PROOF STEP]
have HsubG:"subgroup H G"
[PROOF STATE]
proof (prove)
using this:
H \<in> subgroups_of_size (p ^ b)

goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
H \<in> {H. subgroup H G \<and> card H = p ^ b}

goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgroup H G

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence HG:"H \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
by (simp add:subgroup.subset)
[PROOF STATE]
proof (state)
this:
H \<subseteq> carrier G

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from Psize
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have PG:"subgroup P G" and cardP:"card P = p ^ a"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. subgroup P G &&& card P = p ^ a
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
P \<in> {H. subgroup H G \<and> card H = p ^ a}

goal (1 subgoal):
 1. subgroup P G &&& card P = p ^ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define H' where "H' = G\<lparr>carrier := H\<rparr>"
[PROOF STATE]
proof (state)
this:
H' = G\<lparr>carrier := H\<rparr>

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from HsubG
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
[PROOF STEP]
interpret Hgroup: group H'
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. Group.group H'
[PROOF STEP]
unfolding H'_def
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. Group.group (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
by (metis subgroup_imp_group)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
H \<in> subgroups_of_size (p ^ b)
[PROOF STEP]
have orderH':"order H' =  p ^ b"
[PROOF STATE]
proof (prove)
using this:
H \<in> subgroups_of_size (p ^ b)

goal (1 subgoal):
 1. order H' = p ^ b
[PROOF STEP]
unfolding H'_def subgroups_of_size_def order_def
[PROOF STATE]
proof (prove)
using this:
H \<in> {H. subgroup H G \<and> card H = p ^ b}

goal (1 subgoal):
 1. card (carrier (G\<lparr>carrier := H\<rparr>)) = p ^ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
order H' = p ^ b

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define \<phi> where "\<phi> = (\<lambda>g. \<lambda>U\<in>rcosets P. U #> inv g)"
[PROOF STATE]
proof (state)
this:
\<phi> = (\<lambda>g. \<lambda>U\<in>rcosets P. U #> inv g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with PG
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
\<phi> = (\<lambda>g. \<lambda>U\<in>rcosets P. U #> inv g)
[PROOF STEP]
interpret Gact: group_action G \<phi> "rcosets P"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
\<phi> = (\<lambda>g. \<lambda>U\<in>rcosets P. U #> inv g)

goal (1 subgoal):
 1. group_action G \<phi> (rcosets P)
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
using this:
subgroup P G
(\<lambda>g. \<lambda>U\<in>rcosets P. U #> inv g) = (\<lambda>g. \<lambda>U\<in>rcosets P. U #> inv g)

goal (1 subgoal):
 1. group_action G (\<lambda>g. \<lambda>U\<in>rcosets P. U #> inv g) (rcosets P)
[PROOF STEP]
by (metis inv_mult_on_rcosets_action)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
H \<in> subgroups_of_size (p ^ b)
[PROOF STEP]
interpret H'act: group_action H' \<phi> "rcosets P"
[PROOF STATE]
proof (prove)
using this:
H \<in> subgroups_of_size (p ^ b)

goal (1 subgoal):
 1. group_action H' \<phi> (rcosets P)
[PROOF STEP]
unfolding H'_def subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
H \<in> {H. subgroup H G \<and> card H = p ^ b}

goal (1 subgoal):
 1. group_action (G\<lparr>carrier := H\<rparr>) \<phi> (rcosets P)
[PROOF STEP]
by (metis (mono_tags) Gact.subgroup_action mem_Collect_eq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from finite_G PG
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
subgroup P G
[PROOF STEP]
have "finite (rcosets P)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup P G

goal (1 subgoal):
 1. finite (rcosets P)
[PROOF STEP]
unfolding RCOSETS_def r_coset_def
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup P G

goal (1 subgoal):
 1. finite (\<Union>a\<in>carrier G. {\<Union>h\<in>P. {h \<otimes> a}})
[PROOF STEP]
by (metis (lifting) finite.emptyI finite_UN_I finite_insert)
[PROOF STATE]
proof (state)
this:
finite (rcosets P)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with orderH' sylow_axioms cardP
[PROOF STATE]
proof (chain)
picking this:
order H' = p ^ b
sylow G p a m
card P = p ^ a
finite (rcosets P)
[PROOF STEP]
have "card H'act.fixed_points mod p = card (rcosets P) mod p"
[PROOF STATE]
proof (prove)
using this:
order H' = p ^ b
sylow G p a m
card P = p ^ a
finite (rcosets P)

goal (1 subgoal):
 1. card H'act.fixed_points mod p = card (rcosets P) mod p
[PROOF STEP]
unfolding sylow_def sylow_axioms_def
[PROOF STATE]
proof (prove)
using this:
order H' = p ^ b
Group.group G \<and> prime p \<and> order G = p ^ a * m \<and> finite (carrier G)
card P = p ^ a
finite (rcosets P)

goal (1 subgoal):
 1. card H'act.fixed_points mod p = card (rcosets P) mod p
[PROOF STEP]
by (metis H'act.fixed_point_congruence)
[PROOF STATE]
proof (state)
this:
card H'act.fixed_points mod p = card (rcosets P) mod p

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card H'act.fixed_points mod p = card (rcosets P) mod p

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from finite_G PG order_G cardP
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
subgroup P G
order G = p ^ a * m
card P = p ^ a
[PROOF STEP]
have "card (rcosets P) * p ^ a  = p ^ a * m"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup P G
order G = p ^ a * m
card P = p ^ a

goal (1 subgoal):
 1. card (rcosets P) * p ^ a = p ^ a * m
[PROOF STEP]
by (metis lagrange)
[PROOF STATE]
proof (state)
this:
card (rcosets P) * p ^ a = p ^ a * m

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with prime_p
[PROOF STATE]
proof (chain)
picking this:
prime p
card (rcosets P) * p ^ a = p ^ a * m
[PROOF STEP]
have "card (rcosets P) = m"
[PROOF STATE]
proof (prove)
using this:
prime p
card (rcosets P) * p ^ a = p ^ a * m

goal (1 subgoal):
 1. card (rcosets P) = m
[PROOF STEP]
by (metis less_nat_zero_code mult_cancel2 mult_is_0 mult.commute order_G zero_less_o_G)
[PROOF STATE]
proof (state)
this:
card (rcosets P) = m

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "card (rcosets P) mod p = m mod p"
[PROOF STATE]
proof (prove)
using this:
card (rcosets P) = m

goal (1 subgoal):
 1. card (rcosets P) mod p = m mod p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (rcosets P) mod p = m mod p

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (rcosets P) mod p = m mod p

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from pNotDvdm prime_p
[PROOF STATE]
proof (chain)
picking this:
\<not> p dvd m
prime p
[PROOF STEP]
have "... \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd m
prime p

goal (1 subgoal):
 1. m mod p \<noteq> 0
[PROOF STEP]
by (metis dvd_eq_mod_eq_0)
[PROOF STATE]
proof (state)
this:
m mod p \<noteq> 0

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card H'act.fixed_points mod p = card (rcosets P) mod p
card (rcosets P) mod p = m mod p
m mod p \<noteq> 0
[PROOF STEP]
have "card H'act.fixed_points \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
card H'act.fixed_points mod p = card (rcosets P) mod p
card (rcosets P) mod p = m mod p
m mod p \<noteq> 0

goal (1 subgoal):
 1. card H'act.fixed_points \<noteq> 0
[PROOF STEP]
by (metis mod_0)
[PROOF STATE]
proof (state)
this:
card H'act.fixed_points \<noteq> 0

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card H'act.fixed_points \<noteq> 0
[PROOF STEP]
obtain N where N:"N \<in> H'act.fixed_points"
[PROOF STATE]
proof (prove)
using this:
card H'act.fixed_points \<noteq> 0

goal (1 subgoal):
 1. (\<And>N. N \<in> H'act.fixed_points \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
N \<in> H'act.fixed_points

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence Ncoset:"N \<in> rcosets P"
[PROOF STATE]
proof (prove)
using this:
N \<in> H'act.fixed_points

goal (1 subgoal):
 1. N \<in> rcosets P
[PROOF STEP]
unfolding H'act.fixed_points_def
[PROOF STATE]
proof (prove)
using this:
N \<in> {m \<in> rcosets P. carrier H' \<subseteq> H'act.stabilizer m}

goal (1 subgoal):
 1. N \<in> rcosets P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
N \<in> rcosets P

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<in> rcosets P
[PROOF STEP]
obtain g where g:"g \<in> carrier G" "N = P #> g"
[PROOF STATE]
proof (prove)
using this:
N \<in> rcosets P

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; N = P #> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding RCOSETS_def
[PROOF STATE]
proof (prove)
using this:
N \<in> (\<Union>a\<in>carrier G. {P #> a})

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; N = P #> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
N = P #> g

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence invg:"inv g \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = P #> g

goal (1 subgoal):
 1. inv g \<in> carrier G
[PROOF STEP]
by (metis inv_closed)
[PROOF STATE]
proof (state)
this:
inv g \<in> carrier G

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence invinvg:"inv (inv g) \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
inv g \<in> carrier G

goal (1 subgoal):
 1. inv (inv g) \<in> carrier G
[PROOF STEP]
by (metis inv_closed)
[PROOF STATE]
proof (state)
this:
inv (inv g) \<in> carrier G

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from N
[PROOF STATE]
proof (chain)
picking this:
N \<in> H'act.fixed_points
[PROOF STEP]
have "carrier H' \<subseteq> H'act.stabilizer N"
[PROOF STATE]
proof (prove)
using this:
N \<in> H'act.fixed_points

goal (1 subgoal):
 1. carrier H' \<subseteq> H'act.stabilizer N
[PROOF STEP]
unfolding H'act.fixed_points_def
[PROOF STATE]
proof (prove)
using this:
N \<in> {m \<in> rcosets P. carrier H' \<subseteq> H'act.stabilizer m}

goal (1 subgoal):
 1. carrier H' \<subseteq> H'act.stabilizer N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
carrier H' \<subseteq> H'act.stabilizer N

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "\<forall>h\<in>H. \<phi> h N = N"
[PROOF STATE]
proof (prove)
using this:
carrier H' \<subseteq> H'act.stabilizer N

goal (1 subgoal):
 1. \<forall>h\<in>H. \<phi> h N = N
[PROOF STEP]
unfolding H'act.stabilizer_def
[PROOF STATE]
proof (prove)
using this:
carrier H' \<subseteq> {g \<in> carrier H'. \<phi> g N = N}

goal (1 subgoal):
 1. \<forall>h\<in>H. \<phi> h N = N
[PROOF STEP]
using H'_def
[PROOF STATE]
proof (prove)
using this:
carrier H' \<subseteq> {g \<in> carrier H'. \<phi> g N = N}
H' = G\<lparr>carrier := H\<rparr>

goal (1 subgoal):
 1. \<forall>h\<in>H. \<phi> h N = N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>h\<in>H. \<phi> h N = N

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with HG Ncoset
[PROOF STATE]
proof (chain)
picking this:
H \<subseteq> carrier G
N \<in> rcosets P
\<forall>h\<in>H. \<phi> h N = N
[PROOF STEP]
have a1:"\<forall>h\<in>H. N #> inv h \<subseteq> N"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
N \<in> rcosets P
\<forall>h\<in>H. \<phi> h N = N

goal (1 subgoal):
 1. \<forall>h\<in>H. N #> inv h \<subseteq> N
[PROOF STEP]
unfolding \<phi>_def
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
N \<in> rcosets P
\<forall>h\<in>H. (\<lambda>U\<in>rcosets P. U #> inv h) N = N

goal (1 subgoal):
 1. \<forall>h\<in>H. N #> inv h \<subseteq> N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>h\<in>H. N #> inv h \<subseteq> N

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "N <#> H \<subseteq> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N <#> H \<subseteq> N
[PROOF STEP]
unfolding set_mult_def r_coset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>h\<in>N. \<Union>k\<in>H. {h \<otimes> k}) \<subseteq> N
[PROOF STEP]
proof(auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h k. \<lbrakk>h \<in> N; k \<in> H\<rbrakk> \<Longrightarrow> h \<otimes> k \<in> N
[PROOF STEP]
fix n h
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h k. \<lbrakk>h \<in> N; k \<in> H\<rbrakk> \<Longrightarrow> h \<otimes> k \<in> N
[PROOF STEP]
assume n:"n \<in> N" and h:"h \<in> H"
[PROOF STATE]
proof (state)
this:
n \<in> N
h \<in> H

goal (1 subgoal):
 1. \<And>h k. \<lbrakk>h \<in> N; k \<in> H\<rbrakk> \<Longrightarrow> h \<otimes> k \<in> N
[PROOF STEP]
with H
[PROOF STATE]
proof (chain)
picking this:
H \<in> subgroups_of_size (p ^ b)
n \<in> N
h \<in> H
[PROOF STEP]
have "inv h \<in> H"
[PROOF STATE]
proof (prove)
using this:
H \<in> subgroups_of_size (p ^ b)
n \<in> N
h \<in> H

goal (1 subgoal):
 1. inv h \<in> H
[PROOF STEP]
by (metis (mono_tags) mem_Collect_eq subgroup.m_inv_closed subgroups_of_size_def)
[PROOF STATE]
proof (state)
this:
inv h \<in> H

goal (1 subgoal):
 1. \<And>h k. \<lbrakk>h \<in> N; k \<in> H\<rbrakk> \<Longrightarrow> h \<otimes> k \<in> N
[PROOF STEP]
with n HG PG a1
[PROOF STATE]
proof (chain)
picking this:
n \<in> N
H \<subseteq> carrier G
subgroup P G
\<forall>h\<in>H. N #> inv h \<subseteq> N
inv h \<in> H
[PROOF STEP]
have "n \<otimes> inv (inv h) \<in> N"
[PROOF STATE]
proof (prove)
using this:
n \<in> N
H \<subseteq> carrier G
subgroup P G
\<forall>h\<in>H. N #> inv h \<subseteq> N
inv h \<in> H

goal (1 subgoal):
 1. n \<otimes> inv (inv h) \<in> N
[PROOF STEP]
unfolding r_coset_def
[PROOF STATE]
proof (prove)
using this:
n \<in> N
H \<subseteq> carrier G
subgroup P G
\<forall>h\<in>H. (\<Union>ha\<in>N. {ha \<otimes> inv h}) \<subseteq> N
inv h \<in> H

goal (1 subgoal):
 1. n \<otimes> inv (inv h) \<in> N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<otimes> inv (inv h) \<in> N

goal (1 subgoal):
 1. \<And>h k. \<lbrakk>h \<in> N; k \<in> H\<rbrakk> \<Longrightarrow> h \<otimes> k \<in> N
[PROOF STEP]
with HG h
[PROOF STATE]
proof (chain)
picking this:
H \<subseteq> carrier G
h \<in> H
n \<otimes> inv (inv h) \<in> N
[PROOF STEP]
show  "n \<otimes> h \<in> N"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
h \<in> H
n \<otimes> inv (inv h) \<in> N

goal (1 subgoal):
 1. n \<otimes> h \<in> N
[PROOF STEP]
by (metis in_mono inv_inv)
[PROOF STATE]
proof (state)
this:
n \<otimes> h \<in> N

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N <#> H \<subseteq> N

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with g
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
N = P #> g
N <#> H \<subseteq> N
[PROOF STEP]
have "((P #> g) <#> H) #> inv g \<subseteq> (P #> g) #> inv g"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = P #> g
N <#> H \<subseteq> N

goal (1 subgoal):
 1. P #> g <#> H #> inv g \<subseteq> P #> g #> inv g
[PROOF STEP]
unfolding r_coset_def
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = (\<Union>h\<in>P. {h \<otimes> g})
N <#> H \<subseteq> N

goal (1 subgoal):
 1. (\<Union>h\<in>(\<Union>h\<in>P. {h \<otimes> g}) <#> H. {h \<otimes> inv g}) \<subseteq> (\<Union>h\<in>\<Union>h\<in>P. {h \<otimes> g}. {h \<otimes> inv g})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P #> g <#> H #> inv g \<subseteq> P #> g #> inv g

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with PG g invg
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
P #> g <#> H #> inv g \<subseteq> P #> g #> inv g
[PROOF STEP]
have "((P #> g) <#> H) #> inv g \<subseteq> P"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
P #> g <#> H #> inv g \<subseteq> P #> g #> inv g

goal (1 subgoal):
 1. P #> g <#> H #> inv g \<subseteq> P
[PROOF STEP]
by (metis coset_mult_assoc coset_mult_one r_inv subgroup.subset)
[PROOF STATE]
proof (state)
this:
P #> g <#> H #> inv g \<subseteq> P

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with g HG PG invg
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
N = P #> g
H \<subseteq> carrier G
subgroup P G
inv g \<in> carrier G
P #> g <#> H #> inv g \<subseteq> P
[PROOF STEP]
have "P <#> (g <# H #> inv g) \<subseteq> P"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = P #> g
H \<subseteq> carrier G
subgroup P G
inv g \<in> carrier G
P #> g <#> H #> inv g \<subseteq> P

goal (1 subgoal):
 1. P <#> (g <# H #> inv g) \<subseteq> P
[PROOF STEP]
by (metis lr_coset_assoc r_coset_subset_G rcos_assoc_lcos setmult_rcos_assoc subgroup.subset)
[PROOF STATE]
proof (state)
this:
P <#> (g <# H #> inv g) \<subseteq> P

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with PG HG g invg
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
H \<subseteq> carrier G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
P <#> (g <# H #> inv g) \<subseteq> P
[PROOF STEP]
have "g <# H #> inv g \<subseteq> P"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
H \<subseteq> carrier G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
P <#> (g <# H #> inv g) \<subseteq> P

goal (1 subgoal):
 1. g <# H #> inv g \<subseteq> P
[PROOF STEP]
by (metis l_coset_subset_G r_coset_subset_G set_mult_inclusion)
[PROOF STATE]
proof (state)
this:
g <# H #> inv g \<subseteq> P

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with g
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
N = P #> g
g <# H #> inv g \<subseteq> P
[PROOF STEP]
have "(g <# H #> inv g) #> inv (inv g) \<subseteq> P #> inv (inv g)"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = P #> g
g <# H #> inv g \<subseteq> P

goal (1 subgoal):
 1. g <# H #> inv g #> inv (inv g) \<subseteq> P #> inv (inv g)
[PROOF STEP]
unfolding r_coset_def
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = (\<Union>h\<in>P. {h \<otimes> g})
(\<Union>h\<in>g <# H. {h \<otimes> inv g}) \<subseteq> P

goal (1 subgoal):
 1. (\<Union>h\<in>\<Union>h\<in>g <# H. {h \<otimes> inv g}. {h \<otimes> inv (inv g)}) \<subseteq> (\<Union>h\<in>P. {h \<otimes> inv (inv g)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g <# H #> inv g #> inv (inv g) \<subseteq> P #> inv (inv g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with HG g invg invinvg
[PROOF STATE]
proof (chain)
picking this:
H \<subseteq> carrier G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
inv (inv g) \<in> carrier G
g <# H #> inv g #> inv (inv g) \<subseteq> P #> inv (inv g)
[PROOF STEP]
have "g <# H \<subseteq> P #> inv (inv g)"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
inv (inv g) \<in> carrier G
g <# H #> inv g #> inv (inv g) \<subseteq> P #> inv (inv g)

goal (1 subgoal):
 1. g <# H \<subseteq> P #> inv (inv g)
[PROOF STEP]
by (metis coset_mult_assoc coset_mult_inv2 l_coset_subset_G)
[PROOF STATE]
proof (state)
this:
g <# H \<subseteq> P #> inv (inv g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with g
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
N = P #> g
g <# H \<subseteq> P #> inv (inv g)
[PROOF STEP]
have "(inv g) <# (g <# H) \<subseteq> inv g <# (P #> inv (inv g))"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = P #> g
g <# H \<subseteq> P #> inv (inv g)

goal (1 subgoal):
 1. inv g <# (g <# H) \<subseteq> inv g <# (P #> inv (inv g))
[PROOF STEP]
unfolding l_coset_def
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
N = P #> g
(\<Union>h\<in>H. {g \<otimes> h}) \<subseteq> P #> inv (inv g)

goal (1 subgoal):
 1. (\<Union>h\<in>\<Union>h\<in>H. {g \<otimes> h}. {inv g \<otimes> h}) \<subseteq> (\<Union>h\<in>P #> inv (inv g). {inv g \<otimes> h})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv g <# (g <# H) \<subseteq> inv g <# (P #> inv (inv g))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with HG g invg invinvg
[PROOF STATE]
proof (chain)
picking this:
H \<subseteq> carrier G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
inv (inv g) \<in> carrier G
inv g <# (g <# H) \<subseteq> inv g <# (P #> inv (inv g))
[PROOF STEP]
have "H \<subseteq> inv g <# (P #> inv (inv g))"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
g \<in> carrier G
N = P #> g
inv g \<in> carrier G
inv (inv g) \<in> carrier G
inv g <# (g <# H) \<subseteq> inv g <# (P #> inv (inv g))

goal (1 subgoal):
 1. H \<subseteq> inv g <# (P #> inv (inv g))
[PROOF STEP]
by (metis inv_inv lcos_m_assoc lcos_mult_one r_inv)
[PROOF STATE]
proof (state)
this:
H \<subseteq> inv g <# (P #> inv (inv g))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with invg
[PROOF STATE]
proof (chain)
picking this:
inv g \<in> carrier G
H \<subseteq> inv g <# (P #> inv (inv g))
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
inv g \<in> carrier G
H \<subseteq> inv g <# (P #> inv (inv g))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto dest:that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem sylow_contained_in_sylow_group:
  assumes H:"H \<in> subgroups_of_size (p ^ b)"
  obtains S where "H \<subseteq> S" and "S \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
H \<in> subgroups_of_size (p ^ b)
[PROOF STEP]
have HG:"H \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
using this:
H \<in> subgroups_of_size (p ^ b)

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
H \<in> {H. subgroup H G \<and> card H = p ^ b}

goal (1 subgoal):
 1. H \<subseteq> carrier G
[PROOF STEP]
by (simp add:subgroup.subset)
[PROOF STATE]
proof (state)
this:
H \<subseteq> carrier G

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>subgroup P G; card P = p ^ a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis sylow_thm)
[PROOF STATE]
proof (state)
this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence Psize:"P \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> {H. subgroup H G \<and> card H = p ^ a}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with H
[PROOF STATE]
proof (chain)
picking this:
H \<in> subgroups_of_size (p ^ b)
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
obtain g where g:"g \<in> carrier G" "H \<subseteq> g <# (P #> inv g)"
[PROOF STATE]
proof (prove)
using this:
H \<in> subgroups_of_size (p ^ b)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; H \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis ex_conj_sylow_group)
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note Psize g
[PROOF STATE]
proof (state)
this:
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)
[PROOF STEP]
have "conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
by (metis conjugation_is_size_invariant)
[PROOF STATE]
proof (state)
this:
conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>S. \<lbrakk>H \<subseteq> S; S \<in> subgroups_of_size (p ^ a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)
conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)
conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding conjugation_action_def
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
H \<subseteq> g <# (P #> inv g)
(\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) g P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto dest:that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem sylow_conjugate:
  assumes P:"P \<in> subgroups_of_size (p ^ a)"
  assumes Q:"Q \<in> subgroups_of_size (p ^ a)"
  obtains g where "g \<in> carrier G" "Q = g <# (P #> inv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from P
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have "card P = p ^ a"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. card P = p ^ a
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
P \<in> {H. subgroup H G \<and> card H = p ^ a}

goal (1 subgoal):
 1. card P = p ^ a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card P = p ^ a

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from Q
[PROOF STATE]
proof (chain)
picking this:
Q \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have Qcard:"card Q = p ^ a"
[PROOF STATE]
proof (prove)
using this:
Q \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. card Q = p ^ a
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
Q \<in> {H. subgroup H G \<and> card H = p ^ a}

goal (1 subgoal):
 1. card Q = p ^ a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card Q = p ^ a

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from Q P
[PROOF STATE]
proof (chain)
picking this:
Q \<in> subgroups_of_size (p ^ a)
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
obtain g where g:"g \<in> carrier G" "Q \<subseteq> g <# (P #> inv g)"
[PROOF STATE]
proof (prove)
using this:
Q \<in> subgroups_of_size (p ^ a)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q \<subseteq> g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule ex_conj_sylow_group)
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with P finite_G
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
finite (carrier G)
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
[PROOF STEP]
have "conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)
finite (carrier G)
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)

goal (1 subgoal):
 1. conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
by (metis conjugation_is_size_invariant)
[PROOF STATE]
proof (state)
this:
conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from g P
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have "conjugation_action (p ^ a) g P = g <# (P #> inv g)"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. conjugation_action (p ^ a) g P = g <# (P #> inv g)
[PROOF STEP]
unfolding conjugation_action_def
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) g P = g <# (P #> inv g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
conjugation_action (p ^ a) g P = g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)
conjugation_action (p ^ a) g P = g <# (P #> inv g)
[PROOF STEP]
have conjSize:"g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
conjugation_action (p ^ a) g P \<in> subgroups_of_size (p ^ a)
conjugation_action (p ^ a) g P = g <# (P #> inv g)

goal (1 subgoal):
 1. g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding conjugation_action_def
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
(\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) g P \<in> subgroups_of_size (p ^ a)
(\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) g P = g <# (P #> inv g)

goal (1 subgoal):
 1. g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with Qcard
[PROOF STATE]
proof (chain)
picking this:
card Q = p ^ a
g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have  card:"card (g <# (P #> inv g)) = card Q"
[PROOF STATE]
proof (prove)
using this:
card Q = p ^ a
g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. card (g <# (P #> inv g)) = card Q
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
card Q = p ^ a
g <# (P #> inv g) \<in> {H. subgroup H G \<and> card H = p ^ a}

goal (1 subgoal):
 1. card (g <# (P #> inv g)) = card Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (g <# (P #> inv g)) = card Q

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from conjSize finite_G
[PROOF STATE]
proof (chain)
picking this:
g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)
finite (carrier G)
[PROOF STEP]
have "finite (g <# (P #> inv g))"
[PROOF STATE]
proof (prove)
using this:
g <# (P #> inv g) \<in> subgroups_of_size (p ^ a)
finite (carrier G)

goal (1 subgoal):
 1. finite (g <# (P #> inv g))
[PROOF STEP]
by (metis (mono_tags) finite_subset mem_Collect_eq subgroup.subset subgroups_of_size_def)
[PROOF STATE]
proof (state)
this:
finite (g <# (P #> inv g))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with g card
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
card (g <# (P #> inv g)) = card Q
finite (g <# (P #> inv g))
[PROOF STEP]
have "Q = g <# (P #> inv g)"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
card (g <# (P #> inv g)) = card Q
finite (g <# (P #> inv g))

goal (1 subgoal):
 1. Q = g <# (P #> inv g)
[PROOF STEP]
by (metis card_subset_eq)
[PROOF STATE]
proof (state)
this:
Q = g <# (P #> inv g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with g
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
Q = g <# (P #> inv g)
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
Q \<subseteq> g <# (P #> inv g)
Q = g <# (P #> inv g)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem num_eq_card_orbit:
  assumes P:"P \<in> subgroups_of_size (p ^ a)"
  shows "subgroups_of_size (p ^ a) = group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroups_of_size (p ^ a) = group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P
[PROOF STEP]
proof(auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> subgroups_of_size (p ^ a) \<Longrightarrow> x \<in> group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P
 2. \<And>x. x \<in> group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
from finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
[PROOF STEP]
interpret conj: group_action G "(conjugation_action (p ^ a))" "(subgroups_of_size (p ^ a))"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. group_action G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a))
[PROOF STEP]
by (rule acts_on_subsets)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> subgroups_of_size (p ^ a) \<Longrightarrow> x \<in> conj.orbit P
 2. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have "group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P = group_action.same_orbit_rel G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) `` {P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conj.orbit P = conj.same_orbit_rel `` {P}
[PROOF STEP]
by (rule conj.orbit_def)
[PROOF STATE]
proof (state)
this:
conj.orbit P = conj.same_orbit_rel `` {P}

goal (2 subgoals):
 1. \<And>x. x \<in> subgroups_of_size (p ^ a) \<Longrightarrow> x \<in> conj.orbit P
 2. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
fix Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> subgroups_of_size (p ^ a) \<Longrightarrow> x \<in> conj.orbit P
 2. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> subgroups_of_size (p ^ a) \<Longrightarrow> x \<in> conj.orbit P
 2. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
assume Q:"Q \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (state)
this:
Q \<in> subgroups_of_size (p ^ a)

goal (2 subgoals):
 1. \<And>x. x \<in> subgroups_of_size (p ^ a) \<Longrightarrow> x \<in> conj.orbit P
 2. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
from P Q
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
Q \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
obtain g where g:"g \<in> carrier G" "Q = g <# (P #> inv g) "
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)
Q \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = g <# (P #> inv g)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule sylow_conjugate)
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
Q = g <# (P #> inv g)

goal (2 subgoals):
 1. \<And>x. x \<in> subgroups_of_size (p ^ a) \<Longrightarrow> x \<in> conj.orbit P
 2. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
with P conj.orbit_char
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
?m \<in> subgroups_of_size (p ^ a) \<Longrightarrow> conj.orbit ?m = {n. \<exists>g. g \<in> carrier G \<and> conjugation_action (p ^ a) g ?m = n}
g \<in> carrier G
Q = g <# (P #> inv g)
[PROOF STEP]
show "Q \<in> group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)
?m \<in> subgroups_of_size (p ^ a) \<Longrightarrow> conj.orbit ?m = {n. \<exists>g. g \<in> carrier G \<and> conjugation_action (p ^ a) g ?m = n}
g \<in> carrier G
Q = g <# (P #> inv g)

goal (1 subgoal):
 1. Q \<in> conj.orbit P
[PROOF STEP]
unfolding conjugation_action_def
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)
?m \<in> subgroups_of_size (p ^ a) \<Longrightarrow> group_action.orbit G (\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) (subgroups_of_size (p ^ a)) ?m = {n. \<exists>g. g \<in> carrier G \<and> (\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) g ?m = n}
g \<in> carrier G
Q = g <# (P #> inv g)

goal (1 subgoal):
 1. Q \<in> group_action.orbit G (\<lambda>g\<in>carrier G. \<lambda>P\<in>subgroups_of_size (p ^ a). g <# (P #> inv g)) (subgroups_of_size (p ^ a)) P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<in> conj.orbit P

goal (1 subgoal):
 1. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Q \<in> subgroups_of_size (p ^ a) \<Longrightarrow> Q \<in> conj.orbit P

goal (1 subgoal):
 1. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Q \<in> subgroups_of_size (p ^ a) \<Longrightarrow> Q \<in> conj.orbit P

goal (1 subgoal):
 1. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
assume "Q \<in> group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P"
[PROOF STATE]
proof (state)
this:
Q \<in> conj.orbit P

goal (1 subgoal):
 1. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
with P conj.orbit_char
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
?m \<in> subgroups_of_size (p ^ a) \<Longrightarrow> conj.orbit ?m = {n. \<exists>g. g \<in> carrier G \<and> conjugation_action (p ^ a) g ?m = n}
Q \<in> conj.orbit P
[PROOF STEP]
obtain g where g:"g \<in> carrier G" "Q = conjugation_action (p ^ a) g P"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)
?m \<in> subgroups_of_size (p ^ a) \<Longrightarrow> conj.orbit ?m = {n. \<exists>g. g \<in> carrier G \<and> conjugation_action (p ^ a) g ?m = n}
Q \<in> conj.orbit P

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; Q = conjugation_action (p ^ a) g P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
Q = conjugation_action (p ^ a) g P

goal (1 subgoal):
 1. \<And>x. x \<in> conj.orbit P \<Longrightarrow> x \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
with finite_G P
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
Q = conjugation_action (p ^ a) g P
[PROOF STEP]
show "Q \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
g \<in> carrier G
Q = conjugation_action (p ^ a) g P

goal (1 subgoal):
 1. Q \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
by (metis conjugation_is_size_invariant)
[PROOF STATE]
proof (state)
this:
Q \<in> subgroups_of_size (p ^ a)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Q \<in> conj.orbit P \<Longrightarrow> Q \<in> subgroups_of_size (p ^ a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem num_sylow_normalizer:
  assumes Psize:"P \<in> subgroups_of_size (p ^ a)"
  shows "card (rcosets\<^bsub>G\<lparr>carrier := group_action.stabilizer G (conjugation_action (p ^ a)) P\<rparr>\<^esub> P) * p ^ a = card (group_action.stabilizer G (conjugation_action (p ^ a)) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := group_action.stabilizer G (conjugation_action (p ^ a)) P\<rparr>\<^esub> P) * p ^ a = card (group_action.stabilizer G (conjugation_action (p ^ a)) P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := group_action.stabilizer G (conjugation_action (p ^ a)) P\<rparr>\<^esub> P) * p ^ a = card (group_action.stabilizer G (conjugation_action (p ^ a)) P)
[PROOF STEP]
from finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
[PROOF STEP]
interpret conj: group_action G "(conjugation_action (p ^ a))" "(subgroups_of_size (p ^ a))"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. group_action G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a))
[PROOF STEP]
by (rule acts_on_subsets)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
from Psize
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have PG:"subgroup P G" and cardP:"card P = p ^ a"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. subgroup P G &&& card P = p ^ a
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
P \<in> {H. subgroup H G \<and> card H = p ^ a}

goal (1 subgoal):
 1. subgroup P G &&& card P = p ^ a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
with finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
subgroup P G
card P = p ^ a
[PROOF STEP]
have "order G = card (conj.orbit P) * card (conj.stabilizer P)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. order G = card (conj.orbit P) * card (conj.stabilizer P)
[PROOF STEP]
by (metis Psize acts_on_subsets group_action.orbit_size)
[PROOF STATE]
proof (state)
this:
order G = card (conj.orbit P) * card (conj.stabilizer P)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
with order_G Psize
[PROOF STATE]
proof (chain)
picking this:
order G = p ^ a * m
P \<in> subgroups_of_size (p ^ a)
order G = card (conj.orbit P) * card (conj.stabilizer P)
[PROOF STEP]
have "p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)"
[PROOF STATE]
proof (prove)
using this:
order G = p ^ a * m
P \<in> subgroups_of_size (p ^ a)
order G = card (conj.orbit P) * card (conj.stabilizer P)

goal (1 subgoal):
 1. p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)
[PROOF STEP]
by (metis num_eq_card_orbit)
[PROOF STATE]
proof (state)
this:
p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
from Psize
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
interpret stabGroup: group "G\<lparr>carrier := conj.stabilizer P\<rparr>"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. Group.group (G\<lparr>carrier := conj.stabilizer P\<rparr>)
[PROOF STEP]
by (metis conj.stabilizer_is_subgroup subgroup_imp_group)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
from finite_G Psize
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have PStab:"subgroup P (G\<lparr>carrier := conj.stabilizer P\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. subgroup P (G\<lparr>carrier := conj.stabilizer P\<rparr>)
[PROOF STEP]
by (rule stabilizer_supergrp_P)
[PROOF STATE]
proof (state)
this:
subgroup P (G\<lparr>carrier := conj.stabilizer P\<rparr>)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
from finite_G Psize
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have "finite (conj.stabilizer P)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. finite (conj.stabilizer P)
[PROOF STEP]
by (metis card.infinite conj.stabilizer_is_subgroup less_nat_zero_code subgroup.finite_imp_card_positive)
[PROOF STATE]
proof (state)
this:
finite (conj.stabilizer P)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
with finite_G PStab stabGroup.lagrange
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
subgroup P (G\<lparr>carrier := conj.stabilizer P\<rparr>)
subgroup ?H (G\<lparr>carrier := conj.stabilizer P\<rparr>) \<Longrightarrow> card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> ?H) * card ?H = order (G\<lparr>carrier := conj.stabilizer P\<rparr>)
finite (conj.stabilizer P)
[PROOF STEP]
have "card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * card P = order (G\<lparr>carrier := conj.stabilizer P\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup P (G\<lparr>carrier := conj.stabilizer P\<rparr>)
subgroup ?H (G\<lparr>carrier := conj.stabilizer P\<rparr>) \<Longrightarrow> card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> ?H) * card ?H = order (G\<lparr>carrier := conj.stabilizer P\<rparr>)
finite (conj.stabilizer P)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * card P = order (G\<lparr>carrier := conj.stabilizer P\<rparr>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * card P = order (G\<lparr>carrier := conj.stabilizer P\<rparr>)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
with cardP
[PROOF STATE]
proof (chain)
picking this:
card P = p ^ a
card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * card P = order (G\<lparr>carrier := conj.stabilizer P\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a
card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * card P = order (G\<lparr>carrier := conj.stabilizer P\<rparr>)

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a
card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * card P = card (carrier (G\<lparr>carrier := conj.stabilizer P\<rparr>))

goal (1 subgoal):
 1. card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P) * p ^ a = card (conj.stabilizer P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in snd_sylow) num_sylow_dvd_remainder:
  shows "card (subgroups_of_size (p ^ a)) dvd m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
from finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
[PROOF STEP]
interpret conj: group_action G "(conjugation_action (p ^ a))" "(subgroups_of_size (p ^ a))"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. group_action G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a))
[PROOF STEP]
by (rule acts_on_subsets)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>subgroup P G; card P = p ^ a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis sylow_thm)
[PROOF STATE]
proof (state)
this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
hence Psize:"P \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> {H. subgroup H G \<and> card H = p ^ a}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
with finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
have "order G = card (conj.orbit P) * card (conj.stabilizer P)"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. order G = card (conj.orbit P) * card (conj.stabilizer P)
[PROOF STEP]
by (metis Psize acts_on_subsets group_action.orbit_size)
[PROOF STATE]
proof (state)
this:
order G = card (conj.orbit P) * card (conj.stabilizer P)

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
with order_G Psize
[PROOF STATE]
proof (chain)
picking this:
order G = p ^ a * m
P \<in> subgroups_of_size (p ^ a)
order G = card (conj.orbit P) * card (conj.stabilizer P)
[PROOF STEP]
have orderEq:"p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)"
[PROOF STATE]
proof (prove)
using this:
order G = p ^ a * m
P \<in> subgroups_of_size (p ^ a)
order G = card (conj.orbit P) * card (conj.stabilizer P)

goal (1 subgoal):
 1. p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)
[PROOF STEP]
by (metis num_eq_card_orbit)
[PROOF STATE]
proof (state)
this:
p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
define k where "k = card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P)"
[PROOF STATE]
proof (state)
this:
k = card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P)

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
with Psize
[PROOF STATE]
proof (chain)
picking this:
P \<in> subgroups_of_size (p ^ a)
k = card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P)
[PROOF STEP]
have "k * p ^ a = card (conj.stabilizer P)"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)
k = card (rcosets\<^bsub>G\<lparr>carrier := conj.stabilizer P\<rparr>\<^esub> P)

goal (1 subgoal):
 1. k * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
by (metis num_sylow_normalizer)
[PROOF STATE]
proof (state)
this:
k * p ^ a = card (conj.stabilizer P)

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
with orderEq
[PROOF STATE]
proof (chain)
picking this:
p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)
k * p ^ a = card (conj.stabilizer P)
[PROOF STEP]
have "p ^ a * m = card (subgroups_of_size (p ^ a)) * p ^ a * k"
[PROOF STATE]
proof (prove)
using this:
p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)
k * p ^ a = card (conj.stabilizer P)

goal (1 subgoal):
 1. p ^ a * m = card (subgroups_of_size (p ^ a)) * p ^ a * k
[PROOF STEP]
by (auto simp:mult.assoc mult.commute)
[PROOF STATE]
proof (state)
this:
p ^ a * m = card (subgroups_of_size (p ^ a)) * p ^ a * k

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
hence "p ^ a * m = p ^ a * card (subgroups_of_size (p ^ a)) * k"
[PROOF STATE]
proof (prove)
using this:
p ^ a * m = card (subgroups_of_size (p ^ a)) * p ^ a * k

goal (1 subgoal):
 1. p ^ a * m = p ^ a * card (subgroups_of_size (p ^ a)) * k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p ^ a * m = p ^ a * card (subgroups_of_size (p ^ a)) * k

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p ^ a * m = p ^ a * card (subgroups_of_size (p ^ a)) * k
[PROOF STEP]
have "m = card (subgroups_of_size (p ^ a)) * k"
[PROOF STATE]
proof (prove)
using this:
p ^ a * m = p ^ a * card (subgroups_of_size (p ^ a)) * k

goal (1 subgoal):
 1. m = card (subgroups_of_size (p ^ a)) * k
[PROOF STEP]
using pa_not_zero
[PROOF STATE]
proof (prove)
using this:
p ^ a * m = p ^ a * card (subgroups_of_size (p ^ a)) * k
p ^ a \<noteq> 0

goal (1 subgoal):
 1. m = card (subgroups_of_size (p ^ a)) * k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = card (subgroups_of_size (p ^ a)) * k

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = card (subgroups_of_size (p ^ a)) * k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m = card (subgroups_of_size (p ^ a)) * k

goal (1 subgoal):
 1. card (subgroups_of_size (p ^ a)) dvd m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
card (subgroups_of_size (p ^ a)) dvd m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in snd_sylow) restrict_locale:
  assumes subgrp:"subgroup P G"
  assumes card:"p ^ a dvd card P"
  shows "snd_sylow (G\<lparr>carrier := P\<rparr>) p a ((card P) div (p ^ a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
from subgrp
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
[PROOF STEP]
interpret groupP: group "G\<lparr>carrier := P\<rparr>"
[PROOF STATE]
proof (prove)
using this:
subgroup P G

goal (1 subgoal):
 1. Group.group (G\<lparr>carrier := P\<rparr>)
[PROOF STEP]
by (metis subgroup_imp_group)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
define k where "k = (card P) div (p ^ a)"
[PROOF STATE]
proof (state)
this:
k = card P div p ^ a

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
with card
[PROOF STATE]
proof (chain)
picking this:
p ^ a dvd card P
k = card P div p ^ a
[PROOF STEP]
have cardP:"card P = p ^ a * k"
[PROOF STATE]
proof (prove)
using this:
p ^ a dvd card P
k = card P div p ^ a

goal (1 subgoal):
 1. card P = p ^ a * k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card P = p ^ a * k

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
hence orderP:"order (G\<lparr>carrier := P\<rparr>) = p ^ a * k"
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a * k

goal (1 subgoal):
 1. order (G\<lparr>carrier := P\<rparr>) = p ^ a * k
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a * k

goal (1 subgoal):
 1. card (carrier (G\<lparr>carrier := P\<rparr>)) = p ^ a * k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
order (G\<lparr>carrier := P\<rparr>) = p ^ a * k

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
from cardP subgrp order_G
[PROOF STATE]
proof (chain)
picking this:
card P = p ^ a * k
subgroup P G
order G = p ^ a * m
[PROOF STEP]
have "p ^ a * k dvd p ^ a * m"
[PROOF STATE]
proof (prove)
using this:
card P = p ^ a * k
subgroup P G
order G = p ^ a * m

goal (1 subgoal):
 1. p ^ a * k dvd p ^ a * m
[PROOF STEP]
by (metis card_subgrp_dvd)
[PROOF STATE]
proof (state)
this:
p ^ a * k dvd p ^ a * m

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
hence "k dvd m"
[PROOF STATE]
proof (prove)
using this:
p ^ a * k dvd p ^ a * m

goal (1 subgoal):
 1. k dvd m
[PROOF STEP]
by (metis nat_mult_dvd_cancel_disj pa_not_zero)
[PROOF STATE]
proof (state)
this:
k dvd m

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
with pNotDvdm
[PROOF STATE]
proof (chain)
picking this:
\<not> p dvd m
k dvd m
[PROOF STEP]
have ndvd:"\<not> p dvd k"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd m
k dvd m

goal (1 subgoal):
 1. \<not> p dvd k
[PROOF STEP]
by (blast intro: dvd_trans)
[PROOF STATE]
proof (state)
this:
\<not> p dvd k

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
define PcalM where "PcalM = {s. s \<subseteq> carrier (G\<lparr>carrier := P\<rparr>) \<and> card s = p ^ a}"
[PROOF STATE]
proof (state)
this:
PcalM = {s. s \<subseteq> carrier (G\<lparr>carrier := P\<rparr>) \<and> card s = p ^ a}

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
define PRelM where "PRelM = {(N1, N2). N1 \<in> PcalM \<and> N2 \<in> PcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := P\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := P\<rparr>\<^esub> g)}"
[PROOF STATE]
proof (state)
this:
PRelM = {(N1, N2). N1 \<in> PcalM \<and> N2 \<in> PcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := P\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := P\<rparr>\<^esub> g)}

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
from subgrp finite_G
[PROOF STATE]
proof (chain)
picking this:
subgroup P G
finite (carrier G)
[PROOF STEP]
have finite_groupP:"finite (carrier (G\<lparr>carrier := P\<rparr>))"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
finite (carrier G)

goal (1 subgoal):
 1. finite (carrier (G\<lparr>carrier := P\<rparr>))
[PROOF STEP]
by (auto simp:subgroup_finite)
[PROOF STATE]
proof (state)
this:
finite (carrier (G\<lparr>carrier := P\<rparr>))

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
interpret Nsylow: snd_sylow "G\<lparr>carrier := P\<rparr>" p a k PcalM PRelM
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a k &&& (PcalM \<equiv> {s. s \<subseteq> carrier (G\<lparr>carrier := P\<rparr>) \<and> card s = p ^ a}) &&& PRelM \<equiv> {(N1, N2). N1 \<in> PcalM \<and> N2 \<in> PcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := P\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := P\<rparr>\<^esub> g)}
[PROOF STEP]
unfolding snd_sylow_def snd_sylow_axioms_def sylow_def sylow_axioms_def k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Group.group (G\<lparr>carrier := P\<rparr>) \<and> prime p \<and> order (G\<lparr>carrier := P\<rparr>) = p ^ a * (card P div p ^ a) \<and> finite (carrier (G\<lparr>carrier := P\<rparr>))) \<and> \<not> p dvd card P div p ^ a &&& (PcalM \<equiv> {s. s \<subseteq> carrier (G\<lparr>carrier := P\<rparr>) \<and> card s = p ^ a}) &&& PRelM \<equiv> {(N1, N2). N1 \<in> PcalM \<and> N2 \<in> PcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := P\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := P\<rparr>\<^esub> g)}
[PROOF STEP]
using groupP.is_group prime_p orderP finite_groupP ndvd PcalM_def PRelM_def k_def
[PROOF STATE]
proof (prove)
using this:
Group.group (G\<lparr>carrier := P\<rparr>)
prime p
order (G\<lparr>carrier := P\<rparr>) = p ^ a * k
finite (carrier (G\<lparr>carrier := P\<rparr>))
\<not> p dvd k
PcalM = {s. s \<subseteq> carrier (G\<lparr>carrier := P\<rparr>) \<and> card s = p ^ a}
PRelM = {(N1, N2). N1 \<in> PcalM \<and> N2 \<in> PcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := P\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := P\<rparr>\<^esub> g)}
k = card P div p ^ a

goal (1 subgoal):
 1. (Group.group (G\<lparr>carrier := P\<rparr>) \<and> prime p \<and> order (G\<lparr>carrier := P\<rparr>) = p ^ a * (card P div p ^ a) \<and> finite (carrier (G\<lparr>carrier := P\<rparr>))) \<and> \<not> p dvd card P div p ^ a &&& (PcalM \<equiv> {s. s \<subseteq> carrier (G\<lparr>carrier := P\<rparr>) \<and> card s = p ^ a}) &&& PRelM \<equiv> {(N1, N2). N1 \<in> PcalM \<and> N2 \<in> PcalM \<and> (\<exists>g\<in>carrier (G\<lparr>carrier := P\<rparr>). N1 = N2 #>\<^bsub>G\<lparr>carrier := P\<rparr>\<^esub> g)}
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
using k_def
[PROOF STATE]
proof (prove)
using this:
k = card P div p ^ a

goal (1 subgoal):
 1. snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)
[PROOF STEP]
by (metis Nsylow.is_snd_sylow)
[PROOF STATE]
proof (state)
this:
snd_sylow (G\<lparr>carrier := P\<rparr>) p a (card P div p ^ a)

goal:
No subgoals!
[PROOF STEP]
qed