Theorem lpirlnr

Description: Left principal ideal rings are left Noetherian. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Assertion	lpirlnr	⊢ ( 𝑅 ∈ LPIR → 𝑅 ∈ LNoeR )

Proof

Step	Hyp	Ref	Expression
1		lpirring	⊢ ( 𝑅 ∈ LPIR → 𝑅 ∈ Ring )
2		eqid	⊢ ( LPIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 )
3		eqid	⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	2 3 4	islpidl	⊢ ( 𝑅 ∈ Ring → ( 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ↔ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) ) )
6	1 5	syl	⊢ ( 𝑅 ∈ LPIR → ( 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ↔ ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) ) )
7	6	biimpa	⊢ ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) )
8		snelpwi	⊢ ( 𝑐 ∈ ( Base ‘ 𝑅 ) → { 𝑐 } ∈ 𝒫 ( Base ‘ 𝑅 ) )
9	8	adantl	⊢ ( ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → { 𝑐 } ∈ 𝒫 ( Base ‘ 𝑅 ) )
10		snfi	⊢ { 𝑐 } ∈ Fin
11	10	a1i	⊢ ( ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → { 𝑐 } ∈ Fin )
12	9 11	elind	⊢ ( ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → { 𝑐 } ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) )
13		eqid	⊢ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } )
14		fveq2	⊢ ( 𝑏 = { 𝑐 } → ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) )
15	14	rspceeqv	⊢ ( ( { 𝑐 } ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) ) → ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) )
16	12 13 15	sylancl	⊢ ( ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) )
17		eqeq1	⊢ ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) → ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ) )
18	17	rexbidv	⊢ ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) → ( ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ↔ ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ) )
19	16 18	syl5ibrcom	⊢ ( ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) ∧ 𝑐 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) → ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ) )
20	19	rexlimdva	⊢ ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) → ( ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑐 } ) → ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ) )
21	7 20	mpd	⊢ ( ( 𝑅 ∈ LPIR ∧ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ) → ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) )
22	21	ralrimiva	⊢ ( 𝑅 ∈ LPIR → ∀ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) )
23		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
24	2 23	islpir	⊢ ( 𝑅 ∈ LPIR ↔ ( 𝑅 ∈ Ring ∧ ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) ) )
25	24	simprbi	⊢ ( 𝑅 ∈ LPIR → ( LIdeal ‘ 𝑅 ) = ( LPIdeal ‘ 𝑅 ) )
26	25	raleqdv	⊢ ( 𝑅 ∈ LPIR → ( ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ↔ ∀ 𝑎 ∈ ( LPIdeal ‘ 𝑅 ) ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ) )
27	22 26	mpbird	⊢ ( 𝑅 ∈ LPIR → ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) )
28	4 23 3	islnr2	⊢ ( 𝑅 ∈ LNoeR ↔ ( 𝑅 ∈ Ring ∧ ∀ 𝑎 ∈ ( LIdeal ‘ 𝑅 ) ∃ 𝑏 ∈ ( 𝒫 ( Base ‘ 𝑅 ) ∩ Fin ) 𝑎 = ( ( RSpan ‘ 𝑅 ) ‘ 𝑏 ) ) )
29	1 27 28	sylanbrc	⊢ ( 𝑅 ∈ LPIR → 𝑅 ∈ LNoeR )