K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
⊢ ∃ a, ↑(dualMap f) a = φ
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
⊢ Function.Surjective ↑(dualMap f)
intro φ
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
⊢ ∃ a, ↑(dualMap f) a = φ
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
⊢ ∃ a, ↑(dualMap f) a = φ
let f' := LinearEquiv.ofInjective f hf
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
⊢ ↑(dualMap f) (↑(Subspace.dualLift (range f)) (↑(LinearEquiv.dualMap (LinearEquiv.symm f')) φ)) = φ
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
⊢ ∃ a, ↑(dualMap f) a = φ
use Subspace.dualLift (range f) (f'.symm.dualMap φ)
case h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑(↑(dualMap f) (↑(Subspace.dualLift (range f)) (↑(LinearEquiv.dualMap (LinearEquiv.symm f')) φ))) x = ↑φ x
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
⊢ ↑(dualMap f) (↑(Subspace.dualLift (range f)) (↑(LinearEquiv.dualMap (LinearEquiv.symm f')) φ)) = φ
ext x
case h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑φ (↑(LinearEquiv.symm f') { val := ↑f x, property := (_ : ↑f x ∈ range f) }) = ↑φ x
case h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑(↑(dualMap f) (↑(Subspace.dualLift (range f)) (↑(LinearEquiv.dualMap (LinearEquiv.symm f')) φ))) x = ↑φ x
rw [LinearMap.dualMap_apply, Subspace.dualLift_of_mem (mem_range_self f x),
  LinearEquiv.dualMap_apply]
case h.h.e_6.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑(LinearEquiv.symm f') { val := ↑f x, property := (_ : ↑f x ∈ range f) } = x
case h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑φ (↑(LinearEquiv.symm f') { val := ↑f x, property := (_ : ↑f x ∈ range f) }) = ↑φ x
congr 1
no goals
case h.h.e_6.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑(LinearEquiv.symm f') { val := ↑f x, property := (_ : ↑f x ∈ range f) } = x
exact LinearEquiv.symm_apply_apply f' x