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	|- B = ( Base ` R )
	islnr2.u	|- U = ( LIdeal ` R )
	islnr2.n	|- N = ( RSpan ` R )
Assertion	islnr2	|- ( R e. LNoeR <-> ( R e. Ring /\ A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )

Proof

Step	Hyp	Ref	Expression
1		islnr2.b	|- B = ( Base ` R )
2		islnr2.u	|- U = ( LIdeal ` R )
3		islnr2.n	|- N = ( RSpan ` R )
4		islnr	|- ( R e. LNoeR <-> ( R e. Ring /\ ( ringLMod ` R ) e. LNoeM ) )
5		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
6		rlmbas	|- ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
7	1 6	eqtri	|- B = ( Base ` ( ringLMod ` R ) )
8		lidlval	|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
9	2 8	eqtri	|- U = ( LSubSp ` ( ringLMod ` R ) )
10		rspval	|- ( RSpan ` R ) = ( LSpan ` ( ringLMod ` R ) )
11	3 10	eqtri	|- N = ( LSpan ` ( ringLMod ` R ) )
12	7 9 11	islnm2	|- ( ( ringLMod ` R ) e. LNoeM <-> ( ( ringLMod ` R ) e. LMod /\ A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
13	12	baib	|- ( ( ringLMod ` R ) e. LMod -> ( ( ringLMod ` R ) e. LNoeM <-> A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
14	5 13	syl	|- ( R e. Ring -> ( ( ringLMod ` R ) e. LNoeM <-> A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
15	14	pm5.32i	|- ( ( R e. Ring /\ ( ringLMod ` R ) e. LNoeM ) <-> ( R e. Ring /\ A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
16	4 15	bitri	|- ( R e. LNoeR <-> ( R e. Ring /\ A. i e. U E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )