Theorem pwslnmlem1

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

	Ref	Expression
Hypothesis	pwslnmlem1.y	|- Y = ( W ^s { i } )
Assertion	pwslnmlem1	|- ( W e. LNoeM -> Y e. LNoeM )

Proof

Step	Hyp	Ref	Expression
1		pwslnmlem1.y	|- Y = ( W ^s { i } )
2		lnmlmod	|- ( W e. LNoeM -> W e. LMod )
3		vsnex	|- { i } e. _V
4		eqid	|- ( Base ` W ) = ( Base ` W )
5		eqid	|- ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) = ( x e. ( Base ` W ) |-> ( { i } X. { x } ) )
6	1 4 5	pwsdiaglmhm	|- ( ( W e. LMod /\ { i } e. _V ) -> ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) e. ( W LMHom Y ) )
7	2 3 6	sylancl	|- ( W e. LNoeM -> ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) e. ( W LMHom Y ) )
8		id	|- ( W e. LNoeM -> W e. LNoeM )
9		eqid	|- ( Base ` Y ) = ( Base ` Y )
10	1 4 5 9	pwssnf1o	|- ( ( W e. LNoeM /\ i e. _V ) -> ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) : ( Base ` W ) -1-1-onto-> ( Base ` Y ) )
11	10	elvd	|- ( W e. LNoeM -> ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) : ( Base ` W ) -1-1-onto-> ( Base ` Y ) )
12		f1ofo	|- ( ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) : ( Base ` W ) -1-1-onto-> ( Base ` Y ) -> ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) : ( Base ` W ) -onto-> ( Base ` Y ) )
13		forn	|- ( ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) : ( Base ` W ) -onto-> ( Base ` Y ) -> ran ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) = ( Base ` Y ) )
14	11 12 13	3syl	|- ( W e. LNoeM -> ran ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) = ( Base ` Y ) )
15	9	lnmepi	|- ( ( ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) e. ( W LMHom Y ) /\ W e. LNoeM /\ ran ( x e. ( Base ` W ) |-> ( { i } X. { x } ) ) = ( Base ` Y ) ) -> Y e. LNoeM )
16	7 8 14 15	syl3anc	|- ( W e. LNoeM -> Y e. LNoeM )