Metamath Proof Explorer

Theorem filnm

Description: Finite left modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis filnm.b 
|- B = ( Base ` W )
Assertion filnm 
|- ( ( W e. LMod /\ B e. Fin ) -> W e. LNoeM )

Proof

Step Hyp Ref Expression
1 filnm.b 
 |-  B = ( Base ` W )
2 simpl 
 |-  ( ( W e. LMod /\ B e. Fin ) -> W e. LMod )
3 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
4 1 3 lssss 
 |-  ( a e. ( LSubSp ` W ) -> a C_ B )
5 4 adantl 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> a C_ B )
6 velpw 
 |-  ( a e. ~P B <-> a C_ B )
7 5 6 sylibr 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> a e. ~P B )
8 simplr 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> B e. Fin )
9 ssfi 
 |-  ( ( B e. Fin /\ a C_ B ) -> a e. Fin )
10 8 5 9 syl2anc 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> a e. Fin )
11 7 10 elind 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> a e. ( ~P B i^i Fin ) )
12 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
13 3 12 lspid 
 |-  ( ( W e. LMod /\ a e. ( LSubSp ` W ) ) -> ( ( LSpan ` W ) ` a ) = a )
14 13 adantlr 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> ( ( LSpan ` W ) ` a ) = a )
15 14 eqcomd 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> a = ( ( LSpan ` W ) ` a ) )
16 fveq2 
 |-  ( b = a -> ( ( LSpan ` W ) ` b ) = ( ( LSpan ` W ) ` a ) )
17 16 rspceeqv 
 |-  ( ( a e. ( ~P B i^i Fin ) /\ a = ( ( LSpan ` W ) ` a ) ) -> E. b e. ( ~P B i^i Fin ) a = ( ( LSpan ` W ) ` b ) )
18 11 15 17 syl2anc 
 |-  ( ( ( W e. LMod /\ B e. Fin ) /\ a e. ( LSubSp ` W ) ) -> E. b e. ( ~P B i^i Fin ) a = ( ( LSpan ` W ) ` b ) )
19 18 ralrimiva 
 |-  ( ( W e. LMod /\ B e. Fin ) -> A. a e. ( LSubSp ` W ) E. b e. ( ~P B i^i Fin ) a = ( ( LSpan ` W ) ` b ) )
20 1 3 12 islnm2 
 |-  ( W e. LNoeM <-> ( W e. LMod /\ A. a e. ( LSubSp ` W ) E. b e. ( ~P B i^i Fin ) a = ( ( LSpan ` W ) ` b ) ) )
21 2 19 20 sylanbrc 
 |-  ( ( W e. LMod /\ B e. Fin ) -> W e. LNoeM )