R : Type u_3
M : Type u_2
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ Submodule.span R (e '' H)
i : ι
hi : ↑(ε i) x ≠ 0
⊢ i ∈ H
R : Type u_3
M : Type u_2
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ Submodule.span R (e '' H)
⊢ ∀ (i : ι), ↑(ε i) x ≠ 0 → i ∈ H
intro i hi
case intro.intro
R : Type u_3
M : Type u_2
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : ↑(Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)
hi : ↑(ε i) (↑(Finsupp.total ι M R e) l) ≠ 0
⊢ i ∈ H
R : Type u_3
M : Type u_2
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ Submodule.span R (e '' H)
i : ι
hi : ↑(ε i) x ≠ 0
⊢ i ∈ H
rcases(Finsupp.mem_span_image_iff_total _).mp hmem with ⟨l, supp_l, rfl⟩
case intro.intro
R : Type u_3
M : Type u_2
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : ↑(Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)
hi : ↑(ε i) (↑(Finsupp.total ι M R e) l) ≠ 0
⊢ ¬↑l i = 0
case intro.intro
R : Type u_3
M : Type u_2
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : ↑(Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)
hi : ↑(ε i) (↑(Finsupp.total ι M R e) l) ≠ 0
⊢ i ∈ H
apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)
no goals
case intro.intro
R : Type u_3
M : Type u_2
ι : Type u_1
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : ↑(Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)
hi : ↑(ε i) (↑(Finsupp.total ι M R e) l) ≠ 0
⊢ ¬↑l i = 0
rwa [← lc_def, h.dual_lc] at hi