This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lpirlidllpi

Description: In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses lpirlidllpi.1 ⊢ B = Base R
lpirlidllpi.2 ⊢ I = LIdeal ⁡ R
lpirlidllpi.3 ⊢ K = RSpan ⁡ R
lpirlidllpi.4 ⊢ φ → R ∈ LPIR
lpirlidllpi.5 ⊢ φ → J ∈ I
Assertion lpirlidllpi ⊢ φ → ∃ x ∈ B J = K ⁡ x

Proof

Step Hyp Ref Expression
1 lpirlidllpi.1 ⊢ B = Base R
2 lpirlidllpi.2 ⊢ I = LIdeal ⁡ R
3 lpirlidllpi.3 ⊢ K = RSpan ⁡ R
4 lpirlidllpi.4 ⊢ φ → R ∈ LPIR
5 lpirlidllpi.5 ⊢ φ → J ∈ I
6 eqid ⊢ LPIdeal ⁡ R = LPIdeal ⁡ R
7 6 2 islpir ⊢ R ∈ LPIR ↔ R ∈ Ring ∧ I = LPIdeal ⁡ R
8 4 7 sylib ⊢ φ → R ∈ Ring ∧ I = LPIdeal ⁡ R
9 8 simpld ⊢ φ → R ∈ Ring
10 8 simprd ⊢ φ → I = LPIdeal ⁡ R
11 5 10 eleqtrd ⊢ φ → J ∈ LPIdeal ⁡ R
12 6 3 1 islpidl ⊢ R ∈ Ring → J ∈ LPIdeal ⁡ R ↔ ∃ x ∈ B J = K ⁡ x
13 12 biimpa ⊢ R ∈ Ring ∧ J ∈ LPIdeal ⁡ R → ∃ x ∈ B J = K ⁡ x
14 9 11 13 syl2anc ⊢ φ → ∃ x ∈ B J = K ⁡ x