[STATEMENT]
lemma (in normal) surj_hom_normal_subgroup:
  assumes \<phi>:"group_hom G F \<phi>"
  assumes \<phi>surj:"\<phi> ` (carrier G) = carrier F"
  shows "(\<phi> ` H) \<lhd> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
proof (rule group.normalI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Group.group F
 2. subgroup (\<phi> ` H) F
 3. \<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
from \<phi>
[PROOF STATE]
proof (chain)
picking this:
group_hom G F \<phi>
[PROOF STEP]
show "group F"
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>

goal (1 subgoal):
 1. Group.group F
[PROOF STEP]
unfolding group_hom_def group_hom_axioms_def
[PROOF STATE]
proof (prove)
using this:
Group.group G \<and> Group.group F \<and> \<phi> \<in> hom G F

goal (1 subgoal):
 1. Group.group F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Group.group F

goal (2 subgoals):
 1. subgroup (\<phi> ` H) F
 2. \<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subgroup (\<phi> ` H) F
 2. \<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
from \<phi> \<phi>surj
[PROOF STATE]
proof (chain)
picking this:
group_hom G F \<phi>
\<phi> ` carrier G = carrier F
[PROOF STEP]
show "subgroup (\<phi> ` H) F"
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>
\<phi> ` carrier G = carrier F

goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
by (rule surj_hom_subgroup)
[PROOF STATE]
proof (state)
this:
subgroup (\<phi> ` H) F

goal (1 subgoal):
 1. \<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
show "\<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
assume f:"f \<in> carrier F"
[PROOF STATE]
proof (state)
this:
f \<in> carrier F

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
with \<phi>surj
[PROOF STATE]
proof (chain)
picking this:
\<phi> ` carrier G = carrier F
f \<in> carrier F
[PROOF STEP]
obtain g where g:"g \<in> carrier G" "f = \<phi> g"
[PROOF STATE]
proof (prove)
using this:
\<phi> ` carrier G = carrier F
f \<in> carrier F

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

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
hence "\<phi> ` H #>\<^bsub>F\<^esub> f = \<phi> ` H #>\<^bsub>F\<^esub> \<phi> g"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
f = \<phi> g

goal (1 subgoal):
 1. \<phi> ` H #>\<^bsub>F\<^esub> f = \<phi> ` H #>\<^bsub>F\<^esub> \<phi> g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> ` H #>\<^bsub>F\<^esub> f = \<phi> ` H #>\<^bsub>F\<^esub> \<phi> g

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> ` H #>\<^bsub>F\<^esub> f = \<phi> ` H #>\<^bsub>F\<^esub> \<phi> g

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = (\<lambda>x. (\<phi> x) \<otimes>\<^bsub>F\<^esub> (\<phi> g)) ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` H #>\<^bsub>F\<^esub> \<phi> g = (\<lambda>x. \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g) ` H
[PROOF STEP]
unfolding r_coset_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {y. \<exists>x\<in>{y. \<exists>x\<in>H. y = \<phi> x}. y = {x \<otimes>\<^bsub>F\<^esub> \<phi> g}} = {y. \<exists>x\<in>H. y = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> ` H #>\<^bsub>F\<^esub> \<phi> g = (\<lambda>x. \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> ` H #>\<^bsub>F\<^esub> \<phi> g = (\<lambda>x. \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = (\<lambda>x. \<phi> (x \<otimes> g)) ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g) ` H = (\<lambda>x. \<phi> (x \<otimes> g)) ` H
[PROOF STEP]
using subset g \<phi> group_hom.hom_mult
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
g \<in> carrier G
f = \<phi> g
group_hom G F \<phi>
\<lbrakk>group_hom ?G ?H ?h; ?x \<in> carrier ?G; ?y \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?h (?x \<otimes>\<^bsub>?G\<^esub> ?y) = ?h ?x \<otimes>\<^bsub>?H\<^esub> ?h ?y

goal (1 subgoal):
 1. (\<lambda>x. \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g) ` H = (\<lambda>x. \<phi> (x \<otimes> g)) ` H
[PROOF STEP]
unfolding image_def
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
g \<in> carrier G
f = \<phi> g
group_hom G F \<phi>
\<lbrakk>group_hom ?G ?H ?h; ?x \<in> carrier ?G; ?y \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?h (?x \<otimes>\<^bsub>?G\<^esub> ?y) = ?h ?x \<otimes>\<^bsub>?H\<^esub> ?h ?y

goal (1 subgoal):
 1. {y. \<exists>x\<in>H. y = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g} = {y. \<exists>x\<in>H. y = \<phi> (x \<otimes> g)}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g) ` H = (\<lambda>x. \<phi> (x \<otimes> g)) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> g) ` H = (\<lambda>x. \<phi> (x \<otimes> g)) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = \<phi> ` (H #> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<phi> (x \<otimes> g)) ` H = \<phi> ` (H #> g)
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>

goal (1 subgoal):
 1. (\<lambda>x. \<phi> (x \<otimes> g)) ` H = \<phi> ` (H #> g)
[PROOF STEP]
unfolding r_coset_def
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>

goal (1 subgoal):
 1. (\<lambda>x. \<phi> (x \<otimes> g)) ` H = \<phi> ` (\<Union>h\<in>H. {h \<otimes> g})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> (x \<otimes> g)) ` H = \<phi> ` (H #> g)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> (x \<otimes> g)) ` H = \<phi> ` (H #> g)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = \<phi> ` (g <# H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` (H #> g) = \<phi> ` (g <# H)
[PROOF STEP]
by (metis coset_eq g(1))
[PROOF STATE]
proof (state)
this:
\<phi> ` (H #> g) = \<phi> ` (g <# H)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> ` (H #> g) = \<phi> ` (g <# H)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = (\<lambda>x. \<phi> (g \<otimes> x)) ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` (g <# H) = (\<lambda>x. \<phi> (g \<otimes> x)) ` H
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>

goal (1 subgoal):
 1. \<phi> ` (g <# H) = (\<lambda>x. \<phi> (g \<otimes> x)) ` H
[PROOF STEP]
unfolding l_coset_def
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>

goal (1 subgoal):
 1. \<phi> ` (\<Union>h\<in>H. {g \<otimes> h}) = (\<lambda>x. \<phi> (g \<otimes> x)) ` H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> ` (g <# H) = (\<lambda>x. \<phi> (g \<otimes> x)) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<phi> ` (g <# H) = (\<lambda>x. \<phi> (g \<otimes> x)) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = (\<lambda>x. (\<phi> g) \<otimes>\<^bsub>F\<^esub> (\<phi> x)) ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<phi> (g \<otimes> x)) ` H = (\<lambda>x. \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x) ` H
[PROOF STEP]
using subset g \<phi> group_hom.hom_mult
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G
g \<in> carrier G
f = \<phi> g
group_hom G F \<phi>
\<lbrakk>group_hom ?G ?H ?h; ?x \<in> carrier ?G; ?y \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?h (?x \<otimes>\<^bsub>?G\<^esub> ?y) = ?h ?x \<otimes>\<^bsub>?H\<^esub> ?h ?y

goal (1 subgoal):
 1. (\<lambda>x. \<phi> (g \<otimes> x)) ` H = (\<lambda>x. \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x) ` H
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> (g \<otimes> x)) ` H = (\<lambda>x. \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> (g \<otimes> x)) ` H = (\<lambda>x. \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x) ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x) ` H = \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
unfolding l_coset_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. \<exists>x\<in>H. y = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x} = \<Union> {y. \<exists>x\<in>{y. \<exists>x\<in>H. y = \<phi> x}. y = {\<phi> g \<otimes>\<^bsub>F\<^esub> x}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x) ` H = \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> x) ` H = \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
have "... = f <#\<^bsub>F\<^esub> \<phi> ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H = f <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
f = \<phi> g

goal (1 subgoal):
 1. \<phi> g <#\<^bsub>F\<^esub> \<phi> ` H = f <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> g <#\<^bsub>F\<^esub> \<phi> ` H = f <#\<^bsub>F\<^esub> \<phi> ` H

goal (1 subgoal):
 1. \<And>x. x \<in> carrier F \<Longrightarrow> \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<phi> ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
show "\<phi> ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \<phi> ` H"
[PROOF STATE]
proof (prove)
using this:
\<phi> ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \<phi> ` H

goal (1 subgoal):
 1. \<phi> ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \<phi> ` H
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<phi> ` H #>\<^bsub>F\<^esub> f = f <#\<^bsub>F\<^esub> \<phi> ` H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>carrier F. \<phi> ` H #>\<^bsub>F\<^esub> x = x <#\<^bsub>F\<^esub> \<phi> ` H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_normal_subgroup:
  assumes groups:"group G" "group F"
  assumes HG:"H \<lhd> G"
  assumes \<phi>:"\<phi> \<in> iso G F"
  shows "(\<phi> ` H) \<lhd> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
from groups \<phi>
[PROOF STATE]
proof (chain)
picking this:
Group.group G
Group.group F
\<phi> \<in> Group.iso G F
[PROOF STEP]
have "group_hom G F \<phi>"
[PROOF STATE]
proof (prove)
using this:
Group.group G
Group.group F
\<phi> \<in> Group.iso G F

goal (1 subgoal):
 1. group_hom G F \<phi>
[PROOF STEP]
unfolding group_hom_def group_hom_axioms_def iso_def
[PROOF STATE]
proof (prove)
using this:
Group.group G
Group.group F
\<phi> \<in> {h \<in> hom G F. bij_betw h (carrier G) (carrier F)}

goal (1 subgoal):
 1. Group.group G \<and> Group.group F \<and> \<phi> \<in> hom G F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
group_hom G F \<phi>

goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
group_hom G F \<phi>

goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
from \<phi>
[PROOF STATE]
proof (chain)
picking this:
\<phi> \<in> Group.iso G F
[PROOF STEP]
have "\<phi> ` (carrier G) = carrier F"
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> Group.iso G F

goal (1 subgoal):
 1. \<phi> ` carrier G = carrier F
[PROOF STEP]
unfolding iso_def bij_betw_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> {h \<in> hom G F. inj_on h (carrier G) \<and> h ` carrier G = carrier F}

