proposition: Lemma solvable_ext_trans (F k E : {subfield L}) : (k <= F <= E)%VS -> solvable_ext k F -> solvable_ext F E -> solvable_ext k E.
proof: Proof. move=> /andP[kF FE] solkF solFE. move: (solkF) (solFE) => /andP[sepkF solmkF] /andP[sepFE solmFE]. have sepkE := separable_trans sepFE. have /solvable_extP [/= l /and3P[EKl galKl subl]] := solvable_prodv (normalClosureSr k F) solFE. apply/solvable_extP; exists [aspace of normalClosure k l] => /=. have galkK := normalClosure_galois sepkF. set K := normalClosure k F in galkK galKl subl EKl *. have /and3P [kK sepkK normkK] := galkK. have /and3P [Kl sepKl normKl] := galKl. have sepkl := separable_trans sepkK sepKl. have kl := subv_trans kK Kl. rewrite normalClosure_galois ?(subv_trans _ (normalClosureSr _ _))//=; last first. by rewrite (subv_trans _ EKl)//= field_subvMr. have KM : (K <= normalClosure k l)%VS := subv_trans Kl (normalClosureSr _ _). have kKM : (k <= K <= normalClosure k l)%VS by rewrite kK KM. rewrite (series_sol (normalField_normal _ normkK))//= -/K. rewrite (isog_sol (normalField_isog _ _ _)) ?normalClosure_galois//=. rewrite [X in _ && X]solmkF andbT /normalClosure. under eq_bigr do rewrite /= (prodv_idPr _)//. rewrite big_prodv_eq_aspace big_enum_val/=. have /'forall_implyP/(_ _ _)/eqP/= sK := galois_normalW galkK. have gKl (i : 'I_#|kAEndf k|) : galois K (enum_val i @: l)%AS. move: (enum_val _) (enum_valP i) => s s_end. have /splitting_galoisField[/= p [pK p_sep [rs p_eq <-]]] := galKl. apply/splitting_galoisField; exists (map_poly s p); split => //=. - by rewrite -(sK _ s_end) mapf_polyOver. - by rewrite separable_map. - rewrite aimg_adjoin_seq -{1}(sK _ s_end); exists (map s rs) => //. by rewrite -map_prod_XsubC eqp_map. rewrite -(injm_sol (gal_big_prodv_cast_inj gKl))//. rewrite (solvableS (img_gal_big_prodv_cast_sub _)) ?sol_setXn// => i /=. move: (enum_val _) (enum_valP i) => s s_end; rewrite -(sK _ s_end). by rewrite -img_map_gal/= morphim_sol. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)