Metamath Proof Explorer

Theorem pwslnm

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

Ref Expression
Hypothesis pwslnm.y ⊢Y=W↑𝑠I
Assertion pwslnm ⊢W∈LNoeM∧I∈Fin→Y∈LNoeM

Proof

Step Hyp Ref Expression
1 pwslnm.y ⊢Y=W↑𝑠I
2 oveq2 ⊢a=∅→W↑𝑠a=W↑𝑠∅
3 2 eleq1d ⊢a=∅→W↑𝑠a∈LNoeM↔W↑𝑠∅∈LNoeM
4 3 imbi2d ⊢a=∅→W∈LNoeM→W↑𝑠a∈LNoeM↔W∈LNoeM→W↑𝑠∅∈LNoeM
5 oveq2 ⊢a=b→W↑𝑠a=W↑𝑠b
6 5 eleq1d ⊢a=b→W↑𝑠a∈LNoeM↔W↑𝑠b∈LNoeM
7 6 imbi2d ⊢a=b→W∈LNoeM→W↑𝑠a∈LNoeM↔W∈LNoeM→W↑𝑠b∈LNoeM
8 oveq2 ⊢a=b∪c→W↑𝑠a=W↑𝑠b∪c
9 8 eleq1d ⊢a=b∪c→W↑𝑠a∈LNoeM↔W↑𝑠b∪c∈LNoeM
10 9 imbi2d ⊢a=b∪c→W∈LNoeM→W↑𝑠a∈LNoeM↔W∈LNoeM→W↑𝑠b∪c∈LNoeM
11 oveq2 ⊢a=I→W↑𝑠a=W↑𝑠I
12 11 eleq1d ⊢a=I→W↑𝑠a∈LNoeM↔W↑𝑠I∈LNoeM
13 12 imbi2d ⊢a=I→W∈LNoeM→W↑𝑠a∈LNoeM↔W∈LNoeM→W↑𝑠I∈LNoeM
14 lnmlmod ⊢W∈LNoeM→W∈LMod
15 eqid ⊢W↑𝑠∅=W↑𝑠∅
16 15 pwslnmlem0 ⊢W∈LMod→W↑𝑠∅∈LNoeM
17 14 16 syl ⊢W∈LNoeM→W↑𝑠∅∈LNoeM
18 vex ⊢b∈V
19 vsnex ⊢c∈V
20 eqid ⊢W↑𝑠b=W↑𝑠b
21 eqid ⊢W↑𝑠c=W↑𝑠c
22 eqid ⊢W↑𝑠b∪c=W↑𝑠b∪c
23 14 ad2antrl ⊢b∈Fin∧¬c∈b∧W∈LNoeM∧W↑𝑠b∈LNoeM→W∈LMod
24 disjsn ⊢b∩c=∅↔¬c∈b
25 24 biimpri ⊢¬c∈b→b∩c=∅
26 25 ad2antlr ⊢b∈Fin∧¬c∈b∧W∈LNoeM∧W↑𝑠b∈LNoeM→b∩c=∅
27 simprr ⊢b∈Fin∧¬c∈b∧W∈LNoeM∧W↑𝑠b∈LNoeM→W↑𝑠b∈LNoeM
28 21 pwslnmlem1 ⊢W∈LNoeM→W↑𝑠c∈LNoeM
29 28 ad2antrl ⊢b∈Fin∧¬c∈b∧W∈LNoeM∧W↑𝑠b∈LNoeM→W↑𝑠c∈LNoeM
30 18 19 20 21 22 23 26 27 29 pwslnmlem2 ⊢b∈Fin∧¬c∈b∧W∈LNoeM∧W↑𝑠b∈LNoeM→W↑𝑠b∪c∈LNoeM
31 30 exp32 ⊢b∈Fin∧¬c∈b→W∈LNoeM→W↑𝑠b∈LNoeM→W↑𝑠b∪c∈LNoeM
32 31 a2d ⊢b∈Fin∧¬c∈b→W∈LNoeM→W↑𝑠b∈LNoeM→W∈LNoeM→W↑𝑠b∪c∈LNoeM
33 4 7 10 13 17 32 findcard2s ⊢I∈Fin→W∈LNoeM→W↑𝑠I∈LNoeM
34 33 impcom ⊢W∈LNoeM∧I∈Fin→W↑𝑠I∈LNoeM
35 1 34 eqeltrid ⊢W∈LNoeM∧I∈Fin→Y∈LNoeM