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 𝐵 = ( Base ‘ 𝑅 )
islnr3.u 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion islnr3 ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ 𝑈 ∈ ( NoeACS ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 islnr3.b 𝐵 = ( Base ‘ 𝑅 )
2 islnr3.u 𝑈 = ( LIdeal ‘ 𝑅 )
3 eqid ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
4 1 2 3 islnr2 ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) ) )
5 eqid ( mrCls ‘ 𝑈 ) = ( mrCls ‘ 𝑈 )
6 2 3 5 mrcrsp ( 𝑅 ∈ Ring → ( RSpan ‘ 𝑅 ) = ( mrCls ‘ 𝑈 ) )
7 6 fveq1d ( 𝑅 ∈ Ring → ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) )
8 7 eqeq2d ( 𝑅 ∈ Ring → ( 𝑥 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) ↔ 𝑥 = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) ) )
9 8 rexbidv ( 𝑅 ∈ Ring → ( ∃ 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) ) )
10 9 ralbidv ( 𝑅 ∈ Ring → ( ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) ↔ ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) ) )
11 1 2 lidlacs ( 𝑅 ∈ Ring → 𝑈 ∈ ( ACS ‘ 𝐵 ) )
12 11 biantrurd ( 𝑅 ∈ Ring → ( ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) ↔ ( 𝑈 ∈ ( ACS ‘ 𝐵 ) ∧ ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) ) ) )
13 10 12 bitrd ( 𝑅 ∈ Ring → ( ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) ↔ ( 𝑈 ∈ ( ACS ‘ 𝐵 ) ∧ ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) ) ) )
14 5 isnacs ( 𝑈 ∈ ( NoeACS ‘ 𝐵 ) ↔ ( 𝑈 ∈ ( ACS ‘ 𝐵 ) ∧ ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( mrCls ‘ 𝑈 ) ‘ 𝑦 ) ) )
15 13 14 bitr4di ( 𝑅 ∈ Ring → ( ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) ↔ 𝑈 ∈ ( NoeACS ‘ 𝐵 ) ) )
16 15 pm5.32i ( ( 𝑅 ∈ Ring ∧ ∀ 𝑥𝑈𝑦 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑦 ) ) ↔ ( 𝑅 ∈ Ring ∧ 𝑈 ∈ ( NoeACS ‘ 𝐵 ) ) )
17 4 16 bitri ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ 𝑈 ∈ ( NoeACS ‘ 𝐵 ) ) )