# Metamath Proof Explorer

## Theorem pwslnmlem1

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

Ref Expression
Hypothesis pwslnmlem1.y ${⊢}{Y}={W}{↑}_{𝑠}\left\{{i}\right\}$
Assertion pwslnmlem1 ${⊢}{W}\in \mathrm{LNoeM}\to {Y}\in \mathrm{LNoeM}$

### Proof

Step Hyp Ref Expression
1 pwslnmlem1.y ${⊢}{Y}={W}{↑}_{𝑠}\left\{{i}\right\}$
2 lnmlmod ${⊢}{W}\in \mathrm{LNoeM}\to {W}\in \mathrm{LMod}$
3 snex ${⊢}\left\{{i}\right\}\in \mathrm{V}$
4 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
5 eqid ${⊢}\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)=\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)$
6 1 4 5 pwsdiaglmhm ${⊢}\left({W}\in \mathrm{LMod}\wedge \left\{{i}\right\}\in \mathrm{V}\right)\to \left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)\in \left({W}\mathrm{LMHom}{Y}\right)$
7 2 3 6 sylancl ${⊢}{W}\in \mathrm{LNoeM}\to \left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)\in \left({W}\mathrm{LMHom}{Y}\right)$
8 id ${⊢}{W}\in \mathrm{LNoeM}\to {W}\in \mathrm{LNoeM}$
9 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
10 1 4 5 9 pwssnf1o ${⊢}\left({W}\in \mathrm{LNoeM}\wedge {i}\in \mathrm{V}\right)\to \left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right):{\mathrm{Base}}_{{W}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}$
11 10 elvd ${⊢}{W}\in \mathrm{LNoeM}\to \left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right):{\mathrm{Base}}_{{W}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}$
12 f1ofo ${⊢}\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right):{\mathrm{Base}}_{{W}}\underset{1-1 onto}{⟶}{\mathrm{Base}}_{{Y}}\to \left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right):{\mathrm{Base}}_{{W}}\underset{onto}{⟶}{\mathrm{Base}}_{{Y}}$
13 forn ${⊢}\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right):{\mathrm{Base}}_{{W}}\underset{onto}{⟶}{\mathrm{Base}}_{{Y}}\to \mathrm{ran}\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)={\mathrm{Base}}_{{Y}}$
14 11 12 13 3syl ${⊢}{W}\in \mathrm{LNoeM}\to \mathrm{ran}\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)={\mathrm{Base}}_{{Y}}$
15 9 lnmepi ${⊢}\left(\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)\in \left({W}\mathrm{LMHom}{Y}\right)\wedge {W}\in \mathrm{LNoeM}\wedge \mathrm{ran}\left({x}\in {\mathrm{Base}}_{{W}}⟼\left\{{i}\right\}×\left\{{x}\right\}\right)={\mathrm{Base}}_{{Y}}\right)\to {Y}\in \mathrm{LNoeM}$
16 7 8 14 15 syl3anc ${⊢}{W}\in \mathrm{LNoeM}\to {Y}\in \mathrm{LNoeM}$