Metamath Proof Explorer

Theorem zringlpir

Description: The integers are a principal ideal ring. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Assertion zringlpir ℤring ∈ LPIR

Proof

Step Hyp Ref Expression
1 zringring ⊢ ℤring ∈ Ring
2 eleq1 ⊢ ( 𝑥 = { 0 } → ( 𝑥 ∈ ( LPIdeal ‘ ℤring ) ↔ { 0 } ∈ ( LPIdeal ‘ ℤring ) ) )
3 simpl ⊢ ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) → 𝑥 ∈ ( LIdeal ‘ ℤring ) )
4 simpr ⊢ ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) → 𝑥 ≠ { 0 } )
5 eqid ⊢ inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) = inf ( ( 𝑥 ∩ ℕ ) , ℝ , < )
6 3 4 5 zringlpirlem2 ⊢ ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) → inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) ∈ 𝑥 )
7 simpll ⊢ ( ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) ∧ 𝑧 ∈ 𝑥 ) → 𝑥 ∈ ( LIdeal ‘ ℤring ) )
8 simplr ⊢ ( ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) ∧ 𝑧 ∈ 𝑥 ) → 𝑥 ≠ { 0 } )
9 simpr ⊢ ( ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 )
10 7 8 5 9 zringlpirlem3 ⊢ ( ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) ∧ 𝑧 ∈ 𝑥 ) → inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) ∥ 𝑧 )
11 10 ralrimiva ⊢ ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) → ∀ 𝑧 ∈ 𝑥 inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) ∥ 𝑧 )
12 breq1 ⊢ ( 𝑦 = inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) → ( 𝑦 ∥ 𝑧 ↔ inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) ∥ 𝑧 ) )
13 12 ralbidv ⊢ ( 𝑦 = inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) → ( ∀ 𝑧 ∈ 𝑥 𝑦 ∥ 𝑧 ↔ ∀ 𝑧 ∈ 𝑥 inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) ∥ 𝑧 ) )
14 13 rspcev ⊢ ( ( inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑥 inf ( ( 𝑥 ∩ ℕ ) , ℝ , < ) ∥ 𝑧 ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 𝑦 ∥ 𝑧 )
15 6 11 14 syl2anc ⊢ ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 𝑦 ∥ 𝑧 )
16 eqid ⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
17 eqid ⊢ ( LPIdeal ‘ ℤring ) = ( LPIdeal ‘ ℤring )
18 dvdsrzring ⊢ ∥ = ( ∥r ‘ ℤring )
19 16 17 18 lpigen ⊢ ( ( ℤring ∈ Ring ∧ 𝑥 ∈ ( LIdeal ‘ ℤring ) ) → ( 𝑥 ∈ ( LPIdeal ‘ ℤring ) ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 𝑦 ∥ 𝑧 ) )
20 1 19 mpan ⊢ ( 𝑥 ∈ ( LIdeal ‘ ℤring ) → ( 𝑥 ∈ ( LPIdeal ‘ ℤring ) ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 𝑦 ∥ 𝑧 ) )
21 20 adantr ⊢ ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) → ( 𝑥 ∈ ( LPIdeal ‘ ℤring ) ↔ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 𝑦 ∥ 𝑧 ) )
22 15 21 mpbird ⊢ ( ( 𝑥 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑥 ≠ { 0 } ) → 𝑥 ∈ ( LPIdeal ‘ ℤring ) )
23 zring0 ⊢ 0 = ( 0g ‘ ℤring )
24 17 23 lpi0 ⊢ ( ℤring ∈ Ring → { 0 } ∈ ( LPIdeal ‘ ℤring ) )
25 1 24 mp1i ⊢ ( 𝑥 ∈ ( LIdeal ‘ ℤring ) → { 0 } ∈ ( LPIdeal ‘ ℤring ) )
26 2 22 25 pm2.61ne ⊢ ( 𝑥 ∈ ( LIdeal ‘ ℤring ) → 𝑥 ∈ ( LPIdeal ‘ ℤring ) )
27 26 ssriv ⊢ ( LIdeal ‘ ℤring ) ⊆ ( LPIdeal ‘ ℤring )
28 17 16 islpir2 ⊢ ( ℤring ∈ LPIR ↔ ( ℤring ∈ Ring ∧ ( LIdeal ‘ ℤring ) ⊆ ( LPIdeal ‘ ℤring ) ) )
29 1 27 28 mpbir2an ⊢ ℤring ∈ LPIR