Theorem pwslnmlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		pwslnmlem1.y	$$⊢Y=W{\uparrow }_{𝑠}\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\}\times \left\{x\right\}\right)=\left(x\in {\mathrm{Base}}_W⟼\left\{i\right\}\times \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\}\times \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\}\times \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\}\times \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\}\times \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\}\times \left\{x\right\}\right):{\mathrm{Base}}_W\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Y\to \left(x\in {\mathrm{Base}}_W⟼\left\{i\right\}\times \left\{x\right\}\right):{\mathrm{Base}}_W\underset{onto}{⟶}{\mathrm{Base}}_Y$$
13		forn	$$⊢\left(x\in {\mathrm{Base}}_W⟼\left\{i\right\}\times \left\{x\right\}\right):{\mathrm{Base}}_W\underset{onto}{⟶}{\mathrm{Base}}_Y\to \mathrm{ran}\left(x\in {\mathrm{Base}}_W⟼\left\{i\right\}\times \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\}\times \left\{x\right\}\right)={\mathrm{Base}}_Y$$
15	9	lnmepi	$$⊢\left(\left(x\in {\mathrm{Base}}_W⟼\left\{i\right\}\times \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\}\times \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}$$