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 ⊢ Base R = Base R
5 2 3 4 islpidl ⊢ R ∈ Ring → a ∈ LPIdeal ⁡ R ↔ ∃ c ∈ Base R a = RSpan ⁡ R ⁡ c
6 1 5 syl ⊢ R ∈ LPIR → a ∈ LPIdeal ⁡ R ↔ ∃ c ∈ Base R a = RSpan ⁡ R ⁡ c
7 6 biimpa ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R → ∃ c ∈ Base R a = RSpan ⁡ R ⁡ c
8 snelpwi ⊢ c ∈ Base R → c ∈ 𝒫 Base R
9 8 adantl ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R ∧ c ∈ Base R → c ∈ 𝒫 Base R
10 snfi ⊢ c ∈ Fin
11 10 a1i ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R ∧ c ∈ Base R → c ∈ Fin
12 9 11 elind ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R ∧ c ∈ Base R → c ∈ 𝒫 Base R ∩ Fin
13 eqid ⊢ RSpan ⁡ R ⁡ c = RSpan ⁡ R ⁡ c
14 fveq2 ⊢ b = c → RSpan ⁡ R ⁡ b = RSpan ⁡ R ⁡ c
15 14 rspceeqv ⊢ c ∈ 𝒫 Base R ∩ Fin ∧ RSpan ⁡ R ⁡ c = RSpan ⁡ R ⁡ c → ∃ b ∈ 𝒫 Base R ∩ Fin RSpan ⁡ R ⁡ c = RSpan ⁡ R ⁡ b
16 12 13 15 sylancl ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R ∧ c ∈ Base R → ∃ b ∈ 𝒫 Base R ∩ Fin RSpan ⁡ 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 ∈ 𝒫 Base R ∩ Fin a = RSpan ⁡ R ⁡ b ↔ ∃ b ∈ 𝒫 Base R ∩ Fin RSpan ⁡ R ⁡ c = RSpan ⁡ R ⁡ b
19 16 18 syl5ibrcom ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R ∧ c ∈ Base R → a = RSpan ⁡ R ⁡ c → ∃ b ∈ 𝒫 Base R ∩ Fin a = RSpan ⁡ R ⁡ b
20 19 rexlimdva ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R → ∃ c ∈ Base R a = RSpan ⁡ R ⁡ c → ∃ b ∈ 𝒫 Base R ∩ Fin a = RSpan ⁡ R ⁡ b
21 7 20 mpd ⊢ R ∈ LPIR ∧ a ∈ LPIdeal ⁡ R → ∃ b ∈ 𝒫 Base R ∩ Fin a = RSpan ⁡ R ⁡ b
22 21 ralrimiva ⊢ R ∈ LPIR → ∀ a ∈ LPIdeal ⁡ R ∃ b ∈ 𝒫 Base R ∩ Fin a = 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 22 25 raleqtrrdv ⊢ R ∈ LPIR → ∀ a ∈ LIdeal ⁡ R ∃ b ∈ 𝒫 Base R ∩ Fin a = RSpan ⁡ R ⁡ b
27 4 23 3 islnr2 ⊢ R ∈ LNoeR ↔ R ∈ Ring ∧ ∀ a ∈ LIdeal ⁡ R ∃ b ∈ 𝒫 Base R ∩ Fin a = RSpan ⁡ R ⁡ b
28 1 26 27 sylanbrc ⊢ R ∈ LPIR → R ∈ LNoeR