lpirlidllpi - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lpirlidllpi		Structured version Visualization version GIF version

Theorem lpirlidllpi 33473

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

**Hypotheses**
Ref	Expression
lpirlidllpi.1	⊢ 𝐵 = (Base‘𝑅)
lpirlidllpi.2	⊢ 𝐼 = (LIdeal‘𝑅)
lpirlidllpi.3	⊢ 𝐾 = (RSpan‘𝑅)
lpirlidllpi.4	⊢ (𝜑 → 𝑅 ∈ LPIR)
lpirlidllpi.5	⊢ (𝜑 → 𝐽 ∈ 𝐼)

**Assertion**
Ref	Expression
lpirlidllpi	⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥}))

Distinct variable groups: 𝑥,𝐵 𝑥,𝐽 𝑥,𝐾 𝑥,𝑅 Allowed substitution hints: 𝜑(𝑥) 𝐼(𝑥)

**Proof of Theorem lpirlidllpi**
Step	Hyp	Ref	Expression
1		lpirlidllpi.4	. . . 4 ⊢ (𝜑 → 𝑅 ∈ LPIR)
2		eqid 2737	. . . . 5 ⊢ (LPIdeal‘𝑅) = (LPIdeal‘𝑅)
3		lpirlidllpi.2	. . . . 5 ⊢ 𝐼 = (LIdeal‘𝑅)
4	2, 3	islpir 21300	. . . 4 ⊢ (𝑅 ∈ LPIR ↔ (𝑅 ∈ Ring ∧ 𝐼 = (LPIdeal‘𝑅)))
5	1, 4	sylib 218	. . 3 ⊢ (𝜑 → (𝑅 ∈ Ring ∧ 𝐼 = (LPIdeal‘𝑅)))
6	5	simpld 494	. 2 ⊢ (𝜑 → 𝑅 ∈ Ring)
7		lpirlidllpi.5	. . 3 ⊢ (𝜑 → 𝐽 ∈ 𝐼)
8	5	simprd 495	. . 3 ⊢ (𝜑 → 𝐼 = (LPIdeal‘𝑅))
9	7, 8	eleqtrd 2839	. 2 ⊢ (𝜑 → 𝐽 ∈ (LPIdeal‘𝑅))
10		lpirlidllpi.3	. . . 4 ⊢ 𝐾 = (RSpan‘𝑅)
11		lpirlidllpi.1	. . . 4 ⊢ 𝐵 = (Base‘𝑅)
12	2, 10, 11	islpidl 21297	. . 3 ⊢ (𝑅 ∈ Ring → (𝐽 ∈ (LPIdeal‘𝑅) ↔ ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥})))
13	12	biimpa 476	. 2 ⊢ ((𝑅 ∈ Ring ∧ 𝐽 ∈ (LPIdeal‘𝑅)) → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥}))
14	6, 9, 13	syl2anc 585	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∃wrex 3062 {csn 4582 ‘cfv 6502 Basecbs 17150 Ringcrg 20185 LIdealclidl 21178 RSpancrsp 21179 LPIdealclpidl 21292 LPIRclpir 21293

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5245 ax-nul 5255 ax-pr 5381 ax-un 7692

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3402 df-v 3444 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5529 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-iota 6458 df-fun 6504 df-fv 6510 df-lpidl 21294 df-lpir 21295

This theorem is referenced by: pidufd 33642

W3C validator