Metamath Proof Explorer

Theorem edompid

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

Ref Expression
Hypothesis edompid.1 
|- ( ph -> D e. EDomn )
Assertion edompid 
|- ( ph -> D e. PID )

Proof

Step Hyp Ref Expression
1 edompid.1 
 |-  ( ph -> D e. EDomn )
2 1 edomidom 
 |-  ( ph -> D e. IDomn )
3 2 idomringd 
 |-  ( ph -> D e. Ring )
4 sneq 
 |-  ( g = ( 0g ` D ) -> { g } = { ( 0g ` D ) } )
5 4 fveq2d 
 |-  ( g = ( 0g ` D ) -> ( ( RSpan ` D ) ` { g } ) = ( ( RSpan ` D ) ` { ( 0g ` D ) } ) )
6 5 eqeq2d 
 |-  ( g = ( 0g ` D ) -> ( i = ( ( RSpan ` D ) ` { g } ) <-> i = ( ( RSpan ` D ) ` { ( 0g ` D ) } ) ) )
7 eqid 
 |-  ( Base ` D ) = ( Base ` D )
8 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
9 3 ringgrpd 
 |-  ( ph -> D e. Grp )
10 9 ad2antrr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i = { ( 0g ` D ) } ) -> D e. Grp )
11 7 8 10 grpidcld 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i = { ( 0g ` D ) } ) -> ( 0g ` D ) e. ( Base ` D ) )
12 simpr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i = { ( 0g ` D ) } ) -> i = { ( 0g ` D ) } )
13 eqid 
 |-  ( RSpan ` D ) = ( RSpan ` D )
14 13 8 rsp0 
 |-  ( D e. Ring -> ( ( RSpan ` D ) ` { ( 0g ` D ) } ) = { ( 0g ` D ) } )
15 3 14 syl 
 |-  ( ph -> ( ( RSpan ` D ) ` { ( 0g ` D ) } ) = { ( 0g ` D ) } )
16 15 ad2antrr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i = { ( 0g ` D ) } ) -> ( ( RSpan ` D ) ` { ( 0g ` D ) } ) = { ( 0g ` D ) } )
17 12 16 eqtr4d 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i = { ( 0g ` D ) } ) -> i = ( ( RSpan ` D ) ` { ( 0g ` D ) } ) )
18 6 11 17 rspcedvdw 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i = { ( 0g ` D ) } ) -> E. g e. ( Base ` D ) i = ( ( RSpan ` D ) ` { g } ) )
19 eqid 
 |-  ( EuclF ` D ) = ( EuclF ` D )
20 eqid 
 |-  inf ( ( ( EuclF ` D ) " ( i \ { ( 0g ` D ) } ) ) , NN0 , < ) = inf ( ( ( EuclF ` D ) " ( i \ { ( 0g ` D ) } ) ) , NN0 , < )
21 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i =/= { ( 0g ` D ) } ) -> D e. EDomn )
22 simplr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i =/= { ( 0g ` D ) } ) -> i e. ( LIdeal ` D ) )
23 simpr 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i =/= { ( 0g ` D ) } ) -> i =/= { ( 0g ` D ) } )
24 7 8 13 19 20 21 22 23 edompidlem 
 |-  ( ( ( ph /\ i e. ( LIdeal ` D ) ) /\ i =/= { ( 0g ` D ) } ) -> E. g e. ( Base ` D ) i = ( ( RSpan ` D ) ` { g } ) )
25 18 24 pm2.61dane 
 |-  ( ( ph /\ i e. ( LIdeal ` D ) ) -> E. g e. ( Base ` D ) i = ( ( RSpan ` D ) ` { g } ) )
26 eqid 
 |-  ( LPIdeal ` D ) = ( LPIdeal ` D )
27 26 13 7 islpidl 
 |-  ( D e. Ring -> ( i e. ( LPIdeal ` D ) <-> E. g e. ( Base ` D ) i = ( ( RSpan ` D ) ` { g } ) ) )
28 3 27 syl 
 |-  ( ph -> ( i e. ( LPIdeal ` D ) <-> E. g e. ( Base ` D ) i = ( ( RSpan ` D ) ` { g } ) ) )
29 28 adantr 
 |-  ( ( ph /\ i e. ( LIdeal ` D ) ) -> ( i e. ( LPIdeal ` D ) <-> E. g e. ( Base ` D ) i = ( ( RSpan ` D ) ` { g } ) ) )
30 25 29 mpbird 
 |-  ( ( ph /\ i e. ( LIdeal ` D ) ) -> i e. ( LPIdeal ` D ) )
31 30 ex 
 |-  ( ph -> ( i e. ( LIdeal ` D ) -> i e. ( LPIdeal ` D ) ) )
32 31 ssrdv 
 |-  ( ph -> ( LIdeal ` D ) C_ ( LPIdeal ` D ) )
33 eqid 
 |-  ( LIdeal ` D ) = ( LIdeal ` D )
34 26 33 islpir2 
 |-  ( D e. LPIR <-> ( D e. Ring /\ ( LIdeal ` D ) C_ ( LPIdeal ` D ) ) )
35 3 32 34 sylanbrc 
 |-  ( ph -> D e. LPIR )
36 2 35 elind 
 |-  ( ph -> D e. ( IDomn i^i LPIR ) )
37 df-pid 
 |-  PID = ( IDomn i^i LPIR )
38 36 37 eleqtrrdi 
 |-  ( ph -> D e. PID )