Metamath Proof Explorer

Theorem edompid

Description: Every Euclidean domain is a PID. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypothesis edompid.1 ⊢ φ → D ∈ EDomn
Assertion edompid ⊢ φ → D ∈ PID

Proof

Step Hyp Ref Expression
1 edompid.1 ⊢ φ → D ∈ EDomn
2 1 edomidom ⊢ φ → D ∈ IDomn
3 2 idomringd ⊢ φ → D ∈ Ring
4 sneq ⊢ g = 0 D → g = 0 D
5 4 fveq2d ⊢ g = 0 D → RSpan ⁡ D ⁡ g = RSpan ⁡ D ⁡ 0 D
6 5 eqeq2d ⊢ g = 0 D → i = RSpan ⁡ D ⁡ g ↔ i = RSpan ⁡ D ⁡ 0 D
7 eqid ⊢ Base D = Base D
8 eqid ⊢ 0 D = 0 D
9 3 ringgrpd ⊢ φ → D ∈ Grp
10 9 ad2antrr ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i = 0 D → D ∈ Grp
11 7 8 10 grpidcld ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i = 0 D → 0 D ∈ Base D
12 simpr ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i = 0 D → i = 0 D
13 eqid ⊢ RSpan ⁡ D = RSpan ⁡ D
14 13 8 rsp0 ⊢ D ∈ Ring → RSpan ⁡ D ⁡ 0 D = 0 D
15 3 14 syl ⊢ φ → RSpan ⁡ D ⁡ 0 D = 0 D
16 15 ad2antrr ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i = 0 D → RSpan ⁡ D ⁡ 0 D = 0 D
17 12 16 eqtr4d ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i = 0 D → i = RSpan ⁡ D ⁡ 0 D
18 6 11 17 rspcedvdw ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i = 0 D → ∃ g ∈ Base D i = RSpan ⁡ D ⁡ g
19 eqid ⊢ EuclF ⁡ D = EuclF ⁡ D
20 eqid ⊢ inf EuclF ⁡ D i ∖ 0 D ℕ 0 < = inf EuclF ⁡ D i ∖ 0 D ℕ 0 <
21 1 ad2antrr ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i ≠ 0 D → D ∈ EDomn
22 simplr ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i ≠ 0 D → i ∈ LIdeal ⁡ D
23 simpr ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i ≠ 0 D → i ≠ 0 D
24 7 8 13 19 20 21 22 23 edompidlem ⊢ φ ∧ i ∈ LIdeal ⁡ D ∧ i ≠ 0 D → ∃ g ∈ Base D i = RSpan ⁡ D ⁡ g
25 18 24 pm2.61dane ⊢ φ ∧ i ∈ LIdeal ⁡ D → ∃ g ∈ Base D i = RSpan ⁡ D ⁡ g
26 eqid ⊢ LPIdeal ⁡ D = LPIdeal ⁡ D
27 26 13 7 islpidl ⊢ D ∈ Ring → i ∈ LPIdeal ⁡ D ↔ ∃ g ∈ Base D i = RSpan ⁡ D ⁡ g
28 3 27 syl ⊢ φ → i ∈ LPIdeal ⁡ D ↔ ∃ g ∈ Base D i = RSpan ⁡ D ⁡ g
29 28 adantr ⊢ φ ∧ i ∈ LIdeal ⁡ D → i ∈ LPIdeal ⁡ D ↔ ∃ g ∈ Base D i = RSpan ⁡ D ⁡ g
30 25 29 mpbird ⊢ φ ∧ i ∈ LIdeal ⁡ D → i ∈ LPIdeal ⁡ D
31 30 ex ⊢ φ → i ∈ LIdeal ⁡ D → i ∈ LPIdeal ⁡ D
32 31 ssrdv ⊢ φ → LIdeal ⁡ D ⊆ LPIdeal ⁡ D
33 eqid ⊢ LIdeal ⁡ D = LIdeal ⁡ D
34 26 33 islpir2 ⊢ D ∈ LPIR ↔ D ∈ Ring ∧ LIdeal ⁡ D ⊆ LPIdeal ⁡ D
35 3 32 34 sylanbrc ⊢ φ → D ∈ LPIR
36 2 35 elind ⊢ φ → D ∈ IDomn ∩ LPIR
37 df-pid ⊢ PID = IDomn ∩ LPIR
38 36 37 eleqtrrdi ⊢ φ → D ∈ PID