ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
⊢ ∀ (l : ι' →₀ R), ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0 → l = 0
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
⊢ LinearIndependent R (v ∘ f)
rw [linearIndependent_iff, Finsupp.total_comp]
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
⊢ l = 0
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
⊢ ∀ (l : ι' →₀ R), ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0 → l = 0
intro l hl
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
h_map_domain : ∀ (x : ι'), ↑(Finsupp.mapDomain f l) (f x) = 0
⊢ l = 0
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
⊢ l = 0
have h_map_domain : ∀ x, (Finsupp.mapDomain f l) (f x) = 0 := by
  rw [linearIndependent_iff.1 h (Finsupp.mapDomain f l) hl]; simp
case h
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
h_map_domain : ∀ (x : ι'), ↑(Finsupp.mapDomain f l) (f x) = 0
x : ι'
⊢ ↑l x = ↑0 x
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
h_map_domain : ∀ (x : ι'), ↑(Finsupp.mapDomain f l) (f x) = 0
⊢ l = 0
ext x
case h.e'_2
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
h_map_domain : ∀ (x : ι'), ↑(Finsupp.mapDomain f l) (f x) = 0
x : ι'
⊢ ↑l x = ↑(Finsupp.mapDomain f l) (f x)
case h
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
h_map_domain : ∀ (x : ι'), ↑(Finsupp.mapDomain f l) (f x) = 0
x : ι'
⊢ ↑l x = ↑0 x
convert h_map_domain x
no goals
case h.e'_2
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x✝ y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
h_map_domain : ∀ (x : ι'), ↑(Finsupp.mapDomain f l) (f x) = 0
x : ι'
⊢ ↑l x = ↑(Finsupp.mapDomain f l) (f x)
rw [Finsupp.mapDomain_apply hf]
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
⊢ ∀ (x : ι'), ↑0 (f x) = 0
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
⊢ ∀ (x : ι'), ↑(Finsupp.mapDomain f l) (f x) = 0
rw [linearIndependent_iff.1 h (Finsupp.mapDomain f l) hl]
no goals
ι : Type u'
ι' : Type u_3
R : Type u_1
K : Type ?u.86731
M : Type u_2
M' : Type ?u.86737
M'' : Type ?u.86740
V : Type u
V' : Type ?u.86745
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M''
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : Module R M''
a b : R
x y : M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
l : ι' →₀ R
hl : ↑(LinearMap.comp (Finsupp.total ι M R v) (Finsupp.lmapDomain R R f)) l = 0
⊢ ∀ (x : ι'), ↑0 (f x) = 0
simp