proposition: Lemma Aut_cprod_full G H K : H \* K = G -> 'Z(H) = 'Z(K) -> Aut_in (Aut H) 'Z(H) \isog Aut 'Z(H) -> Aut_in (Aut K) 'Z(K) \isog Aut 'Z(K) -> Aut_in (Aut G) 'Z(G) \isog Aut 'Z(G).
proof: Proof. move=> defG eqZHK; have [_ defHK cHK] := cprodP defG. have defZ: 'Z(G) = 'Z(H) by rewrite -defHK -center_prod // eqZHK mulGid. have ziHK: H :&: K = 'Z(K). by apply/eqP; rewrite eqEsubset subsetI -{1 2}eqZHK !center_sub setIS. have AutZP := Aut_sub_fullP (@center_sub gT _). move/AutZP=> AutZHfull /AutZP AutZKfull; apply/AutZP=> g injg gZ. have [gH [def_gH ker_gH _ im_gH]] := domP g defZ. have [gK [def_gK ker_gK _ im_gK]] := domP g (etrans defZ eqZHK). have [injgH injgK]: 'injm gH /\ 'injm gK by rewrite ker_gH ker_gK. have [gHH gKK]: gH @* 'Z(H) = 'Z(H) /\ gK @* 'Z(K) = 'Z(K). by rewrite im_gH im_gK -eqZHK -defZ. have [|fH [injfH im_fH fHZ]] := AutZHfull gH injgH. by rewrite im_gH /= -defZ. have [|fK [injfK im_fK fKZ]] := AutZKfull gK injgK. by rewrite im_gK /= -eqZHK -defZ. have cfHK: fK @* K \subset 'C(fH @* H) by rewrite im_fH im_fK. have eq_fHK: {in H :&: K, fH =1 fK}. by move=> z; rewrite ziHK => Zz; rewrite fHZ ?fKZ /= ?eqZHK // def_gH def_gK. exists (cprodm_morphism defG cfHK eq_fHK). rewrite injm_cprodm injfH injfK im_cprodm im_fH im_fK defHK. rewrite -morphimIdom ziHK -eqZHK injm_center // im_fH eqxx. split=> //= z; rewrite {1}defZ => Zz; have [Hz _] := setIP Zz. by rewrite cprodmEl // fHZ // def_gH. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)