Metamath Proof Explorer


Theorem lnrfg

Description: Finitely-generated modules over a Noetherian ring, being homomorphic images of free modules, are Noetherian. (Contributed by Stefan O'Rear, 7-Feb-2015)

Ref Expression
Hypothesis lnrfg.s
|- S = ( Scalar ` M )
Assertion lnrfg
|- ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM )

Proof

Step Hyp Ref Expression
1 lnrfg.s
 |-  S = ( Scalar ` M )
2 eqid
 |-  ( S freeLMod a ) = ( S freeLMod a )
3 eqid
 |-  ( Base ` ( S freeLMod a ) ) = ( Base ` ( S freeLMod a ) )
4 eqid
 |-  ( Base ` M ) = ( Base ` M )
5 eqid
 |-  ( .s ` M ) = ( .s ` M )
6 eqid
 |-  ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) )
7 fglmod
 |-  ( M e. LFinGen -> M e. LMod )
8 7 ad3antrrr
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> M e. LMod )
9 vex
 |-  a e. _V
10 9 a1i
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> a e. _V )
11 1 a1i
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> S = ( Scalar ` M ) )
12 f1oi
 |-  ( _I |` a ) : a -1-1-onto-> a
13 f1of
 |-  ( ( _I |` a ) : a -1-1-onto-> a -> ( _I |` a ) : a --> a )
14 12 13 ax-mp
 |-  ( _I |` a ) : a --> a
15 elpwi
 |-  ( a e. ~P ( Base ` M ) -> a C_ ( Base ` M ) )
16 fss
 |-  ( ( ( _I |` a ) : a --> a /\ a C_ ( Base ` M ) ) -> ( _I |` a ) : a --> ( Base ` M ) )
17 14 15 16 sylancr
 |-  ( a e. ~P ( Base ` M ) -> ( _I |` a ) : a --> ( Base ` M ) )
18 17 ad2antlr
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( _I |` a ) : a --> ( Base ` M ) )
19 2 3 4 5 6 8 10 11 18 frlmup1
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) e. ( ( S freeLMod a ) LMHom M ) )
20 simpllr
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> S e. LNoeR )
21 simprl
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> a e. Fin )
22 2 lnrfrlm
 |-  ( ( S e. LNoeR /\ a e. Fin ) -> ( S freeLMod a ) e. LNoeM )
23 20 21 22 syl2anc
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( S freeLMod a ) e. LNoeM )
24 eqid
 |-  ( LSpan ` M ) = ( LSpan ` M )
25 2 3 4 5 6 8 10 11 18 24 frlmup3
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( ( LSpan ` M ) ` ran ( _I |` a ) ) )
26 rnresi
 |-  ran ( _I |` a ) = a
27 26 fveq2i
 |-  ( ( LSpan ` M ) ` ran ( _I |` a ) ) = ( ( LSpan ` M ) ` a )
28 simprr
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( ( LSpan ` M ) ` a ) = ( Base ` M ) )
29 27 28 syl5eq
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( ( LSpan ` M ) ` ran ( _I |` a ) ) = ( Base ` M ) )
30 25 29 eqtrd
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( Base ` M ) )
31 4 lnmepi
 |-  ( ( ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) e. ( ( S freeLMod a ) LMHom M ) /\ ( S freeLMod a ) e. LNoeM /\ ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( Base ` M ) ) -> M e. LNoeM )
32 19 23 30 31 syl3anc
 |-  ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> M e. LNoeM )
33 4 24 islmodfg
 |-  ( M e. LMod -> ( M e. LFinGen <-> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) )
34 7 33 syl
 |-  ( M e. LFinGen -> ( M e. LFinGen <-> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) )
35 34 ibi
 |-  ( M e. LFinGen -> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) )
36 35 adantr
 |-  ( ( M e. LFinGen /\ S e. LNoeR ) -> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) )
37 32 36 r19.29a
 |-  ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM )