𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.649
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
f' : E →L[𝕜] { x // x ∈ range f } := codRestrict f (range f) (_ : ∀ (x : E), ↑↑f x ∈ range ↑f)
⊢ Submodule.ClosedComplemented (ker f)
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.649
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
⊢ Submodule.ClosedComplemented (ker f)
set f' : E →L[𝕜] range f := f.codRestrict _ (LinearMap.mem_range_self (f : E →ₗ[𝕜] F))
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.649
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
f' : E →L[𝕜] { x // x ∈ range f } := codRestrict f (range f) (_ : ∀ (x : E), ↑↑f x ∈ range ↑f)
g : { x // x ∈ range f } →L[𝕜] E
hg : comp f' g = id 𝕜 { x // x ∈ range f }
⊢ Submodule.ClosedComplemented (ker f)
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.649
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
f' : E →L[𝕜] { x // x ∈ range f } := codRestrict f (range f) (_ : ∀ (x : E), ↑↑f x ∈ range ↑f)
⊢ Submodule.ClosedComplemented (ker f)
rcases f'.exists_right_inverse_of_surjective (f : E →ₗ[𝕜] F).range_rangeRestrict with ⟨g, hg⟩
no goals
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type ?u.649
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : CompleteSpace 𝕜
f : E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 { x // x ∈ range f }
f' : E →L[𝕜] { x // x ∈ range f } := codRestrict f (range f) (_ : ∀ (x : E), ↑↑f x ∈ range ↑f)
g : { x // x ∈ range f } →L[𝕜] E
hg : comp f' g = id 𝕜 { x // x ∈ range f }
⊢ Submodule.ClosedComplemented (ker f)
simpa only [ker_codRestrict] using f'.closedComplemented_ker_of_rightInverse g (ext_iff.1 hg)