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 ⊢ ( 𝜑 → 𝑅 ∈ PID )
Assertion pidufd ( 𝜑 → 𝑅 ∈ UFD )

Proof

Step Hyp Ref Expression
1 pidufd.1 ⊢ ( 𝜑 → 𝑅 ∈ PID )
2 df-pid ⊢ PID = ( IDomn ∩ LPIR )
3 1 2 eleqtrdi ⊢ ( 𝜑 → 𝑅 ∈ ( IDomn ∩ LPIR ) )
4 3 elin1d ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5 4 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑅 ∈ Ring )
7 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
10 8 9 rspsnid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
11 6 7 10 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
12 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
13 11 12 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ 𝑖 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) )
15 14 eldifad ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
16 15 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
17 12 16 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( PrmIdeal ‘ 𝑅 ) )
18 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19 eqid ⊢ ( RPrime ‘ 𝑅 ) = ( RPrime ‘ 𝑅 )
20 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑅 ∈ IDomn )
21 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
22 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑥 = ( 0g ‘ 𝑅 ) )
23 22 sneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → { 𝑥 } = { ( 0g ‘ 𝑅 ) } )
24 23 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) )
25 9 18 rsp0 ⊢ ( 𝑅 ∈ Ring → ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) = { ( 0g ‘ 𝑅 ) } )
26 5 25 syl ⊢ ( 𝜑 → ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) = { ( 0g ‘ 𝑅 ) } )
27 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { ( 0g ‘ 𝑅 ) } ) = { ( 0g ‘ 𝑅 ) } )
28 21 24 27 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑖 = { ( 0g ‘ 𝑅 ) } )
29 eldifsni ⊢ ( 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) → 𝑖 ≠ { ( 0g ‘ 𝑅 ) } )
30 29 ad4antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → 𝑖 ≠ { ( 0g ‘ 𝑅 ) } )
31 30 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) ∧ 𝑥 = ( 0g ‘ 𝑅 ) ) → ¬ 𝑖 = { ( 0g ‘ 𝑅 ) } )
32 28 31 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ¬ 𝑥 = ( 0g ‘ 𝑅 ) )
33 32 neqned ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ≠ ( 0g ‘ 𝑅 ) )
34 18 8 19 9 20 7 33 rsprprmprmidlb ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ( 𝑥 ∈ ( RPrime ‘ 𝑅 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ ( PrmIdeal ‘ 𝑅 ) ) )
35 17 34 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( RPrime ‘ 𝑅 ) )
36 13 35 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → 𝑥 ∈ ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) )
37 36 ne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ )
38 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
39 3 elin2d ⊢ ( 𝜑 → 𝑅 ∈ LPIR )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑅 ∈ LPIR )
41 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑅 ∈ Ring )
42 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
43 41 15 42 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
44 8 38 9 40 43 lpirlidllpi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
45 37 44 r19.29a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ) → ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ )
46 45 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ )
47 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
48 47 19 18 isufd ⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { ( 0g ‘ 𝑅 ) } } ) ( 𝑖 ∩ ( RPrime ‘ 𝑅 ) ) ≠ ∅ ) )
49 4 46 48 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ UFD )