Theorem pwslnmlem1

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

	Ref	Expression
Hypothesis	pwslnmlem1.y	⊢ 𝑌 = ( 𝑊 ↑s { 𝑖 } )
Assertion	pwslnmlem1	⊢ ( 𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM )

Proof

Step	Hyp	Ref	Expression
1		pwslnmlem1.y	⊢ 𝑌 = ( 𝑊 ↑s { 𝑖 } )
2		lnmlmod	⊢ ( 𝑊 ∈ LNoeM → 𝑊 ∈ LMod )
3		vsnex	⊢ { 𝑖 } ∈ V
4		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5		eqid	⊢ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) )
6	1 4 5	pwsdiaglmhm	⊢ ( ( 𝑊 ∈ LMod ∧ { 𝑖 } ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) ∈ ( 𝑊 LMHom 𝑌 ) )
7	2 3 6	sylancl	⊢ ( 𝑊 ∈ LNoeM → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) ∈ ( 𝑊 LMHom 𝑌 ) )
8		id	⊢ ( 𝑊 ∈ LNoeM → 𝑊 ∈ LNoeM )
9		eqid	⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
10	1 4 5 9	pwssnf1o	⊢ ( ( 𝑊 ∈ LNoeM ∧ 𝑖 ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) : ( Base ‘ 𝑊 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
11	10	elvd	⊢ ( 𝑊 ∈ LNoeM → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) : ( Base ‘ 𝑊 ) –1-1-onto→ ( Base ‘ 𝑌 ) )
12		f1ofo	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) : ( Base ‘ 𝑊 ) –1-1-onto→ ( Base ‘ 𝑌 ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) : ( Base ‘ 𝑊 ) –onto→ ( Base ‘ 𝑌 ) )
13		forn	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) : ( Base ‘ 𝑊 ) –onto→ ( Base ‘ 𝑌 ) → ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) = ( Base ‘ 𝑌 ) )
14	11 12 13	3syl	⊢ ( 𝑊 ∈ LNoeM → ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) = ( Base ‘ 𝑌 ) )
15	9	lnmepi	⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) ∈ ( 𝑊 LMHom 𝑌 ) ∧ 𝑊 ∈ LNoeM ∧ ran ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( { 𝑖 } × { 𝑥 } ) ) = ( Base ‘ 𝑌 ) ) → 𝑌 ∈ LNoeM )
16	7 8 14 15	syl3anc	⊢ ( 𝑊 ∈ LNoeM → 𝑌 ∈ LNoeM )