Metamath Proof Explorer

Theorem lnmepi

Description: Epimorphic images of Noetherian modules are Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypothesis lnmepi.b 
|- B = ( Base ` T )
Assertion lnmepi 
|- ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> T e. LNoeM )

Proof

Step Hyp Ref Expression
1 lnmepi.b 
 |-  B = ( Base ` T )
2 lmhmlmod2 
 |-  ( F e. ( S LMHom T ) -> T e. LMod )
3 2 3ad2ant1 
 |-  ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> T e. LMod )
4 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 4 1 lmhmf 
 |-  ( F e. ( S LMHom T ) -> F : ( Base ` S ) --> B )
6 5 3ad2ant1 
 |-  ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> F : ( Base ` S ) --> B )
7 simp3 
 |-  ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> ran F = B )
8 dffo2 
 |-  ( F : ( Base ` S ) -onto-> B <-> ( F : ( Base ` S ) --> B /\ ran F = B ) )
9 6 7 8 sylanbrc 
 |-  ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> F : ( Base ` S ) -onto-> B )
10 eqid 
 |-  ( LSubSp ` T ) = ( LSubSp ` T )
11 1 10 lssss 
 |-  ( a e. ( LSubSp ` T ) -> a C_ B )
12 foimacnv 
 |-  ( ( F : ( Base ` S ) -onto-> B /\ a C_ B ) -> ( F " ( `' F " a ) ) = a )
13 9 11 12 syl2an 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> ( F " ( `' F " a ) ) = a )
14 13 oveq2d 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> ( T |`s ( F " ( `' F " a ) ) ) = ( T |`s a ) )
15 eqid 
 |-  ( T |`s ( F " ( `' F " a ) ) ) = ( T |`s ( F " ( `' F " a ) ) )
16 eqid 
 |-  ( S |`s ( `' F " a ) ) = ( S |`s ( `' F " a ) )
17 eqid 
 |-  ( LSubSp ` S ) = ( LSubSp ` S )
18 simpl2 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> S e. LNoeM )
19 17 10 lmhmpreima 
 |-  ( ( F e. ( S LMHom T ) /\ a e. ( LSubSp ` T ) ) -> ( `' F " a ) e. ( LSubSp ` S ) )
20 19 3ad2antl1 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> ( `' F " a ) e. ( LSubSp ` S ) )
21 17 16 lnmlssfg 
 |-  ( ( S e. LNoeM /\ ( `' F " a ) e. ( LSubSp ` S ) ) -> ( S |`s ( `' F " a ) ) e. LFinGen )
22 18 20 21 syl2anc 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> ( S |`s ( `' F " a ) ) e. LFinGen )
23 simpl1 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> F e. ( S LMHom T ) )
24 15 16 17 22 20 23 lmhmfgima 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> ( T |`s ( F " ( `' F " a ) ) ) e. LFinGen )
25 14 24 eqeltrrd 
 |-  ( ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) /\ a e. ( LSubSp ` T ) ) -> ( T |`s a ) e. LFinGen )
26 25 ralrimiva 
 |-  ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> A. a e. ( LSubSp ` T ) ( T |`s a ) e. LFinGen )
27 10 islnm 
 |-  ( T e. LNoeM <-> ( T e. LMod /\ A. a e. ( LSubSp ` T ) ( T |`s a ) e. LFinGen ) )
28 3 26 27 sylanbrc 
 |-  ( ( F e. ( S LMHom T ) /\ S e. LNoeM /\ ran F = B ) -> T e. LNoeM )