[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I ↔ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
intro e
[GOAL]
case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
obtain ⟨r, hr, hr'⟩ :=
  Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
    (by
      rw [smul_eq_mul]
      exact e.ge)
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ I ≤ I • I
[PROOFSTEP]
rw [smul_eq_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
⊢ I ≤ I * I
[PROOFSTEP]
exact e.ge
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r • n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
simp_rw [smul_eq_mul] at hr' 
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
[PROOFSTEP]
refine' ⟨r, hr' r hr, antisymm _ ((Submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
⊢ I ≤ Submodule.span R {r}
[PROOFSTEP]
intro x hx
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ x ∈ Submodule.span R {r}
[PROOFSTEP]
rw [← hr' x hx]
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
e : IsIdempotentElem I
r : R
hr : r ∈ I
hr' : ∀ (n : R), n ∈ I → r * n = n
x : R
hx : x ∈ I
⊢ r * x ∈ Submodule.span R {r}
[PROOFSTEP]
exact Ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩
[GOAL]
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : FG I
⊢ (∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}) → IsIdempotentElem I
[PROOFSTEP]
rintro ⟨e, he, rfl⟩
[GOAL]
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
⊢ IsIdempotentElem (Submodule.span R {e})
[PROOFSTEP]
simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
[PROOFSTEP]
obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ Submodule.span R {e} = ⊥ ∨ Submodule.span R {e} = ⊤
[PROOFSTEP]
simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]
[GOAL]
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 0 ∨ span {e} = ⊤
[PROOFSTEP]
apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 1 → span {e} = ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
he : IsIdempotentElem 1
h : FG (Submodule.span R {1})
H : IsIdempotentElem (Submodule.span R {1})
⊢ span {1} = ⊤
[PROOFSTEP]
simp
[GOAL]
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : FG I
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case mpr.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : FG ⊥
⊢ IsIdempotentElem ⊥
[PROOFSTEP]
simp [IsIdempotentElem]
[GOAL]
case mpr.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : FG ⊤
⊢ IsIdempotentElem ⊤
[PROOFSTEP]
simp [IsIdempotentElem]
