Theorem edompid

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

	Ref	Expression
Hypothesis	edompid.1	⊢ ( 𝜑 → 𝐷 ∈ EDomn )
Assertion	edompid	⊢ ( 𝜑 → 𝐷 ∈ PID )

Proof

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