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 ⊢ 𝑌 = ( 𝑊 ↑s 𝐼 )
Assertion pwslnm ( ( 𝑊 ∈ LNoeM ∧ 𝐼 ∈ Fin ) → 𝑌 ∈ LNoeM )

Proof

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