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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	islnr2.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
	islnr2.n	⊢ 𝑁 = ( RSpan ‘ 𝑅 )
Assertion	islnr2	⊢ ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )

Proof

Step	Hyp	Ref	Expression
1		islnr2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		islnr2.u	⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
3		islnr2.n	⊢ 𝑁 = ( RSpan ‘ 𝑅 )
4		islnr	⊢ ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ ( ringLMod ‘ 𝑅 ) ∈ LNoeM ) )
5		rlmlmod	⊢ ( 𝑅 ∈ Ring → ( ringLMod ‘ 𝑅 ) ∈ LMod )
6		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
7	1 6	eqtri	⊢ 𝐵 = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
8		lidlval	⊢ ( LIdeal ‘ 𝑅 ) = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
9	2 8	eqtri	⊢ 𝑈 = ( LSubSp ‘ ( ringLMod ‘ 𝑅 ) )
10		rspval	⊢ ( RSpan ‘ 𝑅 ) = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
11	3 10	eqtri	⊢ 𝑁 = ( LSpan ‘ ( ringLMod ‘ 𝑅 ) )
12	7 9 11	islnm2	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LNoeM ↔ ( ( ringLMod ‘ 𝑅 ) ∈ LMod ∧ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
13	12	baib	⊢ ( ( ringLMod ‘ 𝑅 ) ∈ LMod → ( ( ringLMod ‘ 𝑅 ) ∈ LNoeM ↔ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
14	5 13	syl	⊢ ( 𝑅 ∈ Ring → ( ( ringLMod ‘ 𝑅 ) ∈ LNoeM ↔ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
15	14	pm5.32i	⊢ ( ( 𝑅 ∈ Ring ∧ ( ringLMod ‘ 𝑅 ) ∈ LNoeM ) ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )
16	4 15	bitri	⊢ ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑖 ∈ 𝑈 ∃ 𝑔 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑖 = ( 𝑁 ‘ 𝑔 ) ) )