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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion ply1lpir ( 𝑅 ∈ DivRing → 𝑃 ∈ LPIR )

Proof

Step Hyp Ref Expression
1 ply1lpir.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
4 2 3 syl ⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ Ring )
5 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
6 eqid ⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
7 5 6 lidlss ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑃 ) → 𝑖 ⊆ ( Base ‘ 𝑃 ) )
8 7 adantl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → 𝑖 ⊆ ( Base ‘ 𝑃 ) )
9 eqid ⊢ ( idlGen1p ‘ 𝑅 ) = ( idlGen1p ‘ 𝑅 )
10 1 9 6 ig1pcl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) ∈ 𝑖 )
11 8 10 sseldd ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝑃 ) )
12 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
13 1 9 6 12 ig1prsp ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → 𝑖 = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) } ) )
14 sneq ⊢ ( 𝑗 = ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) → { 𝑗 } = { ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) } )
15 14 fveq2d ⊢ ( 𝑗 = ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) → ( ( RSpan ‘ 𝑃 ) ‘ { 𝑗 } ) = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) } ) )
16 15 rspceeqv ⊢ ( ( ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑖 = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( idlGen1p ‘ 𝑅 ) ‘ 𝑖 ) } ) ) → ∃ 𝑗 ∈ ( Base ‘ 𝑃 ) 𝑖 = ( ( RSpan ‘ 𝑃 ) ‘ { 𝑗 } ) )
17 11 13 16 syl2anc ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → ∃ 𝑗 ∈ ( Base ‘ 𝑃 ) 𝑖 = ( ( RSpan ‘ 𝑃 ) ‘ { 𝑗 } ) )
18 4 adantr ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → 𝑃 ∈ Ring )
19 eqid ⊢ ( LPIdeal ‘ 𝑃 ) = ( LPIdeal ‘ 𝑃 )
20 19 12 5 islpidl ⊢ ( 𝑃 ∈ Ring → ( 𝑖 ∈ ( LPIdeal ‘ 𝑃 ) ↔ ∃ 𝑗 ∈ ( Base ‘ 𝑃 ) 𝑖 = ( ( RSpan ‘ 𝑃 ) ‘ { 𝑗 } ) ) )
21 18 20 syl ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → ( 𝑖 ∈ ( LPIdeal ‘ 𝑃 ) ↔ ∃ 𝑗 ∈ ( Base ‘ 𝑃 ) 𝑖 = ( ( RSpan ‘ 𝑃 ) ‘ { 𝑗 } ) ) )
22 17 21 mpbird ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( LIdeal ‘ 𝑃 ) ) → 𝑖 ∈ ( LPIdeal ‘ 𝑃 ) )
23 22 ex ⊢ ( 𝑅 ∈ DivRing → ( 𝑖 ∈ ( LIdeal ‘ 𝑃 ) → 𝑖 ∈ ( LPIdeal ‘ 𝑃 ) ) )
24 23 ssrdv ⊢ ( 𝑅 ∈ DivRing → ( LIdeal ‘ 𝑃 ) ⊆ ( LPIdeal ‘ 𝑃 ) )
25 19 6 islpir2 ⊢ ( 𝑃 ∈ LPIR ↔ ( 𝑃 ∈ Ring ∧ ( LIdeal ‘ 𝑃 ) ⊆ ( LPIdeal ‘ 𝑃 ) ) )
26 4 24 25 sylanbrc ⊢ ( 𝑅 ∈ DivRing → 𝑃 ∈ LPIR )