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 𝑚 S R LNoeM S LNoeM

Proof

Step Hyp Ref Expression
1 brlmic R 𝑚 S R LMIso S
2 n0 R LMIso S a a R LMIso S
3 1 2 bitri R 𝑚 S a a R LMIso S
4 lmimlmhm a R LMIso S a R LMHom S
5 4 adantr a R LMIso S R LNoeM a R LMHom S
6 simpr a R LMIso S R LNoeM R LNoeM
7 eqid Base R = Base R
8 eqid Base S = Base S
9 7 8 lmimf1o a 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 R LMIso S ran a = Base S
13 12 adantr a R LMIso S R LNoeM ran a = Base S
14 8 lnmepi a R LMHom S R LNoeM ran a = Base S S LNoeM
15 5 6 13 14 syl3anc a R LMIso S R LNoeM S LNoeM
16 islmim2 a R LMIso S a R LMHom S a -1 S LMHom R
17 16 simprbi a R LMIso S a -1 S LMHom R
18 17 adantr a R LMIso S S LNoeM a -1 S LMHom R
19 simpr a R LMIso S S LNoeM S LNoeM
20 dfdm4 dom a = ran a -1
21 f1odm a : Base R 1-1 onto Base S dom a = Base R
22 9 21 syl a R LMIso S dom a = Base R
23 22 adantr a R LMIso S S LNoeM dom a = Base R
24 20 23 eqtr3id a R LMIso S S LNoeM ran a -1 = Base R
25 7 lnmepi a -1 S LMHom R S LNoeM ran a -1 = Base R R LNoeM
26 18 19 24 25 syl3anc a R LMIso S S LNoeM R LNoeM
27 15 26 impbida a R LMIso S R LNoeM S LNoeM
28 27 exlimiv a a R LMIso S R LNoeM S LNoeM
29 3 28 sylbi R 𝑚 S R LNoeM S LNoeM