proposition: Lemma cfker_dprod phi psi : cfker phi <*> cfker psi \subset cfker (cfDprod phi psi).
proof: Proof. rewrite -genM_join gen_subG; apply/subsetP=> _ /mulsgP[x y kKx kHy ->] /=. have [[Kx _] [Hy _]] := (setIdP kKx, setIdP kHy). have Gxy: (x * y)%g \in G by rewrite -(dprodW KxH) mem_mulg. rewrite inE Gxy; apply/forallP=> g. have [Gg | G'g] := boolP (g \in G); last by rewrite !cfun0 1?groupMl. have{g Gg} [k [h [Kk Hh -> _]]] := mem_dprod KxH Gg. rewrite mulgA -(mulgA x) (centsP cKH y) // mulgA -mulgA !cfDprodE ?groupM //. by rewrite !cfkerMl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)