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 ‘ 𝐵 ) ) )