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 ^s I )
Assertion pwslnm 
|- ( ( W e. LNoeM /\ I e. Fin ) -> Y e. LNoeM )

Proof

Step Hyp Ref Expression
1 pwslnm.y 
 |-  Y = ( W ^s I )
2 oveq2 
 |-  ( a = (/) -> ( W ^s a ) = ( W ^s (/) ) )
3 2 eleq1d 
 |-  ( a = (/) -> ( ( W ^s a ) e. LNoeM <-> ( W ^s (/) ) e. LNoeM ) )
4 3 imbi2d 
 |-  ( a = (/) -> ( ( W e. LNoeM -> ( W ^s a ) e. LNoeM ) <-> ( W e. LNoeM -> ( W ^s (/) ) e. LNoeM ) ) )
5 oveq2 
 |-  ( a = b -> ( W ^s a ) = ( W ^s b ) )
6 5 eleq1d 
 |-  ( a = b -> ( ( W ^s a ) e. LNoeM <-> ( W ^s b ) e. LNoeM ) )
7 6 imbi2d 
 |-  ( a = b -> ( ( W e. LNoeM -> ( W ^s a ) e. LNoeM ) <-> ( W e. LNoeM -> ( W ^s b ) e. LNoeM ) ) )
8 oveq2 
 |-  ( a = ( b u. { c } ) -> ( W ^s a ) = ( W ^s ( b u. { c } ) ) )
9 8 eleq1d 
 |-  ( a = ( b u. { c } ) -> ( ( W ^s a ) e. LNoeM <-> ( W ^s ( b u. { c } ) ) e. LNoeM ) )
10 9 imbi2d 
 |-  ( a = ( b u. { c } ) -> ( ( W e. LNoeM -> ( W ^s a ) e. LNoeM ) <-> ( W e. LNoeM -> ( W ^s ( b u. { c } ) ) e. LNoeM ) ) )
11 oveq2 
 |-  ( a = I -> ( W ^s a ) = ( W ^s I ) )
12 11 eleq1d 
 |-  ( a = I -> ( ( W ^s a ) e. LNoeM <-> ( W ^s I ) e. LNoeM ) )
13 12 imbi2d 
 |-  ( a = I -> ( ( W e. LNoeM -> ( W ^s a ) e. LNoeM ) <-> ( W e. LNoeM -> ( W ^s I ) e. LNoeM ) ) )
14 lnmlmod 
 |-  ( W e. LNoeM -> W e. LMod )
15 eqid 
 |-  ( W ^s (/) ) = ( W ^s (/) )
16 15 pwslnmlem0 
 |-  ( W e. LMod -> ( W ^s (/) ) e. LNoeM )
17 14 16 syl 
 |-  ( W e. LNoeM -> ( W ^s (/) ) e. LNoeM )
18 vex 
 |-  b e. _V
19 snex 
 |-  { c } e. _V
20 eqid 
 |-  ( W ^s b ) = ( W ^s b )
21 eqid 
 |-  ( W ^s { c } ) = ( W ^s { c } )
22 eqid 
 |-  ( W ^s ( b u. { c } ) ) = ( W ^s ( b u. { c } ) )
23 14 ad2antrl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( W e. LNoeM /\ ( W ^s b ) e. LNoeM ) ) -> W e. LMod )
24 disjsn 
 |-  ( ( b i^i { c } ) = (/) <-> -. c e. b )
25 24 biimpri 
 |-  ( -. c e. b -> ( b i^i { c } ) = (/) )
26 25 ad2antlr 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( W e. LNoeM /\ ( W ^s b ) e. LNoeM ) ) -> ( b i^i { c } ) = (/) )
27 simprr 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( W e. LNoeM /\ ( W ^s b ) e. LNoeM ) ) -> ( W ^s b ) e. LNoeM )
28 21 pwslnmlem1 
 |-  ( W e. LNoeM -> ( W ^s { c } ) e. LNoeM )
29 28 ad2antrl 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( W e. LNoeM /\ ( W ^s b ) e. LNoeM ) ) -> ( W ^s { c } ) e. LNoeM )
30 18 19 20 21 22 23 26 27 29 pwslnmlem2 
 |-  ( ( ( b e. Fin /\ -. c e. b ) /\ ( W e. LNoeM /\ ( W ^s b ) e. LNoeM ) ) -> ( W ^s ( b u. { c } ) ) e. LNoeM )
31 30 exp32 
 |-  ( ( b e. Fin /\ -. c e. b ) -> ( W e. LNoeM -> ( ( W ^s b ) e. LNoeM -> ( W ^s ( b u. { c } ) ) e. LNoeM ) ) )
32 31 a2d 
 |-  ( ( b e. Fin /\ -. c e. b ) -> ( ( W e. LNoeM -> ( W ^s b ) e. LNoeM ) -> ( W e. LNoeM -> ( W ^s ( b u. { c } ) ) e. LNoeM ) ) )
33 4 7 10 13 17 32 findcard2s 
 |-  ( I e. Fin -> ( W e. LNoeM -> ( W ^s I ) e. LNoeM ) )
34 33 impcom 
 |-  ( ( W e. LNoeM /\ I e. Fin ) -> ( W ^s I ) e. LNoeM )
35 1 34 eqeltrid 
 |-  ( ( W e. LNoeM /\ I e. Fin ) -> Y e. LNoeM )