goal (1 subgoal):
 1. \<phi> ` carrier G = carrier F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> ` carrier G = carrier F

goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> ` carrier G = carrier F

goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
note HG
[PROOF STATE]
proof (state)
this:
H \<lhd> G

goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
group_hom G F \<phi>
\<phi> ` carrier G = carrier F
H \<lhd> G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>
\<phi> ` carrier G = carrier F
H \<lhd> G

goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
using normal.surj_hom_normal_subgroup
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>
\<phi> ` carrier G = carrier F
H \<lhd> G
\<lbrakk>?H \<lhd> ?G; group_hom ?G ?F ?\<phi>; ?\<phi> ` carrier ?G = carrier ?F\<rbrakk> \<Longrightarrow> ?\<phi> ` ?H \<lhd> ?F

goal (1 subgoal):
 1. \<phi> ` H \<lhd> F
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<phi> ` H \<lhd> F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) triv_subgroup:
  shows "subgroup {\<one>} G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup {\<one>} G
[PROOF STEP]
unfolding subgroup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({\<one>} \<subseteq> carrier G \<and> (\<forall>x y. x \<in> {\<one>} \<longrightarrow> y \<in> {\<one>} \<longrightarrow> x \<otimes> y \<in> {\<one>})) \<and> \<one> \<in> {\<one>} \<and> (\<forall>x. x \<in> {\<one>} \<longrightarrow> inv x \<in> {\<one>})
[PROOF STEP]
by auto


[STATEMENT]
lemma (in group) card_rcosets_triv:
  assumes "finite (carrier G)"
  shows "card (rcosets {\<one>}) = order G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (rcosets {\<one>}) = order G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (rcosets {\<one>}) = order G
[PROOF STEP]
have "subgroup {\<one>} G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup {\<one>} G
[PROOF STEP]
by (rule triv_subgroup)
[PROOF STATE]
proof (state)
this:
subgroup {\<one>} G

goal (1 subgoal):
 1. card (rcosets {\<one>}) = order G
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
subgroup {\<one>} G
[PROOF STEP]
have "card (rcosets {\<one>}) * card {\<one>} = order G"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup {\<one>} G

goal (1 subgoal):
 1. card (rcosets {\<one>}) * card {\<one>} = order G
[PROOF STEP]
using lagrange
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup {\<one>} G
subgroup ?H G \<Longrightarrow> card (rcosets ?H) * card ?H = order G

goal (1 subgoal):
 1. card (rcosets {\<one>}) * card {\<one>} = order G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (rcosets {\<one>}) * card {\<one>} = order G

goal (1 subgoal):
 1. card (rcosets {\<one>}) = order G
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
card (rcosets {\<one>}) * card {\<one>} = order G

goal (1 subgoal):
 1. card (rcosets {\<one>}) = order G
[PROOF STEP]
by (auto simp:card_Suc_eq)
[PROOF STATE]
proof (state)
this:
card (rcosets {\<one>}) = order G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) normal_subgroup_intersect:
  assumes "M \<lhd> G" and "N \<lhd> G"
  shows "M \<inter> N \<lhd> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<inter> N \<lhd> G
[PROOF STEP]
using assms subgroup_intersect is_group normal_inv_iff
[PROOF STATE]
proof (prove)
using this:
M \<lhd> G
N \<lhd> G
\<lbrakk>subgroup ?H G; subgroup ?H' G\<rbrakk> \<Longrightarrow> subgroup (?H \<inter> ?H') G
Group.group G
?N \<lhd> G = (subgroup ?N G \<and> (\<forall>x\<in>carrier G. \<forall>h\<in>?N. x \<otimes> h \<otimes> inv x \<in> ?N))

goal (1 subgoal):
 1. M \<inter> N \<lhd> G
[PROOF STEP]
by simp


