Metamath Proof Explorer

Theorem islnm

Description: Property of being a Noetherian left module. (Contributed by Stefan O'Rear, 12-Dec-2014)

Ref Expression
Hypothesis islnm.s 
|- S = ( LSubSp ` M )
Assertion islnm 
|- ( M e. LNoeM <-> ( M e. LMod /\ A. i e. S ( M |`s i ) e. LFinGen ) )

Proof

Step Hyp Ref Expression
1 islnm.s 
 |-  S = ( LSubSp ` M )
2 fveq2 
 |-  ( w = M -> ( LSubSp ` w ) = ( LSubSp ` M ) )
3 2 1 eqtr4di 
 |-  ( w = M -> ( LSubSp ` w ) = S )
4 oveq1 
 |-  ( w = M -> ( w |`s i ) = ( M |`s i ) )
5 4 eleq1d 
 |-  ( w = M -> ( ( w |`s i ) e. LFinGen <-> ( M |`s i ) e. LFinGen ) )
6 3 5 raleqbidv 
 |-  ( w = M -> ( A. i e. ( LSubSp ` w ) ( w |`s i ) e. LFinGen <-> A. i e. S ( M |`s i ) e. LFinGen ) )
7 df-lnm 
 |-  LNoeM = { w e. LMod | A. i e. ( LSubSp ` w ) ( w |`s i ) e. LFinGen }
8 6 7 elrab2 
 |-  ( M e. LNoeM <-> ( M e. LMod /\ A. i e. S ( M |`s i ) e. LFinGen ) )