Metamath Proof Explorer

Theorem pidufd

Description: Every principal ideal domain is a unique factorization domain. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypothesis pidufd.1 
|- ( ph -> R e. PID )
Assertion pidufd 
|- ( ph -> R e. UFD )

Proof

Step Hyp Ref Expression
1 pidufd.1 
 |-  ( ph -> R e. PID )
2 df-pid 
 |-  PID = ( IDomn i^i LPIR )
3 1 2 eleqtrdi 
 |-  ( ph -> R e. ( IDomn i^i LPIR ) )
4 3 elin1d 
 |-  ( ph -> R e. IDomn )
5 4 idomringd 
 |-  ( ph -> R e. Ring )
6 5 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> R e. Ring )
7 simplr 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> x e. ( Base ` R ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
10 8 9 rspsnid 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> x e. ( ( RSpan ` R ) ` { x } ) )
11 6 7 10 syl2anc 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> x e. ( ( RSpan ` R ) ` { x } ) )
12 simpr 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> i = ( ( RSpan ` R ) ` { x } ) )
13 11 12 eleqtrrd 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> x e. i )
14 simpr 
 |-  ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) -> i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) )
15 14 eldifad 
 |-  ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) -> i e. ( PrmIdeal ` R ) )
16 15 ad2antrr 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> i e. ( PrmIdeal ` R ) )
17 12 16 eqeltrrd 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> ( ( RSpan ` R ) ` { x } ) e. ( PrmIdeal ` R ) )
18 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
19 eqid 
 |-  ( RPrime ` R ) = ( RPrime ` R )
20 4 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> R e. IDomn )
21 simplr 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> i = ( ( RSpan ` R ) ` { x } ) )
22 simpr 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> x = ( 0g ` R ) )
23 22 sneqd 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> { x } = { ( 0g ` R ) } )
24 23 fveq2d 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> ( ( RSpan ` R ) ` { x } ) = ( ( RSpan ` R ) ` { ( 0g ` R ) } ) )
25 9 18 rsp0 
 |-  ( R e. Ring -> ( ( RSpan ` R ) ` { ( 0g ` R ) } ) = { ( 0g ` R ) } )
26 5 25 syl 
 |-  ( ph -> ( ( RSpan ` R ) ` { ( 0g ` R ) } ) = { ( 0g ` R ) } )
27 26 ad4antr 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> ( ( RSpan ` R ) ` { ( 0g ` R ) } ) = { ( 0g ` R ) } )
28 21 24 27 3eqtrd 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> i = { ( 0g ` R ) } )
29 eldifsni 
 |-  ( i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) -> i =/= { ( 0g ` R ) } )
30 29 ad4antlr 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> i =/= { ( 0g ` R ) } )
31 30 neneqd 
 |-  ( ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) /\ x = ( 0g ` R ) ) -> -. i = { ( 0g ` R ) } )
32 28 31 pm2.65da 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> -. x = ( 0g ` R ) )
33 32 neqned 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> x =/= ( 0g ` R ) )
34 18 8 19 9 20 7 33 rsprprmprmidlb 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> ( x e. ( RPrime ` R ) <-> ( ( RSpan ` R ) ` { x } ) e. ( PrmIdeal ` R ) ) )
35 17 34 mpbird 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> x e. ( RPrime ` R ) )
36 13 35 elind 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> x e. ( i i^i ( RPrime ` R ) ) )
37 36 ne0d 
 |-  ( ( ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) /\ x e. ( Base ` R ) ) /\ i = ( ( RSpan ` R ) ` { x } ) ) -> ( i i^i ( RPrime ` R ) ) =/= (/) )
38 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
39 3 elin2d 
 |-  ( ph -> R e. LPIR )
40 39 adantr 
 |-  ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) -> R e. LPIR )
41 5 adantr 
 |-  ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) -> R e. Ring )
42 prmidlidl 
 |-  ( ( R e. Ring /\ i e. ( PrmIdeal ` R ) ) -> i e. ( LIdeal ` R ) )
43 41 15 42 syl2anc 
 |-  ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) -> i e. ( LIdeal ` R ) )
44 8 38 9 40 43 lpirlidllpi 
 |-  ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) -> E. x e. ( Base ` R ) i = ( ( RSpan ` R ) ` { x } ) )
45 37 44 r19.29a 
 |-  ( ( ph /\ i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ) -> ( i i^i ( RPrime ` R ) ) =/= (/) )
46 45 ralrimiva 
 |-  ( ph -> A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) )
47 eqid 
 |-  ( PrmIdeal ` R ) = ( PrmIdeal ` R )
48 47 19 18 isufd 
 |-  ( R e. UFD <-> ( R e. IDomn /\ A. i e. ( ( PrmIdeal ` R ) \ { { ( 0g ` R ) } } ) ( i i^i ( RPrime ` R ) ) =/= (/) ) )
49 4 46 48 sylanbrc 
 |-  ( ph -> R e. UFD )