[STATEMENT]
theorem normal_intersection_quotient_isom:
  shows "(\<lambda>X. the_elem ((\<lambda>g. H #> g) ` X)) \<in> iso ((G\<lparr>carrier := S\<rparr>) Mod (H \<inter> S)) (((G\<lparr>carrier := H <#> S\<rparr>)) Mod H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>X. the_elem ((#>) H ` X)) \<in> Group.iso (G\<lparr>carrier := S\<rparr> Mod H \<inter> S) (G\<lparr>carrier := H <#> S\<rparr> Mod H)
[PROOF STEP]
using normal_intersection_hom_kernel[symmetric] normal_intersection_hom normal_intersection_hom_surj
[PROOF STATE]
proof (prove)
using this:
H \<inter> S = kernel (G\<lparr>carrier := S\<rparr>) (G\<lparr>carrier := H <#> S\<rparr> Mod H) ((#>) H)
group_hom (G\<lparr>carrier := S\<rparr>) (G\<lparr>carrier := H <#> S\<rparr> Mod H) ((#>) H)
(#>) H ` carrier (G\<lparr>carrier := S\<rparr>) = carrier (G\<lparr>carrier := H <#> S\<rparr> Mod H)

goal (1 subgoal):
 1. (\<lambda>X. the_elem ((#>) H ` X)) \<in> Group.iso (G\<lparr>carrier := S\<rparr> Mod H \<inter> S) (G\<lparr>carrier := H <#> S\<rparr> Mod H)
[PROOF STEP]
by (metis group_hom.FactGroup_iso_set)