[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hf : IsClosable f
hfg : g ≤ f
⊢ IsClosable g
[PROOFSTEP]
cases' hf with f' hf
[GOAL]
case intro
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
⊢ IsClosable g
[PROOFSTEP]
have : g.graph.topologicalClosure ≤ f'.graph := by
  rw [← hf]
  exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
⊢ Submodule.topologicalClosure (graph g) ≤ graph f'
[PROOFSTEP]
rw [← hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
⊢ Submodule.topologicalClosure (graph g) ≤ Submodule.topologicalClosure (graph f)
[PROOFSTEP]
exact Submodule.topologicalClosure_mono (le_graph_of_le hfg)
[GOAL]
case intro
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
this : Submodule.topologicalClosure (graph g) ≤ graph f'
⊢ IsClosable g
[PROOFSTEP]
use g.graph.topologicalClosure.toLinearPMap
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
this : Submodule.topologicalClosure (graph g) ≤ graph f'
⊢ Submodule.topologicalClosure (graph g) = graph (Submodule.toLinearPMap (Submodule.topologicalClosure (graph g)))
[PROOFSTEP]
rw [Submodule.toLinearPMap_graph_eq]
[GOAL]
case h.hg
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hfg : g ≤ f
f' : E →ₗ.[R] F
hf : Submodule.topologicalClosure (graph f) = graph f'
this : Submodule.topologicalClosure (graph g) ≤ graph f'
⊢ ∀ (x : E × F), x ∈ Submodule.topologicalClosure (graph g) → x.fst = 0 → x.snd = 0
[PROOFSTEP]
exact fun _ hx hx' => f'.graph_fst_eq_zero_snd (this hx) hx'
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ ∃! f', Submodule.topologicalClosure (graph f) = graph f'
[PROOFSTEP]
refine' exists_unique_of_exists_of_unique hf fun _ _ hy₁ hy₂ => eq_of_eq_graph _
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
x✝¹ x✝ : E →ₗ.[R] F
hy₁ : Submodule.topologicalClosure (graph f) = graph x✝¹
hy₂ : Submodule.topologicalClosure (graph f) = graph x✝
⊢ graph x✝¹ = graph x✝
[PROOFSTEP]
rw [← hy₁, ← hy₂]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ closure f = Exists.choose hf
[PROOFSTEP]
simp [closure, hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬IsClosable f
⊢ closure f = f
[PROOFSTEP]
simp [closure, hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ Submodule.topologicalClosure (graph f) = graph (closure f)
[PROOFSTEP]
rw [closure_def hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ Submodule.topologicalClosure (graph f) = graph (Exists.choose hf)
[PROOFSTEP]
exact hf.choose_spec
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ f ≤ closure f
[PROOFSTEP]
by_cases hf : f.IsClosable
[GOAL]
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ f ≤ closure f
[PROOFSTEP]
refine' le_of_le_graph _
[GOAL]
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ graph f ≤ graph (closure f)
[PROOFSTEP]
rw [← hf.graph_closure_eq_closure_graph]
[GOAL]
case pos
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ graph f ≤ Submodule.topologicalClosure (graph f)
[PROOFSTEP]
exact (graph f).le_topologicalClosure
[GOAL]
case neg
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : ¬IsClosable f
⊢ f ≤ closure f
[PROOFSTEP]
rw [closure_def' hf]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ closure f ≤ closure g
[PROOFSTEP]
refine' le_of_le_graph _
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ graph (closure f) ≤ graph (closure g)
[PROOFSTEP]
rw [← (hg.leIsClosable h).graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ Submodule.topologicalClosure (graph f) ≤ graph (closure g)
[PROOFSTEP]
rw [← hg.graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f g : E →ₗ.[R] F
hg : IsClosable g
h : f ≤ g
⊢ Submodule.topologicalClosure (graph f) ≤ Submodule.topologicalClosure (graph g)
[PROOFSTEP]
exact Submodule.topologicalClosure_mono (le_graph_of_le h)
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ IsClosed (closure f)
[PROOFSTEP]
rw [IsClosed, ← hf.graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : IsClosable f
⊢ _root_.IsClosed ↑(Submodule.topologicalClosure (graph f))
[PROOFSTEP]
exact f.graph.isClosed_topologicalClosure
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ HasCore (closure f) f.domain
[PROOFSTEP]
refine' ⟨f.le_closure.1, _⟩
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ closure (domRestrict (closure f) f.domain) = closure f
[PROOFSTEP]
congr
[GOAL]
case e_f
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
⊢ domRestrict (closure f) f.domain = f
[PROOFSTEP]
ext x y hxy
[GOAL]
case e_f.h.h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
⊢ x ∈ (domRestrict (closure f) f.domain).domain ↔ x ∈ f.domain
[PROOFSTEP]
simp only [domRestrict_domain, Submodule.mem_inf, and_iff_left_iff_imp]
[GOAL]
case e_f.h.h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
⊢ x ∈ f.domain → x ∈ (closure f).domain
[PROOFSTEP]
intro hx
[GOAL]
case e_f.h.h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : E
hx : x ∈ f.domain
⊢ x ∈ (closure f).domain
[PROOFSTEP]
exact f.le_closure.1 hx
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
⊢ ↑(domRestrict (closure f) f.domain) x = ↑f y
[PROOFSTEP]
let z : f.closure.domain := ⟨y.1, f.le_closure.1 y.2⟩
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
⊢ ↑(domRestrict (closure f) f.domain) x = ↑f y
[PROOFSTEP]
have hyz : (y : E) = z := by simp
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
⊢ ↑y = ↑z
[PROOFSTEP]
simp
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
hyz : ↑y = ↑z
⊢ ↑(domRestrict (closure f) f.domain) x = ↑f y
[PROOFSTEP]
rw [f.le_closure.2 hyz]
[GOAL]
case e_f.h'
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
x : { x // x ∈ (domRestrict (closure f) f.domain).domain }
y : { x // x ∈ f.domain }
hxy : ↑x = ↑y
z : { x // x ∈ (closure f).domain } := { val := ↑y, property := (_ : ↑y ∈ (closure f).domain) }
hyz : ↑y = ↑z
⊢ ↑(domRestrict (closure f) f.domain) x = ↑(closure f) z
[PROOFSTEP]
exact domRestrict_apply (hxy.trans hyz)
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ graph (inverse (closure f)) = Submodule.topologicalClosure (graph (inverse f))
[PROOFSTEP]
rw [inverse_graph hf, inverse_graph hcf, ← hf'.graph_closure_eq_closure_graph]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ Submodule.map (LinearEquiv.prodComm R E F) (Submodule.topologicalClosure (graph f)) =
    Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f))
[PROOFSTEP]
apply SetLike.ext'
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ ↑(Submodule.map (LinearEquiv.prodComm R E F) (Submodule.topologicalClosure (graph f))) =
    ↑(Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f)))
[PROOFSTEP]
simp only [Submodule.topologicalClosure_coe, Submodule.map_coe, LinearEquiv.prodComm_apply]
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ (fun a => Prod.swap a) '' _root_.closure ↑(graph f) = _root_.closure ((fun a => Prod.swap a) '' ↑(graph f))
[PROOFSTEP]
apply (image_closure_subset_closure_image continuous_swap).antisymm
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
have h1 := Set.image_equiv_eq_preimage_symm f.graph (LinearEquiv.prodComm R E F).toEquiv
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 :
  ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)) '' ↑(graph f) =
    ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)).symm ⁻¹' ↑(graph f)
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
have h2 := Set.image_equiv_eq_preimage_symm (_root_.closure f.graph) (LinearEquiv.prodComm R E F).toEquiv
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 :
  ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)) '' ↑(graph f) =
    ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)).symm ⁻¹' ↑(graph f)
h2 :
  ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)) '' _root_.closure ↑(graph f) =
    ↑(LinearEquiv.toEquiv (LinearEquiv.prodComm R E F)).symm ⁻¹' _root_.closure ↑(graph f)
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
simp only [LinearEquiv.coe_toEquiv, LinearEquiv.prodComm_apply, LinearEquiv.coe_toEquiv_symm] at h1 h2 
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 : (fun a => Prod.swap a) '' ↑(graph f) = ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' ↑(graph f)
h2 :
  (fun a => Prod.swap a) '' _root_.closure ↑(graph f) =
    ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' _root_.closure ↑(graph f)
