[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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)
[PROOFSTEP]
set f' : E →L[𝕜] range f := f.codRestrict _ (LinearMap.mem_range_self (f : E →ₗ[𝕜] F))
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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)
[PROOFSTEP]
rcases f'.exists_right_inverse_of_surjective (f : E →ₗ[𝕜] F).range_rangeRestrict with ⟨g, hg⟩
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
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)
[PROOFSTEP]
simpa only [ker_codRestrict] using f'.closedComplemented_ker_of_rightInverse g (ext_iff.1 hg)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
⊢ ({ x // x ∈ p } × { x // x ∈ q }) ≃L[𝕜] E
[PROOFSTEP]
haveI := hp.completeSpace_coe
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
this : CompleteSpace ↑↑p
⊢ ({ x // x ∈ p } × { x // x ∈ q }) ≃L[𝕜] E
[PROOFSTEP]
haveI := hq.completeSpace_coe
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
this✝ : CompleteSpace ↑↑p
this : CompleteSpace ↑↑q
⊢ ({ x // x ∈ p } × { x // x ∈ q }) ≃L[𝕜] E
[PROOFSTEP]
refine' (p.prodEquivOfIsCompl q h).toContinuousLinearEquivOfContinuous _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace E
p q : Subspace 𝕜 E
h : IsCompl p q
hp : IsClosed ↑p
hq : IsClosed ↑q
this✝ : CompleteSpace ↑↑p
this : CompleteSpace ↑↑q
⊢ Continuous ↑(Submodule.prodEquivOfIsCompl p q h)
[PROOFSTEP]
exact (p.subtypeL.coprod q.subtypeL).continuous
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
⊢ Submodule.ClosedComplemented p
[PROOFSTEP]
obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
⊢ Submodule.ClosedComplemented p
[PROOFSTEP]
haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
this : FiniteDimensional 𝕜 { x // x ∈ q }
⊢ Submodule.ClosedComplemented p
[PROOFSTEP]
exact closedComplemented_of_closed_compl hq hp q.closed_of_finiteDimensional
