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=BaseR
islnr3.u ⊢U=LIdeal⁡R
Assertion islnr3 ⊢R∈LNoeR↔R∈Ring∧U∈NoeACS⁡B

Proof

Step Hyp Ref Expression
1 islnr3.b ⊢B=BaseR
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∩Finx=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∩Finx=RSpan⁡R⁡y↔∃y∈𝒫B∩Finx=mrCls⁡U⁡y
10 9 ralbidv ⊢R∈Ring→∀x∈U∃y∈𝒫B∩Finx=RSpan⁡R⁡y↔∀x∈U∃y∈𝒫B∩Finx=mrCls⁡U⁡y
11 1 2 lidlacs ⊢R∈Ring→U∈ACS⁡B
12 11 biantrurd ⊢R∈Ring→∀x∈U∃y∈𝒫B∩Finx=mrCls⁡U⁡y↔U∈ACS⁡B∧∀x∈U∃y∈𝒫B∩Finx=mrCls⁡U⁡y
13 10 12 bitrd ⊢R∈Ring→∀x∈U∃y∈𝒫B∩Finx=RSpan⁡R⁡y↔U∈ACS⁡B∧∀x∈U∃y∈𝒫B∩Finx=mrCls⁡U⁡y
14 5 isnacs ⊢U∈NoeACS⁡B↔U∈ACS⁡B∧∀x∈U∃y∈𝒫B∩Finx=mrCls⁡U⁡y
15 13 14 bitr4di ⊢R∈Ring→∀x∈U∃y∈𝒫B∩Finx=RSpan⁡R⁡y↔U∈NoeACS⁡B
16 15 pm5.32i ⊢R∈Ring∧∀x∈U∃y∈𝒫B∩Finx=RSpan⁡R⁡y↔R∈Ring∧U∈NoeACS⁡B
17 4 16 bitri ⊢R∈LNoeR↔R∈Ring∧U∈NoeACS⁡B