proposition: Lemma quotient_sdprodr_isom G A B M : A ><| B = G -> M <| B -> {f : {morphism B / M >-> coset_of (A <*> M)} | isom (B / M) (G / (A <*> M)) f & forall L, L \subset B -> f @* (L / M) = A <*> L / (A <*> M)}.
proof: Proof. move=> defG nsMH; have [defA defB]: A = <<A>>%G /\ B = <<B>>%G. by have [[K1 H1 -> ->] _ _ _] := sdprodP defG; rewrite /= !genGid. do [rewrite {}defA {}defB; move: {A}<<A>>%G {B}<<B>>%G => K H] in defG nsMH *. have [[nKH /isomP[injKH imKH]] sMH] := (sdprod_isom defG, normal_sub nsMH). have [[nsKG sHG mulKH _ _] nKM] := (sdprod_context defG, subset_trans sMH nKH). have nsKMG: K <*> M <| G. by rewrite -quotientYK // -mulKH -quotientK ?cosetpre_normal ?quotient_normal. have [/= f inj_f im_f] := third_isom (joing_subl K M) nsKG nsKMG. rewrite quotientYidl //= -imKH -(restrm_quotientE nKH sMH) in f inj_f im_f. have /domP[h [_ ker_h _ im_h]]: 'dom (f \o quotm _ nsMH) = H / M. by rewrite ['dom _]morphpre_quotm injmK. have{} im_h L: L \subset H -> h @* (L / M) = K <*> L / (K <*> M). move=> sLH; have [sLG sKKM] := (subset_trans sLH sHG, joing_subl K M). rewrite im_h morphim_comp morphim_quotm [_ @* L]restrm_quotientE ?im_f //. rewrite quotientY ?(normsG sKKM) ?(subset_trans sLG) ?normal_norm //. by rewrite (quotientS1 sKKM) joing1G. exists h => //; apply/isomP; split; last by rewrite im_h //= (sdprodWY defG). by rewrite ker_h injm_comp ?injm_quotm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)