Metamath Proof Explorer

Theorem lnmlmic

Description: Noetherian is an invariant property of modules. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion lnmlmic 
|- ( R ~=m S -> ( R e. LNoeM <-> S e. LNoeM ) )

Proof

Step Hyp Ref Expression
1 brlmic 
 |-  ( R ~=m S <-> ( R LMIso S ) =/= (/) )
2 n0 
 |-  ( ( R LMIso S ) =/= (/) <-> E. a a e. ( R LMIso S ) )
3 1 2 bitri 
 |-  ( R ~=m S <-> E. a a e. ( R LMIso S ) )
4 lmimlmhm 
 |-  ( a e. ( R LMIso S ) -> a e. ( R LMHom S ) )
5 4 adantr 
 |-  ( ( a e. ( R LMIso S ) /\ R e. LNoeM ) -> a e. ( R LMHom S ) )
6 simpr 
 |-  ( ( a e. ( R LMIso S ) /\ R e. LNoeM ) -> R e. LNoeM )
7 eqid 
 |-  ( Base ` R ) = ( Base ` R )
8 eqid 
 |-  ( Base ` S ) = ( Base ` S )
9 7 8 lmimf1o 
 |-  ( a e. ( R LMIso S ) -> a : ( Base ` R ) -1-1-onto-> ( Base ` S ) )
10 f1ofo 
 |-  ( a : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> a : ( Base ` R ) -onto-> ( Base ` S ) )
11 forn 
 |-  ( a : ( Base ` R ) -onto-> ( Base ` S ) -> ran a = ( Base ` S ) )
12 9 10 11 3syl 
 |-  ( a e. ( R LMIso S ) -> ran a = ( Base ` S ) )
13 12 adantr 
 |-  ( ( a e. ( R LMIso S ) /\ R e. LNoeM ) -> ran a = ( Base ` S ) )
14 8 lnmepi 
 |-  ( ( a e. ( R LMHom S ) /\ R e. LNoeM /\ ran a = ( Base ` S ) ) -> S e. LNoeM )
15 5 6 13 14 syl3anc 
 |-  ( ( a e. ( R LMIso S ) /\ R e. LNoeM ) -> S e. LNoeM )
16 islmim2 
 |-  ( a e. ( R LMIso S ) <-> ( a e. ( R LMHom S ) /\ `' a e. ( S LMHom R ) ) )
17 16 simprbi 
 |-  ( a e. ( R LMIso S ) -> `' a e. ( S LMHom R ) )
18 17 adantr 
 |-  ( ( a e. ( R LMIso S ) /\ S e. LNoeM ) -> `' a e. ( S LMHom R ) )
19 simpr 
 |-  ( ( a e. ( R LMIso S ) /\ S e. LNoeM ) -> S e. LNoeM )
20 dfdm4 
 |-  dom a = ran `' a
21 f1odm 
 |-  ( a : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> dom a = ( Base ` R ) )
22 9 21 syl 
 |-  ( a e. ( R LMIso S ) -> dom a = ( Base ` R ) )
23 22 adantr 
 |-  ( ( a e. ( R LMIso S ) /\ S e. LNoeM ) -> dom a = ( Base ` R ) )
24 20 23 eqtr3id 
 |-  ( ( a e. ( R LMIso S ) /\ S e. LNoeM ) -> ran `' a = ( Base ` R ) )
25 7 lnmepi 
 |-  ( ( `' a e. ( S LMHom R ) /\ S e. LNoeM /\ ran `' a = ( Base ` R ) ) -> R e. LNoeM )
26 18 19 24 25 syl3anc 
 |-  ( ( a e. ( R LMIso S ) /\ S e. LNoeM ) -> R e. LNoeM )
27 15 26 impbida 
 |-  ( a e. ( R LMIso S ) -> ( R e. LNoeM <-> S e. LNoeM ) )
28 27 exlimiv 
 |-  ( E. a a e. ( R LMIso S ) -> ( R e. LNoeM <-> S e. LNoeM ) )
29 3 28 sylbi 
 |-  ( R ~=m S -> ( R e. LNoeM <-> S e. LNoeM ) )