Theorem pwslnmlem0

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

	Ref	Expression
Hypothesis	pwslnmlem0.y	|- Y = ( W ^s (/) )
Assertion	pwslnmlem0	|- ( W e. LMod -> Y e. LNoeM )

Proof

Step	Hyp	Ref	Expression
1		pwslnmlem0.y	|- Y = ( W ^s (/) )
2		0ex	|- (/) e. _V
3	1	pwslmod	|- ( ( W e. LMod /\ (/) e. _V ) -> Y e. LMod )
4	2 3	mpan2	|- ( W e. LMod -> Y e. LMod )
5		eqid	|- ( Base ` W ) = ( Base ` W )
6	1 5	pwsbas	|- ( ( W e. LMod /\ (/) e. _V ) -> ( ( Base ` W ) ^m (/) ) = ( Base ` Y ) )
7	2 6	mpan2	|- ( W e. LMod -> ( ( Base ` W ) ^m (/) ) = ( Base ` Y ) )
8		fvex	|- ( Base ` W ) e. _V
9		map0e	|- ( ( Base ` W ) e. _V -> ( ( Base ` W ) ^m (/) ) = 1o )
10	8 9	ax-mp	|- ( ( Base ` W ) ^m (/) ) = 1o
11		df1o2	|- 1o = { (/) }
12	10 11	eqtri	|- ( ( Base ` W ) ^m (/) ) = { (/) }
13		snfi	|- { (/) } e. Fin
14	12 13	eqeltri	|- ( ( Base ` W ) ^m (/) ) e. Fin
15	7 14	eqeltrrdi	|- ( W e. LMod -> ( Base ` Y ) e. Fin )
16		eqid	|- ( Base ` Y ) = ( Base ` Y )
17	16	filnm	|- ( ( Y e. LMod /\ ( Base ` Y ) e. Fin ) -> Y e. LNoeM )
18	4 15 17	syl2anc	|- ( W e. LMod -> Y e. LNoeM )