Metamath Proof Explorer


Theorem pwslnmlem0

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

Ref Expression
Hypothesis pwslnmlem0.y Y=W𝑠
Assertion pwslnmlem0 WLModYLNoeM

Proof

Step Hyp Ref Expression
1 pwslnmlem0.y Y=W𝑠
2 0ex V
3 1 pwslmod WLModVYLMod
4 2 3 mpan2 WLModYLMod
5 eqid BaseW=BaseW
6 1 5 pwsbas WLModVBaseW=BaseY
7 2 6 mpan2 WLModBaseW=BaseY
8 fvex BaseWV
9 map0e BaseWVBaseW=1𝑜
10 8 9 ax-mp BaseW=1𝑜
11 df1o2 1𝑜=
12 10 11 eqtri BaseW=
13 snfi Fin
14 12 13 eqeltri BaseWFin
15 7 14 eqeltrrdi WLModBaseYFin
16 eqid BaseY=BaseY
17 16 filnm YLModBaseYFinYLNoeM
18 4 15 17 syl2anc WLModYLNoeM