[STATEMENT]
lemma (in group) setmult_lcos_assoc:
     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
      \<Longrightarrow> (x <# H) <#> K = x <# (H <#> K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> x <# H <#> K = x <# (H <#> K)
[PROOF STEP]
by (force simp add: l_coset_def set_mult_def m_assoc)


[STATEMENT]
lemma (in group) normal_subgroup_set_mult_closed:
  assumes "M \<lhd> G" and "N \<lhd> G"
  shows "M <#> N \<lhd> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M <#> N \<lhd> G
[PROOF STEP]
proof (rule normalI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subgroup (M <#> N) G
 2. \<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
M \<lhd> G
N \<lhd> G
[PROOF STEP]
show "subgroup (M <#> N) G"
[PROOF STATE]
proof (prove)
using this:
M \<lhd> G
N \<lhd> G

goal (1 subgoal):
 1. subgroup (M <#> N) G
[PROOF STEP]
using second_isomorphism_grp.normal_set_mult_subgroup normal_imp_subgroup
[PROOF STATE]
proof (prove)
using this:
M \<lhd> G
N \<lhd> G
second_isomorphism_grp ?H ?G ?S \<Longrightarrow> subgroup (?H <#>\<^bsub>?G\<^esub> ?S) ?G
?H \<lhd> ?G \<Longrightarrow> subgroup ?H ?G

goal (1 subgoal):
 1. subgroup (M <#> N) G
[PROOF STEP]
unfolding second_isomorphism_grp_def second_isomorphism_grp_axioms_def
[PROOF STATE]
proof (prove)
using this:
M \<lhd> G
N \<lhd> G
?H \<lhd> ?G \<and> subgroup ?S ?G \<Longrightarrow> subgroup (?H <#>\<^bsub>?G\<^esub> ?S) ?G
?H \<lhd> ?G \<Longrightarrow> subgroup ?H ?G

goal (1 subgoal):
 1. subgroup (M <#> N) G
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
subgroup (M <#> N) G

goal (1 subgoal):
 1. \<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
show "\<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
assume x:"x \<in> carrier G"
[PROOF STATE]
proof (state)
this:
x \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
have "M <#> N #> x = M <#> (N #> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M <#> N #> x = M <#> (N #> x)
[PROOF STEP]
by (metis assms(1,2) normal_inv_iff setmult_rcos_assoc subgroup.subset x)
[PROOF STATE]
proof (state)
this:
M <#> N #> x = M <#> (N #> x)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M <#> N #> x = M <#> (N #> x)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
have "\<dots> = M <#> (x <# N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M <#> (N #> x) = M <#> (x <# N)
[PROOF STEP]
by (metis assms(2) normal.coset_eq x)
[PROOF STATE]
proof (state)
this:
M <#> (N #> x) = M <#> (x <# N)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M <#> (N #> x) = M <#> (x <# N)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
have "\<dots> = (M #> x) <#> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M <#> (x <# N) = M #> x <#> N
[PROOF STEP]
by (metis assms(1,2) normal_imp_subgroup rcos_assoc_lcos subgroup.subset x)
[PROOF STATE]
proof (state)
this:
M <#> (x <# N) = M #> x <#> N

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M <#> (x <# N) = M #> x <#> N

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
have "\<dots> = (x <# M) <#> N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M #> x <#> N = x <# M <#> N
[PROOF STEP]
by (metis assms(1) normal.coset_eq x)
[PROOF STATE]
proof (state)
this:
M #> x <#> N = x <# M <#> N

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M #> x <#> N = x <# M <#> N

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
have "\<dots> = x <# (M <#> N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x <# M <#> N = x <# (M <#> N)
[PROOF STEP]
by (metis assms(1,2) normal_imp_subgroup setmult_lcos_assoc subgroup.subset x)
[PROOF STATE]
proof (state)
this:
x <# M <#> N = x <# (M <#> N)

goal (1 subgoal):
 1. \<And>x. x \<in> carrier G \<Longrightarrow> M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
show "M <#> N #> x = x <# (M <#> N)"
[PROOF STATE]
proof (prove)
using this:
M <#> N #> x = x <# (M <#> N)

goal (1 subgoal):
 1. M <#> N #> x = x <# (M <#> N)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
M <#> N #> x = x <# (M <#> N)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>carrier G. M <#> N #> x = x <# (M <#> N)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) restrict_group_imp_subgroup:
  assumes "H \<subseteq> carrier G" "group (G\<lparr>carrier := H\<rparr>)"
  shows "subgroup H G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. H \<subseteq> carrier G
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H
 3. \<one> \<in> H
 4. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
H \<subseteq> carrier G
[PROOF STEP]
show "H \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> carrier G

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

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H
 2. \<one> \<in> H
 3. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H
 2. \<one> \<in> H
 3. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H
 2. \<one> \<in> H
 3. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
assume "x \<in> H" "y \<in> H"
[PROOF STATE]
proof (state)
this:
x \<in> H
y \<in> H

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H
 2. \<one> \<in> H
 3. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
hence "x \<in> carrier (G\<lparr>carrier := H\<rparr>)" "y \<in> carrier (G\<lparr>carrier := H\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> H
y \<in> H

goal (1 subgoal):
 1. x \<in> carrier (G\<lparr>carrier := H\<rparr>) &&& y \<in> carrier (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier (G\<lparr>carrier := H\<rparr>)
y \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H
 2. \<one> \<in> H
 3. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
Group.group (G\<lparr>carrier := H\<rparr>)
x \<in> carrier (G\<lparr>carrier := H\<rparr>)
y \<in> carrier (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
show "x \<otimes> y \<in> H"
[PROOF STATE]
proof (prove)
using this:
Group.group (G\<lparr>carrier := H\<rparr>)
x \<in> carrier (G\<lparr>carrier := H\<rparr>)
y \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. x \<otimes> y \<in> H
[PROOF STEP]
using assms(2) group.is_monoid monoid.m_closed
[PROOF STATE]
proof (prove)
using this:
Group.group (G\<lparr>carrier := H\<rparr>)
x \<in> carrier (G\<lparr>carrier := H\<rparr>)
y \<in> carrier (G\<lparr>carrier := H\<rparr>)
Group.group (G\<lparr>carrier := H\<rparr>)
Group.group ?G \<Longrightarrow> Group.monoid ?G
\<lbrakk>Group.monoid ?G; ?x \<in> carrier ?G; ?y \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?x \<otimes>\<^bsub>?G\<^esub> ?y \<in> carrier ?G

goal (1 subgoal):
 1. x \<otimes> y \<in> H
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<in> H

goal (2 subgoals):
 1. \<one> \<in> H
 2. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<one> \<in> H
 2. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
show "\<one> \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one> \<in> H
[PROOF STEP]
using assms(2) group.is_monoid monoid.one_closed
[PROOF STATE]
proof (prove)
using this:
Group.group (G\<lparr>carrier := H\<rparr>)
Group.group ?G \<Longrightarrow> Group.monoid ?G
Group.monoid ?G \<Longrightarrow> \<one>\<^bsub>?G\<^esub> \<in> carrier ?G

goal (1 subgoal):
 1. \<one> \<in> H
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<one> \<in> H

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
assume "x \<in> H"
[PROOF STATE]
proof (state)
this:
x \<in> H

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
hence x:"x \<in> carrier (G\<lparr>carrier := H\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> H

goal (1 subgoal):
 1. x \<in> carrier (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
hence "inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier (G\<lparr>carrier := H\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
using assms(2) group.inv_closed
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (G\<lparr>carrier := H\<rparr>)
Group.group (G\<lparr>carrier := H\<rparr>)
\<lbrakk>Group.group ?G; ?x \<in> carrier ?G\<rbrakk> \<Longrightarrow> inv\<^bsub>?G\<^esub> ?x \<in> carrier ?G

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
hence "inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G
[PROOF STEP]
using x assms(1)
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier (G\<lparr>carrier := H\<rparr>)
x \<in> carrier (G\<lparr>carrier := H\<rparr>)
H \<subseteq> carrier G

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
have "inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>
[PROOF STEP]
using assms(2) group.l_inv x
[PROOF STATE]
proof (prove)
using this:
Group.group (G\<lparr>carrier := H\<rparr>)
\<lbrakk>Group.group ?G; ?x \<in> carrier ?G\<rbrakk> \<Longrightarrow> inv\<^bsub>?G\<^esub> ?x \<otimes>\<^bsub>?G\<^esub> ?x = \<one>\<^bsub>?G\<^esub>
x \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
have "x \<in> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
using x assms(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (G\<lparr>carrier := H\<rparr>)
H \<subseteq> carrier G

goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>
x \<in> carrier G
[PROOF STEP]
have "inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>
x \<in> carrier G

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x
[PROOF STEP]
using inv_equality[symmetric]
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> carrier G
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<otimes> x = \<one>
x \<in> carrier G
\<lbrakk>?t \<otimes> ?x = \<one>; ?x \<in> carrier G; ?t \<in> carrier G\<rbrakk> \<Longrightarrow> ?t = inv ?x

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x

goal (1 subgoal):
 1. \<And>x. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
thus "inv x \<in> H"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x

goal (1 subgoal):
 1. inv x \<in> H
[PROOF STEP]
using assms(2) group.inv_closed x
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x
Group.group (G\<lparr>carrier := H\<rparr>)
\<lbrakk>Group.group ?G; ?x \<in> carrier ?G\<rbrakk> \<Longrightarrow> inv\<^bsub>?G\<^esub> ?x \<in> carrier ?G
x \<in> carrier (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. inv x \<in> H
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inv x \<in> H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) normal_subgroup_factorize:
  assumes "N \<lhd> G" and "N \<subseteq> H" and "subgroup H G"
  shows "subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
interpret GModN: group "G Mod N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.group (G Mod N)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
N \<lhd> G

goal (1 subgoal):
 1. Group.group (G Mod N)
[PROOF STEP]
by (rule normal.factorgroup_is_group)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
have "N \<lhd> G\<lparr>carrier := H\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N \<lhd> G\<lparr>carrier := H\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
N \<lhd> G
N \<subseteq> H
subgroup H G

goal (1 subgoal):
 1. N \<lhd> G\<lparr>carrier := H\<rparr>
[PROOF STEP]
by (metis normal_restrict_supergroup)
[PROOF STATE]
proof (state)
this:
N \<lhd> G\<lparr>carrier := H\<rparr>

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
hence grpHN:"group (G\<lparr>carrier := H\<rparr> Mod N)"
[PROOF STATE]
proof (prove)
using this:
N \<lhd> G\<lparr>carrier := H\<rparr>

goal (1 subgoal):
 1. Group.group (G\<lparr>carrier := H\<rparr> Mod N)
[PROOF STEP]
by (rule normal.factorgroup_is_group)
[PROOF STATE]
proof (state)
this:
Group.group (G\<lparr>carrier := H\<rparr> Mod N)

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
have "(<#>\<^bsub>G\<lparr>carrier:=H\<rparr>\<^esub>) = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k})
[PROOF STEP]
using set_mult_def
[PROOF STATE]
proof (prove)
using this:
?H <#>\<^bsub>?G\<^esub> ?K = (\<Union>h\<in>?H. \<Union>k\<in>?K. {h \<otimes>\<^bsub>?G\<^esub> k})

goal (1 subgoal):
 1. (<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k})
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k})

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k})

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
have "\<dots> = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
have "(<#>) = (\<lambda>U K. (\<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (<#>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})
[PROOF STEP]
using set_mult_def
[PROOF STATE]
proof (prove)
using this:
?H <#>\<^bsub>?G\<^esub> ?K = (\<Union>h\<in>?H. \<Union>k\<in>?K. {h \<otimes>\<^bsub>?G\<^esub> k})

goal (1 subgoal):
 1. (<#>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(<#>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k})
(\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})
(<#>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})
[PROOF STEP]
have "(<#>\<^bsub>G\<lparr>carrier:=H\<rparr>\<^esub>) = (<#>\<^bsub>G\<^esub>)"
[PROOF STATE]
proof (prove)
using this:
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k})
(\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> k}) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})
(<#>) = (\<lambda>U K. \<Union>h\<in>U. \<Union>k\<in>K. {h \<otimes> k})

goal (1 subgoal):
 1. (<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (<#>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (<#>)

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
with grpHN
[PROOF STATE]
proof (chain)
picking this:
Group.group (G\<lparr>carrier := H\<rparr> Mod N)
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (<#>)
[PROOF STEP]
have "group ((G Mod N)\<lparr>carrier := (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N)\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
Group.group (G\<lparr>carrier := H\<rparr> Mod N)
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (<#>)

goal (1 subgoal):
 1. Group.group ((G Mod N)\<lparr>carrier := rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rparr>)
[PROOF STEP]
unfolding FactGroup_def
[PROOF STATE]
proof (prove)
using this:
Group.group \<lparr>carrier = rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N, monoid.mult = (<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>), one = N\<rparr>
(<#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (<#>)

goal (1 subgoal):
 1. Group.group (\<lparr>carrier = rcosets N, monoid.mult = (<#>), one = N\<rparr>\<lparr>carrier := rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Group.group ((G Mod N)\<lparr>carrier := rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rparr>)

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Group.group ((G Mod N)\<lparr>carrier := rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rparr>)

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
have "rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def r_coset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>a\<in>carrier (G\<lparr>carrier := H\<rparr>). {\<Union>h\<in>N. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a}}) \<subseteq> carrier \<lparr>carrier = \<Union>a\<in>carrier G. {\<Union>h\<in>N. {h \<otimes> a}}, monoid.mult = (<#>), one = N\<rparr>
[PROOF STEP]
using assms(3) subgroup.subset
[PROOF STATE]
proof (prove)
using this:
subgroup H G
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. (\<Union>a\<in>carrier (G\<lparr>carrier := H\<rparr>). {\<Union>h\<in>N. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a}}) \<subseteq> carrier \<lparr>carrier = \<Union>a\<in>carrier G. {\<Union>h\<in>N. {h \<otimes> a}}, monoid.mult = (<#>), one = N\<rparr>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Group.group ((G Mod N)\<lparr>carrier := rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rparr>)
rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Group.group ((G Mod N)\<lparr>carrier := rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rparr>)
rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
using GModN.is_group group.restrict_group_imp_subgroup
[PROOF STATE]
proof (prove)
using this:
Group.group ((G Mod N)\<lparr>carrier := rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rparr>)
rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<subseteq> carrier (G Mod N)
Group.group (G Mod N)
\<lbrakk>Group.group ?G; ?H \<subseteq> carrier ?G; Group.group (?G\<lparr>carrier := ?H\<rparr>)\<rbrakk> \<Longrightarrow> subgroup ?H ?G

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) normality_factorization:
  assumes NG:"N \<lhd> G" and NH:"N \<subseteq> H" and HG:"H \<lhd> G"
  shows "(rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) \<lhd> (G Mod N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<lhd> G Mod N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<lhd> G Mod N
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
N \<lhd> G
[PROOF STEP]
interpret GModN: group "G Mod N"
[PROOF STATE]
proof (prove)
using this:
N \<lhd> G

goal (1 subgoal):
 1. Group.group (G Mod N)
[PROOF STEP]
by (metis normal.factorgroup_is_group)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<lhd> G Mod N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<lhd> G Mod N
[PROOF STEP]
proof (auto simp: GModN.normal_inv_iff)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
 2. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
N \<lhd> G
N \<subseteq> H
H \<lhd> G
[PROOF STEP]
show "subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)"
[PROOF STATE]
proof (prove)
using this:
N \<lhd> G
N \<subseteq> H
H \<lhd> G

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
using normal_imp_subgroup normal_subgroup_factorize
[PROOF STATE]
proof (prove)
using this:
N \<lhd> G
N \<subseteq> H
H \<lhd> G
?H \<lhd> ?G \<Longrightarrow> subgroup ?H ?G
\<lbrakk>?N \<lhd> G; ?N \<subseteq> ?H; subgroup ?H G\<rbrakk> \<Longrightarrow> subgroup (rcosets\<^bsub>G\<lparr>carrier := ?H\<rparr>\<^esub> ?N) (G Mod ?N)

goal (1 subgoal):
 1. subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
subgroup (rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N) (G Mod N)

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
fix U V
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
assume U:"U \<in> carrier (G Mod N)" and V:"V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N"
[PROOF STATE]
proof (state)
this:
U \<in> carrier (G Mod N)
V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U \<in> carrier (G Mod N)
V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
obtain g where g:"g \<in> carrier G" "U = N #> g"
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier (G Mod N)
V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> carrier G; U = N #> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier \<lparr>carrier = \<Union>a\<in>carrier G. {N #> a}, monoid.mult = (<#>), one = N\<rparr>
V \<in> (\<Union>a\<in>carrier (G\<lparr>carrier := H\<rparr>). {N #>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a})

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

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
from V
[PROOF STATE]
proof (chain)
picking this:
V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
obtain h where h:"h \<in> H" "V = N #> h"
[PROOF STATE]
proof (prove)
using this:
V \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> H; V = N #> h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def r_coset_def
[PROOF STATE]
proof (prove)
using this:
V \<in> (\<Union>a\<in>carrier (G\<lparr>carrier := H\<rparr>). {\<Union>h\<in>N. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a}})

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h \<in> H; V = (\<Union>ha\<in>N. {ha \<otimes> h})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h \<in> H
V = N #> h

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
hence hG:"h \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
h \<in> H
V = N #> h

goal (1 subgoal):
 1. h \<in> carrier G
[PROOF STEP]
using HG normal_imp_subgroup subgroup.mem_carrier
[PROOF STATE]
proof (prove)
using this:
h \<in> H
V = N #> h
H \<lhd> G
?H \<lhd> ?G \<Longrightarrow> subgroup ?H ?G
\<lbrakk>subgroup ?H ?G; ?x \<in> ?H\<rbrakk> \<Longrightarrow> ?x \<in> carrier ?G

goal (1 subgoal):
 1. h \<in> carrier G
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
h \<in> carrier G

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
hence ghG:"g \<otimes> h \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier G

goal (1 subgoal):
 1. g \<otimes> h \<in> carrier G
[PROOF STEP]
using g m_closed
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier G
g \<in> carrier G
U = N #> g
\<lbrakk>?x \<in> carrier G; ?y \<in> carrier G\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier G

goal (1 subgoal):
 1. g \<otimes> h \<in> carrier G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<otimes> h \<in> carrier G

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
from g h
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
U = N #> g
h \<in> H
V = N #> h
[PROOF STEP]
have "g \<otimes> h \<otimes> inv g \<in> H"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
U = N #> g
h \<in> H
V = N #> h

goal (1 subgoal):
 1. g \<otimes> h \<otimes> inv g \<in> H
[PROOF STEP]
using HG normal_inv_iff
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
U = N #> g
h \<in> H
V = N #> h
H \<lhd> G
?N \<lhd> G = (subgroup ?N G \<and> (\<forall>x\<in>carrier G. \<forall>h\<in>?N. x \<otimes> h \<otimes> inv x \<in> ?N))

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

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g \<otimes> h \<otimes> inv g \<in> H

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
have "U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> (g \<otimes> h \<otimes> inv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
from g U
[PROOF STATE]
proof (chain)
picking this:
g \<in> carrier G
U = N #> g
U \<in> carrier (G Mod N)
[PROOF STEP]
have "inv\<^bsub>G Mod N\<^esub> U = N #> inv g"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
U = N #> g
U \<in> carrier (G Mod N)

goal (1 subgoal):
 1. inv\<^bsub>G Mod N\<^esub> U = N #> inv g
[PROOF STEP]
using NG normal.inv_FactGroup normal.rcos_inv
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
U = N #> g
U \<in> carrier (G Mod N)
N \<lhd> G
\<lbrakk>?H \<lhd> ?G; ?X \<in> carrier (?G Mod ?H)\<rbrakk> \<Longrightarrow> inv\<^bsub>?G Mod ?H\<^esub> ?X = set_inv\<^bsub>?G\<^esub> ?X
\<lbrakk>?H \<lhd> ?G; ?x \<in> carrier ?G\<rbrakk> \<Longrightarrow> set_inv\<^bsub>?G\<^esub> (?H #>\<^bsub>?G\<^esub> ?x) = ?H #>\<^bsub>?G\<^esub> inv\<^bsub>?G\<^esub> ?x

goal (1 subgoal):
 1. inv\<^bsub>G Mod N\<^esub> U = N #> inv g
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G Mod N\<^esub> U = N #> inv g

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
hence "U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = (N #> g) <#> (N #> h) <#> (N #> inv g)"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G Mod N\<^esub> U = N #> inv g

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g <#> (N #> h) <#> (N #> inv g)
[PROOF STEP]
using g h
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G Mod N\<^esub> U = N #> inv g
g \<in> carrier G
U = N #> g
h \<in> H
V = N #> h

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g <#> (N #> h) <#> (N #> inv g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g <#> (N #> h) <#> (N #> inv g)

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g <#> (N #> h) <#> (N #> inv g)

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
have "\<dots> = N #> (g \<otimes> h) <#> (N #> inv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N #> g <#> (N #> h) <#> (N #> inv g) = N #> g \<otimes> h <#> (N #> inv g)
[PROOF STEP]
using g hG NG normal.rcos_sum
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
U = N #> g
h \<in> carrier G
N \<lhd> G
\<lbrakk>?H \<lhd> ?G; ?x \<in> carrier ?G; ?y \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?H #>\<^bsub>?G\<^esub> ?x <#>\<^bsub>?G\<^esub> (?H #>\<^bsub>?G\<^esub> ?y) = ?H #>\<^bsub>?G\<^esub> ?x \<otimes>\<^bsub>?G\<^esub> ?y

goal (1 subgoal):
 1. N #> g <#> (N #> h) <#> (N #> inv g) = N #> g \<otimes> h <#> (N #> inv g)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
N #> g <#> (N #> h) <#> (N #> inv g) = N #> g \<otimes> h <#> (N #> inv g)

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
N #> g <#> (N #> h) <#> (N #> inv g) = N #> g \<otimes> h <#> (N #> inv g)

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
have "\<dots> = N #> (g \<otimes> h \<otimes> inv g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N #> g \<otimes> h <#> (N #> inv g) = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
using g inv_closed ghG NG normal.rcos_sum
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
U = N #> g
?x \<in> carrier G \<Longrightarrow> inv ?x \<in> carrier G
g \<otimes> h \<in> carrier G
N \<lhd> G
\<lbrakk>?H \<lhd> ?G; ?x \<in> carrier ?G; ?y \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?H #>\<^bsub>?G\<^esub> ?x <#>\<^bsub>?G\<^esub> (?H #>\<^bsub>?G\<^esub> ?y) = ?H #>\<^bsub>?G\<^esub> ?x \<otimes>\<^bsub>?G\<^esub> ?y

goal (1 subgoal):
 1. N #> g \<otimes> h <#> (N #> inv g) = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
N #> g \<otimes> h <#> (N #> inv g) = N #> g \<otimes> h \<otimes> inv g

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g

goal (1 subgoal):
 1. \<And>x h. \<lbrakk>x \<in> carrier (G Mod N); h \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N\<rbrakk> \<Longrightarrow> x <#> h <#> inv\<^bsub>G Mod N\<^esub> x \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g \<otimes> h \<otimes> inv g \<in> H
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g
[PROOF STEP]
show "U <#> V <#> inv\<^bsub>G Mod N\<^esub> U \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N"
[PROOF STATE]
proof (prove)
using this:
g \<otimes> h \<otimes> inv g \<in> H
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = N #> g \<otimes> h \<otimes> inv g

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N
[PROOF STEP]
unfolding RCOSETS_def r_coset_def
[PROOF STATE]
proof (prove)
using this:
g \<otimes> h \<otimes> inv g \<in> H
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U = (\<Union>ha\<in>N. {ha \<otimes> (g \<otimes> h \<otimes> inv g)})

goal (1 subgoal):
 1. U <#> V <#> inv\<^bsub>G Mod N\<^esub> U \<in> (\<Union>a\<in>carrier (G\<lparr>carrier := H\<rparr>). {\<Union>h\<in>N. {h \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> a}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U <#> V <#> inv\<^bsub>G Mod N\<^esub> U \<in> rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rcosets\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N \<lhd> G Mod N

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in normal) fact_group_trivial_iff:
  assumes "finite (carrier G)"
  shows "(carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}) = (H = carrier G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}) = (H = carrier G)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>} \<Longrightarrow> H = carrier G
 2. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
assume "carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}"
[PROOF STATE]
proof (state)
this:
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}

goal (2 subgoals):
 1. carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>} \<Longrightarrow> H = carrier G
 2. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}

goal (2 subgoals):
 1. carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>} \<Longrightarrow> H = carrier G
 2. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
with assms lagrange
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
subgroup ?H G \<Longrightarrow> card (rcosets ?H) * card ?H = order G
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
have "order (G Mod H) * card H = order G"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup ?H G \<Longrightarrow> card (rcosets ?H) * card ?H = order G
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}

goal (1 subgoal):
 1. order (G Mod H) * card H = order G
[PROOF STEP]
unfolding FactGroup_def order_def
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup ?H G \<Longrightarrow> card (rcosets ?H) * card ?H = card (carrier G)
carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr> = {\<one>\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub>}

goal (1 subgoal):
 1. card (carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>) * card H = card (carrier G)
[PROOF STEP]
using is_subgroup
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup ?H G \<Longrightarrow> card (rcosets ?H) * card ?H = card (carrier G)
carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr> = {\<one>\<^bsub>\<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>\<^esub>}
subgroup H G

goal (1 subgoal):
 1. card (carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>) * card H = card (carrier G)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
order (G Mod H) * card H = order G

goal (2 subgoals):
 1. carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>} \<Longrightarrow> H = carrier G
 2. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
order (G Mod H) * card H = order G
[PROOF STEP]
have "card H = order G"
[PROOF STATE]
proof (prove)
using this:
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
order (G Mod H) * card H = order G

goal (1 subgoal):
 1. card H = order G
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
card (carrier (G Mod H)) * card H = card (carrier G)

goal (1 subgoal):
 1. card H = card (carrier G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card H = order G

goal (2 subgoals):
 1. carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>} \<Longrightarrow> H = carrier G
 2. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
thus "H = carrier G"
[PROOF STATE]
proof (prove)
using this:
card H = order G

goal (1 subgoal):
 1. H = carrier G
[PROOF STEP]
using subgroup.subset is_subgroup assms card_subset_eq
[PROOF STATE]
proof (prove)
using this:
card H = order G
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G
subgroup H G
finite (carrier G)
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?A = card ?B\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. H = carrier G
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
card H = card (carrier G)
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G
subgroup H G
finite (carrier G)
\<lbrakk>finite ?B; ?A \<subseteq> ?B; card ?A = card ?B\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. H = carrier G
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
H = carrier G

goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
[PROOF STEP]
have ordergt0:"order G > 0"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. 0 < order G
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. 0 < card (carrier G)
[PROOF STEP]
by (metis subgroup.finite_imp_card_positive subgroup_self)
[PROOF STATE]
proof (state)
this:
0 < order G

goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
assume "H = carrier G"
[PROOF STATE]
proof (state)
this:
H = carrier G

goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
hence "card H = order G"
[PROOF STATE]
proof (prove)
using this:
H = carrier G

goal (1 subgoal):
 1. card H = order G
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
H = carrier G

goal (1 subgoal):
 1. card H = card (carrier G)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card H = order G

goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
with assms is_subgroup lagrange
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
subgroup H G
subgroup ?H G \<Longrightarrow> card (rcosets ?H) * card ?H = order G
card H = order G
[PROOF STEP]
have "card (rcosets H) * order G = order G"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)
subgroup H G
subgroup ?H G \<Longrightarrow> card (rcosets ?H) * card ?H = order G
card H = order G

goal (1 subgoal):
 1. card (rcosets H) * order G = order G
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card (rcosets H) * order G = order G

goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
with ordergt0
[PROOF STATE]
proof (chain)
picking this:
0 < order G
card (rcosets H) * order G = order G
[PROOF STEP]
have "card (rcosets H) = 1"
[PROOF STATE]
proof (prove)
using this:
0 < order G
card (rcosets H) * order G = order G

goal (1 subgoal):
 1. card (rcosets H) = 1
[PROOF STEP]
by (metis mult_eq_self_implies_10 mult.commute neq0_conv)
[PROOF STATE]
proof (state)
this:
card (rcosets H) = 1

goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
hence "order (G Mod H) = 1"
[PROOF STATE]
proof (prove)
using this:
card (rcosets H) = 1

goal (1 subgoal):
 1. order (G Mod H) = 1
[PROOF STEP]
unfolding order_def FactGroup_def
[PROOF STATE]
proof (prove)
using this:
card (rcosets H) = 1

goal (1 subgoal):
 1. card (carrier \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
order (G Mod H) = 1

goal (1 subgoal):
 1. H = carrier G \<Longrightarrow> carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
thus "carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}"
[PROOF STATE]
proof (prove)
using this:
order (G Mod H) = 1

goal (1 subgoal):
 1. carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
using factorgroup_is_group
[PROOF STATE]
proof (prove)
using this:
order (G Mod H) = 1
Group.group (G Mod H)

goal (1 subgoal):
 1. carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}
[PROOF STEP]
by (metis group.order_one_triv_iff)
[PROOF STATE]
proof (state)
this:
carrier (G Mod H) = {\<one>\<^bsub>G Mod H\<^esub>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in normal) factgroup_finite:
  assumes "finite (carrier G)"
  shows "finite (rcosets H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (rcosets H)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

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

goal (1 subgoal):
 1. finite (\<Union>a\<in>carrier G. {H #> a})
[PROOF STEP]
by auto


[STATEMENT]
lemma (in normal) factgroup_subgroup_union_char:
  assumes "subgroup A (G Mod H)"
  shows "(\<Union>A) = {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> A = {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Union> A \<subseteq> {x \<in> carrier G. H #> x \<in> A}
 2. {x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union> A
[PROOF STEP]
show "\<Union>A \<subseteq> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> A \<subseteq> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
assume x:"x \<in> \<Union>A"
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> A

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Union> A
[PROOF STEP]
obtain a where a:"a \<in> A" "x \<in> a"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Union> A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; x \<in> a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> A
x \<in> a

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
subgroup A (G Mod H)
a \<in> A
x \<in> a
[PROOF STEP]
have xx:"x \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
a \<in> A
x \<in> a

goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
using subgroup.subset
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
a \<in> A
x \<in> a
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def r_coset_def
[PROOF STATE]
proof (prove)
using this:
subgroup A \<lparr>carrier = \<Union>a\<in>carrier G. {\<Union>h\<in>H. {h \<otimes> a}}, monoid.mult = (<#>), one = H\<rparr>
a \<in> A
x \<in> a
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
from assms a
[PROOF STATE]
proof (chain)
picking this:
subgroup A (G Mod H)
a \<in> A
x \<in> a
[PROOF STEP]
obtain y where y:"y \<in> carrier G" "a = H #> y"
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
a \<in> A
x \<in> a

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> carrier G; a = H #> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using subgroup.subset
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
a \<in> A
x \<in> a
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> carrier G; a = H #> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding FactGroup_def RCOSETS_def
[PROOF STATE]
proof (prove)
using this:
subgroup A \<lparr>carrier = \<Union>a\<in>carrier G. {H #> a}, monoid.mult = (<#>), one = H\<rparr>
a \<in> A
x \<in> a
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> carrier G; a = H #> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y \<in> carrier G
a = H #> y

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
x \<in> a
y \<in> carrier G
a = H #> y
[PROOF STEP]
have "x \<in> H #> y"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
x \<in> a
y \<in> carrier G
a = H #> y

goal (1 subgoal):
 1. x \<in> H #> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> H #> y

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
hence "H #> y = H #> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> H #> y

goal (1 subgoal):
 1. H #> y = H #> x
[PROOF STEP]
using y is_subgroup repr_independence
[PROOF STATE]
proof (prove)
using this:
x \<in> H #> y
y \<in> carrier G
a = H #> y
subgroup H G
\<lbrakk>?y \<in> ?H #> ?x; ?x \<in> carrier G; subgroup ?H G\<rbrakk> \<Longrightarrow> ?H #> ?x = ?H #> ?y

goal (1 subgoal):
 1. H #> y = H #> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H #> y = H #> x

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
with y(2) a(1)
[PROOF STATE]
proof (chain)
picking this:
a = H #> y
a \<in> A
H #> y = H #> x
[PROOF STEP]
have "H #> x \<in> A"
[PROOF STATE]
proof (prove)
using this:
a = H #> y
a \<in> A
H #> y = H #> x

goal (1 subgoal):
 1. H #> x \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H #> x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> \<Union> A \<Longrightarrow> x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
with xx
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier G
H #> x \<in> A
[PROOF STEP]
show "x \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
H #> x \<in> A

goal (1 subgoal):
 1. x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> carrier G. H #> x \<in> A}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> A \<subseteq> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. {x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union> A
[PROOF STEP]
show "{x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union>A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> x \<in> \<Union> A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> x \<in> \<Union> A
[PROOF STEP]
assume x:"x \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> x \<in> \<Union> A
[PROOF STEP]
hence xx:"x \<in> carrier G" "H #> x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. x \<in> carrier G &&& H #> x \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier G
H #> x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> x \<in> \<Union> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> carrier G
H #> x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> x \<in> \<Union> A
[PROOF STEP]
have "x \<in> H #> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> H #> x
[PROOF STEP]
by (metis is_subgroup rcos_self xx(1))
[PROOF STATE]
proof (state)
this:
x \<in> H #> x

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> x \<in> \<Union> A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier G
H #> x \<in> A
x \<in> H #> x
[PROOF STEP]
show "x \<in> \<Union>A"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
H #> x \<in> A
x \<in> H #> x

goal (1 subgoal):
 1. x \<in> \<Union> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{x \<in> carrier G. H #> x \<in> A} \<subseteq> \<Union> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in normal) factgroup_subgroup_union_subgroup:
  assumes "subgroup A (G Mod H)"
  shows "subgroup (\<Union>A) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (\<Union> A) G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgroup (\<Union> A) G
[PROOF STEP]
have "subgroup {x \<in> carrier G. H #> x \<in> A} G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup {x \<in> carrier G. H #> x \<in> A} G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. {x \<in> carrier G. H #> x \<in> A} \<subseteq> carrier G
 2. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 4. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
show "{x \<in> carrier G. H #> x \<in> A} \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier G. H #> x \<in> A} \<subseteq> carrier G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> carrier G. H #> x \<in> A} \<subseteq> carrier G

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
assume "x \<in> {x \<in> carrier G. H #> x \<in> A}" and "y \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> carrier G. H #> x \<in> A}
y \<in> {x \<in> carrier G. H #> x \<in> A}

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
hence x:"x \<in> carrier G" "H #> x \<in> A" and y:"y \<in> carrier G" "H #> y \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> carrier G. H #> x \<in> A}
y \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. (x \<in> carrier G &&& H #> x \<in> A) &&& y \<in> carrier G &&& H #> y \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier G
H #> x \<in> A
y \<in> carrier G
H #> y \<in> A

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
hence xyG:"x \<otimes> y \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
H #> x \<in> A
y \<in> carrier G
H #> y \<in> A

goal (1 subgoal):
 1. x \<otimes> y \<in> carrier G
[PROOF STEP]
by (metis m_closed)
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<in> carrier G

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
from assms x y
[PROOF STATE]
proof (chain)
picking this:
subgroup A (G Mod H)
x \<in> carrier G
H #> x \<in> A
y \<in> carrier G
H #> y \<in> A
[PROOF STEP]
have "(H #> x) <#> (H #> y) \<in> A"
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
x \<in> carrier G
H #> x \<in> A
y \<in> carrier G
H #> y \<in> A

goal (1 subgoal):
 1. H #> x <#> (H #> y) \<in> A
[PROOF STEP]
using subgroup.m_closed
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
x \<in> carrier G
H #> x \<in> A
y \<in> carrier G
H #> y \<in> A
\<lbrakk>subgroup ?H ?G; ?x \<in> ?H; ?y \<in> ?H\<rbrakk> \<Longrightarrow> ?x \<otimes>\<^bsub>?G\<^esub> ?y \<in> ?H

goal (1 subgoal):
 1. H #> x <#> (H #> y) \<in> A
[PROOF STEP]
unfolding FactGroup_def
[PROOF STATE]
proof (prove)
using this:
subgroup A \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>
x \<in> carrier G
H #> x \<in> A
y \<in> carrier G
H #> y \<in> A
\<lbrakk>subgroup ?H ?G; ?x \<in> ?H; ?y \<in> ?H\<rbrakk> \<Longrightarrow> ?x \<otimes>\<^bsub>?G\<^esub> ?y \<in> ?H

goal (1 subgoal):
 1. H #> x <#> (H #> y) \<in> A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
H #> x <#> (H #> y) \<in> A

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
hence "H #> (x \<otimes> y) \<in> A"
[PROOF STATE]
proof (prove)
using this:
H #> x <#> (H #> y) \<in> A

goal (1 subgoal):
 1. H #> x \<otimes> y \<in> A
[PROOF STEP]
by (metis rcos_sum x(1) y(1))
[PROOF STATE]
proof (state)
this:
H #> x \<otimes> y \<in> A

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> {x \<in> carrier G. H #> x \<in> A}; y \<in> {x \<in> carrier G. H #> x \<in> A}\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 3. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
with xyG
[PROOF STATE]
proof (chain)
picking this:
x \<otimes> y \<in> carrier G
H #> x \<otimes> y \<in> A
[PROOF STEP]
show "x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> y \<in> carrier G
H #> x \<otimes> y \<in> A

goal (1 subgoal):
 1. x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<in> {x \<in> carrier G. H #> x \<in> A}

goal (2 subgoals):
 1. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
have "H #> \<one> \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H #> \<one> \<in> A
[PROOF STEP]
using assms subgroup.one_closed
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
subgroup ?H ?G \<Longrightarrow> \<one>\<^bsub>?G\<^esub> \<in> ?H

goal (1 subgoal):
 1. H #> \<one> \<in> A
[PROOF STEP]
unfolding FactGroup_def
[PROOF STATE]
proof (prove)
using this:
subgroup A \<lparr>carrier = rcosets H, monoid.mult = (<#>), one = H\<rparr>
subgroup ?H ?G \<Longrightarrow> \<one>\<^bsub>?G\<^esub> \<in> ?H

goal (1 subgoal):
 1. H #> \<one> \<in> A
[PROOF STEP]
by (metis coset_mult_one monoid.select_convs(2) subset)
[PROOF STATE]
proof (state)
this:
H #> \<one> \<in> A

goal (2 subgoals):
 1. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
 2. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
with assms one_closed
[PROOF STATE]
proof (chain)
picking this:
subgroup A (G Mod H)
\<one> \<in> carrier G
H #> \<one> \<in> A
[PROOF STEP]
show "\<one> \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
\<one> \<in> carrier G
H #> \<one> \<in> A

goal (1 subgoal):
 1. \<one> \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<one> \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
assume "x \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (state)
this:
x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
hence x:"x \<in> carrier G" "H #> x \<in> A"
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> carrier G. H #> x \<in> A}

goal (1 subgoal):
 1. x \<in> carrier G &&& H #> x \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier G
H #> x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
hence invx:"inv x \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
H #> x \<in> A

goal (1 subgoal):
 1. inv x \<in> carrier G
[PROOF STEP]
using inv_closed
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
H #> x \<in> A
?x \<in> carrier G \<Longrightarrow> inv ?x \<in> carrier G

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

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
from assms x
[PROOF STATE]
proof (chain)
picking this:
subgroup A (G Mod H)
x \<in> carrier G
H #> x \<in> A
[PROOF STEP]
have "set_inv (H #> x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
x \<in> carrier G
H #> x \<in> A

goal (1 subgoal):
 1. set_inv (H #> x) \<in> A
[PROOF STEP]
using subgroup.m_inv_closed
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
x \<in> carrier G
H #> x \<in> A
\<lbrakk>subgroup ?H ?G; ?x \<in> ?H\<rbrakk> \<Longrightarrow> inv\<^bsub>?G\<^esub> ?x \<in> ?H

goal (1 subgoal):
 1. set_inv (H #> x) \<in> A
[PROOF STEP]
by (metis inv_FactGroup subgroup.mem_carrier)
[PROOF STATE]
proof (state)
this:
set_inv (H #> x) \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
hence "H #> (inv x) \<in> A"
[PROOF STATE]
proof (prove)
using this:
set_inv (H #> x) \<in> A

goal (1 subgoal):
 1. H #> inv x \<in> A
[PROOF STEP]
by (metis rcos_inv x(1))
[PROOF STATE]
proof (state)
this:
H #> inv x \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> {x \<in> carrier G. H #> x \<in> A} \<Longrightarrow> inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
with invx
[PROOF STATE]
proof (chain)
picking this:
inv x \<in> carrier G
H #> inv x \<in> A
[PROOF STEP]
show "inv x \<in> {x \<in> carrier G. H #> x \<in> A}"
[PROOF STATE]
proof (prove)
using this:
inv x \<in> carrier G
H #> inv x \<in> A

goal (1 subgoal):
 1. inv x \<in> {x \<in> carrier G. H #> x \<in> A}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inv x \<in> {x \<in> carrier G. H #> x \<in> A}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subgroup {x \<in> carrier G. H #> x \<in> A} G

goal (1 subgoal):
 1. subgroup (\<Union> A) G
[PROOF STEP]
with assms factgroup_subgroup_union_char
[PROOF STATE]
proof (chain)
picking this:
subgroup A (G Mod H)
subgroup ?A (G Mod H) \<Longrightarrow> \<Union> ?A = {x \<in> carrier G. H #> x \<in> ?A}
subgroup {x \<in> carrier G. H #> x \<in> A} G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subgroup A (G Mod H)
subgroup ?A (G Mod H) \<Longrightarrow> \<Union> ?A = {x \<in> carrier G. H #> x \<in> ?A}
subgroup {x \<in> carrier G. H #> x \<in> A} G

goal (1 subgoal):
 1. subgroup (\<Union> A) G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgroup (\<Union> A) G

goal:
No subgoals!
[PROOF STEP]
qed