Metamath Proof Explorer

Theorem islnr2

Description: Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses islnr2.b ⊢ B = Base R
islnr2.u ⊢ U = LIdeal ⁡ R
islnr2.n ⊢ N = RSpan ⁡ R
Assertion islnr2 ⊢ R ∈ LNoeR ↔ R ∈ Ring ∧ ∀ i ∈ U ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g

Proof

Step Hyp Ref Expression
1 islnr2.b ⊢ B = Base R
2 islnr2.u ⊢ U = LIdeal ⁡ R
3 islnr2.n ⊢ N = RSpan ⁡ R
4 islnr ⊢ R ∈ LNoeR ↔ R ∈ Ring ∧ ringLMod ⁡ R ∈ LNoeM
5 rlmlmod ⊢ R ∈ Ring → ringLMod ⁡ R ∈ LMod
6 rlmbas ⊢ Base R = Base ringLMod ⁡ R
7 1 6 eqtri ⊢ B = Base ringLMod ⁡ R
8 lidlval ⊢ LIdeal ⁡ R = LSubSp ⁡ ringLMod ⁡ R
9 2 8 eqtri ⊢ U = LSubSp ⁡ ringLMod ⁡ R
10 rspval ⊢ RSpan ⁡ R = LSpan ⁡ ringLMod ⁡ R
11 3 10 eqtri ⊢ N = LSpan ⁡ ringLMod ⁡ R
12 7 9 11 islnm2 ⊢ ringLMod ⁡ R ∈ LNoeM ↔ ringLMod ⁡ R ∈ LMod ∧ ∀ i ∈ U ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
13 12 baib ⊢ ringLMod ⁡ R ∈ LMod → ringLMod ⁡ R ∈ LNoeM ↔ ∀ i ∈ U ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
14 5 13 syl ⊢ R ∈ Ring → ringLMod ⁡ R ∈ LNoeM ↔ ∀ i ∈ U ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
15 14 pm5.32i ⊢ R ∈ Ring ∧ ringLMod ⁡ R ∈ LNoeM ↔ R ∈ Ring ∧ ∀ i ∈ U ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g
16 4 15 bitri ⊢ R ∈ LNoeR ↔ R ∈ Ring ∧ ∀ i ∈ U ∃ g ∈ 𝒫 B ∩ Fin i = N ⁡ g