⊢ _root_.closure (Prod.swap '' ↑(graph f)) ⊆ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
rw [h1, h2]
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
h1 : (fun a => Prod.swap a) '' ↑(graph f) = ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' ↑(graph f)
h2 :
  (fun a => Prod.swap a) '' _root_.closure ↑(graph f) =
    ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' _root_.closure ↑(graph f)
⊢ _root_.closure (↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' ↑(graph f)) ⊆
    ↑↑(LinearEquiv.symm (LinearEquiv.prodComm R E F)) ⁻¹' _root_.closure ↑(graph f)
[PROOFSTEP]
apply continuous_swap.closure_preimage_subset
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
⊢ IsClosable (inverse f) ↔ LinearMap.ker (closure f).toFun = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
⊢ IsClosable (inverse f) → LinearMap.ker (closure f).toFun = ⊥
[PROOFSTEP]
intro ⟨f', h⟩
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
⊢ LinearMap.ker (closure f).toFun = ⊥
[PROOFSTEP]
rw [LinearMap.ker_eq_bot']
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
⊢ ∀ (m : { x // x ∈ (closure f).domain }), ↑(closure f).toFun m = 0 → m = 0
[PROOFSTEP]
intro ⟨x, hx⟩ hx'
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : ↑(closure f).toFun { val := x, property := hx } = 0
⊢ { val := x, property := hx } = 0
[PROOFSTEP]
simp only [Submodule.mk_eq_zero]
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : ↑(closure f).toFun { val := x, property := hx } = 0
⊢ x = 0
[PROOFSTEP]
rw [toFun_eq_coe, eq_comm, image_iff] at hx' 
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
⊢ x = 0
[PROOFSTEP]
have : (0, x) ∈ graph f'
[GOAL]
case this
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
⊢ (0, x) ∈ graph f'
[PROOFSTEP]
rw [← h, inverse_graph hf]
[GOAL]
case this
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
⊢ (0, x) ∈ Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f))
[PROOFSTEP]
rw [← hf'.graph_closure_eq_closure_graph, ← SetLike.mem_coe, Submodule.topologicalClosure_coe] at hx' 
[GOAL]
case this
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ _root_.closure ↑(graph f)
⊢ (0, x) ∈ Submodule.topologicalClosure (Submodule.map (LinearEquiv.prodComm R E F) (graph f))
[PROOFSTEP]
apply image_closure_subset_closure_image continuous_swap
[GOAL]
case this.a
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ _root_.closure ↑(graph f)
⊢ (0, x) ∈ Prod.swap '' _root_.closure ↑(graph f)
[PROOFSTEP]
simp only [Set.mem_image, Prod.exists, Prod.swap_prod_mk, Prod.mk.injEq]
[GOAL]
case this.a
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ _root_.closure ↑(graph f)
⊢ ∃ a b, (a, b) ∈ _root_.closure ↑(graph f) ∧ b = 0 ∧ a = x
[PROOFSTEP]
exact ⟨x, 0, hx', rfl, rfl⟩
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
f' : F →ₗ.[R] E
h : Submodule.topologicalClosure (graph (inverse f)) = graph f'
x : E
hx : x ∈ (closure f).domain
hx' : (x, 0) ∈ graph (closure f)
this : (0, x) ∈ graph f'
⊢ x = 0
[PROOFSTEP]
exact graph_fst_eq_zero_snd f' this rfl
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
⊢ LinearMap.ker (closure f).toFun = ⊥ → IsClosable (inverse f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
h : LinearMap.ker (closure f).toFun = ⊥
⊢ IsClosable (inverse f)
[PROOFSTEP]
use f.closure.inverse
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
h : LinearMap.ker (closure f).toFun = ⊥
⊢ Submodule.topologicalClosure (graph (inverse f)) = graph (inverse (closure f))
[PROOFSTEP]
exact (closure_inverse_graph hf hf' h).symm
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ closure (inverse f) = inverse (closure f)
[PROOFSTEP]
apply eq_of_eq_graph
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
hf' : IsClosable f
hcf : LinearMap.ker (closure f).toFun = ⊥
⊢ graph (closure (inverse f)) = graph (inverse (closure f))
[PROOFSTEP]
rw [closure_inverse_graph hf hf' hcf, ((inverse_isClosable_iff hf hf').mpr hcf).graph_closure_eq_closure_graph]
