Metamath Proof Explorer

Theorem ply1lpir

Description: The ring of polynomials over a division ring has the principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypothesis ply1lpir.p ⊢ P = Poly 1 ⁡ R
Assertion ply1lpir ⊢ R ∈ DivRing → P ∈ LPIR

Proof

Step Hyp Ref Expression
1 ply1lpir.p ⊢ P = Poly 1 ⁡ R
2 drngring ⊢ R ∈ DivRing → R ∈ Ring
3 1 ply1ring ⊢ R ∈ Ring → P ∈ Ring
4 2 3 syl ⊢ R ∈ DivRing → P ∈ Ring
5 eqid ⊢ Base P = Base P
6 eqid ⊢ LIdeal ⁡ P = LIdeal ⁡ P
7 5 6 lidlss ⊢ i ∈ LIdeal ⁡ P → i ⊆ Base P
8 7 adantl ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → i ⊆ Base P
9 eqid ⊢ idlGen 1p ⁡ R = idlGen 1p ⁡ R
10 1 9 6 ig1pcl ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → idlGen 1p ⁡ R ⁡ i ∈ i
11 8 10 sseldd ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → idlGen 1p ⁡ R ⁡ i ∈ Base P
12 eqid ⊢ RSpan ⁡ P = RSpan ⁡ P
13 1 9 6 12 ig1prsp ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → i = RSpan ⁡ P ⁡ idlGen 1p ⁡ R ⁡ i
14 sneq ⊢ j = idlGen 1p ⁡ R ⁡ i → j = idlGen 1p ⁡ R ⁡ i
15 14 fveq2d ⊢ j = idlGen 1p ⁡ R ⁡ i → RSpan ⁡ P ⁡ j = RSpan ⁡ P ⁡ idlGen 1p ⁡ R ⁡ i
16 15 rspceeqv ⊢ idlGen 1p ⁡ R ⁡ i ∈ Base P ∧ i = RSpan ⁡ P ⁡ idlGen 1p ⁡ R ⁡ i → ∃ j ∈ Base P i = RSpan ⁡ P ⁡ j
17 11 13 16 syl2anc ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → ∃ j ∈ Base P i = RSpan ⁡ P ⁡ j
18 4 adantr ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → P ∈ Ring
19 eqid ⊢ LPIdeal ⁡ P = LPIdeal ⁡ P
20 19 12 5 islpidl ⊢ P ∈ Ring → i ∈ LPIdeal ⁡ P ↔ ∃ j ∈ Base P i = RSpan ⁡ P ⁡ j
21 18 20 syl ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → i ∈ LPIdeal ⁡ P ↔ ∃ j ∈ Base P i = RSpan ⁡ P ⁡ j
22 17 21 mpbird ⊢ R ∈ DivRing ∧ i ∈ LIdeal ⁡ P → i ∈ LPIdeal ⁡ P
23 22 ex ⊢ R ∈ DivRing → i ∈ LIdeal ⁡ P → i ∈ LPIdeal ⁡ P
24 23 ssrdv ⊢ R ∈ DivRing → LIdeal ⁡ P ⊆ LPIdeal ⁡ P
25 19 6 islpir2 ⊢ P ∈ LPIR ↔ P ∈ Ring ∧ LIdeal ⁡ P ⊆ LPIdeal ⁡ P
26 4 24 25 sylanbrc ⊢ R ∈ DivRing → P ∈ LPIR