Theorem islnm2

Description: Property of being a Noetherian left module with finite generation expanded in terms of spans. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	islnm2.b	|- B = ( Base ` M )
	islnm2.s	|- S = ( LSubSp ` M )
	islnm2.n	|- N = ( LSpan ` M )
Assertion	islnm2	|- ( M e. LNoeM <-> ( M e. LMod /\ A. i e. S E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )

Proof

Step	Hyp	Ref	Expression
1		islnm2.b	|- B = ( Base ` M )
2		islnm2.s	|- S = ( LSubSp ` M )
3		islnm2.n	|- N = ( LSpan ` M )
4	2	islnm	|- ( M e. LNoeM <-> ( M e. LMod /\ A. i e. S ( M |`s i ) e. LFinGen ) )
5		eqid	|- ( M |`s i ) = ( M |`s i )
6	5 2 3 1	islssfg2	|- ( ( M e. LMod /\ i e. S ) -> ( ( M |`s i ) e. LFinGen <-> E. g e. ( ~P B i^i Fin ) ( N ` g ) = i ) )
7		eqcom	|- ( ( N ` g ) = i <-> i = ( N ` g ) )
8	7	rexbii	|- ( E. g e. ( ~P B i^i Fin ) ( N ` g ) = i <-> E. g e. ( ~P B i^i Fin ) i = ( N ` g ) )
9	6 8	bitrdi	|- ( ( M e. LMod /\ i e. S ) -> ( ( M |`s i ) e. LFinGen <-> E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
10	9	ralbidva	|- ( M e. LMod -> ( A. i e. S ( M |`s i ) e. LFinGen <-> A. i e. S E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
11	10	pm5.32i	|- ( ( M e. LMod /\ A. i e. S ( M |`s i ) e. LFinGen ) <-> ( M e. LMod /\ A. i e. S E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )
12	4 11	bitri	|- ( M e. LNoeM <-> ( M e. LMod /\ A. i e. S E. g e. ( ~P B i^i Fin ) i = ( N ` g ) ) )