proposition: Lemma morphimR A B : A \subset D -> B \subset D -> f @* [~: A, B] = [~: f @* A, f @* B].
proof: Proof. move/subsetP=> sAD /subsetP sBD. rewrite morphim_gen; last first; last congr <<_>>. by apply/subsetP=> _ /imset2P[x y Ax By ->]; rewrite groupR; auto. apply/setP=> fz; apply/morphimP/imset2P=> [[z _] | [fx fy]]. case/imset2P=> x y Ax By -> -> {z fz}. have Dx := sAD x Ax; have Dy := sBD y By. by exists (f x) (f y); rewrite ?(imset_f, morphR) // ?(inE, Dx, Dy). case/morphimP=> x Dx Ax ->{fx}; case/morphimP=> y Dy By ->{fy} -> {fz}. by exists [~ x, y]; rewrite ?(inE, morphR, groupR, imset2_f). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)