R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
⊢ ∀ (x : M), x ∈ N → x = 0
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
⊢ N = ⊥
rw [Submodule.eq_bot_iff]
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
⊢ x = 0
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
⊢ ∀ (x : M), x ∈ N → x = 0
intro x hx
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr x) i = ↑(↑b.repr 0) i
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
⊢ x = 0
refine' b.ext_elem fun i ↦ _
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr x) i = ↑(↑b.repr 0) i
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬map ϕ N < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr x) i = ↑(↑b.repr 0) i
rw [(eq_bot_iff_generator_eq_zero _).mpr hgen] at hϕ
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr x) i = 0
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr x) i = ↑(↑b.repr 0) i
rw [LinearEquiv.map_zero, Finsupp.zero_apply]
no goals
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < map ψ N
inst✝ : IsPrincipal (map ϕ N)
hgen : generator (map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr x) i = 0
exact
  (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _
    ⟨x, hx, rfl⟩