Metamath Proof Explorer

Theorem lpirlnr

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

Ref Expression
Assertion lpirlnr ⊢R∈LPIR→R∈LNoeR

Proof

Step Hyp Ref Expression
1 lpirring ⊢R∈LPIR→R∈Ring
2 eqid ⊢LPIdeal⁡R=LPIdeal⁡R
3 eqid ⊢RSpan⁡R=RSpan⁡R
4 eqid ⊢BaseR=BaseR
5 2 3 4 islpidl ⊢R∈Ring→a∈LPIdeal⁡R↔∃c∈BaseRa=RSpan⁡R⁡c
6 1 5 syl ⊢R∈LPIR→a∈LPIdeal⁡R↔∃c∈BaseRa=RSpan⁡R⁡c
7 6 biimpa ⊢R∈LPIR∧a∈LPIdeal⁡R→∃c∈BaseRa=RSpan⁡R⁡c
8 snelpwi ⊢c∈BaseR→c∈𝒫BaseR
9 8 adantl ⊢R∈LPIR∧a∈LPIdeal⁡R∧c∈BaseR→c∈𝒫BaseR
10 snfi ⊢c∈Fin
11 10 a1i ⊢R∈LPIR∧a∈LPIdeal⁡R∧c∈BaseR→c∈Fin
12 9 11 elind ⊢R∈LPIR∧a∈LPIdeal⁡R∧c∈BaseR→c∈𝒫BaseR∩Fin
13 eqid ⊢RSpan⁡R⁡c=RSpan⁡R⁡c
14 fveq2 ⊢b=c→RSpan⁡R⁡b=RSpan⁡R⁡c
15 14 rspceeqv ⊢c∈𝒫BaseR∩Fin∧RSpan⁡R⁡c=RSpan⁡R⁡c→∃b∈𝒫BaseR∩FinRSpan⁡R⁡c=RSpan⁡R⁡b
16 12 13 15 sylancl ⊢R∈LPIR∧a∈LPIdeal⁡R∧c∈BaseR→∃b∈𝒫BaseR∩FinRSpan⁡R⁡c=RSpan⁡R⁡b
17 eqeq1 ⊢a=RSpan⁡R⁡c→a=RSpan⁡R⁡b↔RSpan⁡R⁡c=RSpan⁡R⁡b
18 17 rexbidv ⊢a=RSpan⁡R⁡c→∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b↔∃b∈𝒫BaseR∩FinRSpan⁡R⁡c=RSpan⁡R⁡b
19 16 18 syl5ibrcom ⊢R∈LPIR∧a∈LPIdeal⁡R∧c∈BaseR→a=RSpan⁡R⁡c→∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b
20 19 rexlimdva ⊢R∈LPIR∧a∈LPIdeal⁡R→∃c∈BaseRa=RSpan⁡R⁡c→∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b
21 7 20 mpd ⊢R∈LPIR∧a∈LPIdeal⁡R→∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b
22 21 ralrimiva ⊢R∈LPIR→∀a∈LPIdeal⁡R∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b
23 eqid ⊢LIdeal⁡R=LIdeal⁡R
24 2 23 islpir ⊢R∈LPIR↔R∈Ring∧LIdeal⁡R=LPIdeal⁡R
25 24 simprbi ⊢R∈LPIR→LIdeal⁡R=LPIdeal⁡R
26 25 raleqdv ⊢R∈LPIR→∀a∈LIdeal⁡R∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b↔∀a∈LPIdeal⁡R∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b
27 22 26 mpbird ⊢R∈LPIR→∀a∈LIdeal⁡R∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b
28 4 23 3 islnr2 ⊢R∈LNoeR↔R∈Ring∧∀a∈LIdeal⁡R∃b∈𝒫BaseR∩Fina=RSpan⁡R⁡b
29 1 27 28 sylanbrc ⊢R∈LPIR→R∈LNoeR