F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ↑(Subfield.closure (Set.range ↑(algebraMap F E) ∪ ∅)) = Set.range ↑(algebraMap F E)
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ↑⊥ = Set.range ↑(algebraMap F E)
change ↑(Subfield.closure (Set.range (algebraMap F E) ∪ ∅)) = Set.range (algebraMap F E)
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ↑(Subfield.map (algebraMap F E) (Subfield.closure Set.univ)) = ↑(algebraMap F E) '' Set.univ
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ↑(Subfield.closure (Set.range ↑(algebraMap F E) ∪ ∅)) = Set.range ↑(algebraMap F E)
rw [Set.union_empty, ← Set.image_univ, ← RingHom.map_field_closure]
no goals
F : Type u_2
inst✝² : Field F
E : Type u_1
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ ↑(Subfield.map (algebraMap F E) (Subfield.closure Set.univ)) = ↑(algebraMap F E) '' Set.univ
simp