R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
⊢ x = 0
refine (mk_eq_zero _ _).mp (show (⟨x, hNO hx⟩ : O) = 0 from 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬⊥ < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) 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✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬⊥ < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) i = 0
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬⊥ < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) i = ↑(↑b.repr 0) i
rw [LinearEquiv.map_zero, Finsupp.zero_apply]
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬⊥ < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) i ∈
    LinearMap.submoduleImage (LinearMap.comp (Finsupp.lapply i) ↑b.repr) N
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬⊥ < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) i = 0
refine (Submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 <| hϕ (Finsupp.lapply i ∘ₗ ↑b.repr)) _ ?_
no goals
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b✝ : Basis ι R M
N O : Submodule R M
b : Basis ι R { x // x ∈ O }
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬⊥ < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
hgen : generator (LinearMap.submoduleImage ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ ↑(↑b.repr { val := x, property := (_ : x ∈ O) }) i ∈
    LinearMap.submoduleImage (LinearMap.comp (Finsupp.lapply i) ↑b.repr) N
exact (LinearMap.mem_submoduleImage_of_le hNO).mpr ⟨x, hx, rfl⟩