Metamath Proof Explorer

Theorem islnr3

Description: Relate left-Noetherian rings to Noetherian-type closure property of the left ideal system. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypotheses islnr3.b ⊢ B = Base R
islnr3.u ⊢ U = LIdeal ⁡ R
Assertion islnr3 ⊢ R ∈ LNoeR ↔ R ∈ Ring ∧ U ∈ NoeACS ⁡ B

Proof

Step Hyp Ref Expression
1 islnr3.b ⊢ B = Base R
2 islnr3.u ⊢ U = LIdeal ⁡ R
3 eqid ⊢ RSpan ⁡ R = RSpan ⁡ R
4 1 2 3 islnr2 ⊢ R ∈ LNoeR ↔ R ∈ Ring ∧ ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = RSpan ⁡ R ⁡ y
5 eqid ⊢ mrCls ⁡ U = mrCls ⁡ U
6 2 3 5 mrcrsp ⊢ R ∈ Ring → RSpan ⁡ R = mrCls ⁡ U
7 6 fveq1d ⊢ R ∈ Ring → RSpan ⁡ R ⁡ y = mrCls ⁡ U ⁡ y
8 7 eqeq2d ⊢ R ∈ Ring → x = RSpan ⁡ R ⁡ y ↔ x = mrCls ⁡ U ⁡ y
9 8 rexbidv ⊢ R ∈ Ring → ∃ y ∈ 𝒫 B ∩ Fin x = RSpan ⁡ R ⁡ y ↔ ∃ y ∈ 𝒫 B ∩ Fin x = mrCls ⁡ U ⁡ y
10 9 ralbidv ⊢ R ∈ Ring → ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = RSpan ⁡ R ⁡ y ↔ ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = mrCls ⁡ U ⁡ y
11 1 2 lidlacs ⊢ R ∈ Ring → U ∈ ACS ⁡ B
12 11 biantrurd ⊢ R ∈ Ring → ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = mrCls ⁡ U ⁡ y ↔ U ∈ ACS ⁡ B ∧ ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = mrCls ⁡ U ⁡ y
13 10 12 bitrd ⊢ R ∈ Ring → ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = RSpan ⁡ R ⁡ y ↔ U ∈ ACS ⁡ B ∧ ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = mrCls ⁡ U ⁡ y
14 5 isnacs ⊢ U ∈ NoeACS ⁡ B ↔ U ∈ ACS ⁡ B ∧ ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = mrCls ⁡ U ⁡ y
15 13 14 bitr4di ⊢ R ∈ Ring → ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = RSpan ⁡ R ⁡ y ↔ U ∈ NoeACS ⁡ B
16 15 pm5.32i ⊢ R ∈ Ring ∧ ∀ x ∈ U ∃ y ∈ 𝒫 B ∩ Fin x = RSpan ⁡ R ⁡ y ↔ R ∈ Ring ∧ U ∈ NoeACS ⁡ B
17 4 16 bitri ⊢ R ∈ LNoeR ↔ R ∈ Ring ∧ U ∈ NoeACS ⁡ B