case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b → Fintype.card ι = Set.finrank K (Set.range b)

case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Fintype.card ι = Set.finrank K (Set.range b) → LinearIndependent K b
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (Set.range b)
constructor
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
h : LinearIndependent K b
⊢ Fintype.card ι = Set.finrank K (Set.range b)
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b → Fintype.card ι = Set.finrank K (Set.range b)
intro h
no goals
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
h : LinearIndependent K b
⊢ Fintype.card ι = Set.finrank K (Set.range b)
exact (finrank_span_eq_card h).symm
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
⊢ LinearIndependent K b
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Fintype.card ι = Set.finrank K (Set.range b) → LinearIndependent K b
intro hc
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
⊢ LinearIndependent K b
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
⊢ LinearIndependent K b
let f := Submodule.subtype (span K (Set.range b))
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
⊢ LinearIndependent K b
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
⊢ LinearIndependent K b
let b' : ι → span K (Set.range b) := fun i =>
  ⟨b i, mem_span.2 fun p hp => hp (Set.mem_range_self _)⟩
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
⊢ LinearIndependent K b
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
⊢ LinearIndependent K b
have hs : ⊤ ≤ span K (Set.range b') := by
  intro x
  have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
  have hf : f '' Set.range b' = Set.range b := by
    ext x
    simp [Set.mem_image, Set.mem_range]
  rw [hf] at h
  have hx : (x : V) ∈ span K (Set.range b) := x.property
  conv at hx =>
    arg 2
    rw [h]
  simpa [mem_map] using hx
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
hi : LinearMap.ker f = ⊥
⊢ LinearIndependent K b
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
⊢ LinearIndependent K b
have hi : LinearMap.ker f = ⊥ := ker_subtype _
no goals
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
hi : LinearMap.ker f = ⊥
⊢ LinearIndependent K b
convert (linearIndependent_of_top_le_span_of_card_eq_finrank hs hc).map' _ hi
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
⊢ ⊤ ≤ span K (Set.range b')
intro x
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
have hf : f '' Set.range b' = Set.range b := by
  ext x
  simp [Set.mem_image, Set.mem_range]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
rw [hf] at h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
have hx : (x : V) ∈ span K (Set.range b) := x.property
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
conv at hx =>
  arg 2
  rw [h]
no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
simpa [mem_map] using hx
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x✝ : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
x : V
⊢ x ∈ ↑f '' Set.range b' ↔ x ∈ Set.range b
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
⊢ ↑f '' Set.range b' = Set.range b
ext x
no goals
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x✝ : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
x : V
⊢ x ∈ ↑f '' Set.range b' ↔ x ∈ Set.range b
simp [Set.mem_image, Set.mem_range]